DRAGO: Repairing LLM-Generated Formal Specifications with Deterministic Diagnosis

Forum topic · 小凯 · 2026-10-19

Summary

LLMs are increasingly used as formalizers, translating natural-language reasoning problems into formal specifications solvable by symbolic solvers. However, many specifications run successfully yet are semantically wrong, encoding incorrect constraints, domains, objectives, predicates, or goals—and once execution succeeds, solver error feedback disappears. Purely LLM-based diagnosis, lacking formal ground truth, misses these errors and introduces regressions in 11.8% of initially correct specifications. DRAGO replaces ungrounded critique with deterministic, formalism-specific diagnosis, accepting 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 cuts regressions to 1.3%—nearly an order of magnitude improvement—and boosts answer accuracy by 12.9 percentage points over zero-shot formalization and 8.7 points over LLM-diagnostic repair. The team also uncovered two rendering defects in Planetarium making 50% (3,086 instances) of its floor-tile split inconsistent with reference formalizations, and released a corrected split. Paper: arXiv:2610.22568.

Paper Overview

Field: NLP Authors: Giovanni Vaccarino, Emanuele La Malfa, Dehai Min, Hanrong Zhang, Pier Luca Lanzi, Lu Cheng, Michael J. Wooldridge, Philip S. Yu, Sara Bernardini Published: 2026-10-19 arXiv: 2610.22568

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.

Key Contributions

Deterministic diagnosis: replaces ungrounded LLM critique with formalism-specific, verifiable error analysis
Reference-free acceptance predicate: only accepts rewrites when diagnosed error weight strictly decreases, avoiding regressions
Strong results: regressions reduced to 1.3% (≈10× improvement); +12.9 pp accuracy over zero-shot formalization, +8.7 pp over LLM-diagnostic repair
Benchmark fix: identified and corrected two Planetarium rendering defects affecting half of its floor-tile split

--- *Auto-collected on 2026-10-19*