深入审视大语言模型的逻辑推理：工具的选择至关重要
计算与语言
2024-07-12 v2
摘要
大语言模型（LLM）的出现展示了在有效解决逻辑推理任务方面的有希望的进展。最近的几种方法提出将 LLM 的角色从推理者转变为自然语言陈述与符号表示之间的翻译器，然后将这些符号表示发送给外部符号求解器进行求解。这种范式在逻辑推理（即演绎推理）中确立了当前最先进的结果。然而，尚不清楚这些方法性能的差异是源于所采用的方法论还是所使用的特定符号求解器。目前缺乏符号求解器之间的一致性比较，以及它们如何影响整体报告的性能。这一点很重要，因为每个符号求解器也有其自身的输入符号语言，在翻译过程中呈现出不同程度的挑战。为了填补这一空白，我们在 3 个演绎推理基准上进行了实验，使用了增强有广泛使用的符号求解器 Z3、Pyke 和 Prover9 的 LLM。不同 LLM 生成的符号翻译的工具可执行率表现出近 50% 的性能差异。这突显了根植于非常基本的工具选择中的显著性能差异。翻译的可执行率与 Prover9 结果的准确性之间的几乎线性相关性，突显了 LLM 翻译成 Prover9 符号语言的能力与这些翻译的正确性之间的强一致性。
引用
@article{arxiv.2406.00284,
title = {A Closer Look at Logical Reasoning with LLMs: The Choice of Tool Matters},
author = {Long Hei Matthew Lam and Ramya Keerthy Thatikonda and Ehsan Shareghi},
journal= {arXiv preprint arXiv:2406.00284},
year = {2024}
}
备注
Code and data are publicly available at: https://github.com/Mattylam/Logic_Symbolic_Solvers_Experiment