DeepMind 用 AI 智能体形式化验证 Signal 加密协议，属业内首次
roydanroy · x · 2026-11-11
Google DeepMind 宣布用新框架 AlphaProof Code 对 Signal 加密协议的实际代码完成形式化验证——即用数学证明代码满足关键安全属性。这被视为软件安全领域的重大挑战级突破。
- AlphaProof Code 是一个多 LLM 智能体框架：人类专家与 AI 协作确定要证明什么，再由一组智能体执行证明。
- 流程上，研究者先用多个模型把 Signal 的安全目标翻译成形式化数学规范，人类专家逐一审核；随后由 Gemini Carbon 驱动的智能体生成超过 600 万行 Lean 证明代码。
这是首次有 AI 在如此深度上形式化验证一个广泛部署的加密协议，也是该类协议实现首次被任何方法（无论是否用 AI）完成形式化验证。
所属事件:DeepMind AlphaProof Code 机器码级形式化验证 Signal 协议(27 条相关)→
「研究」频道最新
- LeapQuant 免训练量化线性注意力，B200 内核最高提速 3.7 倍 — tianyin_xu · 2026-11-12
- SPoT 意外收获：只在可解数学题上训练，也能识别域外不可答问题 — polkirichenko · 2026-11-12
- SPoT 实验数据：5 个安全基准提升 17.7pp，4 个数学基准提升 4.7pp — polkirichenko · 2026-11-12
- Sokoban 推箱子 LLM 评测上线：全网挑战模型最短路线纪录 — banteg · 2026-11-12
- 1920年《大众机械》预言成真:日食观测证实光线被引力弯曲 — generativist · 2026-11-12
- ELIZA 原始代码 2021 年才现世:2600 行纸稿靠人手敲回 — demian_ai · 2026-11-12