UC Berkeley 团队发布 Vero 基准：测试 AI 智能体能否构建形式化验证的软件仓库
2026.09.02 · 事件 · 基准发布 · 论文预印本
首个仓库级基准，要求 AI 同时编写实现与形式化证明，最强配置仅完成 27/43 实例。
UC Berkeley 等机构发布 Vero 基准，包含 43 个多模块 Lean 4 实例，要求 AI 智能体在仓库级别同时编写实现和形式化证明。最强配置 GPT-5.5 (xhigh) 在代码+证明模式下完整解决 27/43 实例，通过 87.3% 的规范，但仍有 10 个实例未被任何配置解决。
- 首个仓库级形式化验证基准
- 43 个多模块 Lean 4 实例
- 最强配置完整解决 27/43
- 10 个实例所有配置均未解决
- 证明单个规范已非难点
为什么值得看
揭示 AI 在真实代码库中形式化验证的瓶颈，推动智能体长程推理能力发展。
适合谁关注
AI 编程工具开发者、形式化验证研究者、软件工程从业者