cs.CLNov 2, 2026
SaveSolver-Like Behavior in Large Language Models as Formalizers
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.
Figures & tables
Figure 1: Overview on a calendar scheduling problem (1). An LLM as formalizer writes a reasoning trace (2) and then a program (3), which is run and scored. The middle paragraph is solver-like : it solves the problem in the trace, finding first the common free intervals and then the meeting time, which is the solver’s job; in real traces such a passage runs to hundreds or thousands of tokens. Our ontology (§ 3 ) labels every generation (4): whether the reasoning trace is solver-like (A), how much of the reasoning answer the program inherits (B), and whether the program’s output matches the reasoning answer, which is checked for correctness (C). Here the program searches independently, so the solver-like behavior, 45% of the trace, was wasted.
Figure 2: Ontology of solver-like behavior, with an example of each node on a toy seating problem (left). A describes the reasoning trace: whether it contains solver-like behavior (A1), and how much of an answer it reaches (A2). B describes how much of the reasoning answer the program inherits rather than computes; B1–B3 require A1 = SLB. C compares the program’s output with a complete reasoning answer (C1), and checks the reasoning answer with the validator (C2).
| Node | Reference | Agree | 95% CI |
| A1 paragraph | human, blind | 103/110 | .87–.97 |
| SLB precision | human, blind | 38/42 | .78–.96 |
| SLB recall | human, blind | 38/41 | .81–.97 |
| A2 extent | human + script | 39/40 | .87–1.00 |
| B program | model, blind | 19/20 | .76–.99 |
| B program (held out) | human, not blind | 38/40 | .83–.99 |
Table 1: Agreement of each ontology judge with reference labels, with Wilson 95% confidence intervals. A1: one annotator, labeling blind (70 development and 40 held-out paragraphs). A2: complete labels verified by humans, partial ones by searching the trace for the program’s answer and having a second model read the passages found. B: blind reference labels by a second model; held out: a human shown the judge’s evidence, on programs labeled B1–B4. A1 and held-out B references cover both FLs of every dataset. C1 and C2 are computed by scripts from the A2 extraction, so they need no agreement check.
Figure 3: H1 and H2: solver-like behavior is common, and the program rarely inherits it. For each dataset and FL, the share of traces with SLB (A1) and the mean solver-like ratio, with 95% confidence intervals. Each SLB bar is split by the program’s label (B): programs that inherit the reasoning answer (B1–B3, grey) at the bottom, independent programs (B4) in the model’s colour, and programs with no output (missing, failed, or printed nothing) hatched; most of these are Qwen’s Z3 programs, which call Z3 methods that do not exist. DeepSeek is run in one FL per dataset (–).
Figure 4: H3: the amount of solver-like behavior is not associated with accuracy. Change in the probability that the program is correct per unit of each measure, from a linear model with fixed effects for model, dataset and FL and for the problem, with 95% confidence intervals. Grey: the ratio’s effect within each dataset.
Figure 5: H4: on the same 100 problems, Python draws more solver-like behavior than each dataset’s declarative FL (in parentheses). Mean solver-like ratio per model, with 95% confidence intervals.
Figure 6: Placeholders all but remove solver-like behavior without costing accuracy; cautionary prompts remove about a quarter of it, and batching shortens all reasoning at a cost in accuracy. Change from the baseline prompt on the same problems in solver-like tokens per problem (% of the baseline mean), solver-like ratio, and program accuracy (points): pooled estimate with 95% bootstrap confidence interval, and one dot per model. Each method is measured where it was run: cautionary prompts for every model, dataset and FL (2,000 pairs), batching ( ) for Qwen and GPT-OSS in every dataset and FL except PDDL (1,400), placeholders for Qwen and GPT-OSS on Calendar and Meeting Planning in Python and Z3 (800). The subsets differ, so the text compares each method with the cautionary prompts on its own problems.
Appendix figures & tables11 assets
Supplementary material from the paper’s appendix.
Appendix
| Not in FL | |||||
| Model | Task | FL | 0 | A | B |
| DeepSeek | Calendar | Python | 0 | 0 | 0 |
| Meeting | Python | 0 | 0 | 0 | |
| ZebraLogic | Z3 | 0 | 0 | 1 | |
| BlocksWorld | PDDL | – | – | – | |
| GPT-OSS | Calendar | Python | 0 | 0 | 0 |
Table 2: Runs: each model, task and formal language has 300 generations (100 problems under each of three prompts; 6,000 in total). Not in FL: programs not written in the requested FL under the baseline (0) and Cautionary A and B prompts. DeepSeek is run in one FL per dataset.
Figure 7: A trace with every paragraph and its A1 label. Paragraph 1 only interprets Frank’s preference, which is not solver-like; paragraph 3 checks the schedules and rules out every slot but one. Although the trace has already found the unique answer, the program searches for it independently (B4), so the SLB is wasted.
Figure 8: Programs labeled B1–B3, each with an excerpt of the solver-like trace it follows and the B judge’s evidence. All three are scored correct. The hardcoded program only prints the itinerary from the trace; the partly fixed one computes the times but along the single itinerary chosen in the trace; the steered one searches all departures and meeting times, but with a tie-break chosen so that the search returns the itinerary the trace expected.
Listing 1: Baseline Prompt: Universal CSP formalization prompt with no cautionary warnings, shown with the Calendar Scheduling output specification.
Listing 2: Cautionary Prompt A: The Baseline prompt with an added outcome-focused warning against solver-like reasoning, illustrated with a multi-step problem containing a conditional. Shown with the Calendar Scheduling output specification.
Listing 3: Cautionary Prompt B: The Baseline prompt with an added act-focused definition of solver-like behavior, illustrated with a single-step GSM8K problem. Shown with the Calendar Scheduling output specification.
Listing 4: Batching and placeholders (§ 6 ). Top: the instruction that ends a batched prompt. Middle: the note that precedes a Calendar Scheduling problem with placeholders (Meeting Planning’s note also introduces locations, durations and TRAVEL ). Bottom: the task of a Calendar Scheduling problem with placeholders; the program receives VALUES = {"Person1": "Judy", "Person2": "Nicole", "Day1": "Monday", "T3": "9:00", ..., "D1": 30} .
Listing 5: Baseline prompts in the declarative formal languages. Top: the Z3 prefix, followed by the Z3 output format for Calendar Scheduling, which gives the import and coding steps. Bottom: the PDDL prefix for BlocksWorld, which supplies the ground-truth problem PDDL as a reference; its output format asks for a domain and a problem as a JSON object.
Listing 6: Prompt of the A1 judge, applied to one segment of a trace at a time. V and VP are read as SLB , P and N as none . “Prose” in the judge prompts refers to the reasoning trace.
Listing 7: Prompt of the A2 judge, which extracts the reasoning answer from the paragraphs the A1 judge labeled SLB and decides whether it is complete.
Listing 8: Prompt of the B judge, which labels the program B1–B4 with its evidence.