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 流的攻击者所替换的模型。仅凭模型的输出来判断是不可靠的，即使它产生了高质量的响应。推理的密码学证明（Cryptographic proofs of inference）解决了这个问题：它们允许模型提供商承诺一个模型，然后证明每一个响应都是由该模型生成的。此类证明可以支持从消费级产品到内部安全的各种应用，并可以为验证是否符合 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 参数混合专家模型），在采用 4 位量化权重、预填充阶段使用整数算术的情况下，单张 H100 GPU 生成证明的速度约为 110 Token/秒，每个 1,024 Token 请求的证明大小约为 19 MB。这大约是常见开源库 vLLM 运行模型本身所需 GPU 时间的 70-95 倍。
2. 正如我们在 section 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：篡改检测

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

zkSNARKs 如何提供帮助：提供商可以要求服务器在每次响应时提供一个有效的 zkSNARK。证明绑定到了权重的特定承诺（commitment）上，因此它不仅证明了是*某个*模型产生了响应，还证明了是*承诺的*模型产生了响应。入侵服务器的攻击者或试图替代其他模型的模型，必须为预期的权重生成有效的证明以避免被检测到，而这是它们无法做到的。用户也可以接收这些证明，因为它们不会泄露任何内部信息（由于零知识属性），并且检查成本低廉（由于简洁性）；这限制了攻击者通过推理 API 所能做到的事情。

挑战 3：文本溯源

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

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

例如，在一个漏洞被频频发现的世界里，在发布新代码之前，模型提供商可以向代码开发者提供一份“失败证明”（Proof-of-Failure），证明该模型提供商在特定模型上花费了至少 X 个 Token，但并未达到特定结果（例如，在尝试了至少 100 万个 Token 后，这个特定模型没有在某个特定补丁中发现任何漏洞）。

挑战 4：模型审批

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

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

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

我们的系统：FlashProve

FlashProve 是一个用于大型混合专家（MoE）语言模型可证明推理的系统。更多详情请参阅我们的技术报告；此处我们简要概述该系统。

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

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

评估时，承诺的模型会产生这些输出 Token。

任何持有该承诺、提示词和回复的人都可以对其进行检查，无需权重且计算能力有限，并确信承诺的权重在该提示词上运行会准确产生这些 Token。

保证

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

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

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

证明文件不会泄露陈述之外的任何信息（零知识）。验证者对权重、计算的中间值或每一层运行了哪些专家一无所知。模型架构（不包括权重）并未隐藏。
证明文件很小且验证成本低（简洁性）。被认证的计算是在 H100 GPU 上运行 400B 参数（量化版本约 232 GB）模型的执行过程，而验证者接收的是一个约 19 MB 的证明文件，在 24 核 CPU 上几秒钟即可验证完毕。审计员或硬件配置远不如提供商的用户可以在没有复杂基础设施的情况下检查证明文件。

评估

我们使用公开可用的 4-bit 权重，在 Llama 4 Maverick（一个 400B 参数的混合专家模型，每个 Token 使用约 17B 参数）上对该协议的实现进行了测量。每个验证者请求是一个包含 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 秒），包括离线阶段的检查。

与纯推理的比较：我们运行了 vLLM（一个广泛使用的推理引擎），使用同一模型的 FP8 版本在 8 个 H100 上运行，发现按每个 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 上。每一层的模型权重被分割成多个分段，每次证明一层的一个分段。权重保存在普通内存中并进行流式传输，因此配备约 290 GB 主机内存的单个 80 GB GPU 就足够了。

事后证明与实时证明

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

形式化验证带来的可信度

密码学代码出了名的脆弱且容易出错。用户如何信任我们今天发布的代码？

答案是形式化验证：我们使用 Lean 证明助手来规范协议和所需的安全性属性。我们以机器可检查且保证正确（直到编译器错误）的形式证明了这些属性。我们针对三个顶级属性：

完备性：如果陈述是正确的，则生成的证明会被验证者接受。
可靠性：任何虚假的证明都会被验证者拒绝（概率微乎其微的情况除外）。
零知识：除了验证者从响应本身可以推断的内容之外，证明不会透露关于模型权重的任何信息。⁴

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

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

其次，必须对可执行代码进行审计，以确保其与已证明安全属性的形式化定义协议相匹配。如何最好地协助这一工作取决于属性，因为可靠性仅取决于验证者，零知识仅取决于证明者，而完备性则取决于它们的交互。

对于可靠性，我们只需要验证者代码是正确的（拥有“证明”的全部价值在于，如果你信任验证者，你就可以完全不信任证明者）。除了 C++ 验证者之外，我们还提供了一个可执行的 Lean 验证者。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’s 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 证明 GPT-J（6B）耗时约 20 分钟（≈0.001 tok/s）。VerInf 证明了 Llama 4 Maverick（即我们证明的同一个 400B 参数 MoE 模型），速度约为 0.02 tok/s。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 token/秒的速度证明了一个 13B 模型。据我们所知，此前唯一已知的 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、论文、代码）完全一致。
该证明是关于贪婪解码（greedy decoding）下的整数模型。我们证明的是已发布权重的精确整数版本，证明断言每个被检查的 token 都是该模型的贪婪选择。浮点实现或采样解码的回复可能会在某些位置偏离，从而不再与所证明的计算完全精确匹配。通常预期且经经验测试表明，整数版本在通用情况下与真实浮点推理的误差率在一个很小的范围内（即使考虑了浮点计算的非确定性），但这不包括对抗性设计的提示词。
架构隐藏。我们的系统假设所服务的模型使用混合专家（MoE）架构，其中每个 Transformer 层的前馈模块被多个专家子网络和一个仅为每个 Token 激活一小部分专家的路由器所取代，并且我们的系统利用 MoE 结构来提高效率。其他架构（例如稠密模型）也被广泛使用，其描述可能包含模型提供商希望保密的知识产权。事实上，人们也可以想象一个进一步隐藏模型架构的系统：证明者通过隐藏承诺同时对权重和架构（即用于推理的“可执行代码”）进行承诺，而验证者的声明是关于检查该承诺的可执行文件在承诺模型上的执行情况。
侧信道攻击。该协议当前的保证是，证明本身不会透露关于所承诺模型权重的任何信息。然而，“侧信道攻击”（例如测量生成证明所需的时间）可能会泄露有关权重的信息。我们认为这超出了本次发布的范围。
更长的上下文。该系统目前支持证明长达 1,024 个 Token 的上下文推理。与聊天场景中累积的上下文相比，这相当短。理想情况下，这种上下文长度可以增加到前沿模型的完整上下文窗口（通常具有数十万到数百万个 Token 的上下文窗口）。