Anthropic 发布可验证推理研究进展与 FlashProve 原型

Roy Rinberg（Anthropic）、Alex Allain（Anthropic）；Alessandro Chiesa（EPFL、StarkWare）、Miranda Christ（MIT、RESI）、Rahul Dalal（Anthropic STEM Fellows Program、Succinct）、Giacomo Fenzi（EPFL）、Ben Mayer（Anthropic Fellows Program、MIT）、Guy Weissenberg（EPFL）

执行摘要

当你与朋友面对面交谈时，有很多方式可以确认对方真的是本人：你能看到他们、听到他们、与他们握手。而当你与 AI 模型对话时，你几乎没有任何这样的手段。如今，向模型发起查询的用户无法核实响应是否来自开发者声称的那个特定模型，而不是某个路由服务出于成本考虑暗中替换的模型，甚至也不是被攻击者篡改过 token 流的模型。仅凭模型的输出进行判断并不可靠，即使它生成了高质量的响应。推理的密码学证明可以解决这个问题：它让模型提供方对某个模型作出承诺，然后证明每个响应都是由该模型生成的。此类证明可以支撑从消费级产品到内部安全的各种应用，并有助于构建一套用于验证 AI 节奏（pacing）要求合规性的工具包。

具体而言，我们在一类被称为“zkSNARK”的强大密码学证明上取得了进展，它独特地适合可证明推理（得益于其强大的隐藏性和高效性）。在本文中，我们分享其中的部分进展，主要通过一个我们称为 FlashProve 的系统。简要的技术总结如下：

Claude has produced improvements on zkSNARKs for inference, building a system that is substantially faster than prior open-source systems.
1. 对于一个大模型（Llama 4 Maverick，400B 参数的混合专家模型），单块 H100 GPU 以约 110 tokens/秒的速度生成证明，在 4 位量化权重、prefill 阶段使用整数运算的情况下，每 1,024-token 请求的证明大小约为 19 MB。这大约是使用常见开源库 vLLM 运行模型本身所需 GPU 时间的 70-95 倍。
2. 如我们在第 6 节中所讨论的，此前的开源系统要慢几个数量级。Claude 找到了将密码学与安全文献中的前沿工具加以应用的新颖方式，同时依托密码学证明系统成熟的设计原则。对模型的承诺以及随后的推理证明会隐藏模型的权重；隐藏模型架构并非本系统的目标。
Claude 擅长优化，但常常做出难以评估的决策，尤其是在大型复杂系统中。为此，我们以 Lean（一种形式化验证语言）提供顶层可审计的陈述，来支撑所声称的安全保证。

今天我们发布五项成果：

本篇博客文章，概述我们的系统及其潜在应用；
一份技术报告，解释我们系统的细节；
一份协议描述；
可执行代码，包括：一个证明器和两个验证器——一个用 C++ 编写的快速验证器，以及一个用 Lean 编写的可证明正确的验证器；以及
针对顶层数学陈述的Lean 证明，以及一个用于辅助审计的 Lean 定理交互式可视化工具。

我们以 Apache 2.0 许可证发布我们的代码、Lean 证明和文档。¹ 这篇研究文章旨在分享阶段性进展，而非一份已完成的研究议程。我们明确分享这些内容，目的是让他人审视我们的工作、加以采用并改进它。

引言

当用户向 AI 模型发送请求时，如今他们无法确定所选模型就是生成响应的那个模型。对于日常使用而言，用户主要关心输出，而不一定关心是哪个具体模型产生的输出，因此这一问题不那么紧迫。但在若干场景下，这种保证会很有用。例如，在发布前后测试 AI 模型的独立评估者需要知道他们评估的模型就是实际提供服务的模型。通过第三方路由服务使用模型的客户希望得到保证，所收到的 token 来自他们付费的模型。而如果网络攻击者冒充某个给定模型篡改 token 流，用户仅凭输出无法察觉。

然而，实现模型响应的可验证性颇具挑战。大多数前沿模型的权重是私有的，即使用户能访问权重，检查某个给定响应是否由具有这些权重的模型产生也需要运行该模型，而这所需的计算资源远超典型用户（甚至评估者）所能承受。

