AI能写代码，为何还要证明自己？

AI已经能编写代码，可为什么还得接受证明？

让AI写几行代码，早就不再新鲜。真正困难的是把它放进包含大量文件、接口和依赖的真实项目后，还能说明“写出来的东西确实达到要求”。

UC Berkeley等机构近日推出Vero基准，专门考察这种能力。它把任务置于Lean 4形式化环境中，要求智能体在仓库层面完成两个步骤：先写出实现，再为该实现生成机器可以核验的证明。项目涵盖43个多模块实例，包含743个API和2705条形式化规范，并涉及加密协议、分布式系统等场景。

这样的设计看似有些苛刻，却比一段精彩的演示更接近我们真正关切的问题：AI给出的代码，究竟只是“看起来能用”，还是在各种边界条件下也有充分依据可以信赖？

从代码跑通到真正正确，仍有距离

普通测试通常只说明，给定的若干输入获得了预期输出。形式化证明的追问更加严格：在既定规则范围内，是否所有可能出现的情况都成立。二者并非相互取代。测试能够发现部分错误，证明则把需求转化为机器可检查的约束。

Vero的意义正在于此。它并非让模型补全一个函数，而是要求模型同时处理接口、跨文件依赖、实现取舍和证明。任何一个环节衔接不上，整个实例都可能无法通过。项目还允许审计者证明某条规范本身无法满足，或指出参考代码存在错误，从而避免将有缺陷的题目记在模型名下。

论文报告的结果也没有把AI描述成“问题已经解决”。最强配置在“代码加证明”模式下，43个实例中完整解决了27个；最难的仓库仍未关闭任何规范。这个数字表明进展很快，同时也说明，“会生成”与“能够交付可靠软件”之间依旧存在明显距离。

仓库级任务为何更贴近现实

许多AI编程演示只展示一个孤立的函数：输入清晰，文件不多，成功标准也容易解释。真实项目却往往相反。一个改动可能影响其他模块，文档中的需求也可能不完整，旧代码还会保留一些无人察觉的假设。

仓库级验证把这些复杂性保留在题目里。智能体不能仅靠补全语法蒙混过关，还必须让不同文件彼此一致，最终提交一份可供复查的证明。对使用者而言，这类评测比“生成速度提高多少”更能回答一个实际问题：在没有人逐行盯守的情况下，它能否依然产出可审计的结果。

当然，形式化验证也不是万能护身符。证明只能表明实现符合已经写下的规范；如果规范遗漏隐私、可用性或业务目标，机器也会一丝不苟地证明一个并不理想的要求。Vero检验的是代码与证明能否协同完成任务，并不能代替团队判断需求是否正确。

以后评估AI代码，我会多问一个问题

先问“它能不能运行”当然没问题。随后还应追问：测试覆盖了哪些边界？接口和数据约束写在哪里？是否存在独立检查，而非由模型自己声称“已经验证”？对于支付、权限、数据处理等代码，还需有人确认规范没有遗漏实际风险。

这也是Vero给普通用户的启示。我们不必立刻学习Lean 4，但可以清楚区分“演示成功”和“可靠交付”。让AI起草代码、解释报错、补充测试都很实用；一旦涉及真实数据和实际损失，保留人工审查、测试以及可追溯记录，仍是更稳妥的做法。

AI会写代码，解决的已是能力问题；AI能否把自身工作交给一套独立规则检验，才开始触及信任问题。