Gemini 4 Carbon 4 周完成 650 万行证明 实现加密协议数学验证突破

DeepMind 推出由 Gemini 4 Carbon 驱动的 AlphaProof Code 方法，仅用 4 周就生成约 650 万行 Lean 证明代码，完成了对广泛使用的 Signal 加密协议底层约 14 万条机器码的数学可靠性验证，这是史上首次将广泛使用的加密协议直接验证到实际运行的机器码层面。该方法模拟 AI 数学研究团队分工协作，生成的证明会通过 Lean 自动校验，仅约 1% 的内容需要专家复核，还成功识别出 Signal 过往的两个已知漏洞。目前相关研究规范和全部证明代码已开源。这项突破大幅降低了传统形式化验证的高门槛，未来可延伸应用到银行系统、医疗设备固件、电网软件等关键程序的安全验证场景。该成果由深耕相关领域二十余年的跨领域研究团队完成，实现了长期以来的科研愿景。