Formalize, Don’t Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers

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

question and benchmark

This paper studies whether LLM-generated combinatorial solvers are more reliable when the model formalizes a problem for a solver backend than when it writes a complete algorithm or adds search heuristics. It introduces CP-SynC-XL, an extension of the CP-SynC benchmark: 100 heterogeneous problems (58 CSPs and 42 COPs) and 4,577 parameterized instances (median 60 per problem; Sec. 4.1, p. 5). The abstract reports: “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).” (abstract, p. 1). The instance count is inconsistent inside the paper: Appendix B.3 says “This filtering leaves 2,565 instances in the final evaluation set reported in the figures and tables.” (App. B.3, p. 16), Tables 6 and 8 use N = 2,565, and Table 5 uses N ≈ 4,500. Inference: the Table 1 fractions are therefore probably over the filtered 2,565-instance pool, not over 4,577; the paper does not say so in the Table 1 caption.

The benchmark includes constraint-satisfaction and constraint-optimization problems drawn from CSPLib and the PyCSP3 problem suite, and each problem ships with a reference verifier for CSP feasibility and COP optimality against a curated reference solver (Sec. 4.1, p. 5). Each generated solver receives a natural-language problem, typed input parameters, and an output schema. Correctness means that the returned output passes the reference verifier; a schema-valid output alone is only “provided.” The paper defines fidelity as correct/provided, the fraction of returned answers that pass verification (Sec. 4.2, p. 6).

The controlled factors are representation and prompt. The three representations are (1) native Python search, where the LLM must implement pruning, dynamic programming, branch-and-bound, or another algorithm with the standard library; (2) Python plus OR-Tools CP-SAT, where the LLM declares variables, constraints, and objectives and CP-SAT searches; and (3) MiniZinc plus OR-Tools, where the LLM writes a declarative model and a formatter converts assignments to the required schema (Sec. 3.1, pp. 3–4; the MiniZinc paradigm follows the two-step pipeline of Song and Cohen 2025). Each representation receives a baseline correctness prompt and a heuristic prompt that additionally asks for efficiency.

generation and independent validation

Apply the common pipeline in these steps. First, prompt the model to generate the solver artifact. Second, run a smoke check on a small instance: execute solve_instance(data_dict) for the Python and Python + OR-Tools variants, or compile and solve the MiniZinc model and then run the formatter, and validate the returned dictionary against the expected output schema and value ranges. Third, run a scaling check on a harder instance under a tighter time budget (Fig. 2 calls it a separate mid-difficulty instance; App. C gives a 30 s execution limit). Fourth, if either check fails, feed the artifact and failure feedback back to the model for up to four refinement rounds. Fifth, record the earliest artifact that passes the smoke check (the first-working artifact) and the first artifact that also passes scaling as the final artifact (or the most recent revision if none passes within the budget). Sixth, run both artifacts on every benchmark instance and compare outputs with the reference verifier. The paper emphasizes the scope of the first checks: “Neither stage verifies solution correctness against the reference solver; SAT/UNSAT checking is deferred to the downstream evaluation described in Sec. 4.2” (Sec. 3.2, p. 4), where both artifacts are checked against the reference. Refinement is mostly runnability recovery: “refinement is dominated by basic runnability recovery—fixing crashes, format violations, and timeouts—not by speedups on solvers that already run” (Sec. 3.2, p. 5).

The evaluation framework imposes all solver runtime budgets externally (256 s per instance in the evaluation) and the prompt forbids generated code from setting internal time or step limits and from registering callbacks whose purpose is early stopping. It also enforces the assigned backend: Python + OR-Tools must use ortools.sat.python.cp_model only, with no pure-Python fallback or third-party solver such as gurobipy. The paper says that without this clause LLMs wrapped CP-SAT in a try/except that fell back to a hand-rolled Python loop, which would contaminate the paradigm comparison (Sec. 3.3, pp. 4–5).

Inference: For Verus, this is a direct pattern for separating runnability from proof validity. A generated Rust function could first compile, then pass a small proof smoke check, then be checked on a larger proof suite; only the final Verus run can establish correctness. A verifier must reject an artifact that compiles but has a weakened ensures clause. Verus proof obligations and Rust contracts replace CP-SAT’s reference checker; the paper does not study Verus.

representation results

