Anthropic 发布可验证推理系统 FlashProve，单张 H100 上约 110 tokens/秒生成证明

罗伊·林伯格 (Anthropic), 亚历克斯·阿莱恩 (Anthropic); 亚历山德罗·奇亚西 (EPFL, StarkWare), 米兰达·克里斯蒂 (MIT, RESI), 拉胡尔·达拉尔 (Anthropic STEM 奖学金计划, Succinct), 吉亚科莫·费尔齐 (EPFL), 本·迈耶 (Anthropic 奖学金计划, MIT), 盖伊·魏森伯格 (EPFL)

执行摘要

当你和朋友的面对面交谈时，你有许多方法可以知道真的是他们：你可以看到他们，听到他们，和他们的手握手。当你和 AI 模型交谈时，你几乎没有任何方法。今天，查询模型的用户无法检查响应是否来自开发者声称正在响应的特定模型，而是由路由服务出于成本原因秘密替换的模型，甚至是由篡改了令牌流的攻击者。仅根据模型的输出进行判断是不可靠的，即使它产生了高质量的响应。密码学推理证明可以解决这个问题：它们允许模型提供者承诺一个模型，然后证明每个响应都是由该模型产生的。这样的证明可以支持从消费产品到内部安全等各种应用，并可以为验证符合 AI 节奏要求提供工具包。

具体来说，我们在一种强大的密码学证明类型“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 个令牌/秒的速度生成证明，每个 1024 令牌请求的证明大小约为 19 MB，当使用 4 位量化权重并在预填充中使用整数运算时。这是在 vLLM（一个常见的开源库）上运行模型本身的 GPU 时间的 70-95 倍。
2. 之前的开源系统慢几个数量级，正如我们在第 6 节中讨论的那样。Claude 找到了应用密码学和安全性文献中的最先进工具的新方法，同时依赖于成熟的密码学证明系统设计原则。对模型的承诺以及随后的推理证明隐藏了模型的权重；隐藏模型的架构不是该系统的目标。
Claude 擅长优化，但经常做出难以评估的决定，尤其是在大型复杂系统中。我们通过提供 Lean（一种形式化验证语言）中的顶级可审计声明来对抗这一点，以支持所声称的安全保证。

今天我们发布了五个工件：

当前的博客文章，概述了我们的系统和其潜在应用；
一个技术报告，解释了我们系统的细节；
一个协议描述；
可执行代码，包括：一个证明器和两个验证器，一个快速验证器（C++），和一个可证明正确的验证器（Lean）；以及
Lean 证明，用于顶级数学声明，以及一个 Lean 定理的交互式可视化器，以帮助进行审计。

我们在 Apache 2.0 许可下发布我们的代码、Lean 证明和文档。¹ 这篇研究文章旨在分享中间进展，而不是一个完整的研究议程。我们明确地分享这个，目的是让其他人看看我们已经做了什么，拿走它并加以改进。

引言

当用户向AI模型发送请求时，如今他们没有办法确切知道他们选择的模型是生成响应的那个模型。在日常使用中，用户主要关心输出结果，而不一定关心具体是哪个模型产生了它，因此这并不是一个紧迫的问题。但是，在几种情况下，这种保证会很有用。例如，在发布前后测试AI模型的独立评估者需要知道他们正在评估的模型就是正在服务的模型。通过第三方路由服务使用模型的客户希望确保他们支付的模型产生了这些标记。如果一个网络攻击者在假装成为某个模型时修改了标记流，用户仅从输出中无法检测到这一点。

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

可证明推理（PI）的目标是使具有有限计算资源且没有任何关于权重的信息，用户能够验证响应来自请求的模型。PI的动机既在于增加客户对AI提供者的信任，也因为它可以用来向独立评估者提供保证，并允许提供者证明他们正在满足某些承诺和法律义务，因此它也对控制AI发展的前沿和AI监管有影响。

