Repairing LLM-Generated Specifications with Deterministic Diagnosis

1 Introduction

• Runnable specifications can still encode semantic errors, while LLM-based diagnosis without a reference can miss errors or falsely flag correct artifacts and cause regressions.Solver feedback becomes sparse once execution succeeds, leaving little actionable feedback for repair.Source: §1 · pp. 1–2
• DRAGO diagnoses candidate artifacts with deterministic, formalism-specific checks and retains rewrites only when an evidence-gated predicate confirms strict error-weight reduction.The framework is instantiated for logical reasoning, constraint programming, and planning.Source: §1 · p. 2
• DRAGO improves answer accuracy by 12.9 percentage points over zero-shot formalization and 8.7 percentage points over LLM-diagnostic repair, while reducing regressions to 1.3% from 11.8%.The regression rates are among initially correct artifacts; results span five benchmarks and four models.Source: §1 · p. 2
• Two rendering defects make 50% (3,086 instances) of Planetarium’s floor-tile test split inconsistent with its references; the authors patch the affected instances and release a corrected split.The defects highlight that benchmark instances can themselves undermine reliable evaluation.Source: §1 · p. 2

2 Related Work

• Solver-backed formalization spans logical reasoning, planning, and constraint modeling, but shifts the challenge to faithfully translating natural-language semantics into formal artifacts.Examples include Logic-LM, SatLM, and LINC (Olausson et al., 2023; Pan et al., 2023; Ye et al., 2023), and planning systems (Liu et al., 2023; Hao et al., 2025a; Huang and Zhang, 2025).Source: §2 · pp. 2–3
• Execution, validator, and symbolic-diagnosis approaches use feedback to repair artifacts, whereas DRAGO relies on the problem statement and artifact alone through an interface shared across formalisms.Prior examples include Logic-LM (Pan et al., 2023), OptiMUS (AhmadiTeshnizi et al., 2024), and planning validators such as VAL.Source: §2 · p. 3
• LLM self-critique and self-verification have documented reliability limits without references, while emerging approaches incorporate external evidence and verification.Examples include intrinsic self-correction (Huang et al., 2024), self-verification (Stechly et al., 2025), and behavioral probing (Lian et al., 2026).Source: §2 · p. 3

3 Methodology

• The framework represents a natural-language problem as an artifact in a solver-facing language, executed by a backend to expose an observable trace.The trace may include parse status, errors, solver status, proof outcomes, objective values, assignments, or planner metadata.Source: §3 · p. 3

3.1 Existing Repair Feedback and Its Limitations

• Successful execution can leave semantic errors such as omitted constraints or incorrect objectives undetected because execution feedback vanishes in the silent-success region.Execution failures can provide reliable signals, but successful execution does not establish alignment with the natural-language intent.Source: §3.1 · p. 4
• LLM self-review diagnoses alignment without a ground-truth reference, creating a noisy channel that can miss errors or hallucinate flaws in correct artifacts.A generic repair policy conditions each proposed rewrite on the current artifact, trace, and feedback history.Source: §3.1 · pp. 3–4

3.2 DRAGO: Deterministic Diagnosis and Evidence-Gated Repair

• DRAGO diagnoses a candidate from the problem, artifact, and observable execution trace, then gives structured findings and repair instructions to a revision model.Its checks are formalism-specific, while the repair interface is shared across formalisms.Source: §3.2 · p. 4
• DRAGO combines contract checks, reference-free solver probes, and specification-alignment checks; lexical cues are advisory and cannot trigger rewrites alone.Examples include checking schema consistency, localizing conflicts with deletion probes, and comparing stated object counts with PDDL objects.Source: §3.2 · p. 4
• A rewrite is retained only if it is well-formed, strictly reduces the weighted blocking findings, and satisfies conservatism checks; accepted rewrites therefore cannot cycle.The predicate is not a correctness oracle and does not consult benchmark answers.Source: §3.2 · p. 5