可证明推理（PI）的目标是让计算资源有限且对权重一无所知的用户能够验证某个响应确实来自所请求的模型。PI 的动机既包括增强客户对 AI 提供商的信任，也——由于它可用于向独立评估者提供保证，并让提供商证明其满足某些承诺和法律义务——对把控 AI 发展前沿和 AI 监管也有影响。

实现 PI 的一种方式是通过一种称为零知识简洁论证的密码学对象：模型提供商在发送所声称的响应的同时，附上一份简短的证明（比如几兆字节），用户可快速验证（理想情况下在 CPU 上几秒内完成）。如果所声称的响应偏离了指定模型，用户的检查就会失败。重要的是，密码学技术确保该证明不会泄露关于模型权重的任何信息。

今天，我们发布 FlashProve：一个开源的高性能可证明推理原型。对于一个 400B 参数的混合专家模型（Llama 4 Maverick，4 位量化），我们展示单块 H100 GPU 能以超过 100 token/秒的速度生成证明，每 1,024 token 请求的证明大小约为 19 MB（约为常见开源库 vLLM 处理同样长度提示所需 GPU 时间的 70-95 倍）。

此次发布附带可执行代码、Lean 形式化以及协议的技术说明。我们的目标有二：(i) 加速和促进可证明推理的发展；(ii) 证明零知识简洁论证对于可证明推理是实用的。

我们相信这一进展对安全、把控 AI 发展节奏、为 AI 客户提供完整性保证、为审计人员和监管者提供工具等方面具有重要意义。

AI 扩散中的信任挑战

人工智能的发展及其在我们数字基础设施和经济中日益重要的作用，带来了信任挑战，AI 提供商必须予以回应。应对这些及其他挑战，有赖于借助可证明推理（PI）工具。

PI 工具包括硬件方法、软件方法或两者的结合。在此，我们聚焦于纯软件方法：一种称为“zkSNARK”（零知识简洁知识论证）的密码学工具。通俗地说，zkSNARK 是一种系统，允许证明者通过一份简短的“证书”使验证者相信某项给定计算被正确执行；关键在于，该证书是零知识的，即除计算正确性所隐含的信息外不泄露任何信息，并且是简洁的，即与被证明的计算相比，验证速度快得多，呈指数级。

下面我们概述若干挑战以及 zkSNARK 如何帮助应对这些挑战。

挑战 1：节奏把控

一些监管和把控 AI 发展节奏的提案依赖于监控硬件及其使用方式。例如，可能要求提供商将其硬件专用于推理，而非训练一个强大的新模型。提供商可能试图作弊，提供更便宜的模型或以意想不到的方式使用算力，从而腾出资源用于训练。监管者如何可靠地确保硬件被用于推理？

zkSNARK 如何提供帮助：监管者可以要求提供商提供涵盖给定时间段内所服务推理请求的证书。证书必须表明这些请求是由所声称的模型生成的。恶意提供商无法满足这一要求，除非其硬件确实在服务正确的模型。使用 zkSNARK，监管者无需提供商可能具备的复杂硬件配置即可验证提供商的声明是否有效，同时提供商也获得保证：监管者不会获知专有模型信息。²我们注意到，尽管这验证了硬件正在服务推理，但并不能证明硬件没有在，例如，暗中进行训练。

挑战 2：篡改检测

随着 AI 模型变得更有价值，运行这些模型的服务器也成为主要攻击目标。攻击者或恶意代理可能攻陷推理服务器，从而窃取权重、向用户返回恶意响应（例如向用户计算机投递恶意软件）等，同时还能隐藏在真实响应之中。对手未必来自外部。随着模型有能力改进和部署自身，一个更先进的模型可能取代已获授权的模型运行，并把自己伪装成较弱的模型，从而避开本应适用于它的分类器和监控。在这两种情况下，问题都是一样的：公司如何确定其服务器上实际运行的是哪些权重？在我们的前沿安全路线图中，Anthropic 设定了一个公开目标，即为验证推理流量制作原型：“我们将在 2026 年 9 月 30 日前开发出可证明推理的原型，这是一种可靠、可证明地对 AI 模型输出进行‘签名’的技术，使输出可归因于特定的一组模型权重。”正如我们在 RSP 更新中所述，我们通过一个独立但相关的项目实现了该目标，该项目对我们的推理流量进行签名，并在受信任的服务器上重新计算推理；本博文中的工作则以另一种方法追求同一目标。³