实现PI的一种方法是通过一个称为零知识简洁论证的密码学对象：模型提供者除了声称的响应外，还会发送一个短的证明（例如，几兆字节），用户可以快速验证（理想情况下，在CPU上几秒钟）。如果声称的响应偏离了指定的模型，用户的检查将失败。重要的是，密码学技术确保证明不会透露任何关于模型权重的信息。

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

发布包含可执行代码、Lean形式化以及协议的技术描述。我们的目标是双重的：(i) 加速和促进可证明推理的开发；(ii) 证明零知识简洁论证对于可证明推理是实用的。

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

AI普及中的信任挑战

人工智能的发展及其在我们数字基础设施和经济中的日益增长的作用引发了信任挑战，人工智能提供者必须回答这些问题。通过依赖 可证明推理 (PI) 的工具来解决这些和其他挑战。

PI 工具包括硬件方法、软件方法或两者的组合。在这里，我们专注于仅使用软件的方法：一种称为“zkSNARK”（零知识简洁知识论证）的加密工具。非正式地说，zkSNARK 是一个系统，允许一个 证明者 通过一个简短的“证书”，向一个 验证者 证明给定的计算被执行正确；关键在于，证书是 零知识 的，因为它不会透露除计算的正确性所隐含的信息之外的其他信息，并且是简洁的，因为它与已证明的计算相比，验证速度要快得多。

下面我们概述几个挑战以及 zkSNARK 如何帮助解决这些挑战。

挑战 1：节奏

Some proposals to regulate and pace AI development rely on monitoring hardware and how it is used. For example, a provider might be required to devote its hardware to inference rather than to training a powerful new model. The provider might try to cheat by serving cheaper models or using compute in an unexpected way, freeing up resources for training. How can a regulator reliably ensure that the hardware is used for inference?

zkSNARK 如何提供帮助：监管者可以向提供者索要涵盖在给定时期内处理的推理请求的证书。证书必须表明这些请求是由所声称的模型生成的。一个恶意的提供者如果不能满足此请求，除非其硬件确实在为正确的模型提供服务。使用 zkSNARK，监管者可以在不需要提供者可能拥有的复杂的硬件设置的情况下验证提供者的声明是否有效，同时提供者也有保证，即监管者不会学到专有的模型信息。² 我们注意到，尽管这验证了硬件正在提供推理，但它并没有证明硬件没有，例如，在旁边进行训练。

挑战 2：篡改检测

随着 AI 模型的价值日益增长，运行它们的服务器成为首要目标。攻击者或恶意代理可能攻陷推理服务器以窃取权重、向用户发送恶意响应（例如向用户的计算机传递恶意软件），等等，而这一切都混迹于真实响应之中。对手不必是外部的。随着模型能够自我改进和部署，一个更高级的模型可能会取代被授权的模型，并伪装成较弱的模型，以避免分类器和监控措施。在两种情况下，问题都是一样的：公司如何才能确保 哪些权重 实际上在其服务器上运行？在我们的前沿安全路线图中，Anthropic 设定了一个公开目标，即开发一个验证推理流量的原型：“我们将在 2026 年 9 月 30 日前开发一个可验证推理的原型，这是一种可靠地、可证明地‘签名’ AI 模型输出的技术，使其可归因于特定的模型权重集。” 如我们在 RSP 更新中所述，我们通过一个单独但相关的项目达成了这一目标，该项目对推理流量进行签名并在可信服务器上重新计算推理；本文中的工作通过不同的方法追求相同的目标。³

zkSNARKs 如何提供帮助： 提供者可以要求服务器在每次响应时提供一个有效的 zkSNARK。一个证明与对权重的特定承诺绑定，因此它不仅证明某个模型生成了响应，而且证明 承诺的 模型确实如此。攻击者如果攻陷了服务器，或者一个模型取代了另一个模型，就必须为预期的权重生成有效的证明以避免被检测，而他们无法做到这一点。用户也可以收到这些证明，因为它们不泄露任何内部信息（通过零知识）并且检查起来很便宜（通过简洁性）；这限制了攻击者可以通过推理 API 完成的操作。

挑战 3：文本溯源

