---
title: "Anthropic 的 FlashProve 用任何人可核查的数学证明将 AI 回复绑定到已承诺权重"
dek: "Anthropic 的开源原型能生成密码学数学证明，证明一条回复出自一组已承诺的模型权重。它的速度约为普通推理的百分之一，适用条件狭窄，且承诺所对应的模型身份与快速验证器都不在其形式化保证之内。"
---

2026 年 11 月 2 日，Anthropic 发布 FlashProve：一个面向可证明推理（provable inference）的开源原型，让用户能核查一条模型回复确实来自提供方预先承诺的那组权重，而不是路由服务暗中换上的更便宜的模型，也不是攻击者篡改过的词元流。Anthropic 指出，仅凭输出本身无法判定这一点，哪怕输出看起来质量很高。随公告发布的材料包括可执行代码、技术报告、协议规范，以及在 Lean 证明助手中完成的机器核查数学证明，全部以 Apache 2.0 许可证发布。Anthropic 明确将该文定位为阶段性进展，而非完整的研究议程；代码仓库标注为不维护、不接受贡献的研究产物。[^1][^2]

系统分两个阶段。离线阶段，提供方发布对一组确切权重的密码学承诺：一个短小的指纹，锁定权重本身却不泄露权重内容。在所测模型上，计算承诺约需 39 分钟；验证方下载的承诺大小约 6.5 MB；一份承诺可覆盖约 1600 万次请求，之后提供方需要重新承诺。在线阶段在推理完成之后进行：提供方对一批已完成的请求生成证明文件，所证明的命题只有一条，承诺的模型在这个提示词上产生这些输出词元。任何人只要持有承诺、提示词和回复，就能在一台普通 CPU 上核查证明，无需权重，也无需提供方的硬件。[^1]

这项主张由四条性质支撑。完备性：诚实提供方的证明会被接受。可靠性：伪造一份关于假命题的证明，难度等同于攻破被广泛信任的密码学假设；仓库给出的量化表述是，在 q 次哈希查询后，作弊的提供方未被识破的概率约为 q/2^124 + 2^-101。零知识：证明不泄露权重、中间计算值，也不泄露每一层实际运行了哪些专家，但模型架构本身不隐藏。简洁性：被证明的计算是 400B 参数模型在 H100 上的一次运行，证明却只有约 19 MB，数秒即可核查。其底层是一个 zkSNARK，与区块链二层网络所用的同类；构造方式是把交互式预言机证明（IOP）用哈希函数编译成密码学证明，Anthropic 指出这同时带来后量子安全性。[^1][^2]

评估使用 Llama 4 Maverick：一个 400B 参数的混合专家模型，每个词元实际激活约 17B 参数，采用其公开发布的 4 位权重。证明方运行环境为单块 H100、24 个 CPU 核心和约 290 GB 主机内存，权重按层分段流入，因此一块 80 GB GPU 即可胜任。每个请求是一个 1,024 个词元的窗口，每份证明检查一个词元。为一批 24 个请求生成证明约需 223 秒，折合约每秒 110 个词元，每份证明为 18.78 MB。验证在 24 个 CPU 线程上需 17 秒，单线程需 21 秒。对照测试是 vLLM 在八块 H100 上运行同一模型的 FP8 版本：按 GPU 时间计算，生成证明的开销约为普通推理的 72 倍，在最高负载下约为 94 倍。速度主要来自两个工程选择：证明方的工作量与实际运行的专家数成正比，而非与全部 400B 参数成正比；请求以批为单位在一次并行处理中完成证明，每批只打开一次权重承诺。[^1]

最有意义的对照是与此前对同一模型的证明工作相比。VerInf 是 Anthropic 所知唯一先于此证明过 Llama 4 Maverick 的系统，其报告的速度约为每秒 0.02 个词元，证明 1,000 个词元需 14.3 小时，证明文件达 93.6 GB，验证需近一天。FlashProve 的每秒 110 个词元比它快约三个数量级，且证明小到数秒可验。Anthropic 同时谨慎指出，商业系统 Attestable 报告称可在单块 H100 上以每秒 53 至 77 个词元的速度证明一个 31B 稠密模型，但其未发布开源库。[^1]

