你有没有过这种 review：diff 铺开一千两百行，你从顶上滑到底下，中间喝了半杯水，鼠标在 Approve 上悬了两秒。
然后评论区留下一句“整体没啥问题，建议这块补个注释”。
【灯光渐暗，演出结束，感谢观赏】
说的不是别人，是我们所有人。这行把“人看一眼”当成上线前最后一道防线，而站在那道防线上的人，眼睛是半闭着的。大家都知道，大家都不说。因为一旦说破，整条流水线就得停下来重新设计，而没人想在这个季度干这件事——流水线一停，第一个被问“为什么停”的还是你。
所以这个月初 arXiv 上那篇讲 LARK 的论文（2611.02028），我一开始是抗拒的。
形式化验证这四个字，你懂的。开会时有人提一嘴，全场点头，然后继续回去跑单测。听多了自动免疫，语感上跟“我们明年一定重视文档”是同一个家族。
但这次戳到我的不是证明本身，是它把“人”的位置挪了。
原来的流程：AI 生成 → 人逐行读 → 人点头 → 上线。LARK 的流程：人在生成之前先看一遍算子层面的 Lean 语义，一次性；AI 生成；机器去证这份生成物跟 PyTorch 参考实现在函数行为和内存行为上等价；上线。
人只在那一个点上，负一次责。
从“每次都得看”变成“看一次”，从“看一千行”变成“看几十行定义”。这不叫减负——这叫把一件本来就没在真干的事，改成一件能干成的事。
我觉得方向对，理由很土：人根本审不动 AI 写的底层 kernel。
不是不愿意，是物理上办不到。GPU kernel 那玩意儿，一个下标写反，语法完美，编译通过，跑起来照样给你吐数——只是在某些 shape 下那个数是错的。你打算用眼睛去抓这个？人眼的分辨率不接这种活。它擅长的是发现“这行注释怎么没对齐”。
时间也不站在人这边。生成的速度早就超过验证的速度，专家人工审那条线，堵在窗口很久了。你可以想象成后厨的出菜速度是服务员的十倍，菜一盘盘堆在取餐口，谁也没空管凉没凉。
再说我们心里真正的信仰：测试绿了就是对的。
这话我信了很多年，也不太敢公开怀疑，因为怀疑它显得你不重视质量。但测试给的是证据，不是保证。它只说明你想到的那几条路是通的；你想不到的那些房间里有没有人，它不知道，也不打算知道。
所以“覆盖率”这个指标最喜剧的地方在于：它衡量你踩过多少块地板，不衡量地板底下有没有洞。
——洞一般不长在你踩过的地方，不然它多没面子。
LARK 在这儿换了路子：它不测，它证。证的是生成的 kernel 与参考实现等价，精确算术下，函数行为和内存行为一起管。
中间那步拆解挺聪明。智能体先把整个 kernel 的语义切成小片，每片切得对不对由 Lean 4 自己校验，然后逐片写证明，最后拼回整体——绕开了“直接证一个大 kernel 等价”这种理论上可行、实践里没人干得动的事。
到这里我都还只是“嗯，做得不错”。
真正让我笑出声的是那组数字。
KernelCraft 上，配一个很朴素的 ReAct 智能体，GLM 5.3 把 12 个 Level-1 kernel 里的 10 个完整验完了；Opus 5.5 那边，5 个 Level-2 全过。这还算常规操作，工具好用嘛，应该的。
然后他们从主流开源 LLM 服务框架里随机抽了 10 个生产级 kernel 来验。9 个过，第 10 个——验出一个此前没人知道的数据竞争。
一个本来专门给 AI 的产出做安全验证的工具，顺手把人给查了一遍。
【关于本次事故责任归属的补充说明：暂无】
我们吵了两年“AI 写的代码能不能信”，吵的时候语气里始终带着一个没说出口的前提：人类写的那条线是可靠基准。现在这个基准被拿去量了一下。人写的那堆里也躺着一个没人发现的数据竞争，谁也不知道它躺了多久，可能比某些人的工龄还长。
（友情提示：数据竞争这种 bug，你跑一万遍测试也未必逮得到，因为它挑时机。你没见过它，不等于它没在。这条对人和对 AI 一视同仁，不搞双标。）
顺带一句，这篇论文作者十个人，Zixi Zhang 一作，后面一长串，剑桥那边 George Constantinides、Robert Mullins 这些名字在。十个人干一件事——放在“随便写个 prompt 让 AI 出 kernel”的年代，这个人力配比本身就说明了点问题，不用我多说。
我原本想在这儿插一个我自己 review 时抓到 bug 的例子来对称一下。想想算了。我真正抓到过的那次，是把一个变量名的拼写错误看成了缩进问题，性质上更接近眼花，不像审查。
打住，这个包袱有点冷，你们自己脑补笑一下。
所以这篇东西在我这儿的定位，不是“AI 生成的代码终于可验证了”。
是“人类终于可以不用假装自己在验证了”。
这两句差得挺远。前一句是技术进展，后一句是承认一个存在了很久的尴尬。我们过去那套逐行看 diff 的仪式，说白了是一种责任分摊机制——出了事，可以说“这道关我过了”。至于看得认不认真，没有第三方能验，也没人真想验。真验起来，第一个不同意的是排期。
现在把信任从“我的眼睛”挪到“一份被机器反复检查的语义定义”上。责任其实更重了，但至少是实的。
（郑重声明：以上感慨不构成对任何在位审查者的指责，包括我自己。评论区如果有“我们组 review 是真的认真”的朋友，欢迎来教我，我真诚地想学 🫠）