SatLM：使用声明式提示的可满足性辅助语言模型
SatLM: Satisfiability-Aided Language Models Using Declarative Prompting
AI总结：
提出SatLM方法，利用LLM生成声明式规范并借助自动定理证明器求解，在8个数据集上超越程序辅助模型，GSM子集提升23%，LSAT和BoardgameQA取得新最优。
摘要：
先前的工作已将大型语言模型（LLM）中的思维链提示与程序化表示相结合，以进行有效且透明的推理。虽然这种方法对于仅需要前向推理（例如直接算术）的任务效果良好，但对于需要更复杂规划和搜索的约束求解问题则效果较差。在本文中，我们提出了一种新的可满足性辅助语言建模（SatLM）方法，以提高LLM的推理能力。我们使用LLM生成声明式任务规范，而非命令式程序，并利用现成的自动定理证明器来得出最终答案。这种方法有两个关键优势。声明式规范比推理步骤更接近问题描述，因此LLM可以更准确地从描述中解析出它。此外，通过将实际推理任务卸载给自动定理证明器，我们的方法可以保证答案相对于解析出的规范的正确性，并避免求解过程中的规划错误。我们在8个不同的数据集上评估了SATLM，并表明它在命令式范式中始终优于程序辅助语言模型。特别是，在GSM算术推理数据集的一个具有挑战性的子集上，SATLM比程序辅助语言模型高出23%；SATLM还在LSAT和BoardgameQA上取得了新的最先进成果，超越了先前在各自训练集上训练的模型。
英文摘要：
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 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 8 different datasets and show that it consistently outperforms program-aided LMs in the 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 and BoardgameQA, surpassing previous models that are trained on the respective training sets.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
