利用确定性诊断修复 LLM 生成的形式化规约

研究人员提出规约修复框架 DRAGO，通过确定性、特定形式体系的诊断与无参考接受谓词来纠正 LLM 生成的语义错误形式化规约。在涵盖 SMT-LIB2、MiniZinc 和 PDDL 的五个基准测试中，DRAGO 将回归率从纯 LLM 诊断的 11.8% 降至 1.3%，平均答案准确率比零样本形式化提升 12.9 个百分点、比 LLM 诊断修复提升 8.7 个百分点。