Repairing LLM-Generated Specifications with Deterministic Diagnosis

A repair framework called DRAGO cuts regressions in LLM-generated formal specifications to 1.3%, nearly an order of magnitude below purely LLM-based diagnosis, which regressed 11.8% of initially correct specifications, according to the arXiv paper 2610.22568v1. DRAGO replaces ungrounded LLM critique with deterministic, formalism-specific diagnosis and keeps a rewrite only when the diagnosed error weight strictly decreases under a reference-free acceptance predicate. Across five benchmarks spanning SMT-LIB2 logical reasoning, MiniZinc constraint programming and PDDL planning, DRAGO improved answer accuracy by 12.9 percentage points over zero-shot formalization and 8.7 percentage points over LLM-diagnostic repair, and the authors also found two rendering defects in Planetarium that make 50% (3,086 instances) of its floor-tile split inconsistent with reference formalizations, releasing a corrected split.

arXiv:2610.22568v1 Announce Type: new 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.