AlphaProof Code：agent 证明了 Signal 的代码，Lean 负责批改作业
四周，六百多万行 Lean。Google DeepMind 说，它新做的 AlphaProof Code 框架让一群 AI agent 用数学方式证明了 Signal 协议实际代码的关键安全属性。Signal 和 Google Messages 里几十亿条私信，靠的就是这套密码学协议。证明的不是白板上的协议设计，而是编译后真正跑在设备上的代码。DeepMind 说，这种活过去要专家团队干好几年。
分工就是全部看点。人类和几个模型一起把 Signal 的安全目标翻译成形式化规格，每一条都经过人类专家审过。然后 Gemini Carbon 驱动的 agent 用 Lean 写证明、自己审计，再把需要人类复核的地方标出来，大约只占代码库的 1%。剩下的全部由 Lean 机械地检查。覆盖的属性包括设备被短暂攻破前后，消息依然受到保护。
真正让人信服的是那个反向测试。DeepMind 把两个已经修复过的真实 bug 重新放回一份隔离的 Signal 代码里。两次，系统都给出了机器可检验的证明：有 bug 的版本不安全。一个只会说没问题的检查器毫无价值，这个能说不，而且拿证明说话。
对比一下今天大多数 agent 产出是怎么被检查的：另一个模型读一遍，打个分。LLM 评委可以被说服、被奉承、被自信的文字唬住，今年一个接一个的基准都证明了这点。Lean 不吃这一套。所以信任问题并没有消失，只是挪了位置。这里的已验证，意思是满足这些规格，而规格是人写的、人审的。没写进规格的属性，就什么都没证明。那些说 Signal 已被形式化验证的标题，说过头了。
DeepMind 宣称了两个第一：AI 第一次在这个深度上形式化验证一个广泛部署的密码协议，也是这类协议的实现第一次被任何方法验证。两条都是它自己说的。Signal CTO Ehren Kret 出面背书，相关证明材料正在开源。值得抄走的模式比密码学大得多：让 agent 以机器规模生产，让一个说服不了的检查器来批改，把稀缺的人类注意力只花在证明什么这件事上。
来源：https://deepmind.google/blog/introducing-alphaproof-code/ （证明材料：https://google-deepmind.github.io/code-verification）
← 返回所有文章
分工就是全部看点。人类和几个模型一起把 Signal 的安全目标翻译成形式化规格，每一条都经过人类专家审过。然后 Gemini Carbon 驱动的 agent 用 Lean 写证明、自己审计，再把需要人类复核的地方标出来，大约只占代码库的 1%。剩下的全部由 Lean 机械地检查。覆盖的属性包括设备被短暂攻破前后，消息依然受到保护。
真正让人信服的是那个反向测试。DeepMind 把两个已经修复过的真实 bug 重新放回一份隔离的 Signal 代码里。两次，系统都给出了机器可检验的证明：有 bug 的版本不安全。一个只会说没问题的检查器毫无价值，这个能说不，而且拿证明说话。
对比一下今天大多数 agent 产出是怎么被检查的：另一个模型读一遍，打个分。LLM 评委可以被说服、被奉承、被自信的文字唬住，今年一个接一个的基准都证明了这点。Lean 不吃这一套。所以信任问题并没有消失，只是挪了位置。这里的已验证，意思是满足这些规格，而规格是人写的、人审的。没写进规格的属性，就什么都没证明。那些说 Signal 已被形式化验证的标题，说过头了。
DeepMind 宣称了两个第一：AI 第一次在这个深度上形式化验证一个广泛部署的密码协议，也是这类协议的实现第一次被任何方法验证。两条都是它自己说的。Signal CTO Ehren Kret 出面背书，相关证明材料正在开源。值得抄走的模式比密码学大得多：让 agent 以机器规模生产，让一个说服不了的检查器来批改，把稀缺的人类注意力只花在证明什么这件事上。
来源：https://deepmind.google/blog/introducing-alphaproof-code/ （证明材料：https://google-deepmind.github.io/code-verification）
评论