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