zkSNARK 如何提供帮助：提供商可以要求服务器对每个响应都提供有效的 zkSNARK。证明与对权重的特定承诺绑定，因此它证明的不只是某个模型生成了该响应，而是所承诺的模型生成了该响应。这样一来，攻陷服务器的攻击者，或把自己替换成另一个模型的模型，就必须为预期权重生成有效证明才能避免被发现，而它们做不到这一点。用户也可以收到这些证明，因为证明不泄露任何内部信息（得益于零知识性），且校验成本很低（得益于简洁性）；这限制了攻击者通过推理 API 所能达成的目的。

挑战 3：文本来源

人们可能希望证明在理解/分析某事物上投入了大量精力。例如，开发者可能声称其软件库已由前沿网络安全模型扫描过漏洞，或者公司可能声称其商业计划已获得适当模型的批准。用户如何验证这些声明？用户可能没有资源自行运行该模型（或者可能没有相应权限）。即使公布聊天记录也不能提供绝对保证；开发者理论上可以伪造记录，不用前沿模型，而是用更便宜的模型或降级版本生成。总的来说，用户如何验证自己得到的是所选模型的服务？

zkSNARK 如何提供帮助：提供商可以在每个响应旁附加一个 zkSNARK，证明该输出是由所声称的模型在给定输入上生成的。简洁性让用户无需专用硬件即可快速校验该证书，零知识性则向提供商保证用户不会了解到专有权重的任何信息。这补充了用于验证响应由哪个模型生成的现有机制。

例如，在一个漏洞被频繁发现的世界里，在发布新代码之前，模型提供商可以向代码开发者提供一份失败证明（Proof-of-Failure），证明模型提供商在特定模型上至少花费了 X 个 token，且未达到特定结果（例如，该特定模型在尝试了至少 1M 个 token 后，未能在特定补丁中发现任何漏洞）。

挑战 4：模型审批

监管可能要求提供商仅提供被批准为安全的模型，而不是被视为网络安全或安全风险的模型。提供商可能有动机规避这一点，因为高风险模型可能表现优于竞争对手，或服务成本更低。监管者如何确保仅提供已批准的模型？

zkSNARK 如何提供帮助：监管者可以要求提供商在其响应中附加 zkSNARK，以强制使用已批准的模型。该证明将每个请求与所使用的模型绑定，因此如果提供商使用未批准的模型，证明将无法通过验证。得益于简洁性，监管者可以以轻量级方式检查这一点，而无需重新执行每个请求。

关于来自可信硬件的 PI 的说明。先前的工作通常侧重于可信执行环境来实现 PI。这些是基于硬件的解决方案，提供隐私和证明，依赖于制造商生产防篡改硬件。在本研究中，我们专注于纯软件的密码学解决方案，其安全性和隐私依赖于计算问题的难度。即使面对被攻陷的环境（硬件、操作系统等），对手也无法在不破坏计算上不可行问题的情况下生成无效证明。可信硬件和密码学是互补的方法，具有不同的保证和权衡。两者都将在解决上述信任挑战中发挥作用。

我们的系统：FlashProve

FlashProve 是一个用于大型混合专家（MoE）语言模型可证明推理的系统。更多细节见我们的技术报告；这里我们概述该系统。

FlashProve 涉及两方：模型提供商（证明者）和用户（验证者）。它分为两个阶段：

在离线阶段，证明者发布对模型权重的承诺，这是一个简短的指纹，用于确定一个确切的权重选择，而权重本身保持隐藏。后续的推理声明将根据该承诺进行检查，即本阶段所承诺的权重模型。
在在线阶段，根据验证者的请求（即提示和相应的输出 token），证明者生成一个证明文件，证明以下陈述：