Domains, Benchmarks, and Models

• The evaluation spans MiniZinc on Text2Zinc and CP-Bench, SMT-LIB2 on FOLIO and ProverQA-hard, and PDDL on Planetarium.The four models comprise two Anthropic models, Qwen3-Coder 30B, and Gemma 4 31B.Source: §4 · p. 5

Metrics

• Accuracy is instance-level: answer-level correctness for FOL and CSP, and semantic equivalence to the reference for PDDL.For FOL and CSP, a correct answer need not imply an exact match to intended semantics.Source: §4 · p. 5

Baselines and Implementation Details

• DRAGO is compared with zero-shot generation and LLM-diagnostic repair, using the same generation and repair model while differing in diagnosis and acceptance.Both repair methods use a one-round budget, and each formalism uses one DRAGO configuration across evaluated models and benchmarks.Source: §4 · pp. 5–6

Domains, Benchmarks, and Models

• Table 1 reports mean accuracy percentages and sample standard deviations; Planetarium uses 300 sampled problems, including 58 inconsistent references that cap accuracy at 80.7%.The table marks each model-benchmark best method and shows DRAGO's gain over the best baseline.Source: Table 1 · p. 6

5.1 Main Results

• DRAGO improves accuracy over zero-shot generation for every model on every benchmark and achieves the best performance in 19 of 20 model-benchmark comparisons.It also has a higher mean than LLM-diagnostic repair on every CSP benchmark.Source: §5.1 · p. 6
• Across FOL and CSP, DRAGO gains about 13 points on ProverQA-hard for both hosted models and up to 27 points for hosted models and 36 points for Gemma on CSP.Its sole loss to LLM-diagnostic repair is Text2Zinc/Qwen, by 2.4 points, though DRAGO still improves over zero-shot there.Source: §5.1 · p. 6
• PDDL gains range from 0.6 percentage points for Sonnet to +8.2 percentage points for Gemma, despite an approximately 80.7% benchmark-defect ceiling.Unconditional self-review costs Sonnet 9.4 points and Qwen 7.2 points.Source: §5.1 · pp. 6–7

5.2 Do Repairs Fix More Than They Break?

• On FOLIO and ProverQA-hard, LLM-diagnostic repair breaks 5.7% and 7.3% of all instances, while DRAGO holds regressions to about 1%.The figure partitions instances into wrong-to-right, right-to-wrong, and no-change transitions; pooled across runs, DRAGO breaks 1.3% of initially correct artifacts versus 11.8% for LLM-diagnostic repair.Source: Figure 1 · p. 7, §5.2 · p. 7

5.3 Diagnosis or Acceptance Gate?

• Holding acceptance fixed, DRAGO outperforms LLM-d+A in 16 of 20 configurations by +7.1 points on average; removing the gate costs 5.1 points in FOL, 1.8 in CSP, and 0.9 in PDDL.The ablations attribute repair of incorrect artifacts to grounded diagnosis and preservation of correct ones to the acceptance gate.Source: Figure 2 · p. 7, §5.3 · pp. 7–8

6.1 State-of-the-Art Comparison

• DRAGO beats or ties sample-and-select in all ten hosted configurations and its oracle in nine, by up to 18.2 points; it leads three of four FOL and three of four CSP configurations against domain-specific systems.Table 3 compares open-source models in single-trajectory configurations: Draft-and-Prune for FOL and CP-SynC for CSP.Source: §6.1 · p. 8, Table 3 · p. 8

6.2 Diagnosis Quality

• On hosted FOL runs, DRAGO raises a blocking finding on 95.3% of initially wrong artifacts and 42.6% of initially correct ones, while its gate rejects 94.6% of proposed rewrites that would break correct answers.LLM self-review flags 100% of initially wrong and 90.6% of initially correct artifacts.Source: §6.2 · p. 8

6.3 Pitfalls in Evaluating Formalization Tasks

