用于程序验证的代理式证明

本文评估了 Claude Code 在代理式证明框架下于 CLEVER（Lean 4 可验证代码生成基准）上的表现。结果显示，该代理能为绝大多数问题生成有效规范，并在端到端程序生成与验证流程中达到极高成功率。此外，它能提供高质量的自我反馈以识别失败原因和数据集中的漏洞。研究表明，现有的程序验证基准难度已滞后于现代代理证明器的能力，亟需更严谨的评估方法。实证结果证实，紧密集成的“编译器在环”代理范式是当前基础程序验证最有效的方法。