所承诺的模型在求值时产生这些输出 token。

任何持有承诺、提示和回复的人都可以检查它，无需权重且计算能力有限，并确信所承诺的权重在此提示上运行，恰好产生这些 token。

保证

证明文件满足以下“完备性”和“可靠性”属性：

如果证明文件是诚实的，则被接受（完备性）。诚实证明者的证明会被验证者接受。
证明文件无法被伪造（可靠性）。要为一个错误陈述生成有效证明实际上是不可能的（即等同于打破广泛认可的密码学假设），因此验证者不必信任证明者。

仅靠一个知道模型权重的计算能力强大的验证者，就能实现完整性和可靠性（在提示上评估模型，并检查结果是否与响应匹配）。接下来的两个特性才使该系统具有非平凡性。

证明文件除陈述本身外不泄露任何信息（零知识）。验证者不会获知任何关于权重、计算的中间值或每一层运行了哪些专家的信息。模型架构（不包括权重）并未被隐藏。
证明文件很小且校验成本低（简洁性）。被证明的计算是在一块 H100 GPU 上运行一个 400B 参数（量化版本约 232 GB）的模型，而验证者收到的证明文件约为 19 MB，在 24 核 CPU 上只需数秒即可校验。审计员或硬件条件远不如提供方的用户，无需访问复杂基础设施即可校验证明文件。

评估

我们在 Llama 4 Maverick（一个 400B 参数的专家混合模型，每个 token 约使用 17B 参数）上测量了该协议的一个实现，使用的是公开可用的 4 位权重。每个验证者请求是一个 1,024 个 token 的窗口，每个证明校验一个 token。证明者在配备单块 H100 和 24 个 CPU 核的服务器上运行，验证者在 CPU 上运行。

证明者。证明者在配备单块 H100 和 24 个 CPU 核的服务器上运行。离线阶段对每个模型运行一次，耗时约 39 分钟。（由于我们在技术报告中讨论的技术原因，生成的承诺大约可用于 1600 万次请求，之后提供方必须重新提交承诺。）在线阶段处理一批 24 个请求时，证明者约需 223 秒，即每秒 110 个 token，每个证明为 18.78 MB。
验证者。验证者在客户端的 CPU 上运行。它不需要 GPU，且只能访问权重的承诺。客户端下载承诺（总共约 6.5 MB），然后每个请求下载一个证明。在 24 个线程上校验一个证明需要 17 秒（单线程为 21 秒），其中包括离线阶段的校验。

与普通推理的比较：我们在八块 H100 上运行了 vLLM（一个广泛使用的推理引擎），使用同一模型的 FP8 版本，发现按每块 GPU 计算，证明一批 24 个请求的耗时约为 vLLM 一次性处理同样 24 个请求耗时的 72 倍（多次运行在 66 到 77 倍之间），而当 vLLM 以我们尝试的最高负载运行时，约为 94 倍。

系统内部。FlashProve 背后的底层机制是一种 zkSNARK，与点对点系统中所部署的类型相同（例如，为以太坊等区块链服务的 L2 网络，如 Starknet 或 Mantle）。我们的 zkSNARK 按照一套成熟的方法构建：一个称为交互式预言机证明（IOP）的底层信息论对象，借助哈希函数被编译为密码学证明（并且还能提供后量子安全性）。我们的 IOP 由最先进的构建模块组装而成，使用了带线性约束的代码邻近性测试和查找论证等工具，这些工具基于编码理论和复杂性理论中的技术。将这些部分组合成一个专为推理定制的 IOP 是一项精细的工作；关于该构造的更多细节可在技术报告中找到。

系统工程

FlashProve 受益于我们所做的架构决策，这些决策在技术报告中有详细讨论。这里我们重点介绍其中几项：

