Repairing LLM-Generated Specifications with Deterministic Diagnosis

Giovanni Vaccarino; Emanuele La Malfa; Dehai Min; Hanrong Zhang; Pier Luca Lanzi; Lu Cheng; Michael J. Wooldridge; Philip S. Yu

cs.AIOct 15, 2026

Repairing LLM-Generated Specifications with Deterministic Diagnosis

Authors: Giovanni Vaccarino, Emanuele La Malfa, Dehai Min, Hanrong Zhang, Pier Luca Lanzi, Lu Cheng, Michael J. Wooldridge, Philip S. Yu,

Organizations: Department of Computer Science, University of Oxford, Oxford, UK · Department of Computer Science, University of Illinois Chicago, Chicago, IL, USA · Dipartimento di Elettronica, Informazione e Bioingegneria, Politecnico di Milano, Milan, Italy · Institute for Decentralized AI (IDAI) ·

Abstract

Large language models (LLMs) are increasingly used as formalizers: given a reasoning problem expressed in natural language, they produce a formal specification that a symbolic solver can then solve, with guarantees relative to that specification. Many specifications are runnable yet semantically wrong, encoding incorrect constraints, domains, objectives, predicates, or goals, and solver-error feedback dries up once execution succeeds. Purely LLM-based diagnosis, lacking a formal ground truth, often fails to spot these errors, and its ungrounded critiques cause regressions in 11.8% of initially correct specifications in our experiments. We propose DRAGO, a repair framework that replaces this ungrounded critique with deterministic, formalism-specific diagnosis, and retains a rewrite only when the diagnosed error weight strictly decreases under a reference-free acceptance predicate. Across five benchmarks spanning logical reasoning (SMT-LIB2), constraint programming (MiniZinc), and planning (PDDL), DRAGO cuts regressions by nearly an order of magnitude, to 1.3%, while improving answer accuracy by 12.9 percentage points over zero-shot formalization and 8.7 percentage points over LLM-diagnostic repair, averaged across benchmarks. We also uncover two rendering defects in Planetarium that cause 50% (3,086 instances) of its floor-tile split to be inconsistent with the reference formalizations, and release a corrected split.

Figures & tables

		Haiku 4.5			Sonnet 4.6			Qwen3-Coder 30B			Gemma 4 31B
Domain	Benchmark	Zero	LLM-d	DRAGO	Zero	LLM-d	DRAGO	Zero	LLM-d	DRAGO	Zero	LLM-d	DRAGO
FOL	FOLIO	$75.0$	$81.5$	$\mathbf{85.5}$	$85.0$	$81.2$	$\mathbf{90.1}$	$60.9$	$63.7$	$\mathbf{64.8}$	$85.0$	$85.8$	$\mathbf{87.6}$
		$\pm 0.7$	$\pm 1.9$	$\pm 0.8$ $(+4.0)$	$\pm 0.2$	$\pm 2.1$	$\pm 1.3$ $(+5.1)$	$\pm 0.5$	$\pm 1.8$	$\pm 0.3$ $(+1.1)$	$\pm 0.9$	$\pm 1.1$	$\pm 0.4$ $(+1.8)$
	ProverQA	$77.1$	$74.4$	$\mathbf{89.4}$	$77.2$	$74.1$	$\mathbf{90.3}$	$60.8$	$59.8$	$\mathbf{68.8}$	$75.1$	$74.2$	$\mathbf{83.7}$
		$\pm 0.3$	$\pm 0.8$	$\pm 0.5$ $(+12.3)$	$\pm 0.4$	$\pm 1.0$	$\pm 0.2$ $(+13.1)$	$\pm 0.4$	$\pm 1.1$	$\pm 0.6$ $(+8.0)$	$\pm 0.1$	$\pm 0.3$	$\pm 0.1$ $(+8.6)$
CSP	Text2Zinc	$17.5$	$29.6$	$\mathbf{42.2}$	$40.4$	$52.0$	$\mathbf{57.1}$	$12.0$	$\mathbf{22.2}$	$19.8$	$20.4$	$38.7$	$\mathbf{56.5}$

