# When Do Symbolic Solvers Enhance Reasoning in Large Language Models?

arXiv: https://arxiv.org/abs/2512.03272 · HTML: https://mlsanity.com/paper/2512.03272/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 27 of its 32 references that are in the map.
- First posted on arXiv 2 Dec 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 27 of 27)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Shortcut Learning in Deep Neural Networks](https://mlsanity.com/paper/2004.07780/) (2020)
- [A Survey on Evaluation of Large Language Models](https://mlsanity.com/paper/2307.03109/) (2023)
- [Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks](https://mlsanity.com/paper/2211.12588/) (2022)
- [MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models](https://mlsanity.com/paper/2309.12284/) (2023)
- [PAL: Program-aided Language Models](https://mlsanity.com/paper/2211.10435/) (2022)
- [Towards Reasoning in Large Language Models: A Survey](https://mlsanity.com/paper/2212.10403/) (2022)
- [Faith and Fate: Limits of Transformers on Compositionality](https://mlsanity.com/paper/2305.18654/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [What Algorithms can Transformers Learn? A Study in Length Generalization](https://mlsanity.com/paper/2310.16028/) (2023)
- [A Careful Examination of Large Language Model Performance on Grade School Arithmetic](https://mlsanity.com/paper/2405.00332/) (2024)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Explaining Answers with Entailment Trees](https://mlsanity.com/paper/2104.08661/) (2021)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [OverThink: Slowdown Attacks on Reasoning LLMs](https://mlsanity.com/paper/2502.02542/) (2025)
- [Don't Overthink it. Preferring Shorter Thinking Chains for Improved LLM Reasoning](https://mlsanity.com/paper/2505.17813/) (2025)
- [Puzzle Solving using Reasoning of Large Language Models: A Survey](https://mlsanity.com/paper/2402.11291/) (2024)
- [Meta Reasoning for Large Language Models](https://mlsanity.com/paper/2406.11698/) (2024)
- [Case-Based or Rule-Based: How Do Transformers Do the Math?](https://mlsanity.com/paper/2402.17709/) (2024)

## Abstract (arXiv)

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.