让 AI 写代码已经是老话题。让 AI 写完代码，再拿出一份数学级证明，告诉全世界“这段代码绝对没问题”——这才是新战场。UC Berkeley 等机构发布的 Vero 基准，恰好把这个战场推到了聚光灯下：它要求智能体在仓库级规模下，一边写实现，一边写证明，两边都不能偷懒。
让 AI 写代码，难的是证明自己写对了
代码跑得通，和代码被证明正确，是两件截然不同的事。前者只要测试用例够多就能交差；后者要求你把程序的每一步行为，都翻译成数学语言，再在 Lean 4 里一步步推导给机器看。Vero 的狠劲儿在于——它不让你挑简单的证明题做，而是把所有证明任务塞进真实的多模块仓库，让智能体面对一片谁也绕不过去的复杂性。
Vero 的出现不是偶然
过去几年，代码生成基准多到泛滥，但几乎都不碰“正确性”的硬核定义。HumanEval 考函数补全，SWE-bench 考问题修复，它们看的是功能对不对，而不是行为有没有被严格验证。Vero 直接换了一把尺子：仓库里的每个模块，不仅要能编译、能运行，还要满足 2705 条形式化规范。智能体交出来的代码，必须在逻辑上立得住，而不是在测试里蒙混过关。
和旧基准划清界限
43 个多模块 Lean 4 实例，听起来数量不大，但每一道都重得吓人。它们选自真实开源仓库，模块之间互相依赖，改一个函数往往牵连十几个定义。Vero 还准备了 743 个计分 API 来检测中间步骤，也就是说，智能体每往前走一步，系统都能看清它走到了哪里。这不是一场开卷考试，更像是在迷宫里装了一墙监控——你走没走对路，机器一清二楚。
仓库级复杂度：真正的战场
为什么非要在仓库级做这件事？道理很简单：单文件证明和仓库级证明的难度根本不在一个量级。你在一个孤立的函数上证明加法交换律，和在几十个文件、上千行代码的抽象层之间证明一个不变量，完全不是一回事。Vero 的“仓库级”三个字，直接把形式化验证的难度拉到了现实软件工程的维度。
43 个模块如何咬合
多模块意味着跨文件的依赖关系——你在模块 A 里修改了一个定义，模块 B 的证明可能立刻崩掉，模块 C 又把模块 B 当作前提。这种连锁反应是仓库级验证中最折磨人的地方。Vero 特意选用了真实仓库中的多模块实例，让智能体必须学会“考古”：理解模块之间的关系、追踪依赖链、在修改一处之后修复一堆下游的证明。这种能力，恰恰是现在代码模型最欠缺的。
2705 条规范不是装饰品
规范写得越细，智能体的自由空间就越小。Vero 的规范覆盖了函数的前置条件、后置条件、数据结构不变量等方方面面，几乎把工程里“隐式假设”的部分全部显式化。对智能体来说，这意味着它不能只写一个“看起来对”的实现，还要从规范里读懂每一个约束，再把约束翻译成 Lean 4 的证明目标。规范本身也在考理解力——读不懂题，何谈解题。
智能体被卡在了哪里
Vero 跑出来的结果，并不意外地打脸：代码生成得分和证明生成得分之间，出现了惊人的断层。智能体在“写代码”这件事上的表现，比“写证明”高出好几个身位。几乎每个模型都能生成看似合理的代码骨架，但真正为这些代码补完形式化证明时，几乎所有智能体都崩溃了。
代码写得好，不等于证明写得好
这种断层有一个技术根源：证明任务会放大智能体的“幻觉”问题。写错一个类型签名，编译不通过，模型能立刻尝试修复；但在 Lean 4 里证明一个命题时，模型往往会“一本正经”地编造一个不存在的中间步骤，或者虚构一个根本没有定义过的引理。这种幻觉不是靠增大模型规模就能解决的，它需要模型真正理解证明状态，而这一步的难度远超自然语言生成。
证明是另一维度的技能
写代码是一个从描述到实现的过程，信息是递减的；写证明是从实现里提炼不变量、构造中间引理，信息是递增的。模型惯于在文本分布里做“最可能的下一步”预测，但证明搜索的目标函数完全不同——每一步都必须被逻辑规则锁定，每一步都必须和上下文精准匹配。Vero 的 743 个计分 API，恰好把这种“每一步”精确地暴露出来：模型在决策边界上的一点点偏移，累积起来就是断崖式的失败。
形式化验证走向工程化的前夜
Vero 的出现，给 AI 编码领域敲了一记警钟：别再把“生成代码”当作终点。如果智能体想进入严肃的软件工程领域，它必须面对“正确性证明”这道门槛。Vero 最大的价值不是给出一份排行榜，而是把差距量化了——实现和证明之间的鸿沟，不是靠堆数据就能填平的，它需要全新的模型架构、搜索策略，甚至是全新的训练范式。
Vero 给出的信号
对研究者来说，Vero 最有价值的信号是：代码能力和证明能力之间存在一种强关联，但两者的训练路径不能互相替代。可能需要一种双引擎设计——一个引擎负责生成实现，另一个引擎负责在证明空间里搜索路径。后者目前几乎没有被充分训练过。Vero 把这个问题摆上了桌面，并且给了所有人一把可以反复测量的尺子。
值得盯紧的方向
接下来真正值得关注的方向，是证明策略的自动化。Vero 的计分 API 显示，智能体在 Lean 4 战术状态的每一步选择都有迹可循，这为强化学习提供了绝佳的奖励信号。也许下一步，就会有人用搜索算法替代自回归生成，在证明空间里做真正的规划。到那时候，Vero 的分数才可能从“惨不忍睹”变成“勉强够用”。但那一步，恰恰是所有试图跨界到形式化验证的团队，最难迈出的一步。
