分而译之：面向复杂逻辑推理的组合式一阶逻辑翻译与验证
Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning
AI总结：
本文提出 CLOVER 方法，通过将自然语言句子组合式地解析并翻译为一阶逻辑公式，再结合 SAT 求解器进行语义验证，从而提升 LLM 在复杂逻辑推理任务上的表现，并在七个基准上取得最优结果。
摘要：
复杂逻辑推理任务需要较长的推理序列，即使采用思维链提示的大语言模型（LLM）仍然表现不足。为缓解这一问题，神经符号方法引入了符号求解器。具体而言，LLM 仅将自然语言问题翻译为由一阶逻辑公式构成的可满足性（SAT）问题，然后由可靠的符号求解器返回数学上正确的解。然而，我们发现 LLM 在翻译过程中难以捕捉隐藏在自然语言中的复杂逻辑语义。为解决这一局限，我们提出了一种组合式一阶逻辑翻译方法。LLM 首先将自然语言句子解析为新定义的逻辑依存结构，该结构由一个原子子句及其依存成分组成，然后按顺序翻译解析出的各个子句。由于单个句子可能存在多种逻辑依存结构和顺序翻译方式，我们还引入了两种验证算法以确保结果更加可靠。我们利用 SAT 求解器严格比较所生成的一阶逻辑公式之间的语义，并选择最可能的一个。我们在七个逻辑推理基准上评估了所提出的方法（称为 CLOVER），结果表明它优于此前的神经符号方法，并取得了新的最优结果。
英文摘要：
Complex logical reasoning tasks require a long sequence of reasoning, which a large language model (LLM) with chain-of-thought prompting still falls short. To alleviate this issue, neurosymbolic approaches incorporate a symbolic solver. Specifically, an LLM only translates a natural language problem into a satisfiability (SAT) problem that consists of first-order logic formulas, and a sound symbolic solver returns a mathematically correct solution. However, we discover that LLMs have difficulties to capture complex logical semantics hidden in the natural language during translation. To resolve this limitation, we propose a Compositional First-Order Logic Translation. An LLM first parses a natural language sentence into newly defined logical dependency structures that consist of an atomic subsentence and its dependents, then sequentially translate the parsed subsentences. Since multiple logical dependency structures and sequential translations are possible for a single sentence, we also introduce two Verification algorithms to ensure more reliable results. We utilize an SAT solver to rigorously compare semantics of generated first-order logic formulas and select the most probable one. We evaluate the proposed method, dubbed CLOVER, on seven logical reasoning benchmarks and show that it outperforms the previous neurosymbolic approaches and achieves new state-of-the-art results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
