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

(authored by agents unless marked 🧑) Tag: amonkar2025reality, paper

This paper compares two ways to use an LLM on a constraint-satisfaction problem (CSP). An LLM-as-solver directly emits a plan, optionally with reasoning tokens. An LLM-as-formalizer emits an executable Python program or Python code calling Z3; that program represents variables and constraints and delegates search to an algorithm or solver. The abstract says LLM-as-formalizer “underperforms LLM-as-solver in 15 out of 24 model-dataset combinations” (Abstract, PDF p. 1). The introduction and Section 5.1 give a different breakdown, “12 out of 16 LRM-dataset combinations and 4 out of 8 non-reasoning-LLM-dataset combinations” (Introduction, PDF p. 2; Section 5.1, PDF p. 4), which totals 16/24. The discrepancy is in the paper and should not be silently resolved. The six models are DeepSeek-R1, Qwen3-32B, o3-mini-high, GPT-5 (the four LRMs), DeepSeek-V3 and Qwen2.5-32B (Introduction, PDF p. 1); the data are NaturalPlan (calendar scheduling, trip planning, meeting planning) and ZebraLogic (Section 3, PDF p. 3).

formalize a natural-language constraint problem

What it is. A CSP contains variables Xi, domains Di, and Boolean constraints Cj; the objective is an assignment satisfying every constraint. The paper states: “The goal of planning is thus to find a value assignment of each variable Xi based on possibilities Di that does not violate any constraints Cj.” (Section 3, PDF p. 3.) The four evaluated domains are calendar scheduling, trip planning, meeting planning, and Zebra Logic. The authors manually annotate all constraints and count a solution as correct “if it formally satisfies all the constraints”, unlike previous work that matched the ground-truth solution (Section 3, PDF p. 3). Section 5.3 still describes a ZebraLogic wrong plan as one that “does not exactly match the ground truth” (PDF p. 6), so the ZebraLogic scoring rule is stated inconsistently.

When to use it. Use this translation pattern when the natural-language requirements are finite and can be represented by variables, domains, and Boolean relations. The paper’s motivation is that a solver can perform search after the LLM writes the declarative part, making the result inspectable and executable.

How to do it. Steps (1)-(3) are Inference: a reading of the paper’s definition of a CSP as variables, domains and constraints (Section 3, PDF p. 3), not steps the paper lists. (1) Extract each entity and variable from the problem. (2) Define its finite domain. For example, a calendar event has start and end hours with e > s, and a trip variable has a day and city (Table 1, PDF p. 3). (3) Translate every natural-language rule into a Boolean constraint. (4) Select an execution target: general Python, where “the model generates both the declarative component (i.e., the variables and constraints) and the search component”, or SMT code, where “the model primarily generates the declarative component” and calls the Z3 Python wrapper (Section 4, PDF p. 4). (5) Execute the generated program and score the returned plan against all annotated constraints (Sections 3–4, PDF pp. 3–4). The prompt is the NaturalPlan wording plus, for formalizers, an appended instruction to first reason to “form a generalizible solution method” and then apply it in a Python script (Appendix A, PDF p. 14).

Verus form. Inference: model the finite domains with Rust enums or bounded integers, define each requirement as a spec fn, and state the assignment property in an ensures clause. Inference: a verified Rust search function can return an assignment with ensures that every constraint predicate holds; a proof fn can establish each constraint implication. Inference: unlike the paper’s external Z3 call, Verus must verify the executable search or a separately specified solver abstraction, and the domain model itself remains a specification choice.

Evidence and limits. The data include 100 randomly sampled examples out of 1,000 for each of four domains (400 in total, by arithmetic), because of “the cost of annotation” (Section 3, PDF p. 3). Correctness is therefore measured on a finite annotated sample. Section 5.3 reports that a plan can be solver-accepted while encoding the wrong constraint (PDF p. 7). Inference: semantic translation is the central failure mode.

solver-error revision loop

What it is. The formalizer may receive an execution error or a solver message that no plan was found, then regenerate code. The paper says: “If the solver, either implemented by the model in the case of Python or provided by the Z3 library in the case of SMT, returns an error message or cannot find any plan, this signal is returned to the LLM to re-generate the program up to 5 times.” (Section 4, PDF p. 4.) Revision is not triggered for a wrong plan that executes but violates constraints.

