# A Reality Check of Language Models as Formalizers on Constraint Satisfaction Problems

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 33 of its 37 references that are in the map.
- First posted on arXiv 19 May 2025.

## Placed in

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

## Builds on (most cited first, 30 of 33)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [s1: Simple test-time scaling](https://mlsanity.com/paper/2501.19393/) (2025)
- [Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting](https://mlsanity.com/paper/2305.04388/) (2023)
- [LLM+P: Empowering Large Language Models with Optimal Planning Proficiency](https://mlsanity.com/paper/2304.11477/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Explain Yourself! Leveraging Language Models for Commonsense Reasoning](https://mlsanity.com/paper/1906.02361/) (2019)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [Analysing Mathematical Reasoning Abilities of Neural Models](https://mlsanity.com/paper/1904.01557/) (2019)
- [Large Language Models are Better Reasoners with Self-Verification](https://mlsanity.com/paper/2212.09561/) (2022)
- [Towards Revealing the Mystery behind Chain of Thought: A Theoretical Perspective](https://mlsanity.com/paper/2305.15408/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Faithful Chain-of-Thought Reasoning](https://mlsanity.com/paper/2301.13379/) (2023)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning](https://mlsanity.com/paper/2502.01100/) (2025)
- [On the Self-Verification Limitations of Large Language Models on Reasoning and Planning Tasks](https://mlsanity.com/paper/2402.08115/) (2024)
- [Translating Natural Language to Planning Goals with Large-Language Models](https://mlsanity.com/paper/2302.05128/) (2023)
- [NATURAL PLAN: Benchmarking LLMs on Natural Language Planning](https://mlsanity.com/paper/2406.04520/) (2024)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [LLMs Still Can't Plan; Can LRMs? A Preliminary Evaluation of OpenAI's o1 on PlanBench](https://mlsanity.com/paper/2409.13373/) (2024)
- [Algorithm of Thoughts: Enhancing Exploration of Ideas in Large Language Models](https://mlsanity.com/paper/2308.10379/) (2023)
- [Planning Anything with Rigor: General-Purpose Zero-Shot Planning with LLM-based Formalized Programming](https://mlsanity.com/paper/2410.12112/) (2024)
- [Steering Large Language Models between Code Execution and Textual Reasoning](https://mlsanity.com/paper/2410.03524/) (2024)
- [On the Limit of Language Models as Planning Formalizers](https://mlsanity.com/paper/2412.09879/) (2024)
- [PlanGEN: A Multi-Agent Framework for Generating Planning and Reasoning Trajectories for Complex Problem Solving](https://mlsanity.com/paper/2502.16111/) (2025)

## Built on by (most cited first, 1 of 1)

- [End-to-end PDDL Planning with Hardcoded and Dynamic Agents](https://mlsanity.com/paper/2512.09629/) (2025)

## Abstract (arXiv)

Recent work shows superior performance when using large language models (LLMs) as formalizers instead of as end-to-end solvers for symbolic reasoning problems. Given the problem description, the LLM generates a formal program that derives a solution via an external solver. We systematically investigate the formalization capability of LLMs on real-life constraint satisfaction problems on 4 benchmarks, 6 LLMs, and 2 types of formal languages. We show that LLM-as-formalizer by no means trivializes the problem but underperforms LLM-as-solver in 15 out of 24 model-dataset combinations, despite the former's verifiability and interpretability. Although the formalization space is magnitudes smaller than the search space, our scaling analysis shows that LLM-as-formalizer still drastically degrades as problem complexity increases similar to LLM-as-solver. To better understand this limitation, we observe excessive, solver-like reasoning tokens that sometimes lead to hard-coded solutions, highlighting a key challenge for improving LLM-based formalization.