Are LLMs Better Formalizers than Solvers on Complex Problems?
This work addresses the practical effectiveness of LLMs in formalizing logical reasoning for real-life problems, revealing current limitations and providing remedies for future research.
The study challenges the assumption that LLMs are better as formalizers than solvers for complex constraint satisfaction problems, showing that in few-shot settings, LLM-as-formalizer underperforms LLM-as-solver across 4 domains and 6 LLMs.
A trending line of recent work advocates for using large language models (LLMs) as formalizers instead of as end-to-end solvers for logical reasoning problems. Instead of generating the solution, the LLM generates a formal program that derives a solution via an external solver. While performance gain of the seemingly scalable LLM-as-formalizer over the seemingly unscalable LLM-as-solver has been widely reported, we show that this superiority does not hold on real-life constraint satisfaction problems. On 4 domains, we systematically evaluate 6 LLMs including 4 large reasoning models with inference-time scaling, paired with 5 pipelines including 2 types of formalism. We show that in few-shot settings, LLM-as-formalizer underperforms LLM-as-solver. While LLM-as-formalizer promises accuracy, robustness, faithfulness, and efficiency, we observe that the present LLMs do not yet deliver any of those, as their limited ability to generate formal programs leads to failure to scale with complexity, hard-coded solutions, and excessive reasoning tokens. We present our detailed analysis and actionable remedies to drive future research that improves LLM-as-formalizer.