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
一键三连「点赞」「转发」「小心心」
欢迎在评论区留下你的想法！
— 完 —
🌟 点亮星标 🌟
科技前沿进展每日见
