DRAGO框架用确定性诊断将LLM生成规范的回退率从11.8%降至1.3%

该论文提出DRAGO修复框架，旨在解决大语言模型作为形式化器时生成的规范虽可运行但语义错误的问题。传统纯LLM诊断因缺乏形式真值往往无法识别此类错误，且其无根基的批评会导致初始正确规范出现11.8%的回退。DRAGO通过引入特定形式主义的确定性诊断替代无根基批评，仅在参考无关接受谓词下诊断错误权重严格降低时才保留重写。

实验显示，在涵盖逻辑推理（SMT-LIB2）、约束规划（MiniZinc）和规划（PDDL）的五个基准测试中，DRAGO将回退率降低了近一个数量级至1.3%，同时将答案准确率分别比零-shot形式化和LLM诊断修复提高了12.9和8.7个百分点。此外，研究还发现Planetarium工具存在两个渲染缺陷，导致其50%（3,086个实例）的地砖分割与参考形式化不一致，作者已发布修正后的分割数据。

事实层面，DRAGO确实显著降低了回退率并提升了准确率，且发现了Planetarium的具体缺陷。推断层面，这表明在需要严格保证的Agent任务中，混合确定性诊断与LLM可能优于纯LLM路径。猜测层面，该框架是否适用于其他未测试的形式主义或大规模工业场景仍需验证，目前仅基于文中五个基准的结果。