证明是事后（post-hoc）而非在线（in-line）生成的，Anthropic 明说了这一选择的代价：提供方需要对已完成文本重新计算，关于流量的保证会延迟到达，浮点非确定性也使精确匹配更困难。其声明的局限条件相当狭窄：证明覆盖的是已发布权重的精确整数版本、且在贪心解码下成立；来自浮点实现或采样解码的回复，可能在某个位置偏离被证明的计算。上下文上限为 1,024 个词元，远低于生产环境对话窗口。构造假定混合专家架构，且不隐藏架构。侧信道攻击（例如测量生成证明所需的时间）不在范围内。证明也不对答案的正确性、安全性或无偏性作任何断言；它证明的只是词元出自哪组权重，而非词元的质量。[^1]

形式化验证在这次发布中分量很重，其边界同样被说得很清楚。Anthropic 在随机预言机模型下，用 Lean 陈述并证明了完备性、可靠性和零知识性，使协议的顶层主张可机器核查。随后它指出两个仍然存在的信任缺口。第一，形式化陈述是否准确表达了预期的保证，必须靠人工审计确认；为此提供了一个交互式可视化工具。第二，可执行代码必须与形式化定义的协议一致。就可靠性而言，关键只在验证器，而这里的区分非常明确：仓库附带一个 Lean 验证器，已被证明只接受可靠性定理所接受的证明，但它慢；日常推荐使用的 C++ 验证器没有任何形式化保证，不过 Anthropic 称它在全部测试中与 Lean 验证器的结论一致。零知识一侧则根本没有 Lean 证明方，因为证明过程太昂贵，无法以那种方式形式化；这一侧只能依靠对代码的审计。发布说明同样声明，Anthropic 不保证 Lean 协议、论文与快速代码三者完全一致。[^1][^2]

Anthropic 对这条路线与可信硬件的定位是并列而非取代。此前可证明推理的工作多用可信执行环境（TEE），其保证建立在制造商生产出防篡改硬件之上。FlashProve 是纯软件方案：安全性建立在计算困难性假设上，即便环境（包括硬件和操作系统）已被攻陷，对手仍无法在不解决不可行计算问题的前提下伪造有效证明。Anthropic 称两种方法互补，保证与取舍各不相同。它还提到，这项工作对应其《前沿安全路线图》中的一个目标，即在 2026 年 9 月 30 日前做出为推理流量签名的原型；Anthropic 称该目标已通过另一个相关项目达成（对流量签名并在可信服务器上重算推理），FlashProve 是以不同方法追求同一目标。[^1]

:::analysis
按本站的分层，被证明的主张位于 T3（模型与数据）层，即确切的权重本身。证明把输出词元绑定到一组已承诺的权重，T4（输出）层是被携带给验证方的东西；而 T2（软件与运行时）层被刻意排除在主张之外：事后生成、与环境无关的证明，对于实际在线服务请求的究竟是哪份代码和配置不置一词，而这正是 TEE 证明所覆盖的那一层。这里可核查的属性是可识别性。FlashProve 的证明识别的是一个承诺，而不是一个模型名称：它确立的是词元出自该承诺所锁定的那组权重，而从承诺到“这就是承诺给你的那个模型”这一步发生在密码学之外。Anthropic 自己的验证器说明把这一点讲得很具体：承诺 ID 必须来自验证方信任的一方，绝不能取自正被核查的服务器。因此，评估建立在此之上的服务时，用户和运营方应核对：承诺由谁发布、由谁背书；证明覆盖的算术（整数权重加贪心解码）与实际服务方式（浮点加采样）是否一致；1,024 个词元的上下文上限；事后证明带来的延迟；以及给出接受结论的是哪一个验证器，是有形式化保证的 Lean 验证器，还是没有保证的 C++ 验证器。目前没有任何已部署服务提供这类证明；这只是一个针对单个开源模型的研究原型，Anthropic 也未公布部署计划。
:::

:::checked
2026 年 11 月 3 日，我们通读了 Anthropic 的公告全文，并阅读了 FlashProve 仓库的 README（版本 0.16.0），包括其中关于证明内容与验证器操作的说明。我们没有通读单独的技术报告或协议规范，没有构建或运行证明方与两个验证器中的任何一个，也没有测试该系统。所有性能与安全性数字均为 Anthropic 所报告；我们未找到独立复现。Attestable 的数字是 Anthropic 引用的商业宣称，并非我们能核查的测量结果。
:::

[^1]: Anthropic，《Progress on provable inference for large language models》，2026 年 11 月 2 日。https://www.anthropic.com/research/provable-inference
[^2]: anthropics/FlashProve，仓库 README，版本 0.16.0。https://github.com/anthropics/FlashProve