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·· 11 小时前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 个百分点。
正文 · AI 翻译
摘要：大型语言模型（LLM）正越来越多地被用作形式化器：给定一个用自然语言表述的推理问题，它们会生成一份形式化规范，随后符号求解器可以求解该规范，并相对于该规范提供保证。许多规范虽然可以运行，但在语义上是错误的，编码了不正确的约束、域、目标、谓词或目标函数，而一旦执行成功，求解器错误反馈便不再出现。纯基于 LLM 的诊断由于缺乏形式化真值，往往无法发现这些错误，而且其无依据的批评在我们的实验中导致 11.8% 的初始正确规范出现回归。我们提出 DRAGO，一个修复框架，它用确定性的、针对特定形式体系的诊断取代这种无依据的批评，并且仅当诊断出的错误权重在无参考接受谓词下严格下降时，才保留重写。在涵盖逻辑推理（SMT-LIB2）、约束编程（MiniZinc）和规划（PDDL）的五个基准上，DRAGO 将回归减少近一个数量级，降至 1.3%，同时在基准平均上，相比零样本形式化将答案准确率提高 12.9 个百分点，相比 LLM 诊断修复提高 8.7 个百分点。我们还发现了 Planetarium 中的两个渲染缺陷，这些缺陷导致其 floor-tile 划分中有 50%（3,086 个实例）与参考形式化不一致，并发布了一个修正后的划分。
| 学科： | 人工智能（cs.AI）；计算与语言（cs.CL） |
| 引用为： | arXiv:2610.22568 [cs.AI] |
| （或 arXiv:2610.22568v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.22568 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Giovanni Vaccarino [查看电子邮件]
[v1]
2026年10月15日星期四 19:12:54 UTC（425 KB）
来源：arXiv cs.AI · arxiv.org