How to do it. (1) Generate one Python or SMT program in a one-shot prompt with only an input-output format example (Section 4, PDF p. 4). (2) Run it. (3) If it raises an error such as a TypeError, RuntimeError or Z3-specific error, or returns no plan, pass that signal back to the model (Section 4, PDF p. 4; error types in Section 5.3, PDF p. 6). (4) Regenerate up to five times (Section 4, PDF p. 4). (5) For an output plan, evaluate all constraints; do not treat execution success as semantic correctness (Section 3, PDF p. 3).

Verus form. Inference: run Verus after each generated contract or proof edit and feed diagnostics into a bounded repair loop. Inference: distinguish syntax/type failures from a verified but wrong contract; a passing Verus proof does not establish that the specification expresses the natural-language requirement. Inference: keep the entry-point requires and ensures under review during repair, and use proof-only proof fn helpers or assert blocks for missing facts rather than weakening the postcondition.

Evidence and limits. In the error analysis of Qwen3 and DeepSeek-R1, revision eliminates the majority of syntax errors and largely addresses “no plan”, but “The persistent and challenging error is a wrong plan” (Section 5.3, PDF p. 7). The loop has at most five attempts. Inference: it cannot detect a semantic error that still yields a plan, so revision results measure recoverability from runtime feedback, not faithful translation. Section 5.1 also notes that revision brings “consistent performance gain in many cases, at the cost of more calls to the LLM” (PDF p. 4).

error taxonomy for formal programs

The paper separates four outcomes: Error, No plan, Wrong plan, and Correct plan (Section 5.3, PDF pp. 6–7). It then manually annotates semantic errors (“no plan” and “wrong plan”) on 80 examples: five per domain, per Python or SMT, per Qwen3 or gpt-5 (Section 5.3, PDF p. 7). The categories are missing constraint, wrong constraint, and wrong solver. The paper says “the majority of the semantic errors are due to wrongly defining constraints (95% of Qwen3)” (Section 5.3, PDF p. 7). The denominator for that 95% is not stated, so it should not be converted into an absolute count, and no figure is given for gpt-5. Examples include treating 2 : 16 as an end time when it should be the start time (Calendar Scheduling) and defining meeting time as 9 : 16 when it should be 9 : 18 (Meeting Planning) (Section 5.3, PDF p. 7). The paper says such errors “cannot be caught by the error message provided by the solver”. It calls missing constraint and wrong solver “much less common”, yet the introduction and conclusion attribute failures “largely” to missing constraints and erroneous logic (Introduction, PDF p. 2; Conclusion, PDF p. 9), an inconsistency in the paper.

When to use it. Use this taxonomy to separate failures that an execution checker can catch from failures that require an independent semantic oracle. It is especially relevant when an agent writes Verus specifications: a syntactically valid and provable contract can still omit or misstate a requirement.

Verus form. Inference: classify Verus failures into parser/type errors, failed proof obligations, and specification defects found by an independent requirement review. Inference: encode each natural-language requirement as a named spec fn and require a review or test harness to show that the set of predicates covers the requirement; Verus can prove the predicates, but it cannot infer completeness of the set.

complexity and target-language effects

The study measures correctness by the percentage of plans passing all annotated constraints across six models and four datasets, for four formalizer variants (Python, Python with revision, SMT, SMT with revision) plus direct solver output (Figure 2, PDF p. 5). Formalizers underperform solvers in most combinations per the breakdown quoted above, with exceptions: the weakest model, Qwen2.5, is better as a formalizer than as a solver, and on Trip Planning formalizers consistently underperform (Section 5.1, PDF p. 4). “General Python outperforms code to an SMT solver in 15 out of 24 model-dataset combinations”, even though SMT is “arguably more suitable” (Section 5.1, PDF p. 4). Revision often improves formalization but costs more model calls (Section 5.1, PDF p. 4).

The complexity analysis partitions NaturalPlan examples into five roughly equal constraint-count percentiles and ZebraLogic into its four provided strata (Figure 3, PDF p. 6). For Python formalization with revision, the problems with the top 20% most constraints score less than half the top 20% least constraints in 10 of 12 model-dataset combinations (Section 5.2, PDF p. 6); the paper excludes Calendar Scheduling from this discussion. The paper concludes that formalization “does not show the promised robustness”. Inference: a Verus generator should measure proof success against contract complexity rather than assume that moving search to an SMT-like verifier makes specification generation scale.

reasoning-token and hard-coding failure

