AlphaProof Code 与 MathForm-8B：同一 Lean 流水线的两个阶段，而非两个对手

仔细阅读 AlphaProof Code 论文，会发现一个公告并未强调的数字：在 DeepMind 的五名研究人员花四周时间验证 Signal 的过程中，无法自动化的部分是前端环节。人类专家与多种模型协同工作，把 Signal 的安全目标转化为正式的 Lean 规范，并且在任何证明工作开始之前，每一条规范都由专家审查过。这就是瓶颈所在。MathForm-8B 是 OpenBMB 于 2026 年 8 月 14 日在 Hugging Face 上发布的 80 亿参数自动形式化模型，它正是为了把这一步自动化而做出的直接尝试——接收自然语言数学陈述，并输出可供他人证明的 Lean 4 定理陈述。把它们并排放在一起，你比较的并不是两个产品。你看到的是同一条流水线中前后相继的两个阶段，二者之间隔着数学与协议安全之间的差异。

流水线，按工作发生的先后顺序

对真实软件进行形式化验证有三项任务。第一，确定必须成立的是什么，并用形式化语言写下来。第二，证明实现满足它。第三，机械地检查证明，因为错误的证明比没有证明更糟。

MathForm-8B 只做一件事，且面向一类狭窄的输入：教科书式的数学命题。给它“对每个实数 x，x² 非负”，它会返回 Lean 4 中的导入项、类型和定理头。它不返回的是证明，而且其作者明确表示，证明搜索是别人的问题。它报告的数字均由厂商提供且未经复现：在六项基准上，语法检查下的平均 Pass@8 为 88.06%，更严格的一致性检查下为 72.37%——这两个数字之间的差距，诚实衡量了语法上有效的陈述有多少次所表达的含义与所要求的不同。

AlphaProof Code 负责第二项和第三项工作，外加一个 MathForm-8B 无法触及的规范阶段。Signal 的安全目标并非 MathForm 训练所依据的那种数学命题；它们是关于协议的陈述——消息在设备被临时攻陷之前和之后都保持受保护，发起方和响应方确为其声称的身份。将这些目标转化为 Lean 需要协议专业知识，而任何 8B 自动形式化器都不具备这种知识。规范一旦存在，证明工作便完全交给智能体，检查工作则交给 Lean 内核以及一个守门智能体，它使用 比较器 对照一份留出的规范副本。

使用每一项实际需要你付出多少代价

• 权重 — MathForm-8B：可下载，Apache 2.0，四个 BF16 格式的 safetensors 分片，基于 Qwen3-8B 微调。AlphaProof Code：无。此次发布包含一个 Lean 开发项目、一个 AArch64 语义以及一个位于 github.com/google-deepmind/code-verification 的 libsignal 绑定。

• 运行它 — MathForm-8B：在你自有的硬件上使用 Transformers、vLLM 或 SGLang，它们都提供兼容 OpenAI 的端点。AlphaProof Code：没有端点、没有 API、没有候补名单、没有价格；它是一个研究框架，DeepMind 称其在规模化之前需要“持续研究”。

• 输入 — MathForm-8B：一段自然语言数学陈述。AlphaProof Code：一份形式化规范，以及你希望针对该规范进行证明的二进制文件。

• 输出 — MathForm-8B：一个 Lean 4 定理陈述，未经证明。AlphaProof Code：一个经机器校验的证明，或当代码有误时给出一个反证。

• 人工审核——MathForm-8B：你审核生成的陈述，而在一致性为 72.37% 的情况下，你将会审核其中很大一部分。AlphaProof Code：专家在证明工作开始前审核每一项规范，随后智能体将代码库中约 1% 标记出来供二次检查。

• 已知限制——MathForm-8B：仅限数学陈述，不生成证明；其 README 中链接的代码仓库在发布时仍只是占位符。AlphaProof Code：对 SPQR 修复不提供后量子保证，不提供载荷隐私，每次提升仅支持一个会话，并且其 MAC 伪造界在单个会话中接近 25,000 条消息时会变得空洞。

