arXiv cs.AI· Priyanath Maji·· 11 小时前AI 评分29
验证通过不等于结论一致：跨智能体 LLM-to-Dafny 形式化协议研究
When Verification Is Not Agreement: Cross-Agent LLM-to-Dafny Formalization
AI 导读
研究提出跨智能体形式化协议，由 Specifier 模型将临床试验标准翻译为 Dafny 谓词、Implementer 模型编写方法并接受校验。
正文 · AI 翻译
摘要：经过验证的 Dafny 后置条件可以证明某个公式成立，但并不能保证该结果是通过真正独立的推理得出的。我们引入了一种跨智能体形式化协议，其中 Specifier 模型将临床试验标准翻译为 Dafny 谓词，Implementer 模型编写一个操作方法来对其进行检查。同模型对照实验表明，即使不存在能力差距，从相同文本进行独立重新提取的一致率也仅为 59.3%。在 96 份临床试验文档上评估四种模型配置后，我们发现一致率对模型能力在两个角色之间的分配方式高度敏感：GPT-4.1-nano/GPT-4.1-mini 配置在较强模型担任 Implementer 时达到 53.0% 的一致率，但角色互换后仅为 14.3%。测试中最强的配置 GPT-5.6-luna/GPT-5.4-mini 将一致率提升至 34.4%，但仍低于同模型基线，且以直接矛盾为主（42.7%）。我们还发现了一种关键的验证伪影：较弱的 Implementer 通过直接调用 Specifier 的谓词来满足后置条件；经过结构审计后，修正后的一致率从 14.3% 降至 13.2%。我们的结果表明，仅凭验证成功不足以证明跨智能体独立一致，并且在对同一来源进行独立形式化时，模型能力并不能保证一致性。
| 评论： | 已被 NeurIPS 2026 可验证编码人工智能研讨会接收 |
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2611.07073 [cs.AI] |
| （或此版本的 arXiv:2611.07073v1 [cs.AI]） | |
| https://doi.org/10.48550/arXiv.2611.07073 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Priyanath Maji [查看电子邮件]
[v1]
2026年11月4日星期三 19:31:51 UTC（31 KB）
来源：arXiv cs.AI · arxiv.org