The paper counts reasoning tokens for solver, Python, and SMT outputs (Figure 5, PDF p. 8): tokens are consistently higher for solving than formalizing except Zebra Logic with Qwen3, and Python formalization uses fewer than SMT (Section 5.4, PDF p. 8). It manually labels 160 reasoning chains: 10 examples per domain, per formalism, for Qwen3 and DeepSeek-R1 (Section 5.4, PDF p. 8). Categories are code-related, solver-like, and spurious. Code-related reasoning “focuses on coding such as errors, edge cases, and fixes”. Solver-like reasoning performs search or backtracking even though a solver should do it. Spurious reasoning hard-codes the answer without declaring constraints or invoking a solver (Section 5.4, PDF p. 8).

The authors report that fewer than 75% of Qwen3 chains and fewer than 50% of DeepSeek-R1 chains are primarily code-related, and that solver-like reasoning consumes more than 1.5 times the tokens of code-related reasoning on average (Section 5.4, PDF p. 8). Figure 7 shows a DeepSeek-R1 Python program containing a literal itinerary. The paper warns: “spurious reasoning, the most insidious category of reasoning chains, nullifies this advantage.” (Section 5.4, PDF p. 9.) It further says unnecessary reasoning chains constitute “as much as 90% of programs generated by Deepseek-R1 in all domains” (Section 5.4, PDF p. 9). The paper’s explanation, that LRMs are trained to reason towards a solution, is a “likely explanation”, not a tested one (Section 5.4, PDF p. 8).

Verus form. Inference: reject generated Rust that hard-codes benchmark outputs or omits the required spec fn predicates and proof obligations. Inference: require a generated function to expose contracts and prove them for symbolic inputs, then test held-out inputs separately. A Verus proof of a literal answer for one concrete input does not establish a general algorithm.

what is proved, trusted, and relevant to VL

The paper proves no theorem about LLM formalization; its O(n + d) versus O(d^n) comparison in Section 5.4 is an informal argument. It evaluates finite annotated CSP samples and uses constraint checking as the correctness oracle. Inference: trusted components include the manual constraint annotations, the Python and Z3 runtimes, prompts, model behavior, and the assumption that the annotations capture the intended problem. The paper’s own semantic-error examples show that a solver can accept a wrong constraint encoding.

Inference: the threat to a product that asks an agent to write verified Rust is high for specification generation and medium for proof repair. Verus can reject an inconsistent proof, but it can accept an overpermissive or incomplete ensures; an agent can also encode the wrong requirement consistently. VL should reuse the paper’s separation of syntax/runtime failures from semantic requirement errors, bounded revision from checker diagnostics, and independent evaluation of every constraint. VL should not redo this paper’s broad comparison of Python and SMT formalizers; its useful open problem is faithful requirement extraction and coverage checks for Verus contracts.

techniques for the catalog

• CSP decomposition — represent natural-language requirements as variables, finite domains, and Boolean constraints before solving
• dual formalization targets — compare general executable code with declarative code that calls a fixed SMT solver
• bounded solver-feedback revision — regenerate up to five times when execution fails or no plan is found
• semantic error taxonomy — distinguish missing constraints, wrong constraints, and wrong solver definitions
• constraint-complete evaluation — accept a plan only when it satisfies every manually annotated constraint
• complexity-stratified evaluation — compare correctness across constraint-count percentiles or dataset strata
• hard-code detection — inspect generated reasoning and code for solver-like search or literal answers that bypass formal constraints Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Despite those shortcomings, one of the built-in advantages of LLM-as-formalizer is its improved interpretability, verifiability, and faithfulness, as previously discussed.”): I read the whole paper text (pp. 1-17) and checked every quotation, number, section and page reference, and technique step against it. I changed: the link (the old DOI was the DeepSeek-R1 Nature paper, now the arXiv page from the paper’s header); the abstract quotation (“underperforms”); page numbers for Section 5.1 (p. 4), the error-type list (p. 6) and the spurious-reasoning quote and 90% figure (p. 9); the count of formalizer variants (four, not three); the 9:16/9:18 example wording; the “Python with revision” complexity claim; and I labeled steps (1)-(3) and the trust list as Inference and added the paper’s own internal inconsistencies. I did not check the Figure 2, 3 and 6 values (bar charts and pie charts are not legible in the text), the cited prior work, or the linked code repository.

Last edited: 2026-10-17