arXiv cs.AI· Giovanni Vaccarino, Emanuele La Malfa, Dehai Min, Hanrong Zhang, Pier Luca Lanzi, Lu Cheng, Michael J. Wooldridge, Philip S. Yu, Sara Bernardini·· 12 小时前AI 评分38
DRAGO：用确定性诊断修复 LLM 生成的形式化规范
Repairing LLM-Generated Specifications with Deterministic Diagnosis
AI 导读
DRAGO 是一个修复框架，用针对具体形式化语言的确定性诊断替代无依据的 LLM 批评，仅在诊断出的错误权重严格下降时才保留改写。在覆盖 SMT-LIB2、MiniZinc 和 PDDL 的五个基准上，DRAGO 将回归率从 11.8% 降至 1.3%，答案准确率较零样本形式化提升 12.9 个百分点、较 LLM 诊断修复提升 8.7 个百分点。
正文 · 原文
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.
| Subjects: | Artificial Intelligence (cs.AI); Computation and Language (cs.CL) |
| Cite as: | arXiv:2610.22568 [cs.AI] |
| (or arXiv:2610.22568v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.22568 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Giovanni Vaccarino [view email]
[v1]
Thu, 15 Oct 2026 19:12:54 UTC (425 KB)
来源：arXiv cs.AI · arxiv.org