Large language models often solve problems before formalizing programs
Solver-Like Behavior in Large Language Models as Formalizers
Computation and LanguageArtificial Intelligence
Summary
Sometimes large language models write out detailed steps to solve a problem even before turning that problem into a formal computer program. The researchers found that these models often do the hard work of testing and ruling out possibilities in their reasoning text, which they call solver-like behavior. However, the final program they write usually repeats this work, making the reasoning redundant. They also found that this behavior is more common when the program is written in certain languages, and simple changes in how the problem is presented can reduce it a lot without hurting accuracy.
What this means in practice
- •For software developers: Improve debugging and optimization of AI-generated code by analyzing redundant solver-like reasoning within program traces.
- •For automated reasoning engineers: Design better formalizers by structuring problem inputs to reduce redundant solver-like steps and increase formalizing efficiency.
Authors
Rikhil Amonkar, Stuti Mohan, Kevin Nguyen, Ceyhun Efe Kayan, Ronan Le Bras, Li Zhang
Abstract
In the LLM-as-formalizer paradigm, a large language model translates a problem into a formal program and leaves the search to a solver, gaining the solver's guarantees. Formalizers are now often reasoning models that write a long reasoning trace before the program, yet they are judged only by the program's output. We find that the trace routinely does the solver's job, assigning, testing and ruling out values until it often reaches the full answer; we call this solver-like behavior (SLB). We define an ontology of SLB over the trace, the program and its output, and use LLM judges, checked against human labels, to label 2,000 generations from three reasoning models on four constraint satisfaction datasets, each formalized in a declarative and an imperative formal language. SLB appears in 85% of traces and takes 24% of reasoning tokens, yet the program usually recomputes the answer, so the effort is redundant. The 9% of programs that inherit the trace's answer also inherit its errors, and pass output-based evaluation whenever that answer is correct. The amount of SLB is not associated with accuracy, and SLB is more common in imperative Python than in declarative Z3 or PDDL. Cautionary prompts reduce it by only a quarter, but hiding the problem's values behind placeholders, which the program receives only at run time, removes 97% of it without loss of accuracy. Formalizers should therefore be evaluated by how their programs are reached, not only by what they output.