DRAGO: deterministic diagnosis framework to repair LLM-generated formal specifications
The paper introduces DRAGO, a repair framework that replaces ungrounded LLM critiques with deterministic, formalism-specific diagnosis and only accepts rewrites when a reference-free acceptance predicate shows reduced diagnosed error weight. Evaluated on SMT-LIB2, MiniZinc and PDDL benchmarks, DRAGO cuts specification regressions from 11.8% to 1.3% and raises answer accuracy by 12.9 percentage points over zero-shot formalization and 8.7 percentage points over LLM-diagnostic repair; the authors also identify and correct rendering defects that made half of the Planetarium split inconsistent with references.