人们可能希望证明在理解/分析某事物上付出了相当大的努力。例如，开发者可能声称他们的软件库已被前沿网络安全模型扫描漏洞，或者公司可能声称其商业计划已获得适当模型的批准。用户如何验证这些说法？用户可能没有运行模型的资源（或者他们可能没有权限这样做）。即使发布聊天记录也无法提供绝对保证；理论上，开发者可能会伪造它们，不是用前沿模型，而是用一个更便宜的模型或一个降级版本生成。总的来说，用户如何验证他们正在使用他们选择的模型？

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

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

挑战 4：模型批准

法规可能要求提供者仅提供被批准为安全的模型，而不是被认为存在网络安全或安全风险的模型。由于有风险的模型可能会超越竞争对手或提供成本更低，因此提供者可能有动机规避这一规定。监管机构如何确保仅提供已批准的模型？

zkSNARKs 如何提供帮助： 监管机构可以要求提供者在其响应中附加一个 zkSNARK，强制使用已批准的模型。该证明将每个请求绑定到所使用的模型，因此它不会验证提供者是否在使用未批准的模型。监管机构可以轻量级地检查这一点，这要归功于简洁性，而无需重新执行每个请求。

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

我们的系统：FlashProve

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

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

在 离线阶段，证明者发布对模型权重的承诺，这是一个短的指纹，用于锁定一个确切的权重选择，而权重本身仍然隐藏。稍后的推理声明将与此承诺进行核对，即在此阶段承诺的权重模型。
在 在线阶段，在验证者（即提示和相应的输出代币）的请求下，证明者生成一个证明文件，证明以下陈述：

已承诺的模型在评估时会产生这些输出代币。

持有承诺、提示和回复的任何人都可以检查它，无需权重且计算能力有限，并确信已承诺的权重，在对此提示运行时，确实产生了这些代币。

保证

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

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

完备性和可靠性单独可以通过一个知道模型权重的计算能力强大的验证者来实现（在提示上评估模型并检查结果是否与响应匹配）。接下来的两个属性是使系统非平凡的原因。

证明文件不会透露超出陈述的信息（零知识）。 验证者关于权重、计算的中值或每一层运行了哪些专家什么也学不到。不包括权重在内的模型架构不会被隐藏。
证明文件体积小且检查成本低（简洁性）。 证明的计算是一个在H100 GPU上运行的400B参数（量化版本约为232 GB）模型，而验证者收到的证明文件约为19 MB，在24核CPU上只需几秒钟即可检查。审计员或硬件远少于提供者的用户可以在不访问复杂基础设施的情况下检查证明文件。

评估

我们在Llama 4 Maverick（一个400B参数的专家混合模型，每个标记使用约17B参数）上测量了协议的实现（使用公开可用的4位权重）。每个验证器请求是1024个标记的窗口，每个证明检查一个标记。证明者在具有单个H100和24个CPU核心的服务器上运行，验证者在CPU上运行。

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

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

系统内部。 FlashProve 的底层机制是一种在点对点系统中部署的 zkSNARK（例如，L2 网络，如 Starknet 或 Mantle 用于以太坊等区块链）。我们的 zkSNARK 是根据一个成熟的配方构建的：一个称为 交互式预言机证明（IOP）的底层信息论对象通过依赖哈希函数编译成一个密码学证明（并提供后量子安全性）。我们的 IOP 是使用诸如 带线性约束的代码邻近性测试 和 查找论证 等工具，从最先进的构建块中组装而成，这些工具基于编码理论和复杂性理论的技术。将这些部分组合成一个用于推理的自定义 IOP 是一项微妙的工作；有关构造的更多细节可以在技术报告中找到。

系统设计

FlashProve 体现了我们做出的架构决策所带来的好处，这些决策在技术报告中有详细讨论。这里我们重点介绍几点：

证明者的工作与实际运行的专家成正比。在一个 MoE 模型中，一个 token 使用 ~17B 的 400B 参数，并且证明者每 token 的工作量与这些 ~17B 成正比，而不是所有参数（证明仍然隐藏了哪些专家被选择了）。
请求按批次证明，事后进行。证明者在一个并行遍历中读取完成的文本（如在预填充中），并且每批而不是每请求一次打开对权重的承诺。
系统设计为适合单个 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) 达到了 88.3 秒每个证明的 VGG-16 (1500 万参数)，以及 Kang et al. (2022) 在完整分辨率的 ImageNet 上证明了 MobileNet v2。

