AlphaProof Code智能体生成300万行Lean证明，验证Signal核心加密

摘要：Google DeepMind 发布 AlphaProof Code，一套面向复杂软件形式化验证的智能体系统，可调用 Lean 等证明工具，在深度验证流程中生成约 300 万行形式化证明，用于核验 Signal 客户端核心加密实现。其关键方向不是让模型直接输出自然语言解释，而是让智能体围绕可执行证明目标持续分解、检索、重写并检查证明。该项目展示了 AI 驱动软件验证从单点定理证明走向大型代码库深层验证的潜力，但证明生成规模并不等于覆盖全部安全属性，仍需关注验证闭环、证明可维护性及独立复现情况。

---

AlphaProof Code 把代码验证变成智能体闭环

Google DeepMind 发布的 AlphaProof Code 面向复杂软件的形式化验证。其代表性案例中，多个智能体累计生成约 300 万行 Lean 证明，用于验证 Signal 客户端的核心加密实现。这里的关键并非证明文本的绝对数量，而是验证对象已经从单个定理深入到真实安全敏感代码库。

传统形式化验证通常要求工程师先把系统意图翻译为规格，再手工构造中间引理并反复处理证明器报错。AlphaProof Code 将这一过程包装成智能体工作流：模型根据编译器和 Lean 内核给出的反馈定位失败目标，搜索相关定义与既有定理，修改证明草稿，并再次提交机器检查。最终可信对象仍是可由 Lean 内核验证的证明项，而不是模型生成的自然语言论证。

这一区分决定了系统的工程价值：智能体可以降低证明工程中的搜索成本，Lean 内核则提供确定性的最终裁决。模型负责探索候选路径，证明器负责拒绝不成立的步骤，两者形成“生成—验证—修复”闭环。

技术机制：从定理生成转向深度验证

从现有官方摘要看，AlphaProof Code 至少体现了四个工程环节。

1. 把大型代码库切分为可验证义务

Signal 的加密实现包含协议状态、消息编码、密钥处理、边界条件以及实现与规格之间的一致性约束。智能体不能只对一个自然语言问题作答，而要持续识别缺失的证明义务，把它们组织成可执行目标。这个阶段类似程序分析中的分解：先确定“必须证明什么”，再决定“如何证明”。

大型代码库的难点在于依赖关系和上下文规模。局部定理可能缺少可复用引理，全局目标又可能触发较深的依赖链。证明智能体需要在定义检索、依赖探索和假设发现之间反复切换，而不是仅依赖模型参数中隐含的数学知识。

2. 以 Lean 内核反馈驱动修复

Lean 证明失败通常不是简单的语法错误，而可能来自类型不匹配、缺少参数、终止性不成立、某个引理无法访问，或中间目标与系统假设不一致。内核返回的精确错误位置为迭代修复提供了可执行信号。

这与传统代码生成中的“编译错误反馈”类似，但证明环境更严格。普通程序只要通过测试就可能被接受，而 Lean 中每个步骤都必须满足类型系统与逻辑规则。最终证明项能够由小型可信内核独立检查，降低了对生成模型自身判断的依赖。

3. 多智能体分工

300 万行证明规模意味着系统不能只依赖单个长上下文会话。更合理的架构是让不同智能体分别承担代码定位、证明规划、候选生成、失败修复、规格检查和去重等职责，再由编排器控制并行搜索与结果合并。

这种设计可并行探索多条证明路线，但也引入协调成本：多个智能体可能重复构造同一引理，局部成立的证明可能在合并时产生依赖冲突，冗长上下文也会增加模型推理费用。实际部署中，需要对证明任务进行可缓存的依赖图切分，并对候选引理做规范化后再合并。

4. 证明产物仍需独立审查

形式化证明通过内核检查，不等于规格本身完整，也不等于开发意图没有在建模阶段被遗漏。还需要区分三类保证：

• 证明与声明的数学命题一致；
• 数学规格准确表达系统应满足的安全属性；
• 实际生产代码与被验证代码保持一致。

如果实现、规格和构建产物之间存在偏差，再完整的证明也可能只验证了错误对象。因此，部署流程还需要代码哈希绑定、编译器与依赖固定、证明版本追踪，以及变更后的增量重验证。

