要求一边写代码一边证明其正确，最强智能体做出了43题中的27题——最难的那批一题未破
包括 Dawn Song 在内的团队于8月13日在 arXiv 发布了 Vero，称其为首个仓库级可验证代码合成基准。Vero 不是要求智能体写出一个能通过测试的函数，而是要求它在一个多模块代码库上给出可运行的实现，外加一份可由机器检查的证明，表明该实现符合形式化规范。它包含43个由真实仓库构建的实例，覆盖 Lean 4、Dafny、Verus、Coq 等证明与编程语言，领域从密码协议到分布式系统。作者测试的最强智能体配置完整解决了43题中的27题，在最难的仓库上则一条规范也没能闭合。
为什么重要?你读到的关于智能体写软件的几乎每一条论断，都建立在「测试通过」之上；而测试只覆盖有人想到要写的那些情况。机器检查的证明是唯一一种不在乎模型说得多漂亮的证据——证明要么编译通过，要么不通过。这是第一次有人在整个仓库的尺度上按这个标准去衡量智能体，答案是：简单的三分之二能过，困难的三分之一碰都碰不动。下次再有人说某个编程智能体「可靠」时，这是一个值得记住的数字。
在App中阅读——免费，9种语言
相关新闻
一个模型没有用训练所有AI的那套方法就学会了写字。2026-10-06TikTok把购物机器人放进了你正在看的视频里。
2026-10-06Reflection要免费放出一个5010亿参数的模型。
2026-10-06维基媒体怀疑OpenAI的智能体造成了五月的那次宕机。
2026-10-06Meta的助手给你生活里每个人都建了按小时更新的档案。
2026-10-05