MathForm-8B 将不得不弥合的差距

人们很容易会说，自动形式化器本可以写出 Signal 的规范，从而为研究人员省下前期投入的数周时间。但论文本身的论述并非如此，而且原因很具体。协议的规范并不是对某项主张的复述，而是关于敌手模型的一种选择。Signal 的工作包含两条轨道：一条是 Dolev–Yao 符号轨道，其中量子攻击者会在握手之后攻破 Diffie–Hellman；另一条是计算轨道，其中采用经典敌手并给出具体界。这两条轨道针对同一份代码陈述了不同的定理，而在二者之间做出选择是一项具有安全后果的工程决策。任何被训练来把“证明 x² ≥ 0”转成 Lean 的模型，都不会做出这个决定。

一个自动形式化器有望做到的，是这项工作中机械性的部分：给定一个用自然语言表述的安全目标和一组现有的 Lean 定义库，按照项目自身的表达习惯产出该陈述的初稿，供专家修正。这确实是一种实实在在的节省，但比标题所暗示的要小得多。论文报告了一份规范偏差目录，包含 200 多个计算类条目和约 35 个符号类条目——其中 15 个是 Double Ratchet 分析中的缺口或缺陷——这正是人工审查环节发现的内容。一个能够起草陈述的模型，必须对照那份目录来衡量，而不是对照数学基准上的 Pass@8 分数。

当这两个数字完全不可比时

MathForm-8B 的 88.06% 和 AlphaProof Code 的 650 万行衡量的是不同的东西，绝不应被放在同一列中。一个是作者自建基准套件上的命中率；另一个是为一个目标生成的证明数量。厂商坦承，88.06% 使用的是语法检查，而这是一种弱标准——语句可以编译通过，却仍可能形式化了错误的命题，这就是为什么一致性数字要低 16 个百分点。

AlphaProof Code 中一个风格可比的图是验证工作：两个此前已修复的 Signal bug——一个弱状态 bug 和一个小子群 bug——被重新引入一个隔离副本中，而在这两种情况下，系统都生成了机器检查的证明，证明有 bug 的版本不满足安全定理。这是一个负向测试，而负向测试正是自动形式化器基准完全缺失的东西。MathForm-8B 没有报告任何形式为“给定一个故意错误的陈述，模型指出它错了”的结果。

你会如何实际将它们结合使用

具体来说，而且这是比较中唯一有近期可行路径的部分：用自动形式化器起草，用强大的通用模型评审草稿，再用证明智能体尝试完成证明。每个阶段都有不同的失败模式，而通过同一个密钥路由这三者是一种实际便利。在 OrcaRouter 上，超过 200 个模型通过单一 API 提供，按供应商标价、0% 加价，因此，将同一陈述发送给两个模型并比较其 Lean 输出的规范起草循环，只是一次路由 DSL 调用，而不是三份合同和三个 SDK。自动故障转移可应对你选择的模型恰逢状态不佳的情况。

这些东西都无法提供保证。MathForm-8B 给出一个陈述，模型给出评审意见，但仍然需要有某种东西来证明它。目前，唯一一个能在真实部署代码上闭环的已发布系统是 AlphaProof Code，而且它并不出售。

阅读这两篇论文而不是选出一个赢家的原因

MathForm-8B 是一个有用的工件，任务范围狭窄，并且存在真实、经测量得出的准确率上限。AlphaProof Code 是一个工作流演示，其最具可迁移性的发现不是证明体量，而是这种分工：规格工作适合由人类和强大的通用模型承担，证明工作适合由智能体团队和内核承担，而二者之间的边界正是所有难点所在。任何构建验证流水线的人都应认真对待这种分工，并把自动形式化视为降低第一阶段成本的一环——而不是取代它的一环。

对于一个正在决定这个月要下载什么的团队，坦率的总结是：MathForm-8B，可以，如果你使用 Lean 并且想要一个起草辅助工具。AlphaProof Code，去读工件仓库和规范偏差目录，因为这份目录比任何公告都更能告诉你，生产代码的形式化验证仍然无法触及什么。