8 月 22 日 DeepMind 公开的 Vero 基准,把一个所有人回避很久的问题摆到了台面上:仓库级 Lean 4 形式化验证,最强模型 GPT-5.5 也只解出 43 个实例中的 27 个,另有 10 个实例所有受测模型全军覆没。
Vero 是什么?它在 arXiv:2608.13522 里把 Lean 4 评测基准从"单函数"拉到"多模块真实仓库"——从 Python / Dafny / Verus / Coq 真实开源项目抽取实例,涵盖密码协议、分布式系统。每个实例自带固定 API、人工编写形式化规约、参考实现,并提供"仅证明"与"代码+证明"两种模式。还内置了一种"形式化审计"机制——允许智能体提交"规约不可满足"或"参考代码错误"的机器证明,反过来挑基准自己的 bug。
这个设计在批评之前 Lean 基准的盲点:miniCodeProps / VERINA / DafnyBench 都只针对单函数、固定补全、独立算法——单函数的证明一旦依赖某个底层公共引理,被跨文件改动,全仓库证明随之失效。仓库级一致性推理,是验证工具与生成工具"错位"最深的层级。
为什么 DeepMind 走这一步?他们已经在 AlphaProof 上把 Lean 用作数学推理的载体(同一条主线),现在延伸到软件工程——Lean 证明助手核心承诺是:一个 trusted kernel 一步步对照 axiom,如果某一步不成立,checker 直接拒绝。这让"代码看起来对 / 测试通过"的叙事失去地基。AI 时代代码体量爆炸,人手已无力深入每一行评审,形式化的"机器可验证保证"补的是这块短板。
把这件事跟 8 月 21 日 Claude Code 2.1.234 / Antigravity Anywhere Remote Control 摆在一起看最清楚——AI coding 主线已经从"写代码速度"位移到"信任"。Claude Code、Codex、Cursor 在速度上已经推到工程瓶颈位;瓶颈现在压在"信任"这一段。Verified Code Generation 要把速度红利和信任红利同时拿走。Vero 暴露的 27/43 与那 10 个全军覆没的空白,说明形式化验证的难度天花板不在"模型能不能写证明",而在"仓库级一致性"。
这条边界一旦撞上,Claude Code / Codex / Cursor 在"速度 + 部署栈"上抢市场(oncall-kit、Antigravity Remote Control、本地 CodeMender)的同时,中期看 Vero 这类基准会迫使厂商把"仓库级一致性"做成下一轮产品差别化的关键战场。长期真正实现"模型生成代码 + Lean 自我证明 + 编译器级保护"才可能破掉"AI coding 信任赤字"。
但有两条暗面不能忽视:
1. 形式化的天花板在规约完备。 Insight 8/22 同日警示:specification generation 对 LLM 仍是显著挑战——证明可以验证"代码满足规约",但不能替你判断"规约是否抓住了所有重要属性"。这意味着 Vero 里那 27 个"成功"的实例,有一部分可能因为规约漏写了关键属性而被判"对"。工具自己漏的时候,如何发现?Vero 内置的"形式化审计"机制是回答这个,但目前只在受控范围内能跑。
2. 工程量同数量级。 一旦底层辅助函数改了实现,所有依赖它的证明都要重写——这与人类形式化专家的工作流是同等量级的工程难题。Vero 没有回避这一点,而是把它作为基准难度的一部分:能写出"被代码演化反复重写仍保持成立"的证明,才是真正的"仓库级"能力。
CodeMender(DeepMind 另一条线,找与修漏洞)也是同一个"从生成走向验证"结构里更安全的入口。两条线合起来看,DeepMind 正在把 AI 编程整套技术栈从"快写代码"推进到"写出能自证其对的代码"。
下一根钉子:做一份 Vero 子集上 HumanEval-style 的"形式化版本"——人工对照"代码 + Lean 证明"组合能否在工业级场景可信地替代传统的单元测试 + 静态分析。如果答案是 60-70%,硬件 + 路径规划这类高可信领域的 AI coding 才能真正签合同;如果<30%,DeepMind 这一手就只是把"形式化"从数学家的奢侈品变成工程师也能买的中端工具。
#DeepMind #Vero #形式化验证