返回评测
代码生成 代码-安全 未饱和 模态 · 代码 任务 · 分类

Vero 1.0

首个评估 AI Agent 联合实现与机器可检查证明合成的仓库级基准，43 个多模块实例（Python/Dafny/Verus/Coq→Lean 4），最强 Agent 仅解 27/43

UC Berkeley（SunBlaze 团队，Dawn Song 领衔） ·

考察能力

形式化验证 证明合成 实现-证明联合 Lean 4 多模块仓库

构建信息

数据规模
43 multi-module instances
构建方式
从真实仓库（Python/Dafny/Verus/Coq）提炼，人工策展规范 + 参考实现，统一转 Lean 4
评测方式
proof-only 与 code-and-proof 两种模式，Lean 工具链机器检查
核心指标
Fully solved instances (%)

资源链接

论文: arXiv:2608.13522 代码: https://github.com/sunblaze-ucb/vero 官网

模型效果排行

🥇 最强 Agent（frontier coding-agent 配置 + Lean 工具链）
27/43 (62.8%) 2026-08

为什么重要

AI Agent 写代码已经很快，但不提供任何正确性保证——测试只能证伪、不能证明。形式化验证（formal verification）要求 Agent 同时产出”实现”和”机器可检查的正确性证明”，是通往可信 AI 生成软件的关键路径。此前的基准要么只测单个函数，要么只测”给定实现补证明”，从未回答一个开放问题：Agent 能否在真实的多模块代码库上，做出连贯的实现与证明决策？

Vero 是首个在仓库级同时评估”实现合成 + 证明合成”的基准，把形式化验证从”玩具函数”拉到”真实软件模块”。它衡量的是 Agent 能否理解模块接口、写出通过 Lean 4 证明器的正确实现与证明——这对加密协议、分布式系统等”错了就要命”的领域尤为关键。

构建方式

  1. 真实仓库提炼：43 个多模块实例源自真实开源仓库，覆盖 Python、Dafny、Verus、Coq 四种语言，领域横跨加密协议、分布式系统等
  2. 统一 Lean 4 表示：每个实例被整理为多模块 Lean 4 仓库，包含预定的 API 接口、人工策类的形式化规范（formal specification）与参考实现
  3. 双模式评测：
    • proof-only：实现已给出，Agent 只需补证明
    • code-and-proof：实现与证明都要从零生成，联合判定
  4. 审计机制（亮点）：Agent 被允许正式证明”给定规范不可满足”或”参考代码有误”——这一设计在策展阶段就主动暴露并修正了潜在的代码与规范错误，提升基准自身可靠性

关键发现

  • 最强 Agent 仅完全解决 27/43 实例（62.8%）：在最难仓库上”一个规范都关闭不了”——仓库级联合实现与证明合成，对当前前沿编码 Agent 仍是硬骨头
  • 实现与证明必须”连贯”：Agent 不能先写实现再硬套证明，二者的接口选择必须互相匹配，暴露了”孤立的代码生成”与”孤立的证明生成”都不足以覆盖真实可信软件开发
  • 审计机制是双刃剑：允许 Agent 反驳规范，既纠正了基准自身的隐性错误，也提示”形式化规范的编写本身就会出错”——验证链条的每个环节都需被验证

最新进展

  • 2026-08-13：论文提交 arXiv（arXiv:2608.13522），由 Dawn Song 领衔的 UC Berkeley SunBlaze 团队发布，代码与评测 harness 开源

关联基准

  • DeepSWE：零污染软件工程基准，同属”提升评测可信度”阵营
  • SWE-bench Pro：传统仓库级 bug 修复基准，Vero 是其”可信软件”维度的互补
  • CLEVER：函数级形式化验证代码生成基准，Vero 是仓库级的升级

不足与展望

  • 样本量仅 43，且最强 Agent 的具体模型身份未在摘要中指名，需等待完整逐模型分数
  • 统一转 Lean 4 可能引入”翻译失真”，Dafny/Verus/Coq 原生生态的证明风格未被完全保留
  • 目前仅覆盖 4 种源语言，系统级语言（如 Rust 的验证工具链）扩展待后续版本
代码生成 形式化验证 Lean 证明合成 可信软件