面向程序验证的智能体定理证明

智能体系统近来已成为形式数学中自动定理证明的最先进方法。为评估这些能力能在多大程度上延伸到程序验证，我们在一个智能体证明框架下于CLEVER上评估Claude Code，CLEVER是一个面向可验证代码生成的Lean 4基准。结果显示，Claude为98.8%的问题生成了可认为有效的规约（在基准的正确部分上，其中81.3%还被CLEVER基于同构的评分接受），针对正确的标准答案规约认证了87.5%的问题的实现，并在前提自洽的条目上取得98.1%的端到端程序生成与验证管线成功率。在所有阶段，Claude还能对自身尝试给出高质量反馈（经人工复核确认），指出失败的深层原因及数据集中残留的缺陷。这些发现凸显了现有程序验证基准难度与现代智能体证明器能力之间日益扩大的错位，表明需要更严格、更能抵御缺陷的评估方法，尤其需要替代基于同构的生成规约评分的方案。更广泛地说，我们的结果提供了实证证据：编译器在环的紧密智能体范式是当前基础性程序验证最有效的途径。