深入探究大语言模型的逻辑推理：工具的选择至关重要
A Closer Look at Logical Reasoning with LLMs: The Choice of Tool Matters
AI总结：
本研究针对大语言模型结合符号求解器的逻辑推理范式中工具选择影响不明确的问题，通过对比Z3、Pyke、Prover9三类求解器，发现工具选择带来近50%性能差异，且Prover9的翻译可执行率与结果准确率强相关。
摘要：
大语言模型（LLMs）的兴起在有效解决逻辑推理任务方面展现出了可观的进展。近期已有多种方法提出将大语言模型的角色从推理者转变为自然语言表述与符号表示之间的转换器，生成的符号表示随后会被发送至外部符号求解器进行求解。该范式已在逻辑推理（即演绎推理）领域取得了当前最优结果。然而，目前尚不清楚这些方法的性能差异是源于所采用的方法论，还是所使用的特定符号求解器。目前缺乏对不同符号求解器及其对整体报告性能影响的一致性对比。这一点十分重要，因为每个符号求解器都有其自身的输入符号语言，给翻译过程带来了不同程度的挑战。为填补这一空白，我们在3个演绎推理基准上开展实验，为大语言模型配备广泛使用的符号求解器：Z3、Pyke和Prover9。不同大语言模型生成的符号翻译的工具可执行率存在近50%的性能差异。这凸显出仅基础工具选择就会带来显著的性能差距。Prover9的翻译可执行率与结果准确率之间近乎线性的相关性表明，大语言模型翻译成Prover9符号语言的能力与翻译的正确性之间存在强一致性。
英文摘要：
The emergence of Large Language Models (LLMs) has demonstrated promising progress in solving logical reasoning tasks effectively. Several recent approaches have proposed to change the role of the LLM from the reasoner into a translator between natural language statements and symbolic representations which are then sent to external symbolic solvers to resolve. This paradigm has established the current state-of-the-art result in logical reasoning (i.e., deductive reasoning). However, it remains unclear whether the variance in performance of these approaches stems from the methodologies employed or the specific symbolic solvers utilized. There is a lack of consistent comparison between symbolic solvers and how they influence the overall reported performance. This is important, as each symbolic solver also has its own input symbolic language, presenting varying degrees of challenge in the translation process. To address this gap, we perform experiments on 3 deductive reasoning benchmarks with LLMs augmented with widely used symbolic solvers: Z3, Pyke, and Prover9. The tool-executable rates of symbolic translation generated by different LLMs exhibit a near 50% performance variation. This highlights a significant difference in performance rooted in very basic choices of tools. The almost linear correlation between the executable rate of translations and the accuracy of the outcomes from Prover9 highlight a strong alignment between LLMs ability to translate into Prover9 symbolic language, and the correctness of those translations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