• Two Planetarium rendering defects make exactly half of the 6,172 floor-tile split rows inconsistent with references; fixing the problem text recovers 90% of Haiku misses and 84% of Sonnet misses on that family.The audit also found 58 of 100 sampled floor-tile instances inconsistent.Source: §6.3 · p. 8

• DRAGO combines deterministic, reference-free diagnosis with evidence-gated acceptance to improve translation from natural-language problems into formal specifications.Source: §7 · pp. 8–9
• Regressions fall nearly an order of magnitude (1.3% vs. 11.8%) while accuracy improves over both zero-shot generation and LLM self-review.DRAGO also outperforms state-of-the-art per-domain baselines in most configurations with a comparable or lower inference budget.Source: §7 · p. 9
• Two Planetarium defects are uncovered, and the paper releases a corrected split.Source: §7 · p. 9

• For FOL and CSP, answer accuracy does not establish full semantic equivalence, since an artifact may answer correctly while encoding unintended semantics.A different query could expose those unintended semantics.Source: Limitations · p. 9
• Execution-blind under-constraint remains a shared blind spot: omitted axioms, constraints, or goal conditions can execute cleanly without observable failure.Source: Limitations · p. 9
• DRAGO’s repair pattern transfers across formalisms, but each new formalism requires its own diagnostic rules.The typed-finding interface and acceptance discipline are reused.Source: Limitations · p. 9

• DRAGO uses the natural-language instance, current artifact, execution trace, and deterministic diagnoses, but not a reference formalization or gold answer during generation and repair.Final benchmark correctness is used only after the candidate is returned for scoring.Source: §A.1 · p. 12
• The procedure generates and executes an initial artifact, computes diagnoses, and asks an LLM to rewrite it using those findings as targeted feedback.Source: §A.1 · p. 12
• A candidate rewrite is executed and accepted only if reference-free acceptance checks pass; repair stops when no blocking diagnosis remains or the budget runs out.The formalism-specific diagnosis sources and acceptance rules are collected in Table 4.Source: §A.1 · p. 12

• Each formalism’s configuration was distilled from disjoint development data, then frozen and applied unchanged across its benchmarks and evaluated models.ProverQA-hard was fully held out for the FOL configuration; CP-Bench contributed no development instance.Source: §A.2 · p. 12
• Diagnostic potential is lexicographic over execution status and blocking findings, and a candidate is retained only when it strictly reduces that potential.The previous state is restored if no candidate reduces it.Source: §A.2 · p. 12
• Table 4 collects the diagnostic classes and acceptance conditions instantiated for each formalism.Source: Table 4 · p. 13
• FOL checks the SMT-LIB2 contract, premise consistency, entailment status, and possible underdetermination, while alignment checks can flag missing exclusive disjunctions.Sentence-aligned or-to-xor upgrades may be deterministic; other undetermined-to-definite flips require corroboration from an independently generated formalization, subject to a narrow false-salvage exception.Source: §A.2 · pp. 13–14
• MiniZinc checks the model and data schema, uses block-deletion probes to localize unsatisfiable requirements, and lints countability and magnitude or unit mismatches.Source: §A.2 · p. 14
• PDDL checks parsing, grounding, domain and predicate use, and goal form, while planner probes identify unreachable goal atoms or prove joint unsolvability when search exhausts.Timeouts yield no evidence; alignment checks compare stated counts with declared object counts, while identifier-like tokens absent from the declared objects are advisory.Source: §A.2 · p. 14
• PDDL acceptance requires passing the artifact contract, strictly reducing blocking-finding weight without a new finding on a clean axis, and passing conservatism checks against repair-by-weakening.Goal-atom counts may not decrease, and per-category object counts may move only toward counts stated in the problem.Source: §A.2 · p. 14

A.3 Prompt Templates