At the 256-second budget, Python + OR-Tools has the highest correctness for every LLM. Table 1 gives the fractions (instance pool: see the 2,565 versus 4,577 inconsistency above). For DeepSeek-V3.2, baseline Python + OR-Tools correctness is 0.439 and fidelity is 83.9% (0.439/0.523 provided). GPT-5.3-Codex reaches 0.702 correctness and 89.3% fidelity (0.702/0.786). Gemini 3.1 Pro reaches 0.716 correctness and 87.8% fidelity (0.716/0.816). MiniZinc + OR-Tools has higher conditional fidelity but lower overall correctness; the text says it “maintains ≥ 83% fidelity on every (LLM, prompt) pair” (Sec. 4.3, p. 6). Native Python has the lowest fidelity, bottoming at 51.9% for DeepSeek-V3.2 under the heuristic prompt (Table 1, p. 6). The text says Python + OR-Tools fidelity goes “down to 65.0% on DeepSeek-V3.2’s heuristic prompt”, but Table 1 gives 67.8% (0.365/0.538); the paper does not reconcile the two. Inference: for DeepSeek-V3.2 baseline, Tables 6 and 8 imply wrong-mass shares (18.3% for Python + OR-Tools, 28.8% for Python) that exceed Table 1’s provided-minus-correct gaps (8.4 and 18.7 points), while GPT-5.3-Codex and Gemini 3.1 Pro agree; I did not resolve this.

The paper attributes the correctness advantage to delegating search to CP-SAT (Sec. 4.3, p. 6): “The advantage is not that the LLM performs more combinatorial reasoning in Python; rather, delegating search to CP-SAT moves the main burden from designing a complete algorithm to encoding the variables, constraints, and objective faithfully.” The backend is shared by the two solver-backed paradigms, so the paper says the MiniZinc gap “is consistent with a surface-fluency bottleneck rather than a weaker back-end” (p. 6); this is an interpretation, not a tested cause. The paper also says it does not claim this for other backends (App. A).

The outcome decomposition is useful for auditing. Every artifact-instance pair is classified as correct, suboptimal, UNSAT, invalid, or no solution. In the Python + OR-Tools baseline, the paper manually audited the top twelve problems by aggregated UNSAT mass (750 of 837 instances, 89.6%, across all three LLMs) and says “every audited case is a natural-language-to-formal-language mistranslation” (Sec. 4.4, p. 8). The paper names four mechanisms: associative recall (M1: the LLM names the problem before it reads it), long-spec attention drift (M2: one or two textual constraints are silently dropped), output-schema ambiguity between LLM and verifier (M3), and sentinel-value misreading (M4). Appendix F.3 (p. 24) gives the audited counts: M1 120 (16%), M2 282 (38%), M3 270 (36%), M4 78 (10%), which sum to 750, so the percentages are shares of the 750 audited instances. Sec. 4.4 says M2 and M3 together are about 75%; App. F.3 says about 74%. The audit is of one setting (Python + OR-Tools baseline); the paper also describes a fifth, Python-only mechanism M5 (search-procedure bugs; App. F.4, p. 25) that the study does not otherwise cover.

Inference: In VL, this is evidence to prioritize faithful contract and invariant translation before optimizing proof search. A Verus agent should preserve every natural-language requirement as explicit requires, ensures, state-machine transition, or invariant clause, then use the verifier to catch omitted or contradictory conditions. The M1–M4 taxonomy predicts failures in agent-written specifications even when the underlying solver is sound.

heuristic trap and its checks

The heuristic prompt adds stronger variable/value ordering, pruning, and problem decomposition for Python, and tighter bounds, redundant or implied constraints, symmetry breaking, and explicit search annotations (int_search in MiniZinc, AddDecisionStrategy in CP-SAT) for the two solver-backed paradigms (Sec. 3.1, p. 4). The paper compares each heuristic artifact with its paired baseline while holding the LLM, decoding parameters, instances, evaluator, timeouts, and refinement budget fixed (Sec. 3, p. 3).

The effects are small and inconsistent for the stronger models: the paper says “every paradigm-by-metric change stays within ±3.6 percentage points (pp) of the baseline” for GPT-5.3-Codex and Gemini 3.1 Pro (Sec. 4.3, p. 7). From Table 1, this holds for the correctness and fidelity columns; the provided column moves more (for example Gemini 3.1 Pro Python, 0.708 to 0.761). For DeepSeek-V3.2, heuristic prompting gives “−7.4 pp of correctness and −16.1 pp of fidelity on Python + OR-Tools, plus −9.0 pp of fidelity on Python” (p. 7). Sec. 5.1 (p. 8) reports the macro-averaged per-problem correctness change as as much as −6.6 pp on Python + OR-Tools for DeepSeek-V3.2, a different aggregation. The abstract reports “only small median speed-ups (1.03–1.12×)”. The paper defines the heuristic trap as “the recurring pattern in which an efficiency-oriented prompt induces unverified bounds, local approximations, or overcomplicated constraints that sometimes target speed but reduce correctness or fidelity” (Sec. 1, p. 2).

