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 ( K=5 ) 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
Appendix
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.
Formal tools such as SAT and SMT solvers are increasingly embedded in language model reasoning pipelines when a safety or security critical question can be formulated in logic. Unlike chain of thought whose steps are sampled from the model distribution without formal guarantee, a solver produces a sound and independently verifiable answer. However, the soundness guarantee can be lost in the interaction between the solver and the model. The hybrid pipeline has three components: formalizing the question, deciding it, and narrating the result. Prior work has studied the formalization and decision, but not narration, which is the step that turns a formal tool's output into the user answer. To fill the narration gap, we first model the LLM-solver loop as a verified decision procedure. We further evaluate five open-sourced models under prompt injection, and we find certificate gating makes the solver verdict sound, while an adversary can invert a verified conclusion across phrasings and channels. We study the mitigation through hardened prompt that reduces injection significantly but cannot eliminate it and still suffers under adaptive attack. Combining the formal analysis and empirical studies, we show in the LLM-solver loop, robustness does not reach to the answer that the user finally reads.
Zunchen Huang, Songgaojun Deng
Centrum Wiskunde & Informatica, Amsterdam, The Netherlands · Eindhoven University of Technology, Eindhoven, The Netherlands
Recent work provides overwhelming evidence that LLMs, even those trained to scale their reasoning trace, quickly deteriorate at planning as problems become more complex. LLM-as-Formalizers aim to address this by employing LLMs as a bridge to translate natural language descriptions into structured planning representations such as PDDL, which are then fed to a programmatic solver. We observe that its success may be overstated because planning problem descriptions in standard benchmarks often have a one-to-one mapping to PDDL, which departs from real use cases. To address this, we introduce the notion of unraveling problems where a natural yet succinct description translates into a very large PDDL representation. Using unraveling variants of four standard planning domains, we demonstrate that LLM Formalizers also do not always scale. We tackle this challenge by introducing a new paradigm, LLM-as-Higher-Order-Formalizer, where the LLM generates a high-level program that captures the recurrent logic within the description and in turn generates the larger PDDL representation. This decouples token output from the combinatorial explosion of the underlying formalization and search space, leading to improved performance for complex problems.
Large Language Models (LLMs) struggle to solve complex combinatorial problems through direct reasoning, so recent neuro-symbolic systems increasingly use them to synthesize executable solvers. A central design question is how the LLM should represent the solver, and whether it should also attempt to optimize search. We introduce CP-SynC-XL, a benchmark of 100 combinatorial problems (4,577 instances), and evaluate three solver-construction paradigms: native algorithmic search (Python), constraint modeling through a Python solver API (Python + OR-Tools), and declarative constraint modeling (MiniZinc + OR-Tools). We find a consistent representational divergence: Python + OR-Tools attains the highest correctness across LLMs, while MiniZinc + OR-Tools has lower absolute coverage despite using the same OR-Tools back-end. Native Python is the most likely to return a schema-valid solution that fails verification, whereas solver-backed paths preserve higher conditional fidelity. On the heuristic axis, prompting for search optimization yields only small median speed-ups (1.03-1.12x) and a strongly bimodal effect: many instances slow down, and correctness drops sharply on a long tail of problems. A paired code-level audit traces these regressions to a recurring heuristic trap. Under an efficiency-oriented prompt, the LLM may replace complete search with local approximations (Python), inject unverified bounds (Python + OR-Tools), or add redundant declarative machinery that overwhelms or over-constrains the model (MiniZinc + OR-Tools). These findings support a conservative design principle for LLM-generated combinatorial solvers: use the LLM primarily to formalize variables, constraints, and objectives for verified solvers, and separately check any LLM-authored search optimization before use.
Haoyu Wang, Yuliang Song, Tao Li +5
University of Pennsylvania · University of Toronto · Google DeepMind +1