工程权衡：验证规模不等于安全覆盖

约 300 万行证明是 impressive 的工程产出，但也容易造成误读。证明行数更多，意味着覆盖的义务、辅助引理或重复尝试更多，并不自动意味着安全属性覆盖更完整。更有意义的指标应包括：

• 目标代码和关键属性覆盖率；
• 无需人工修改即可通过的证明比例；
• 每次成功证明所需模型调用、Token、GPU 时间和编译时间；
• 证明在 Lean 版本升级后仍可重建的比例；
• 失败证明的分类及人工修复成本；
• 证明对编译器、库版本和代码变更的敏感性。

大型证明库还会带来维护压力。自动生成的证明可能冗长、脆弱或依赖偶然构造；即使每个步骤都有效，后续代码变更也可能迫使大量证明重建。工程上应优先保留稳定、可读且能被形式化证明社区审查的最小证明，并建立类似软件依赖管理的证明缓存与增量验证系统。

另一个现实约束是验证成本。Lean 内核检查单个证明通常很快，但模型生成候选、展开定义、尝试引理和编译失败反馈都会消耗推理资源。复杂代码库中的并行搜索可能产生巨量候选证明，因此需要以“已验证的安全义务”作为调度单位，而不是追求无限生成更多证明。

评测可信度：必须看覆盖与复现，而非只看行数

官方给出的核心数字是三百万行 Lean 证明和 Signal 核心加密验证。要判断其可推广性，还需要检查测试协议是否回答了以下问题：

1. “核心加密”具体对应哪些模块、版本和提交？
2. 哪些性质被形式化，规格来自规范文档、人工建模还是已有证明？
3. 有多少目标在智能体介入前已由人工证明？
4. 智能体贡献与既有证明库、现成形式化框架各占多少？
5. 是否报告基线模型、人工专家和单智能体方案？
6. 证明是否在固定 Lean 与依赖环境下由第三方重新检查？

在安全关键领域，最重要的验证对象通常不是自然语言摘要，而是可重复检查的证明工件、代码版本和环境锁定信息。独立复现若只重跑公开提示并重新生成相同证明，成本很高；更可行的是发布证明项、规范化脚本和哈希清单，让第三方直接对固定产物执行内核检查。

开发者落地建议

对于希望采用类似路线的团队，可以从边界清晰、可形式化的局部模块开始，而不是直接挑战完整密码协议。优先选择已有规格、测试覆盖充分且安全属性明确的组件，并把智能体置于以下闭环中：

1. 解析代码库与已有证明依赖；
2. 从规格生成结构化证明义务；
3. 检索定义、引理和已验证组件；
4. 生成最小 Lean 证明草稿；
5. 调用编译器与内核检查；
6. 对失败进行分类并迭代修复；
7. 将通过验证的证明与源码提交绑定。

生产化时还需要建立证明资产注册表、增量依赖追踪和版本化 CI。安全关键项目不应把模型生成成功直接当作发布许可，而应把“通过 Lean 内核检查”设为必要但不充分的条件，并保留专家对规格完整性和证明可维护性的审查。

行业影响

AlphaProof Code 展示了形式化验证智能体的一条可行路线：让模型承担开放式证明搜索，让小型可信内核承担确定性裁决。随着智能体能够阅读大型代码库、调用编译器并从错误反馈中恢复，形式化验证的瓶颈可能从“证明怎么写”转向“规格从哪里来”以及“如何持续维护证明”。

如果这一方法在更多密码学、操作系统和关键基础设施中得到独立复现，它有望缩短高保证软件从规范到机器可验证工件的时间，并降低专家逐行编写证明的负担。反之，如果所谓深度验证只覆盖狭窄路径，或依赖大量人工修复与选择，其通用价值会明显下降。真正值得持续跟踪的是证明覆盖率、端到端成本和可重复性，而不是证明代码的规模本身。

---

消息来源：Google DeepMind Blog (2026-11-10)

—— 完 ——

主题标签： #AlphaProof Code 关注 #形式化验证 关注 #Lean 关注 #代码智能体 关注 #Signal 关注