arXiv cs.AI· Wieger Wesselink, Kees Huizing, Huub van de Wetering·· 1 天前AI 评分38
用 Claude Opus 5 辅助 Dafny 形式化验证：十步工作流覆盖 37 个算法
LLM-Assisted Verification in Dafny
AI 导读
一项研究提出基于 Dafny 验证系统的十步 LLM 辅助工作流，用 Anthropic 的 Claude Opus 5 与 Opus 5.5 完成算法形式化、契约开发、不变量验证、证明构建与性能优化。在 37 个图论与标记迁移系统算法上完成机器校验验证，其中包括 Hopcroft-Tarjan 三连通性测试，多数验证在数小时至数天内完成。人类验证者的角色由此转向规范审查与策略指导。
正文 · AI 翻译
摘要：复杂算法的形式化验证需要程序规约、不变式构造、数学证明以及自动定理证明器管理方面的专业知识。尽管大语言模型（LLM）能够生成程序代码和证明片段，但可靠地开发完整的机器可检验验证仍然具有挑战性：它需要一个迭代过程，包括构造和验证规约与不变式、构建证明、诊断求解器失败以及优化验证性能。本文提出了一套系统化的十步工作流，用于使用 Dafny 验证系统对科学算法进行 LLM 辅助验证。该工作流整合了算法形式化、契约开发、经验性不变式验证、证明构建、瓶颈分析和资源驱动的证明优化。我们使用 Antrhopic 的 Claude Opus 5 和 Opus 5.5 模型应用了该工作流，将 LLM 驱动的开发与自动化测试和验证反馈相结合，同时保留人工监督以进行正确性关键决策和策略性干预。我们在来自图论和标记迁移系统的 37 个复杂算法上评估了该方法。值得注意的是，我们验证了 Hopfcroft-Tarjan 三连通性测试，表明即使极具挑战性的算法验证任务也可以通过结构化的 LLM 辅助工作流完成。我们的许多机器可检验验证在数小时到几天的交互式开发内完成。我们的结果表明，LLM 辅助工作流可以将人类验证者的角色从详细的证明构建转变为监督、规约审查和策略指导。
| 评论： | 16 页（不含参考文献），含参考文献 20 页；1 幅图，2 张表。投稿至 FSEN 2027 |
| 主题： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI）；软件工程（cs.SE） |
| MSC 分类号： | 68N30, 68Q60, 68V15 |
| ACM 分类号： | D.2.4; I.2.2; F.3.1 |
| 引用为： | arXiv:2611.16886 [cs.LO] |
| （或 arXiv:2611.16886v1 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2611.16886 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Wieger Wesselink [查看电子邮件]
[v1]
2026 年 11 月 12 日星期四 14:48:38 UTC（51 KB）
来源：arXiv cs.AI · arxiv.org