Transformer 证明随后出现：ZKML’s GPT-2 每个标记大约需要 159 秒，参数为 1.17 亿（≈0.006 tok/s），而 Modulus Labs’ 15 亿参数的 GPT-2 XL 需要 90 多小时。性能逐步提高：zkLLM (2024) 在 GPU 上以大约 15 分钟在 2048 个标记的输入上证明了 LLaMA-2-13B，这是 ≈0.001 tok/s 每个新标记，或 ~2.5 tok/s 批量。到 2025 年，zkGPT 将 GPT-2 减少到 21.8 秒 (≈0.05 tok/s)，zkPyTorch 在一个 CPU 核心上以大约 150 秒每个标记证明了 Llama-3 8B (≈0.007 tok/s)，而 ZKTorch 在大约 20 分钟内证明了 GPT-J (60 亿) (≈0.001 tok/s)。 VerInf 以 ≈0.02 tok/s 证明了 Llama 4 Maverick（我们证明的相同 400 亿参数的 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 上证明了 13B 模型大约以 2.5 个 token/秒的速度。我们所知道的关于 Llama 4 Maverick 的唯一早期证明 VerInf，报告在 DGX Spark 上对 1,000 个 token 需要 14.3 小时，证明大小为 93.6 GB，验证几乎需要一天。
FlashProve 在单个 H100 上证明同一模型达到 110 个 token/秒，证明大小为 19 MB，可以在几秒钟内验证。Attestable 独立报告密集的 31B 模型达到 53–77 个 token/秒。

我们相信，这种进展应该会转移到更多的模型和架构上，产生一个灵活而强大的工具，其开销比原生计算大约高 2 个数量级（在我们的测量中大约为 70 到 95 倍），远低于之前的预期。

限制

这次发布是一个研究原型，并且有以下技术限制：

没有对快速可执行代码的正式保证。 我们提供了一个 Lean 协议的实现（包括一个可执行的“慢”Lean 验证器），以及 Lean 中证明的安全属性。论文和快速可执行代码是从 Lean 协议派生的，但我们不保证 Lean、论文和代码三者完全一致。
证明是关于贪婪解码下的整数模型。 我们证明了一个精确的整数版本的已发布权重，并且一个证明断言每个检查的 token 是该模型的贪婪选择。浮点实现或采样解码的回复可能在某个位置偏离，并且不再与所证明的计算完全匹配。整数版本通常预期并且在经验上测试为在真实浮点推理中具有一些小的误差率（即使考虑到浮点计算的不可确定性），尽管这并不涵盖对抗性设计的提示。
架构隐藏。 我们的系统假设所服务的模型使用混合专家（MoE）架构，其中每个 Transformer 层的前馈块被多个专家子网络和一个 路由器 替换，该路由器仅为每个 token 激活一小部分专家，我们的系统使用 MoE 结构以获得效率提升。其他架构，如密集模型，也被广泛使用，并且其描述可能包含模型提供者希望保持机密的知识产权。实际上，也可以想象一个进一步隐藏模型架构的系统：证明者通过隐藏承诺提交权重和架构（即推理的“可执行代码”），验证者的声明是关于检查在承诺模型上执行的该已提交可执行代码。
侧信道攻击。 当前协议的保证是证明本身不会透露关于已提交模型权重的任何信息。然而，“侧信道攻击”，例如测量生成证明所需的时间，可能会潜在地揭示有关权重的信息。我们将此视为本次发布的范围之外。
更长的上下文。 当前系统证明推理的上下文最长为 1,024 个 token。与聊天设置中累积的上下文相比，这相当短。理想情况下，这个上下文长度可以增加到前沿模型的完整上下文窗口（这些模型通常具有 10 万到数百万个 token 的上下文窗口）。