When Do Symbolic Solvers Enhance Reasoning in Large Language Models?

TL;DR

This paper investigates when integrating symbolic solvers with large language models enhances reasoning, finding that symbolic methods help mainly in problems with limited implicit reasoning but large search spaces, especially in constraint satisfaction tasks.

Contribution

The study clarifies the conditions under which symbolic solvers improve LLM reasoning, highlighting their effectiveness in specific problem types and with certain model capabilities.

Findings

Symbolic solvers aid in problems with limited implicit reasoning and large search spaces.

GPT-4o performs well on shallow deductive reasoning tasks.

Symbolic methods significantly improve performance on complex constraint satisfaction problems.

Abstract

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.