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 节奏要求合规性的工具包。

具体而言，我们在一种被称为“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 在 4 位量化权重、预填充阶段使用整数运算的情况下，以约 110 tokens/秒的速度生成证明，每 1,024-token 请求的证明大小约为 19 MB。这大约是在 vLLM（一个常见的开源库）上运行模型本身所需 GPU 时间的 70-95 倍。
2. 正如我们在第 6 节中所讨论的，此前的开源系统要慢上几个数量级。Claude 找到了新颖的方法，将密码学与安全文献中的最先进工具加以应用，同时依托密码学证明系统成熟的设计原则。对模型的承诺以及随后的推理证明会隐藏模型的权重；隐藏模型架构并非本系统的目标。
Claude 擅长优化，但常常做出难以评估的决策，尤其是在大型复杂系统中。我们通过用 Lean（一种形式化验证语言）为所声称的安全保证提供顶层可审计的陈述来应对这一点。

今天我们发布五项成果：

本篇博客文章，概述我们的系统及其潜在应用；
一份技术报告，解释我们系统的细节；
一份（由 Claude 撰写的）协议规范文档；
可执行代码，其中包括：一个证明器和两个验证器——一个用 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，且未达到特定结果（例如，该特定模型在尝试了至少 100 万个 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 成正比，而非全部参数（证明仍然隐藏了哪些专家被选中）。
请求在事后分批进行证明。证明者以一次并行遍历读取已完成的文本（如同预填充），并且每批只打开一次权重承诺，而非每个请求打开一次。
系统设计为可适配单块 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 在 117M 参数下每 token 约需 159 秒（≈0.006 tok/s），而 Modulus Labs 的 1.5B 参数 GPT-2 XL 则需要超过 90 小时。EZKL（2023）证明了一个 1M 参数的 GPT 风格 Transformer，每 token 约需 966 秒（≈0.001 tok/s）。性能逐步提升：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。SASH 的证明器（2026）在单张 H100 上对 Llama 3.1 8B 达到 ≈1.25 tok/s。

最近的商业努力已达到令人瞩目的数字，Attestable 在单张 H100 上以 53–77 tok/s 证明了 Gemma 4 31B；截至撰写本文时，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/秒。

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

局限性

此版本为研究原型，具有以下技术局限性：

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