• The paper uses compact prompt summaries rather than verbatim prompts.Full templates, including formatting instructions, are provided in the released codebase.Source: §A.3 · p. 14
• For runnable artifacts, the LLM-diagnostic baseline first asks for concrete modeling issues or no issue, then requests a rewrite using that feedback.The baseline uses the same artifacts but replaces deterministic diagnosis with LLM self-review.Source: §A.3 · p. 14
• The baseline review is limited to the problem statement, current artifact, executor output, and self-review feedback, without a reference formalization or known answer.Source: §A.3 · p. 14

FOLIO and ProverQA-hard

• The curated FOLIO validation split contains 73 story rows and 202 conclusion examples, while ProverQA-hard contributes 500 examples for deeper multi-step reasoning.FOLIO uses an expert-curated validation release; ProverQA-hard complements it with a controlled set built using symbolic-prover validation.Source: §A.4 · pp. 14–15

Text2Zinc

• The verified Text2Zinc-style file contains 110 instances: 55 minimization, 45 maximization, and 10 satisfaction problems.Reference-answer relabeling corrected straightforward metadata errors, often objective values that did not match the released model/data or source artifact; it was not an expert semantic audit.Source: §A.4 · pp. 15–16

CP-Bench

• The verified CP-Bench subset contains 63 instances: 45 satisfaction, 13 minimization, and 5 maximization problems.It uses the Text2Zinc MiniZinc-facing schema; satisfaction is scored by feasibility and optimization by the corrected objective/output contract.Source: §A.4 · p. 16

Planetarium

• Planetarium evaluation uses a shared seeded sample of 300 problems, with 100 drawn from each of blocksworld, floor-tile, and gripper.The draw is reproducible using Python’s random.Random(42).Source: §A.4 · p. 16
• 50% (3,086 instances) of Planetarium’s floor-tile test split carry two rendering defects: robot positions are lost and adjacency relations are reversed.The defects occur together in all 3,086 rows with init_is_abstract=false; none of the rows carries only one defect.Source: §A.4 · pp. 16–17
• Repairing both defects jointly recovers 52/58 previously failing rows for Haiku and 49/58 for Sonnet; repairing either defect alone recovers at most 6/58.The corrected release patches all 3,086 defective rows, leaves 3,086 clean rows unchanged, and is reported as an ablation because the input repairs use reference PDDL.Source: §A.4 · p. 17

A.5 Implementation Details

• Implementation uses hosted Claude models and open-source Qwen and Gemma models, with formalism-specific repair budgets and diagnosis stacks across FOL, MiniZinc, and PDDL.The open-source models run on a single node of four A100 GPUs; implementation details also specify repeated seeds, software versions, and paired-run protocols.Source: §A.5 · pp. 17–18

A.6 Motivating Silent-Failure Taxonomy

• In zero-shot runs, every hosted-model PDDL failure was runnable but semantically wrong, and 39.1% of CSP failures reached a solver outcome while encoding the wrong model.Most FOL failures likewise came from executable formalizations producing incorrect entailment labels; execution success therefore did not reliably indicate correctness.Source: §A.6 · p. 18

A.7 Interpreting the Paired McNemar Test

• Exact two-sided McNemar tests use only discordant paired outcomes: fixes are cases where DRAGO is correct and its comparator is wrong, while breaks are the reverse.In the example, 8 fixes and 1 break across 20 instances yield a paired accuracy difference of 0.35; the 11 concordant instances do not affect the test.Source: §A.7 · pp. 18–19

A.9 Open-Source Paired Analyses

• Across open-source CSP, FOL, and PDDL, DRAGO’s domain-level fixes substantially outnumber breaks against both zero-shot and LLM-diagnostic repair.Because runs reuse benchmark instances, the analysis uses per-seed significance rates rather than pooled p-values as its inferential summary.Source: §A.9 · p. 20

A.8 Statistical Analysis