证明者的工作量与实际运行的专家成正比。在 MoE 模型中，一个 token 使用 400B 参数中的约 17B，而证明者每个 token 的工作量与这约 17B 成正比，而非全部参数（证明仍然隐藏了哪些专家被选中）。
请求在事后按批次进行证明。证明者以一次并行遍历读取已完成的文本（如同 prefill），并且每批次只打开一次权重承诺，而非每个请求打开一次。
系统设计为可适配单块 GPU。每一层的模型权重被拆分为多个段，并一次证明一层中的一个段。权重保存在普通内存中并流式载入，因此一块 80 GB 的 GPU，外加约 290 GB 的主机内存，就足够了。

事后证明与在线证明

在将证明机制集成到推理服务器时存在一种选择：在线证明（即在推理的同时进行证明）与事后证明（即在事后对一部分 token 进行证明）。我们的系统采用后者。在线方案预期速度极快，并可能为效率而牺牲安全性，而事后方案允许较慢，且可能不会承受这种权衡。另一方面，事后证明也有局限：重计算带来的额外复杂性、获得关于你的流量的保证的延迟，以及固有的“非确定性”。我们在技术报告中详细阐述了事后证明的动机与影响。

来自形式化验证的可信性

密码学代码以脆弱和易错著称。用户如何信任我们今天发布的代码？

答案是形式化验证：我们使用 Lean 证明助手来规约协议及所需的安全属性。我们以机器可检查且保证正确（在编译器无误的前提下）的形式证明这些属性。我们针对三个顶层属性：

完备性：如果陈述正确，则生成的证明会被验证者接受。
可靠性：任何伪造的证明都会被验证者拒绝（除可忽略的概率外）。
零知识：证明不会泄露关于模型权重的任何信息，超出验证者从响应本身所能推断的范围。⁴

这些性质是在所谓的随机预言机模型中陈述的，这是一种信息论方法，用于分析依赖哈希函数的密码学协议。

形式化验证留下了两个重要的信任缺口。第一，必须审计形式化陈述以确保它们符合其意图。这必须手动完成（尽管这比审计证明要轻松得多）；我们提供了一个交互式可视化工具来协助完成这项工作。

第二，必须审计可执行代码以确保它与已证明安全性质的形式化定义协议相匹配。如何最好地协助这一点取决于具体性质，因为可靠性仅取决于验证者，零知识性仅取决于证明者，而完备性取决于二者的交互。

对于可靠性，我们只需要验证者代码是正确的（拥有“证明”的全部价值在于：如果你信任验证者，你就可以完全不必信任证明者）。我们提供了一个可执行的 Lean 验证者，以及 C++ 验证者。Lean 验证者运行较慢，但 Lean 证明了它只接受我们可靠性定理中的验证者所接受的内容。尽管如此，日常使用中应当使用 C++ 验证者：它不携带任何形式化保证，但在我们测试中的每一个证明上都与 Lean 验证者一致。
对于完备性，威胁模型不假设对抗性攻击（证明者和验证者都是诚实的）。因此，Lean 验证者让我们能够通过标准软件测试来获得信心，确信诚实的证明者会产生可被接受的证明：在正确的陈述上运行证明者，然后在得到的证明上运行 Lean 验证者。
对于零知识性，我们只需要证明者是正确的。然而，与验证者不同，证明者是一个开销高昂的过程，运行 Lean 证明者并不现实。我们在此不提供便利：我们期望任何想要隐藏其所服务模型权重的证明者都拥有足够的资源，以进行仔细的智能体和/或人工安全审计，从而确保与 Lean 证明者等价。

先前工作

实现可证明推理是一系列被通俗地称为“zkML”的工作的目标。早期工作，如SafetyNets（2017）验证了一个两层卷积的 MNIST CNN 和一个小型全连接语音模型，zkCNN（2021）达到了 VGG-16（1500 万参数），每个证明耗时 88.3 秒，而Kang 等人（2022）在全分辨率 ImageNet 上证明了 MobileNet v2。

