LLMs are increasingly employed as formalizers: given a reasoning problem described in natural language, the model produces a formal specification that a symbolic solver can handle, with guarantees relative to that specification. Many generated specifications are executable yet semantically incorrect, encoding wrong constraints, domains, objectives, predicates, or goals. Once execution succeeds, solver feedback disappears, making errors hard to detect. Pure LLM‑based diagnosis lacks a formal ground truth, often misses errors, and its ungrounded critiques cause regressions in 11.8% of initially correct specifications in our experiments. To address this, we introduce the DRAGO framework, which replaces ungrounded critique with deterministic, formalism‑specific diagnosis and rewrites only when the diagnosed error weight strictly decreases under a reference‑free acceptance predicate. We evaluate DRAGO on five benchmarks covering logical reasoning (SMT‑LIB2), constraint programming (MiniZinc), and planning (PDDL). DRAGO reduces regressions to about 1.3%, improves answer accuracy by 12.9 percentage points over zero‑shot formalization, and by 8.7 points over LLM‑diagnostic repair. Additionally, we uncover two rendering defects in the Planetarium floor‑tile split that cause 50% (3,086 instances) of its data to be inconsistent with reference formalizations, and we release a corrected split.
Review