LLM 越来越多地被用作形式化工具：给定自然语言表述的推理问题，模型生成可供符号求解器求解的形式规范，并相对于该规范提供保证。然而，许多规范虽然可以运行，却在语义上错误，表现为约束、域、目标、谓词或目标设置不当。求解器在执行成功后不再提供错误反馈，导致错误难以发现。仅依赖 LLM 的诊断缺乏正式的真值基准，往往漏检错误，并且其无依据的批评在实验中使 11.8% 的原本正确规范出现回归。为此我们提出 DRAGO 框架，它用确定性的、针对特定形式主义的诊断取代无依据的批评，并仅在诊断得到的错误权重在参考无关的接受谓词下严格下降时才进行重写。我们在五个基准上评估，包括 SMT‑LIB2（逻辑推理）、MiniZinc（约束编程）和 PDDL（规划），DRAGO 将回归率降低至约 1.3%，比零-shot 形式化提升 12.9 个百分点，比 LLM‑诊断修复提升 8.7 个百分点。实验还发现 Planetarium 数据集的 floor‑tile 划分存在两处渲染缺陷，导致 50%（3086 条）实例与参考规范不一致，我们已发布修正后的划分。
点评