Table 1: Main answer accuracy results, including our approach, DRAGO (gray background). LLM-d denotes the LLM-diagnostic repair baseline. Cells report mean accuracy percentages with the sample standard deviation across independent runs. Planetarium is evaluated as released on

300

sampled problems, of which

58

are inconsistent with their references, capping accuracy at

80.7\%

(Section 6.3 ). Bold marks the best method for each benchmark within each model. The parenthesized

(+x)

beneath each DRAGO mean is its gain over the best baseline.

Figure 1: Correctness transitions of the repair loop on the FOL benchmarks (Haiku) for the LLM-diagnostic baseline and DRAGO on FOLIO and ProverQA-hard. Slices are shares of all instances, pooled over runs.

	Zero	Sample-3	Oracle-3	DRAGO
FOL	$78.6$	$80.0$	$81.3$	$\mathbf{88.8}$
CSP	$39.2$	$44.1$	$46.0$	$\mathbf{59.9}$
PDDL	$68.9$	$69.7$	$71.9$	$\mathbf{70.2}$

Table 2: Sample-and-select inference against DRAGO, aggregated over the hosted-model configurations of each formalism. Bold marks the best implementable method. Selection rules and per-configuration results are in Appendix A.11 , Table 14 .

Figure 2: Component ablations aggregated over the model-benchmark configurations of each formalism. Per-configuration results and exact arm definitions in Appendix A.11 . Best arm per formalism in bold .

	Qwen3-Coder 30B			Gemma 4 31B
	Zero	Sys	DRAGO	Zero	Sys	DRAGO
FOLIO	$60.9$	$\mathbf{70.3}$	$64.8$	$85.0$	$87.1$	$\mathbf{87.6}$
ProverQA	$60.8$	$65.4$	$\mathbf{68.8}$	$75.1$	$75.4$	$\mathbf{83.7}$
CP-Bench	$20.3$	$27.0$	$\mathbf{42.9}$	$43.9$	$47.6$	$\mathbf{70.9}$
Text2Zinc	$12.0$	$\mathbf{20.0}$	$19.8$	$20.4$	$41.8$	$\mathbf{56.5}$

Table 3: Domain-specific systems against DRAGO on the open-source models, in their single-trajectory (

k{=}1

) configurations. Sys: Draft-and-Prune (FOL, top) and CP-SynC (CSP, bottom). Bold marks the best method per benchmark and model.

Appendix figures & tables15 assets

Supplementary material from the paper’s appendix.

Appendix

Formalism	Contract checks	Solver probes	Specification alignment	Acceptance
FOL / SMT-LIB2	Single entity sort; premise assertions plus one named conclusion definition; no solver-control commands; signature vocabulary and arities	Z3 premise-consistency and entailment-status probes; witness models for both readings on underdetermination	Disjunction strength vs. exclusivity marking in the problem statement (advisory)	Changed, parseable, signature-clean, premise-consistent; corroboration for undetermined $\rightarrow$ definite flips
CSP / MiniZinc	Data-schema instantiation; required output conventions; static model check	Deletion probes on UNSAT localize conflicting requirement blocks with the data they reference	Semantic lint: quantity granularity and data/unit magnitudes vs. the problem statement	Passes model check; still runs and solves; no regression to error or UNSAT
PDDL	Parses and grounds against the official domain file; correct :domain ; declared predicates, arities, and objects; flat ground-conjunction goal	Delete-relaxation reachability of goal atoms; bounded complete search (exhaustion proves unsolvability; timeout yields no finding)	Count phrases in the statement vs. per-category object counts (blocking); unmatched identifier mentions (advisory)	Contract holds; strict blocking-weight descent with no new blocking axis; no goal or object-count weakening

Appendix

Table 4: Instantiation of the three diagnostic classes and the acceptance conditions for each formalism. Full rule inventories, thresholds, and defaults are given in the paragraphs below and in the released code.

