Google DeepMind 把「形式化验证」拉进 AI coding 主线:Vero 仓库级 Lean 4 基准 43 题、最强 GPT-5.5 也只解出 27 题

8 月 22 日,Google DeepMind 公开了「Verified Code Generation」研究岗位与配套基准 Vero——它要求 AI Agent 不只产出代码,还要同时产出 Lean 4 形式化证明。这是 AI coding 从「靠测试通过」位移到「机器级可验证」的拐点。

Vero 是什么

Vero 是 arXiv:2608.13522 在 8 月发布的「仓库级 Lean 4 评测基准」,包含 43 个从 Python / Dafny / Verus / Coq 真实开源项目抽取的多模块实例,覆盖密码协议与分布式系统等高可信领域。每个实例都内置固定 API 接口、人工编写形式化规约、参考实现,并同时提供「仅证明」「代码+证明」两种评测模式。基准还内置一种「形式化审计」机制——允许智能体提交「规约不可满足」或「参考代码错误」的机器证明,反向审计基准自身缺陷。

破纪录的关键数字

作者团队用前沿代码智能体与大模型做了完整评测:最强模型 GPT-5.5 在超高推理强度下,只完整解出 43 个实例中的 27 个;另有 10 个实例所有受测模型均未通过。这意味着仓库级形式化开发,对当前 AI 而言仍是「部分可行但远未跑通」。

跟以前 Lean 基准的差别

之前的 miniCodeProps、VERINA、DafnyBench 等 Lean 评测基准,都只针对单函数、固定代码补全、独立算法。Vero 把颗粒度直接拉到多模块真实仓库——单函数的证明一旦依赖某个底层公共引理,被跨文件改动,全仓库证明随之失效,要求的是全局一致性推理。这正是验证工具与生成工具「错位」最深的层级。

为什么 DeepMind 走这一步

DeepMind 已经在 AlphaProof 上把 Lean 用作数学推理的载体,现在把这条链延伸到软件工程。Lean 证明助手的核心承诺是:一个 trusted kernel 一步步对照 axiom,如果某一步不成立,checker 直接拒绝;这让「代码看起来对 / 测试通过」的叙事失去地基。AI 时代代码体量爆炸,人手已无力深入每一行去评审,正式化的「机器可验证保证」补的是这层短板。

为什么这件事比 GitHub Copilot 类产品更难

在 AI coding 大众市场里,Claude Code、Codex、Cursor 已经把「写代码速度」推到了工程瓶颈位;瓶颈位移到「信任」。Verified Code Generation 要把速度红利和信任红利同时拿走。Vero 暴露的 27/43 与 10 题全军覆没,说明形式化验证的难度天花板并不在「模型能不能写证明」,而在于「仓库级一致性」。一旦一个底层辅助函数改了实现,所有依赖它的证明都要重写,这与人类形式化专家的工作流是同等量级的工程难题。

不能忽视的暗面

分析 Insight 8/22 同日警示:形式化验证的天花板在规约(specification)是否完备。2026 一项研究指出,specification generation 对大语言模型仍是显著挑战——证明可以验证「代码满足规约」,但不能替你判断「规约是否抓住了所有重要属性」。CodeMender(DeepMind 另一条线,找与修漏洞)也是同一个「从生成走向验证」结构里更安全的入口。综合这两条线看,DeepMind 正在把 AI 编程的整套技术栈,从「快写代码」推进到「写出能自证其对的代码」。

这条主线对未来半年的意义

短期看,Claude Code / Codex / Cursor 继续在「速度 + 部署栈」上抢市场(oncall-kit、Antigravity Remote Control、本地 CodeMender);中期看,Vero 类基准的 27/43 与 10 题空白,会迫使厂商把「仓库级一致性」做成下一轮产品差别化的关键战场;长期看,真正实现「模型生成代码 + Lean 自我证明 + 编译器级保护」的部署栈,可能是破解「AI coding 信任赤字」的唯一路径。