DeepMind

一个值得停下来想一想的消息 今天日报的头条值得单独展开讲讲：Google DeepMind发布了多LLM智能体框架AlphaProof Code，用AI智能体在Lean定理证明器中生成了超过600万行证明代码，对Signal加密协议的实际部署实现完成了形式化验证。 几个关键事实先摆出来： 这是AI首次在这个深度上验证一个广泛部署的密码协议； 也是Signal这类协议的实现首次被任何方法完整验证——注意，是被AI做到的，而不是被人类专家团队； 整个过程只用了4周； 人类专家只需要复审约1%的代码，其余部分由Lean的内核自动检查。 如果你不熟悉形式化验证，可能感受不到这几个数字的分量。我们来拆一拆。 为什么「验证实现」比「验证设计」难得多 密码学界有一个长期存在的尴尬：协议的数学设计和协议的软件实现，是两个几乎不同的世界。 Signal协议的数学设计（X3DH密钥协商、双棘轮Double Ratchet前向保密机制）早在多年前就被学术界用形式化工具（如Tamarin证明器）分析过，结论是设计层面站得住脚。业界也有过HACL*、Everest等项目，验证过密码学原语的参考实现。 但真正跑在你手机上的libsignal——那个由Rust、C、Java、Swift等多种语言写成、要适配各种平台怪癖、经过无数次重构和性能优化的生产代码——从来没有被完整验证过。原因很简单：**验证实现代码的成本是天文数字。**一个协议的设计可以用几十页数学符号描述，而它的实现是几十万行工程代码，每一条语句、每一次内存操作、每一个边界条件都需要在形式化系统中重建并证明。人类专家做这件事的代价，让「完整验证一个工业级协议实现」长期停留在论文的"future work"里。 而真实世界的漏洞恰恰就藏在这条缝里。历史上大量高危密码漏洞——Heartbleed、各种时序侧信道、状态机混乱导致的密钥泄露——都不是设计缺陷，而是实现缺陷。设计是完美的，代码是有洞的。**用户信任的是代码，学术界证明的却是设计。**这个错位存在了几十年。 AlphaProof Code填的就是这个缝。 AlphaProof的进化线：从IMO到生产代码 理解这件事的意义，需要看到AlphaProof这一年的轨迹。 2024年7月，AlphaProof在 IMO（国际数学奥林匹克）拿到银牌水平成绩；2025年，它达到金牌水平并登上《Nature》，论文披露其训练用了约3000亿token的数学与代码语料，团队构建了约8000万条形式化数学命题的「题库」。当时的叙事是：形式化推理是通往可验证AI的关键路径。 但IMO金牌本质上还是「玩具问题」——题目封闭、边界清晰、证明长度有限。今天这个发布则完成了从竞赛到工程的跨越：**被验证的对象从数学竞赛题换成了数十亿人每天使用的加密软件的部署代码。**这不是难度增加了一档，而是换了赛道——生产代码里充满工程妥协、平台特化、历史包袱，把它「翻译」进Lean并证明等价性，是形式化方法领域公认的最苦最脏的活。 框架层面的信息同样重要：AlphaProof Code是一个多LLM智能体框架，不是一个单一模型。这符合当下最清晰的一条工程趋势——前沿能力越来越不来自单个模型的规模，而来自模型编排：不同智能体分工处理代码理解、证明策略搜索、证明修补，Lean内核则扮演那个永远不会说谎的裁判。600万行证明、4周、人类只审1%，这三个数字合在一起描述的是一种新的人机分工：AI负责在巨大的搜索空间里生成证明，机器检查器负责百分之百的可靠性背书，人类专家只处理机器无法裁决的语义问题（比如「形式化规格本身是否写对了」）。 为什么这件事可能是个拐点 **第一，它把「安全」从概率问题变成确定性问题。**Fuzzing、渗透测试、代码审计，本质上都是抽样——测过的不代表安全，只代表没测出问题。形式化验证是穷举——证明通过意味着在这套规格下不存在某一类错误。AI把它从「奢侈到不可能」变成「4周、1%人工」。如果这个成本曲线继续往下走，未来安全关键的库（密码学、内核、金融清算、医疗设备固件）不做形式化验证，可能就像今天不做单元测试一样不可接受。 **第二，它给「AI写代码」提供了信任锚。**大家都在担心AI生成代码的可靠性，但这里有个有趣的反转：AI恰恰是让形式化验证变得经济可行的力量。AI生成代码 + AI生成证明 + 机器检查证明，构成一个闭环——**AI可以犯错，但证明检查器不会。**这可能是AI编程真正进入安全关键领域的唯一路径：不是让AI变得永远正确，而是让AI的输出变得可验证。 **第三，信号意义大于单一成果。**DeepMind选Signal不是偶然——它是端到端加密的旗帜，被Signal、WhatsApp、Messenger等数十亿用户依赖，是「值得验证」的最高象征物。第一个完整验证的果实摘在这里，等于向整个行业宣告：**没有哪个部署中的协议实现，从今天起在原则上不可验证了。**剩下的只是成本问题，而AI能力的成本曲线，没人敢赌它不下降。 冷静的一面 当然，也要看清边界。形式化验证证明的是「实现符合规格」，它不能证明「规格本身覆盖了所有安全属性」——那1%需要人类复审的部分，正是这个体系里最微妙的地方。侧信道攻击（时序、功耗、电磁泄漏）也很难被纯逻辑层面的验证捕获。而且Lean生态对主流工业语言（C++、Rust之外的多数语言）的形式化支持仍然薄弱，「任何代码都能验证」还有很长的路。 但方向已经清楚了。日报的趋势观察里说「形式化验证从设计层下沉到实现层」，我愿意更进一步：**这是软件可信性的一次范式转移的开端——从「测试到有信心」走向「证明到确定」。**十年后回头看，2026年11月可能就是那条曲线的起点。 本文基于2026-11-12 AI洞察日报头条撰写，相关信息来源：Google DeepMind官方发布、AlphaProof《Nature》论文（2025年11月）。