650万行数学证明，4周交卷！Gemini 4 Carbon啃下加密协议验证硬骨头

4周时间，650万行证明，困扰软件安全研究者多年的难题终于破解，还得靠AI啊。

Gemini 4 Carbon一出，谷歌猛猛甩出硬核Demo，其中，一项名为AlphaProof Code的新方法被CEO劈柴推上C位：

全球数十亿用户聊天依仗的加密协议，终于被从数学上证明代码可靠了。

领衔研究的DeepMind副总裁Pushmeet Kohli难掩兴奋：

这是史上头一回！ 无论靠人还是靠AI，还从来没有人把一款广泛使用的加密协议，直接验证到实际运行的机器码这一层。

Signal首席技术官Ehren Kret也忍不住点赞，称AI Agent能够将实际运行的代码转化为有效的Lean定理，是一项里程碑式的重大突破。

网友们也纷纷感叹： 

这才是 AI Agent 落地工程的终极示范！把几十年的工作压缩到一个月，自动化验证太强了。

好家伙，AI Agent这回连代码安全都开始用数学严格证明了。

怎么做到的？

AI狂写650万行数学证明，四周完成多年验证工作

要知道，过去给软件做形式化验证，一般是数学家和形式化验证专家才能干的“贵族活”；

普通安全测试找到一个Bug修完就完事了；

但形式化验证却得靠专家写出严密的数学证明，确保软件在特定条件下不会出问题。

所以这项工作不仅烧钱费脑，而且还极其耗时，动辄三五年起步，复杂一点的系统甚至要耗上十年八年。

（比如早在2004年，澳大利亚NICTA研究团队就开始为seL4操作系统内核做数学验证，5年间累计投入的工作量，足够让一个人连续干上20年。）

现在，AlphaProof Code把这份繁重的证明工作接了过去。

它的工作方式有点像一支AI数学研究团队。

在这个案例中，首先，5名DeepMind专家会和AI一起，把Signal需要满足的安全要求写成Lean能够理解的数学规范，再由专家逐一审核。

审核通过后，由Gemini Carbon驱动的Agent小工们就开工了。

有的负责攻克不同部分的数学证明，有的负责检查证明结果。

它们一路追着Signal实际编译出来的机器码，一步步把需要证明的安全性质逐项落实到Lean代码里。

但这份答卷可不好糊弄。

Agent写出一段，Lean就检查一段。

只要证明里存在逻辑错误，Lean就绝对不会放行。

△AlphaProof Code工作流程图，图源DeepMind

就这样，五名研究人员各自守着一台工作站，同时推进任务，让AI不停地写、不断地验证。

短短四周内，Agent们就一口气写出了约650万行Lean证明代码，把Signal底层约14万条机器指令都纳入了数学验证。

不仅如此，在这项庞大的证明工作完成后，AI还贴心地帮研究人员筛出了需要重点复核的部分。

谷歌在Blog中透露，最终需要专家进一步检查的代码只占约1%。（Woc，1%？！）

但写出650万行证明，就真的能证明这群Agent真有本事吗？

研究人员们决定再考考它。

于是，他们翻出了Signal以前已经修复的两个真实Bug，并悄悄装回隔离测试版本，看看AlphaProof Code能不能察觉。

（一个涉及旧会话与新会话之间的密钥状态处理，另一个涉及密钥交换时缺少必要检查。）

结果，两道陷阱题全被AlphaProof Code逮了个正着！

AI不仅发现了问题，还分别拿出了通过Lean检查的数学证明，有理有据地证明带有这些Bug的版本确实违反了安全要求。

这下，Agent不仅真能证明代码符合安全要求，连故意塞进去的旧漏洞，也别想蒙混过关了。

更关键的是，DeepMind已经将这次研究的规范和约650万行Lean证明代码全部开源了，感兴趣的小伙伴们可以直接去拿来检查、复现和继续往下研究啦：

Anyway，这套新方法当然也有边界，谷歌Blog中也有写到： 

这次验证针对的是特定版本的Signal核心协议实现及指定安全性质，尚未覆盖整个Signal App和所有攻击场景。

但对于软件安全行业来说，AlphaProof Code意义已经相当直观——

它砍下了过去需要专家们投入大量时间、精力和金钱才能完成的数学验证的门槛。

而且这套办法还可以继续向外延伸。

从银行系统，到医疗设备固件，再到电网软件，那些一旦出错就可能造成严重后果的关键程序，未来都有机会接受同样严格的数学检验。

而站在这套AlphaProof Code背后的，是一个坚持了20多年的守望者。

一场跨越二十年的科研圆梦

对我个人而言，这一刻意义非凡。

二十多年前，我还只是一名刚刚踏上科研之路，研究如何检查复杂软件系统一致性的实习生。

如今，我有幸能亲自见证现代AI让这项艰巨的挑战变得切实可行，实在不可思议…

写下这段话的，正是负责AlphaProof Code研究的谷歌云首席科学家、DeepMind 副总裁Pushmeet Kohli。

△Pushmeet Kohli，图源谷歌

他的故事，要从二十多年前说起。

2004年，Pushmeet还在印度国立技术学院瓦朗加尔分校读计算机本科，一封突如其来的邮件，让他获得了前往美国微软研究院雷德蒙德实验室实习的机会。

在那里，他跟着团队研究如何验证复杂软件系统的可靠性，也由此正式走上了科研道路。

本科毕业后，他前往英国牛津布鲁克斯大学攻读博士学位，并于2007年获得博士学位。

此后，Pushmeet进入微软研究院，一干就是十年，后来一路做到了认知研究团队负责人。

△Pushmeet在微软研究院时期所做的演讲《人工智能的前沿——认知》

2017年，他又转身加入DeepMind，开始带领团队探索如何用AI解决科学难题。

从AlphaFold，到AlphaEvolve、AI Co-Scientist，这些年，他参与推动的项目越来越多，研究版图也从生命科学一路扩展到数学、软件和网络安全。

如今，二十多年过去，当年那个初出茅庐的实习生，已经成了Google DeepMind独当一面的科研大将。

而他年轻时研究的难题，也终于在AI的帮助下迎来了新的解法。

Pushmeet之外，AlphaProof Code背后还站着一群大佬。

比如Swarat Chaudhuri，他既是得克萨斯大学奥斯汀分校计算机科学教授，同时也是Google DeepMind研究员，长期研究如何将AI与形式化验证结合。

△Swarat Chaudhuri

还有密码学领域的老将Jonathan Katz。

他曾在马里兰大学任教二十多年，担任过该校网络安全中心主任，还是ACM和国际密码学研究协会（IACR）的双料Fellow。

△Jonathan Katz，图源马里兰大学

一群深耕密码学、软件验证和AI的研究者，就这样聚到了一起。

而在宣布AlphaProof Code取得突破的帖子里，Pushmeet还特意写下了一句话：

总之，我为我的团队成员感到无比自豪。

是啊，二十多年过去，当年那个埋头钻研解法的年轻人终于等到了答案。

真好。

参考链接：

[1]https://x.com/pushmeet/status/2120127611137634376

[2]https://deepmind.google/blog/introducing-alphaproof-code/

[3]https://github.com/google-deepmind/code-verification?utm_source

[4]https://google-deepmind.github.io/code-verification/#fig-workflow

[5]https://www.youtube.com/watch?v=qgEOSO8ZlOg

文章来自于"量子位"，作者 "文婷"。