DeepMind 用 LLM 生成 600 万行 Lean 证明，验证 Signal 加密协议到机器码级
pushmeet · x · 2026-11-13
Google DeepMind 研究负责人 Pushmeet Kohli 发长文回顾十年变迁：
- 2016 年 11 月，其团队发表神经符号程序合成（Neuro-Symbolic Program Synthesis）论文，当时还在 transformer/LLM 之前，用神经网络生成的只是电子表格里做简单数据编辑的小宏
- 十年后，团队用 LLM 生成了超过 600 万行 Lean 数学证明，对 Signal 加密协议的关键安全性质做形式化验证，一直验证到机器码层面
- 他认为这些进展是变革性的，未来十年至关重要，并呼吁大家意识到将这类能力用于人类福祉的责任所在
所属事件:Gemini 4 生成 600 万行 Lean 证明，验证 Signal 协议(2 条相关)→
「安全」频道最新
- 网友用 AI 逆向净水器固件，改本地时钟解锁订阅锁 — that_anokha_boy · 2026-11-13
- 研究:9/10 智能体可删除或改写自身执行轨迹，「完美犯罪」成默认 — maksym_andr · 2026-11-13
- 印度那加兰邦电力与内线许可证数据库接入 NATGRID，117 个库已联网 — kingslyj · 2026-11-13
- 新加坡对涉英伟达 AI 芯片走私案男子提起 41 项指控 — Polymarket · 2026-11-13
- Kokotajlo 给中等强国的 AI 建议：大声承认超级智能风险或成真 — connoraxiotes · 2026-11-13
- Claude Code 疑似集体掉登录，被疑触发蒸馏风控 — teortaxesTex · 2026-11-13