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

AI已经能编写代码，可为什么还得接受证明？让AI写几行代码，早就不再新鲜。真正困难的是把它放进包含大量文件、接口和依赖的真实项目后，还能说明“写出来的东西确实达到要求”。UC Berkeley等机构近日推出Vero基准，专门考察这种能力。它把任务置于Lean 4形式化环境中，要求智能体在仓库层面完成两个步骤：先写出实现，再为该实现生成机器可以核验的证明。项目涵盖43个多模块实例，包含743个API和2705条形式化规范，并涉及加密协议、分布式系统等场景。这样的设计看似有些苛刻，却比一段精彩的演示更接近我们