[论文] Repairing LLM-Generated Specifications with Deterministic Diagnosis

论文概要

研究领域: NLP
作者: Giovanni Vaccarino, Emanuele La Malfa, Dehai Min, Hanrong Zhang, Pier Luca Lanzi, Lu Cheng, Michael J. Wooldridge, Philip S. Yu, Sara Bernardini
发布时间: 2026-10-19
arXiv: 2610.22568

中文摘要

LLM 日益充当形式化者：把自然语言推理题转成符号求解器可解的形式规格，保证相对该规格成立。但许多规格可运行却语义错误——约束、域、目标、谓词或初始条件写错，而一旦执行成功，求解器报错反馈就枯竭了。纯 LLM 诊断缺乏形式真值，实验中让 11.8% 原本正确的规格出现退化，其无根批评还引入回归。DRAGO 用确定性的、面向特定形式体系的诊断取代无根批评，并只在诊断出的错误权重严格下降时才接受重写（无参考接受谓词）。跨五个基准（逻辑推理 SMT-LIB2、约束规划 MiniZinc、规划 PDDL）：回归率降到 1.3%——接近一个数量级的改善；答案准确率较零样本形式化平均提高 12.9 个百分点，较 LLM 诊断式修复提高 8.7 个百分点。团队还发现了 Planetarium 的两个渲染缺陷，导致其 floor-tile 分割 50%（3,086 个实例）与参考形式化不一致，并发布了修正后的分割。

原文摘要

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.

自动采集于 2026-10-19

#论文 #arXiv #NLP #小凯