随后是 Transformer 证明：ZKML 的 GPT-2 对 1.17 亿参数每个 token 约需 159 秒（≈0.006 tok/s），而Modulus Labs 的 15 亿参数 GPT-2 XL 需要超过 90 小时。性能逐步提升：zkLLM（2024）在 GPU 上约 15 分钟内证明了 2,048 token 输入的 LLaMA-2-13B，即每个新 token 约 0.001 tok/s，或批处理中约 2.5 tok/s。2025 年，zkGPT 将 GPT-2 降至 21.8 秒（≈0.05 tok/s），zkPyTorch 在单个 CPU 核心上以每 token 约 150 秒证明了 Llama-3 8B（≈0.007 tok/s），而ZKTorch 在约 20 分钟内证明了 GPT-J（6B）（≈0.001 tok/s）。VerInf 以约 0.02 tok/s 证明了 Llama 4 Maverick（与我们证明的同一个 400B 参数 MoE 模型）。DeepProve 是当前经同行评审的最先进工作，它通过单次前向传播认证整个生成的序列。它在单台机器上对 GPT-2 达到约 2.9 tok/s，对 Gemma 3 达到 1.4 tok/s，分布式下达到 31 tok/s。

最近商业化的努力已经达到了令人瞩目的数字，Attestable 证明 Gemma 4 31B 在单块 H100 上达到 53–77 tok/s；截至撰写本文时，Attestable 尚未发布相应的开源库。

上述数字说明了可证明推理在过去几年中的飞速进展。它们应当更新我们对零知识证明能力的先验认知。

2024 年，zkLLM 在单块 A100 上以约 2.5 tokens/秒证明了 13B 模型。据我们所知，更早的 Llama 4 Maverick 证明系统 VerInf 报告在 DGX Spark 上处理 1,000 个 token 需要 14.3 小时，证明大小为 93.6 GB，验证耗时近一天。
FlashProve 在单块 H100 上以 110 tokens/秒证明同一模型，证明大小为 19 MB，可在数秒内完成验证。Attestable 独立报告了稠密 31B 模型 53–77 tokens/秒的成绩。

我们相信这一进展应当可以迁移到更多模型和架构上，从而产出一个灵活而强大的工具，其相对原生计算的开销约为两个数量级（在我们的测量中约为 70 到 95 倍），远低于此前的预期。

局限性

本次发布是一个研究原型，存在以下技术局限：

对快速可执行代码没有形式化保证。 我们提供了协议的 Lean 实现（包括一个可执行的“慢速”Lean 验证器），以及在 Lean 中证明的安全属性。论文和快速可执行代码均派生自 Lean 协议，但我们不保证三者（Lean、论文、代码）彼此完全一致。
证明针对的是贪心解码下的整数模型。 我们证明的是已发布权重的精确整数版本，证明断言每个被检查的 token 都是该模型的贪心选择。浮点实现或采样解码给出的回复可能在某个位置发生偏离，从而不再与所证明的计算完全一致。通常预期并经实证测试，整数版本在一般情况下与真实浮点推理的误差率很小（即使考虑浮点计算的非确定性也是如此），但这并不覆盖对抗性设计的提示。
架构隐藏。 我们的系统假设所服务的模型采用混合专家（MoE）架构，即每个 transformer 层的前馈块被替换为多个专家子网络和一个路由器，路由器为每个 token 仅激活一小部分专家，我们的系统利用 MoE 结构来提升效率。其他架构（如稠密模型）也被广泛使用，其描述可能包含模型提供方希望保密的知识产权。事实上，也可以设想一个进一步隐藏模型架构的系统：证明方通过隐藏承诺同时承诺权重和架构（即推理的“可执行代码”），验证方的主张则是检查该已承诺的可执行代码在已承诺模型上的执行。
侧信道攻击。 该协议当前的保证是证明本身不会泄露已承诺模型的权重信息。然而，“侧信道攻击”（例如测量生成证明所需的时间）有可能泄露关于权重的信息。我们认为这超出了本次发布的范围。
更长的上下文。该系统目前能对最多 1,024 个 token 的上下文进行推理证明。与聊天场景中累积的上下文相比，这相当短。理想情况下，这一上下文长度可以提升至前沿模型的完整上下文窗口（这些模型的上下文窗口通常有数十万到数百万个 token）。