Domain	Generation output	Generation inputs and constraints	DRAGO repair inputs and constraints
FOL	SMT-LIB2 script	Natural-language premises, conclusion, and vocabulary signature. The prompt requires one uninterpreted entity sort, premise assertions only, and a named conclusion Boolean definition.	Original problem, vocabulary, current SMT-LIB2 script, solver status, and deterministic FOL diagnoses. The repair must preserve the output contract and make only edits licensed by the English problem and diagnostic evidence.
CSP	MiniZinc model	Problem description, parameter schema, and required output variables. The prompt requires a valid MiniZinc model using external .dzn data and benchmark-specific output conventions.	Original problem, runnable structured MiniZinc model, data file, and failed semantic checks. The repair must keep parameter names, section markers, and output conventions while fixing the diagnosed semantic failure.
PDDL	PDDL problem file	Natural-language planning problem. The prompt requires exactly one PDDL problem file, not a domain file, plan, or explanation.	Original planning problem, generated PDDL, and deterministic reference-free diagnoses. The repair must preserve the planning domain and return exactly one complete PDDL problem file.

Appendix

Table 5: Summary of the generation and DRAGO repair prompt schemas. Exact prompts are released with the codebase.

Question as shipped (floor-tile, $1{\times}3$ grid, two robots)
You have 2 robots. You have 3 tiles. You have 3 colors. Tile tile1 is is to the right of tile tile2. Tile tile2 is is to the right of tile tile3. The robot robot1 has color color1. The robot is at tile robot1. The robot robot2 has color color2. The robot is at tile robot2. Color color1 is available. Color color2 is available. Color color3 is available. Your goal is to have the following: Tile tile1 should be painted with color color1. Tile tile2 should be painted with color color1. Tile tile3 should be painted with color color1.
Reference PDDL (init excerpt)
(robot-at robot1 tile1) (robot-at robot2 tile2) (right tile2 tile1) (right tile3 tile2)

Appendix

Figure 3: The smallest sampled floor-tile instance, verbatim, with the defective sentences in bold. Defect 1 (destroyed robot positions): “The robot is at tile robot1.” fills the tile slot with the robot’s own name; the true positions, (robot-at robot1 tile1) and (robot-at robot2 tile2) , appear nowhere in the question. Defect 2 (reversed adjacency): the reference states (right tile2 tile1) —under the shipped domain file’s action semantics, tile2 is to the right of tile1—while the question asserts the opposite, “Tile tile1 is…to the right of tile tile2.” The duplicated “is is” is verbatim. A model that reads this text faithfully places no robot correctly and builds the mirrored row.

Formalism	Retained benchmarks	$N$	Correct	Incorrect	Non-runnable wrong	Runnable wrong / wrong
FOL	FOLIO, ProverQA-hard	5020	3932	1088	131	$957/1088$ ( $88.0\%$ )
CSP	Text2Zinc, CP-Bench	346	126	220	134	$86/220$ ( $39.1\%$ )
PDDL	Planetarium	600	413	187	0	$187/187$ ( $100.0\%$ )
All	Retained outputs	5966	4471	1495	265	$1230/1495$ ( $82.3\%$ )

Appendix

Table 6: Zero-shot failure taxonomy over the retained saved outputs. The rightmost column reports failures that are runnable but semantically wrong, which ordinary solver-error feedback would not expose as syntax or runtime errors.

		LLM-diag. vs. Zero		DRAGO vs. Zero		DRAGO vs. LLM-diag.
Domain	Model	Fix/Break	$p$	Fix/Break	$p_{\mathrm{Holm}}$	Fix/Break	$p_{\mathrm{Holm}}$
CSP	Haiku	$151/20$	$<.0001$	$232/10$	$<.0001$	$25/8$	$.018$
CSP	Sonnet	$131/41$	$<.0001$	$169/20$	$<.0001$	$23/9$	$.060$
PDDL	Haiku	$42/36$	$.572$	$27/3$	$<.0001$	$53/35$	$.069$
PDDL	Sonnet	$6/90$	$<.0001$	$6/0$	$.063$	$92/2$	$<.0001$
FOL	Haiku	$148/148$	$1.00$	$275/29$	$<.0001$	$311/65$	$<.0001$

Appendix