A paired code audit identifies six heuristic failure modes (Sec. 5.2, p. 8): A unverified “tight” bounds (Python + OR-Tools; 13.5% incidence), B Big-M / MTZ rewrites that weaken propagation (Python + OR-Tools; 4.0%), C hand-computed seeding (Python + OR-Tools; 19.5%), D silent loss of completeness (Python; 16.2%), E COP-to-SAT collapse against an unproven optimum (MiniZinc + OR-Tools; 0.7%), and F overcomplicated redundant-machinery blow-ups (MiniZinc + OR-Tools; 29.1%). Each mode is marked by a source-level detector that the paper calls conservative; App. G (p. 27) says the detectors are “not formal proofs that the pattern caused every downstream failure”. The paper measures both correctness change and runtime ratio per mode (Table 2, p. 9). For Python and Python + OR-Tools, the median per-problem speedup is about 1.0× for every LLM, and 40–63% of common-correct instances are slower with the heuristic prompt. The paper says MiniZinc + OR-Tools “is the only paradigm where heuristics operate at the model level so CP-SAT can exploit them deterministically” (Sec. 5.1, p. 8); even there, Mode F drives both its speed-ups and its heaviest regressions (Sec. 5.2, p. 9). The paper also reports that refinement often preserves the injected heuristic rather than removing it (App. C, p. 18). The conclusion is explicit: “The practical implication is to use the LLM primarily at the formalisation interface—variables, constraints, objectives, and carefully scoped solver-native annotations—and to subject LLM-authored search optimizations to independent validation.” (Sec. 6, p. 10)

Inference: In Verus, “formalisation interface” means contracts, state abstractions, invariants, and proof lemmas whose semantics are checked by Verus. An LLM-generated solver hint, trigger, or proof shortcut should be treated as an optimization candidate and replayed against the unchanged specification. Verus does not expose CP-SAT’s search-annotation API, so the specific six modes require a Verus-specific audit.

trusted evidence and product threat

Inference: the evidence rests on trusting the reference verifier, reference solver, benchmark instance generators, output schemas, timeout controller, and the authors’ manual audits; the paper gives no independent check of these. The paper’s correctness fractions are instance-level fractions at 256 seconds; they are not proof completeness rates. A schema-valid answer can still be rejected, and the “no solution” bin covers “timeout, crash, or schema violation” (Sec. 4.4, p. 7), mostly 256 s timeouts. The benchmark uses three named frontier LLMs from a “late-2025 snapshot”, fixed prompts, at most four refinement rounds, greedy sampling (T = 0), and one external evaluation protocol (App. A, p. 12); the paper does not establish behavior for Verus, Rust, or other models.

Inference: The threat to VL is high for specification translation and moderate for proof-search optimization. An agent can produce a compiling, plausible, verifier-rejected contract or omit a requirement while preserving syntactic validity. The paper supports a product rule: let the agent formalize into a sound backend, keep search optimizations scoped, and independently validate every optimization against the reference specification. VL should not redo a generic benchmark of LLM combinatorial solving; the reusable gap is measuring faithful Rust/Verus formalization and proof maintenance.

techniques for the catalog

• solver-surface comparison — compare native algorithm synthesis with Python API and declarative constraint modeling
• smoke validation — run a generated artifact on a small instance and check execution plus output schema
• scaling validation — rerun on a harder instance under a tighter, externally imposed time budget
• feedback refinement — send failed artifacts and diagnostics back to the LLM for a bounded number of repair rounds
• reference-verifier checking — distinguish schema-valid outputs from outputs that pass feasibility or optimality verification
• fidelity metric — report correct/provided with its instance denominator
• outcome decomposition — classify correct, suboptimal, UNSAT, invalid, and no-solution results
• mistranslation audit — manually inspect the problems with the most UNSAT mass for recalled templates (M1), dropped constraints (M2), schema ambiguity (M3), and sentinel misreads (M4)
• heuristic paired audit — compare baseline and heuristic artifacts with fixed models, data, budgets, and evaluators, and tag regressions with source-level failure-mode detectors
• formalization-first design — use the LLM for variables, constraints, objectives, and scoped annotations, then independently validate search optimizations Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Due to time and compute constraints, we impose a 256 s runtime limit when validating each candidate instance with the reference solver.”): read the paper text from first line to last; checked every quotation, number, section and page reference, and the generation-pipeline steps against the text and Tables 1, 2 and 5-10; changed the abstract quote and page references (Sec. 3.3 is pp. 4-5, the audit text is on p. 8, Sec. 5.1 is on p. 8, the conclusion sentence is on p. 10), the audit percentage denominator (750 audited instances, not 837), the Sec. 3.2 quote ending, the “only setting” wording, and the instance-count and Table 1 versus text inconsistencies; labelled the trust paragraph as inference; I kept the tag, although the first author is Haoyu Wang and the second is Yuliang Song, because the file name is fixed, and the arXiv link comes from the arXiv stamp in the paper text; I did not check figures, the released code or logs, the cited related work, or any of the per-mode code extracts beyond what the text states.

Last edited: 2026-10-17