LLM specification errors cut with formal error diagnosis framework
Repairing LLM-Generated Specifications with Deterministic Diagnosis
Artificial IntelligenceComputation and Language
Summary
Large language models (LLMs) can translate natural language problems into formal rules for computer solvers, but sometimes these rules are wrong even if they run without error. The authors found that using only LLM feedback to fix these mistakes often introduces new errors. They created a system called DRAGO that uses strict, formal checks to find and fix errors in the rules, only accepting changes that improve correctness. Their approach significantly reduces incorrect fixes and improves solver accuracy across different problem types. They also discovered and fixed errors in a popular dataset used to test these systems.
What this means in practice
- •For software developers: Improve reliability of automated formal specifications generated by LLMs to reduce bugs in solver-based programming tools.
- •For operations planners: Use DRAGO-enhanced formalizations to generate more accurate plans and constraints for automated scheduling and logistics.
Authors
Giovanni Vaccarino, Emanuele La Malfa, Dehai Min, Hanrong Zhang, Pier Luca Lanzi, Lu Cheng, Michael J. Wooldridge, Philip S. Yu, Sara Bernardini
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.