Table 7: Domain-level exact McNemar tests, with all repair methods at the one-round budget. Fix/Break counts pool the discordant pairs over the repeated hosted runs (five CSP runs, three PDDL runs, three common FOL runs), except the CSP cells of the rightmost column, which come from the single complete paired run; per-run tests are reported in the accompanying text (Appendix A.8 ). In each comparison, Fix/Break gives the discordant pairs where the left method is correct and the right method is wrong, or vice versa; a significant

p

therefore also flags harmful effects, as in the PDDL/Sonnet LLM-diagnostic column, where the baseline breaks

90

instances against

6

fixes. The two DRAGO comparison columns report Holm–Bonferroni-adjusted values; the LLM-diagnostic-vs-zero column reports unadjusted exact values.

Domain	Model	Paired accuracy gain (pp)	$95\%$ CI
CSP	Haiku	$+24.9$	$[17.9,\ 32.4]$
CSP	Sonnet	$+16.2$	$[10.4,\ 22.0]$
PDDL	Haiku	$+2.3$	$[0.7,\ 4.3]$
PDDL	Sonnet	$+0.3$	$[0.0,\ 1.0]$
FOL	Haiku	$+11.7$	$[9.6,\ 13.8]$
FOL	Sonnet	$+10.6$	$[8.5,\ 12.7]$

Appendix

Table 8: Paired effect sizes for the primary DRAGO-vs-zero-shot comparison, in percentage points. Intervals are

95\%

percentile paired-bootstrap intervals with

4{,}000

replicates over the matched benchmark instances. For FOL, we use the three common runs, resample runs and instance units in two stages, and resample FOLIO at the story level. CSP and PDDL rows use the primary paired run; the point estimates of the additional hosted runs fall inside the reported intervals (see text).

		Qwen3-Coder 30B		Gemma 4 31B
Domain	Benchmark	DRAGO vs. Zero	DRAGO vs. LLM-diag.	DRAGO vs. Zero	DRAGO vs. LLM-diag.
PDDL	Planetarium	$15/5;\ 0/3$	$97/22^{\dagger}$	$80/6;\ 3/3$	$138/61^{\dagger}$
CSP	Text2Zinc	$84/41;\ 1/5$	$61/74;\ 0/5$	$209/10;\ 5/5$	$124/26;\ 5/5$
	CP-Bench	$88/17;\ 5/5$	$74/18;\ 3/5$	$58/7;\ 5/5$	$34/12;\ 1/5$
FOL	ProverQA-hard	$128/8;\ 3/3$	$225/90;\ 3/3$	$130/2;\ 3/3$	$170/28;\ 3/3$
	FOLIO	$61/21;\ 1/5$	$135/123;\ 0/5$	$34/8;\ 2/5$	$59/41;\ 0/5$

Appendix

Table 9: Open-source paired McNemar analyses, grouped by formalism. Each cell reports Fix/Break; significant runs/available runs . Fix/Break sums the discordant paired outcomes over saved runs and is descriptive; significance is assessed separately by an exact two-sided McNemar test in each seed at

\alpha=0.05

. With the exception of the Planetarium DRAGO vs. LLM-diagnostic comparison ( † ), where we pool across seeds (

p=2.0\times 10^{-12}

for Qwen3-Coder,

p=4.9\times 10^{-8}

for Gemma), we do not report pooled

p

-values because repeated runs reuse the same benchmark instances.

Haiku 4.5
Method	Blocks	Floor	Gripper	Overall
Zero	$83.0$	$22.0$	$69.0$	$58.0$
LLM-diag.	$80.0$	$20.0$	$76.0$	$58.7$
DRAGO	$90.0$	$21.0$	$70.0$	$60.3$
Sonnet 4.6
Zero	$100.0$	$40.0$	$99.0$	$79.7$

Appendix

Table 10: Planetarium accuracy by subdomain (

100

instances each). Hosted-model rows report one run; open-model rows are means over three seeded runs.

Subdomain	Model	Method	R $\rightarrow$ R	R $\rightarrow$ W	W $\rightarrow$ R	W $\rightarrow$ W	Net
blocksworld	Haiku 4.5	DRAGO	83	0	7	10	$+7$
	Haiku 4.5	LLM-diag.	77	6	3	14	$-3$
	Sonnet 4.6	DRAGO	100	0	0	0	$0$
	Sonnet 4.6	LLM-diag.	97	3	0	0	$-3$