• Hosted DRAGO gains over zero-shot fall within +24.9 to +27.7 points for Haiku and +15.0 to +19.1 for Sonnet on CSP, versus +2.3 to +3.3 and +0.3 to +1.0 on PDDL.These are 95% paired-bootstrap intervals; additional hosted-run domain estimates also fall within them. Hosted CSP and PDDL analyses use five and three paired runs, respectively, with exact two-sided McNemar tests on discordant pairs.Source: §A.8 · pp. 19–20, Table 8 · p. 21

A.10 Additional Results

• DRAGO’s break rate never exceeds 2.1% of pooled pairs and stays below 0.7% on Planetarium, while LLM-diagnostic repair breaks 3.3%–14.0%.On Planetarium, the baseline incurs 126 regressions for Gemma and 85 for Qwen, versus DRAGO’s 6 and 5.Source: §A.10 · pp. 21–22

A.11 Component Ablations

• On ProverQA-hard/Haiku, gated DRAGO gains 12.3 points over zero-shot while ungated DRAGO nets zero; gated self-review matches DRAGO in only two configurations and loses by 2.8–20.7 points in sixteen others.The ablations hold the repair-stage starting artifacts fixed and use a one-round budget; acceptance alone does not reproduce DRAGO in any formalism across models.Source: §A.11 · pp. 22–23
• Three-sample selection helps most on CSP (+0.9 to +11.1 points over zero-shot), but even its oracle remains 11.1–18.2 points below DRAGO.On ProverQA-hard/Sonnet, only 7 of 500 items show cross-sample disagreement; on Planetarium/Sonnet, only 1 of 300 do.Source: §A.11 · pp. 23–24
• On ProverQA-hard, planning adds +4.6 points for Qwen and +0.3 for Gemma, versus DRAGO’s +8.0 and +8.6; on FOLIO/Qwen, planning gains 5.5 points at a 60.9 zero-shot base.Planning adds essentially nothing where the base model already reads the premises correctly. Draft-and-Prune cells are single runs, and hosted models were omitted from this baseline for compute-budget reasons.Source: §A.11 · p. 25
• CP-SynC uses parallel MiniZinc modeling and checker agents, staged validation with targeted repair, and temperature sampling for reproducible diversity.The authors re-implemented CP-SynC because no executable release was available; each cell is a single run, so run-to-run variance is unmeasured.Source: §A.11 · p. 25
• At k=3, CP-SynC beats LLM-diagnostic repair in every CSP cell by +4.2 to +16.2 points, while DRAGO leads three of four cells at both arms.CP-SynC k=1 and k=3 use 3.8× and 10.1× DRAGO’s mean LLM calls per item, respectively; the k=3 solved-count gains reflect coverage, while accuracy conditional on solving is roughly flat.Source: §A.11 · pp. 25–26, Table 15 · p. 26

A.12 Failure Analysis

• Deletion probes repaired two UNSAT CSP models by identifying reachable-item coverage in Bus Driver Scheduling and stage-horizon indexing in Wolf-Goat-Cabbage as repair targets.For Bus Driver Scheduling, the data spans 0..23 with 0 as a sentinel, so exact coverage of items 1..24 is impossible; the accepted repair restricts coverage to reachable items. In Wolf-Goat-Cabbage, re-indexing the horizon yields a correct solution.Source: §A.12 · p. 26, Figure 4 · p. 28
• DRAGO misses cleanly executing under-constraint: without the wild-turkey closure axiom, Z3 returns undetermined, and the pipeline answers Uncertain.In a representative Qwen run, all Uncertain labels were correct (62/62 on FOLIO and 146/146 on ProverQA-hard), while True- or False-labeled items were wrong (37 and 73 items); reference-free detection would require reasoning about what premises should entail.Source: §A.12 · p. 27

A.13 Licenses

• The corrected Planetarium floor-tile split is released under CC BY 4.0 with attribution to Zuo et al. (2025), and the authors’ code is released under Apache 2.0.Benchmarks are used under their published terms for research evaluation; ProverQA is publicly released without a stated license.Source: §A.13 · p. 27, Table 16 · p. 27