Google DeepMind成功进行AI驱动的代码形式验证
2026年11月14日 · 阅读 1 分钟
Google DeepMind的研究团队利用人工智能对“Signal”的基础代码部分进行了形式验证。这意味着，该加密消息应用程序的至少部分代码已被数学证明无误，能够按预期运行。考虑到最近的AI系统发现了多少软件漏洞，以及有多少人的沟通受到Signal加密技术的保护，此结果令人鼓舞。使用相同加密技术的还有“WhatsApp”和“Google消息”。
DeepMind在此次验证中使用了名为“AlphaProof Code”的框架。研究团队表示，这是一个“将人类专业知识与AI代理相结合、在前所未有的深度进行形式验证的创新代理型框架”。他们指出，形式验证是“安全保障的最高标准”，但如果没有像AI系统这样的规模化自动化，完成这一艰巨任务需要耗费大量时间。
研究团队将验证工作分为两个阶段，首先确定需要验证的对象，然后由多个在Google最新模型“Gemini 4 Carbon”上运行的代理执行验证工作。此外，代理会检查验证结果，并指出需要人类重新检查的部分，但这些部分仅占代码库的1%。这大大缩短了验证时间。通常，软件验证需要手动证明，因此耗时较长。以往正是由于这项工作的繁重，形式验证成为遥不可及的目标。然而，DeepMind团队在一个月内完成了通常需要专家数年才能完成的验证工作。
虽然DeepMind并未验证Signal的所有代码，但他们指出，AI在网络安全领域带来了重大变革，此次验证是加强安全基础设施的第一步。未来的产品发布计划尚未透露，但DeepMind已将代码开源，以支持其他组织和个人的形式验证工作。DeepMind补充道：“对Signal核心加密技术的验证将为保护医疗设备固件到电网软件等其他重要系统打下基础。”