floor-tile	Haiku 4.5	DRAGO	21	1	0	78	$-1$
	Haiku 4.5	LLM-diag.	18	4	2	76	$-2$

Appendix

Table 11: Planetarium correctness transitions by subdomain for the hosted models (

100

instances per subdomain, single paired run). The large floor-tile W

\rightarrow

W mass contains the

58

input–reference-inconsistent instances (Appendix A.4 ). The baseline’s only positive cell (Haiku gripper,

+7

) coexists with regressions on every other subdomain, most severely Sonnet gripper (

17

breaks against

1

fix).

Benchmark	Model	Method	Seeds	$N$	R $\rightarrow$ R	R $\rightarrow$ W	W $\rightarrow$ R	W $\rightarrow$ W	Net
FOLIO	Gemma 4 31B	DRAGO	5	1010	851	8	34	117	$+26$
	Gemma 4 31B	LLM-diag.	5	1010	812	47	55	96	$+8$
	Qwen3-Coder 30B	DRAGO	5	1010	594	21	61	334	$+40$
	Qwen3-Coder 30B	LLM-diag.	5	1010	508	107	135	260	$+28$
ProverQA-hard	Gemma 4 31B	DRAGO	3	1500	1125	2	130	243	$+128$
	Gemma 4 31B	LLM-diag.	3	1500	1078	49	35	338	$-14$

Appendix

Table 12: Open-source correctness transitions from each method’s own initial formalization to its final answer. Counts are pooled over the seeds of each cell, so

N

is benchmark size times seeds; R denotes a correct artifact and W an incorrect or unscored artifact. Net

=

\rightarrow

-

\rightarrow

W. CSP is omitted because the CSP runners do not record initial correctness.

Benchmark	Model	Zero	Solv-err	LLM-d	LLM-d $+$ A	DRAGO $-$ A	DRAGO
FOLIO	Haiku 4.5	$75.0$	$76.7$	$81.5$	$80.2$	$79.2$	$\mathbf{85.5}$
	Sonnet 4.6	$85.0$	$86.1$	$81.2$	$81.2$	$86.1$	$\mathbf{90.1}$
	Qwen3-Coder 30B	$60.9$	$60.4$	$63.7$	$\mathbf{65.8}$	$60.9$	$64.8$
	Gemma 4 31B	$85.0$	$85.2$	$85.8$	$84.2$	$85.2$	$\mathbf{87.6}$
ProverQA-hard	Haiku 4.5	$77.1$	$77.6$	$74.4$	$71.4$	$77.0$	$\mathbf{89.4}$
	Sonnet 4.6	$77.2$	$77.0$	$74.1$	$72.6$	$83.0$	$\mathbf{90.3}$

Appendix

Table 13: Component-ablation accuracy behind the formalism-level aggregation of Figure 2 . All repair arms use the one-round budget and start from the same initial artifacts. Bold marks the best arm per row.

FOLIO
Model	Zero	Sample-3	Oracle-3	DRAGO
Haiku 4.5	$75.0$	$78.6$	$80.2$	$\mathbf{85.5}$
Sonnet 4.6	$85.0$	$86.1$	$87.6$	$\mathbf{90.1}$
ProverQA-hard
Haiku 4.5	$77.1$	$78.2$	$79.2$	$\mathbf{89.4}$
Sonnet 4.6	$77.2$	$77.2$	$78.0$	$\mathbf{90.3}$

Appendix

Table 14: Per-configuration accuracy of the sampling baseline behind Table 2 . Zero and DRAGO report the primary paired run behind Table 1 (FOL cells are means over the repeated runs); Sample-3 is the reference-free selector and Oracle-3 the any-correct ceiling defined above. Bold marks the best implementable method per row. Planetarium/Haiku is the one configuration where the oracle exceeds every implementable arm; realizing it would require the reference-based equivalence judgment of the benchmark scorer itself.

CP-Bench
			CP-SynC
