AI写的代码越来越多，谁证明它是对的

刚看到Vero这个基准测试的消息，脑子里第一反应是，又来了。现在的AI编程基准多得像菜市场的摊位，个个都说自己考核严格。但仔细翻了下资料，Vero确实有点不一样，它是第一个把代码生成和形式化证明放一起考核的基准。简单说，不光看你代码写得对不对，还要看你有没有本事证明自己写对了。

这个痛点其实很真。我这阵子在用Claude Code跑项目，AI写代码确实快，但要确认它没埋雷，反而比我自己写还费劲。你让它解释代码逻辑，它说得头头是道，但那些解释是不是真话，得靠人一点一点验。Vero的思路是逼着agent在仓库级别同时产出代码和证明，相当于让它自己给自己交一份考卷的验算过程，这个方向我觉得是对的。

有个细节挺有意思，Vero的设计里专门加了审计机制，防止agent靠瞎猜搜索蒙混过关。这让我想起上周写的那篇关于训练推理分家的帖子。AI行业里很多指标看着漂亮，是因为挑战者自己也懂得怎么绕开它们。

更往后想一步，Vero图灵测试验证了多少个仓库倒在其次，真正的看点，是它第一次把这个逻辑摆到台面上：AI编程的下一个突破口，很可能是数学架构上的严谨性，不是生成更长的代码。就像给了学生一张卷子，终于开始要求他写出推导过程。CLAUDE CODE用得越熟练我越觉得，代码生成只是表象，能证明自己代码正确才是真正的关卡。

但话说回来，Vero测的都是形式化验证的场景，那是学术界和编译器领域的地盘。真到了业务应用层，仓库里一半都是没人维护的旧代码，指望agent去验证那些烂摊子，怕是连形式化什么都不知道。这基准离落地还有多远，又够喝一壶的了。

---

本文编译自 Hacker News，原文：https://vero.verina.io/
版权归原作者所有，本文为基于公开报道的编译与独立分析。