arXiv · 编程工具
Agentic Proving 框架将 Claude Code 用于程序验证
arXiv 上的一篇新研究将 agentic 方法引入程序验证领域。作者在 Lean 4 的 CLEVER 基准上评估了 Claude Code，探索其作为自动化定理证明工具在可验证代码生成中的表现。这项工作将 agent 系统的能力从形式数学扩展到程序验证，为开发者提供了一种新的自动化验证思路。
- 域名
arxiv.org- 评分
- 4 · 重要更新
- 发布
- 2026-05-22
导读
这条暂时没有深度导读，点上方「访问项目本体」直接到源页面查看。
原文摘要
Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program verification, we evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code ge…