Model	Zero	LLM-d	$k{=}1$	$k{=}3$	DRAGO
Qwen3-Coder 30B	$20.3$	$25.1$	$27.0$	$41.3$	$\mathbf{42.9}$
Gemma 4 31B	$43.9$	$59.3$	$47.6$	$63.5$	$\mathbf{70.9}$
Text2Zinc
Qwen3-Coder 30B	$12.0$	$22.2$	$20.0$	$\mathbf{30.0}$	$19.8$

Appendix

Table 15: Full CP-SynC comparison on CSP, at both the single-trajectory arm (

k{=}1

) reported in Table 3 and the paper-default

k{=}3

. Zero, LLM-d and DRAGO repeat the multi-run means of Table 1 ; each CP-SynC cell is a single run and therefore a point estimate. Bold marks the best method per row; the CP-Bench/Qwen (

42.9\pm 2.7

vs.

41.3

) and Text2Zinc/Qwen (

19.8\pm 1.8

vs.

20.0

k{=}1

) margins are within run-to-run noise. The final row reports the measured inference budget as mean LLM calls per item, against which every accuracy column should be read.

Figure 4: Case study on an UNSAT CSP instance (Bus Driver Scheduling), contrasting the diagnoses of LLM self-review and DRAGO.

Artifact	License
FOLIO Han et al. (2024)	CC BY-SA 4.0
ProverQA Qi et al. (2025)	none stated
Text2Zinc Singirikonda et al. (2025)	CC BY 4.0
CP-Bench Michailidis et al. (2026)	Apache 2.0
Planetarium Zuo et al. (2025)	CC BY 4.0
Corrected floor-tile split (ours)	CC BY 4.0

Appendix

Table 16: Licenses of the benchmarks used and of the artifacts we release. ProverQA is publicly released by its authors without a stated license.

Autoformalization

Autoformalization converts natural-language mathematics, proofs, and specifications into machine-checkable formal languages.

See all 111 papers

Faithful Autoformalization via Roundtrip Verification and Repair
Apr 27, 2026Daneshvar Amrollahi, Jerry Lopez, Clark BarrettLLM Self-Correction Legal NLP
Stanford University, USA
SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification
Aug 9, 2026Wenyao Cui, Huaping Zhang, Yongyi Huang +6CoT Faithfulness LLM Answer Verification
Beijing Institute of Technology Beijing, China · Zhongguancun Academy Beijing, China · Xinjiang Future Enterprise Incubator Co., Ltd. Xinjiang, China +1
Grounded Evaluation and Repair for NL-to-PDDL Problem Generation
Sep 9, 2026Joana Rosa, Pedro Santos, Valdemar Oliveira +3LLM Evaluation LLM Planning
INESC INOV, Lisbon, Portugal · Instituto Superior Técnico, Universidade de Lisboa, Lisbon, Portugal · Motamineral Minerais Industriais S.A. +1

Apr 27, 2026J/K move · Enter open · S save

Faithful Autoformalization via Roundtrip Verification and Repair

Daneshvar Amrollahi, Jerry Lopez, Clark Barrett

Stanford University, USA

LLM Self-Correction Legal NLP Formal Verification Autoformalization

Open paper AskPDF arXiv

When an LLM formalizes natural language, how do we know the output is faithful? We propose a roundtrip verification approach which does not require ground-truth annotations: formalize a statement, translate the result back to natural language, re-formalize, and use a formal tool to check logical equivalence. When the two formalizations agree, this provides evidence of a faithful formalization. When they disagree, a stage-level diagnosis localizes the error to a specific translation step, and a scoped repair operator attempts to correct that step. We evaluate the framework on two statutory domains (the Texas Transportation Code and the Texas Parks and Wildlife Code) using two LLMs (Claude Opus~4.6 and GPT-5.2) with three repair baselines. Diagnosis-guided scoped repair is the most effective method, with effectiveness contingent on the reliability of the diagnosis function. Across both domains and both models, under our full repair system, rules that fail the equivalence check show 1.4x-2.5x more natural language inference (NLI) drift than rules that pass it.

Abstract

Autoformalization

Explore similar work

Faithful Autoformalization via Roundtrip Verification and Repair

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification

Grounded Evaluation and Repair for NL-to-PDDL Problem Generation