Prior work has combined chain-of-thought prompting in large language models (LLMs) with programmatic representations to perform effective and transparent reasoning. While such an approach works very well for tasks that only require forward reasoning (e.g., straightforward arithmetic), it is less effective for constraint solving problems that require more sophisticated planning and search. In this paper, we propose a new satisfiability-aided language modeling (SATLM) approach for improving the reasoning capabilities of LLMs. We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. This approach has two key advantages. The declarative specification is closer to the problem description than the reasoning steps are, so the LLM can parse it out of the description more accurately. Furthermore, by offloading the actual reasoning task to an automated theorem prover, our approach can guarantee the correctness of the answer with respect to the parsed specification and avoid planning errors in the solving process. We evaluate SATLM on 6 different datasets and show that it consistently outperforms program-aided LMs in an imperative paradigm. In particular, SATLM outperforms program-aided LMs by 23% on a challenging subset of the GSM arithmetic reasoning dataset; SATLM also achieves a new SoTA on LSAT, surpassing previous models that are trained on the full training set.

翻译：先前工作将大型语言模型（LLMs）中的链式思维提示与程序化表示相结合，以实现高效且透明的推理。尽管该方法在仅需正向推理（如简单算术）的任务中表现良好，但对于需要更复杂规划与搜索的约束求解问题效果欠佳。本文提出一种新的可满足性辅助语言建模（SATLM）方法，用于提升LLMs的推理能力。我们利用LLM生成声明式任务规约而非命令式程序，并借助现成的自动定理证明器推导最终答案。该方法具有两大优势：声明式规约比推理步骤更贴近问题描述，因此LLM能更准确地从描述中解析它；此外，通过将实际推理任务外包给自动定理证明器，我们的方法能保证解析规约对应答案的正确性，并避免求解过程中的规划错误。我们在6个不同数据集上评估SATLM，结果表明它始终优于命令式范式下的程序辅助语言模型。特别地，在GSM算术推理数据集中具有挑战性的子集上，SATLM较程序辅助语言模型提升23%；其在LSAT数据集上也创下新最先进水平，超越了使用完整训练集训练的先前模型。