DeepMind用AI形式化验证Signal协议
热点事件观察中
DeepMind用AI形式化验证Signal协议
3 篇报道3 个报道来源首报2 天前更新
先了解这件事
AI 综述
Google DeepMind 提出多 LLM 智能体框架 AlphaProof Code，由人类专家与 AI 共同确定待证安全目标，Gemini Carbon 驱动的智能体生成超过 600 万行 Lean 证明，形式化验证了 Signal 协议实际编译代码的关键安全属性。该工作以概念验证形式在四周内完成。 DeepMind 研究人员称，分析范围有限，并未形式化验证整个 Signal 移动应用，只是更大进程中的一个里程碑。团队公开了为 Signal 协议分析编写的规范与证明，供其他形式化验证工作使用。 据 The Decoder 报道，智能体在过程中标记约 1% 的代码库交由人工审查；DeepMind 计划通过 CodeMender 等系统将该方法扩展到电网和医疗设备。
AI 根据报道生成 · 1 天前更新
最新进展11月12日 02:18
Google DeepMind 推出 AlphaProof Code，四周完成 Signal 加密核心的形式化验证报道时间线
沿着报道，了解事件的不同侧面。
11月12日
- The Decoder精选Google DeepMind 推出 AlphaProof Code，四周完成 Signal 加密核心的形式化验证
Google DeepMind 发布 AlphaProof Code，用 AI 智能体对 Signal 加密协议的实际运行代码做形式化验证，原本通常需要数年的工作四周完成。
11月11日
- Ars Technica · AI精选Google DeepMind 用 AlphaProof Code 形式化验证 Signal 协议关键密码学保证
Google DeepMind 研究人员用智能体 AI 对 Signal 协议的多项关键密码学保证完成形式化验证，项目以概念验证形式在四周内完成，所用框架为 AlphaProof Code。
11月10日
- Google DeepMind精选Google DeepMind 提出 AlphaProof Code，用 AI 智能体形式化验证 Signal 协议代码
Google DeepMind 提出多 LLM 智能体框架 AlphaProof Code，由人类专家与 AI 共同确定待证安全目标，Gemini Carbon 驱动的智能体生成超过 600 万行 Lean 证明，形式化验证了 Signal 协议实际编译代码的关键安全属性。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。