符号求解器能提升大模型推理，但只在搜索空间大时有效。
When Do Symbolic Solvers Enhance Reasoning in Large Language Models?
- 用代码生成将问题转为可执行程序，交由符号求解器处理。
- 在需反复回溯的约束满足问题中，性能显著超越纯文本推理。
- 适合解决逻辑谜题等搜索空间大的问题，尤其对小模型有帮助。
大型推理模型通过生成长链思维（CoT）在复杂推理任务中表现优异，但可能因过度思考产生冗长推理链，导致错误。一种有前景的方法是集成符号求解器：利用大模型代码生成能力将推理任务转化为可执行代码，并由符号求解器求解。本文探讨何时传统长链思维可被符号求解器增强。实验表明，该方法仅在问题需要有限隐式推理但搜索空间庞大时有效。最新模型如GPT-4o在浅层演绎问题上表现更好，而符号求解器集成方法显著提升了模型在需反复回溯的约束满足问题中的表现。当提供声明式示例时，CodeLlama-13B甚至在困难的Zebra谜题上优于GPT-4o。
原文摘要 · Abstract (English)
Large Reasoning Models (LRMs) achieve strong performance on complex reasoning tasks by generating long Chains of Thought (CoTs). However, this paradigm might incur substantial token overhead, especially when models "overthink" by producing lengthy reasoning chains, which can even lead to incorrect answers. A promising direction is the symbolic-solver-integrated approach, which leverages the code generation capabilities of LLMs to translate reasoning tasks into executable code and then solve them with a symbolic solver. In this paper, we explore an open question of when the conventional long-CoT can be enhanced by symbolic solvers. Our experimental results show that the symbolic-solver-integrated method only helps when the problem requires limited implicit reasoning but involves an ample search space. The latest LLMs, like GPT-4o, show better performance on deductive problems with shallow reasoning depth, while the symbolic-solver-integrated method significantly improves the LLMs' performance in constraint satisfaction problems that require repeated backtracks. When a declarative exemplar is provided, even CodeLlama-13B can outperform GPT-4o in difficult Zebra puzzles.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。