大语言模型可证明推理的进展

摘要

面对面和朋友说话时，你有很多办法确认对方真的是本人：看得见、听得到、还能握个手。和 AI 模型对话时，这些几乎都没有。今天，用户向模型发起请求，却无法核实回复确实来自开发者声称的那个模型，它可能被路由服务为了省钱偷偷换成了别的模型，甚至可能被攻击者篡改了 token 流。只看模型输出并不可靠，哪怕输出质量很高。推理的密码学证明可以解决这个问题：模型提供方先对某个模型作出承诺，然后证明每一条回复都由该模型生成。这类证明可支撑从消费级产品到内部安全的各类应用，也能为验证 AI 发展节奏（pacing）合规性的工具出一份力。

具体来说，我们在一种被称为 zkSNARK 的密码学证明上取得了进展。由于它具备很强的隐藏性和效率，特别适合可证明推理。本文分享其中部分进展，主要围绕我们称为 FlashProve 的系统。技术要点简述如下：

1. Claude 在面向推理的 zkSNARK 上做出了改进，所构建的系统比此前的开源系统快得多。以一个大模型为例（Llama 4 Maverick，400B 参数的混合专家模型），在 4-bit 量化权重、prefill 阶段使用整数运算的条件下，单张 H100 GPU 的证明生成速度约为 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 模型发送请求时，目前无法确知自己选定的模型就是生成该响应的那个模型。日常使用中，用户大多只关心输出，未必在意具体是哪个模型生成的，这个问题不算紧迫。但在若干场景下，这种保证很有用。例如，在模型发布前后对其进行测试的独立评估者，需要知道自己评估的模型就是实际提供服务的模型。通过第三方路由服务调用模型的客户，希望得到保证：这些 token 来自他们付费的那个模型。而如果网络攻击者篡改了 token 流并冒充某个模型，用户仅凭输出根本无从察觉。

然而，实现模型响应的验证并不容易。大多数前沿模型的权重是保密的；即便用户能拿到权重，要核查某个响应确实由持有这些权重的模型生成，也得把模型跑一遍，而这所需的算力远超普通用户（甚至评估者）所能承担。

可证明推理（provable inference，PI）的目标，是让算力有限、且对模型权重一无所知的用户，也能验证某个回答确实来自所请求的模型。推动 PI 的动机有两个：一是提升客户对 AI 提供商的信任；二是它能为独立评估者提供保证，也让提供商得以证明自己履行了某些承诺和法律义务，因此 PI 还关系到 AI 前沿发展的节奏把控与 AI 监管。

实现 PI 的一条路径，是借助一种称为零知识简洁论证的密码学对象：模型提供商在给出声称的回答的同时，附上一份简短的证明（比如几 MB），用户能够快速验证它（理想情况下，在 CPU 上几秒内完成）。如果声称的回答并非出自指定的模型，用户的校验就会失败。关键在于，密码学技术保证这份证明不会泄露模型权重的任何信息。

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

本次发布包含可执行代码、Lean 形式化，以及协议的技术说明。我们的目标有两个：(i) 加速并推动可证明推理的发展；(ii) 证明零知识简洁论证用于可证明推理是切实可行的。

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

AI 普及中的信任挑战

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

PI 的工具包括硬件方案、软件方案，或两者结合。这里我们只讨论软件方案：一种名为“zkSNARK”（零知识简洁知识论证）的密码学工具。通俗地说，zkSNARK 是一套系统，让证明者通过一份简短的“证书”说服验证者某项计算被正确执行；关键在于，这份证书是零知识的，除了计算正确性本身所隐含的信息外不泄露任何其他信息，同时它是简洁的，验证起来比被证明的计算快指数级。

下面我们列出几个挑战，以及 zkSNARK 如何帮助应对它们。

挑战 1：节奏控制

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

zkSNARK 如何帮忙： 监管者可以要求提供商提交覆盖某段时间内所服务推理请求的证书。证书必须表明这些请求是由所声称的模型生成的。恶意提供商无法满足这一要求，除非其硬件确实在服务正确的模型。借助 zkSNARK，监管者无需搭建提供商可能拥有的复杂硬件环境，就能验证提供商的说法是否成立；同时提供商也得到保证，监管者不会获知专有的模型信息。² 我们注意到，这虽然验证了硬件正在服务推理，但并不能证明硬件没有在做别的事，比如偷偷训练。

挑战 2：篡改检测

AI 模型越有价值，运行它们的服务器就越容易成为首要攻击目标。攻击者或失控的 agent 可能攻陷一台推理服务器，窃取权重、向用户返回恶意响应（比如向用户电脑投递恶意软件），等等，而且全程混在真实响应之中。对手未必来自外部。随着模型有能力改进并部署自身，一个更先进的模型可能顶替被授权运行的那个模型，把自己伪装成较弱的模型，以避开本应针对它的分类器和监控。两种情况下的问题是一样的：公司如何确定服务器上实际运行的究竟是哪一份权重？在我们的 Frontier Safety Roadmap 中，Anthropic 定下了一个公开目标，要为推理流量验证做出原型：“我们将在 2026 年 9 月 30 日前开发出可证明推理的原型，这是一种可靠、可证明地给 AI 模型输出‘签名’的技术，使输出可以归因到某一组特定的模型权重。”如我们在 RSP 更新中所述，我们通过一个独立但相关的项目达成了该目标：对推理流量签名，并在可信服务器上重新计算推理；本文的工作则用另一种方法追求同一个目标。³

zkSNARK 能帮上什么忙： 服务方可以要求服务器为每次响应附上一个有效的 zkSNARK。该证明绑定到对权重的某个特定承诺，因此它证明的不只是响应出自某个模型，而是出自所承诺的那个模型。攻击者若攻陷了服务器，或某个模型想冒充另一个模型，就必须针对预期权重给出有效证明才能不被发现，而他们做不到。用户同样可以拿到这些证明：零知识保证证明不泄露任何内部信息，简洁性保证验证开销很低。这就限制了攻击者通过推理 API 所能达到的目的。

挑战 3：文本溯源

人们可能想证明自己确实在理解、分析某件事上投入了大量精力。比如，开发者声称自己的软件库已被某个前沿网络安全模型扫描过漏洞，或者公司声称自己的商业计划得到了某个合适模型的认可。用户怎么核实这些说法？用户可能没有运行该模型所需的资源，也可能没有相应的权限。即便公开聊天记录也提供不了绝对保证：开发者理论上可以伪造记录，用的不是前沿模型，而是更便宜的模型或降级版本。总的来说，用户如何确认自己用的就是自己选定的那个模型？

zkSNARK 能帮上什么忙： 服务方可以在每条响应后附上一个 zkSNARK，证明该输出是所称模型在给定输入上产生的。简洁性让用户无需专用硬件就能快速验证这份证书，零知识则让服务方放心：用户不会得知任何专有权重的信息。这与现有的机制互补，后者用于验证某条响应出自哪个模型。

举例来说，在漏洞被频繁发现的环境里，模型提供方可以在发布新代码之前，向代码开发者出具一份失败证明（Proof-of-Failure）：证明自己在某个特定模型上至少花费了 X 个 token，且没有取得特定结果，例如，在至少尝试 100 万 token 之后，该模型仍未在某个特定补丁中发现任何 bug。

挑战 4：模型审批

监管机构可能要求服务商只提供经批准安全的模型，而不是被认定存在网络安全或安全风险的模型。服务商可能有动机绕过这一要求，因为高风险模型可能表现优于竞争对手，或者服务成本更低。监管机构如何确保只提供经批准的模型？

zkSNARKs 能帮上什么忙： 监管机构可以要求服务商在响应中附带 zkSNARK，强制其使用经批准的模型。证明会将每次请求与所用模型绑定，因此如果服务商使用了未经批准的模型，证明就无法通过验证。得益于简洁性，监管机构可以轻量地完成检查，无需重新执行每一次请求。

关于可信硬件与 PI 的一点说明。 以往的工作常常依赖可信执行环境来实现 PI。这类基于硬件的方案提供隐私与远程认证，但前提是制造商能生产出防篡改的硬件。本研究聚焦于纯软件的密码学方案，其安全性与隐私性依赖于计算问题的困难性。即使所处环境已被攻破（硬件、操作系统等），攻击者也无法在不破解计算上不可行的问题的前提下伪造出有效证明。可信硬件与密码学是互补的两种路径，提供的保证与权衡各不相同。在应对上述信任挑战时，两者都将发挥作用。

我们的系统：FlashProve

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

FlashProve 涉及两方：模型服务商（证明者）和用户（验证者）。系统分为两个阶段：

• 在离线阶段，证明者发布对模型权重的承诺，即一个简短的指纹，用来锁定某一组确切的权重，而权重本身保持隐藏。后续的推理声明都将对照该承诺进行检查，即本阶段所承诺的权重模型。
• 在在线阶段，收到验证者的请求（即提示词及对应的输出 token）后，证明者生成一个证明文件，证明以下命题：

承诺模型在评估时产生的输出 token。

任何持有承诺、prompt 和回复的人，不需要模型权重，用有限的算力就能验证它，并确信承诺的权重在这个 prompt 上运行，恰好产生这些 token。

保证

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

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

仅靠一个知道模型权重的强大验证者就能实现完备性和可靠性（在 prompt 上运行模型，检查结果是否与回复一致）。下面两条性质才让这套系统真正有价值。

• 证明文件不泄露陈述之外的任何信息（零知识）。 验证者对权重、计算的中间值，以及每一层跑了哪些专家一无所知。模型架构（不含权重）不做隐藏。
• 证明文件很小，验证成本低（简洁性）。 被证明的计算是 400B 参数模型（量化版本约 232 GB）在单张 H100 GPU 上的一次运行，而验证者收到的证明文件约 19 MB，在 24 核 CPU 上几秒即可验证完毕。审计方或硬件远不如服务提供方的用户，无需复杂基础设施就能验证证明文件。

评估

我们在 Llama 4 Maverick（400B 参数的混合专家模型，每个 token 约使用 17B 参数）上用公开的 4-bit 权重实现并测量了该协议。每次验证请求是一个 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 在八张 H100 上运行同一模型的 FP8 版本，结果发现，按单张 GPU 计算，证明一批 24 个请求的耗时约为 vLLM 一次性处理同样 24 个请求的 72 倍（多次运行在 66 到 77 倍之间），而在我们尝试过的最高负载下，这一倍数约为 94 倍。

系统内部。 FlashProve 背后的底层机制是一种 zkSNARK，与点对点系统中部署的那类相同（例如为 Ethereum 等区块链服务的 Starknet、Mantle 等 L2 网络）。我们的 zkSNARK 按照一套成熟的方案构建：先有一个称为交互式预言机证明（IOP）的信息论对象，再借助哈希函数将其编译为密码学证明（因此还具备后量子安全性）。我们的 IOP 由最先进的构件组装而成，用到了带线性约束的码接近性测试和查找论证等工具，它们基于编码理论和复杂性理论中的技术。把这些部件组合成为推理量身定制的 IOP 是一项精细的工作；关于构造的更多细节见技术报告。

系统设计

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

• prover 的工作量与真正参与计算的专家成正比。在 MoE 模型中，一个 token 只用到 400B 参数中的约 17B，因此 prover 处理每个 token 的工作量正比于这约 17B 参数，而非全部参数（证明本身仍然不会暴露选用了哪些专家）。
• 请求在事后按批次进行证明。prover 以一次并行遍历读取已生成的文本（与 prefill 相同），并且每批只打开一次权重承诺，而不是每个请求打开一次。
• 系统按单卡 GPU 设计。每一层的模型权重被切分为若干段，每次只证明一段层。权重存放在普通内存中并按需流式载入，因此一块 80 GB 的 GPU 加上旁边约 290 GB 的主机内存就足够了。

事后证明与在线证明

把证明机制集成进推理服务器时有一个选择：在线证明（即在推理的同时进行证明）还是事后证明（即在事后对一部分 token 进行证明）。我们的系统采用后者。在线方案要求极快的速度，可能为了效率牺牲安全性；事后方案则允许更慢，不必做这种取舍。另一方面，事后证明也有局限：重算带来的额外复杂度、拿到流量保证的延迟，以及固有的“非确定性”。关于事后证明的动机与影响，我们在技术报告中进一步展开。

形式化验证带来的可信性

密码学代码出了名地脆弱、容易出错。用户凭什么信任我们今天发布的代码？

答案是形式化验证：我们用 Lean 证明助手来刻画协议以及期望的安全性质。我们以机器可检验、且保证正确（在编译器无误的前提下）的形式证明这些性质。我们针对三条顶层性质：

1. 完备性：若陈述为真，生成的证明将被验证器接受。
2. 可靠性：任何伪造的证明都会被验证器拒绝（概率可忽略的情形除外）。
3. 零知识：证明不会泄露模型权重的任何信息，验证器仅凭响应本身所能推断的内容除外。⁴

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

形式化验证留下两个重要的信任缺口。第一，必须审计形式化陈述，确保其与意图相符。这只能人工完成（不过比审计证明轻松得多）；我们提供了一个交互式可视化工具来辅助完成。

第二，必须审计可执行代码，确保其与证明安全性质时所依据的形式化定义协议一致。如何最好地辅助这一审计取决于具体性质，因为可靠性只取决于验证器，零知识只取决于证明者，而完备性取决于两者的交互。

• 对于可靠性，我们只需验证器代码正确（“证明”的全部价值就在于此：只要信任验证器，就可以完全不信任证明者）。我们提供了一个可执行的 Lean 验证器，与 C++ 验证器并存。Lean 验证器运行较慢，但 Lean 已证明它只接受我们可靠性定理中验证器所接受的内容。不过，日常使用仍推荐 C++ 验证器：它不附带任何形式化保证，但在我们测试的每一个证明上都与 Lean 验证器一致。
• 对于完备性，威胁模型不假设对抗性攻击（证明者和验证者都是诚实的）。因此，Lean 验证器让我们可以通过标准软件测试来获得信心，确认诚实的证明者会生成被接受的证明：对正确的陈述运行证明者，再对生成的证明运行 Lean 验证器。
• 对于零知识，我们只需证明者正确。但与验证器不同，证明者是一个开销很大的过程，运行 Lean 证明者并不现实。我们在此不提供辅助：我们认为，任何想要隐藏其所服务模型权重的证明者，都应当有足够的资源进行细致的智能体和/或人工安全审计，以确保与 Lean 证明者等价。

先前工作

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

随后是 Transformer 的证明：ZKML 的 GPT-2 对 1.17 亿参数每 token 约需 159 秒（≈0.006 tok/s），Modulus Labs 的 15 亿参数 GPT-2 XL 则需要 90 多小时。EZKL（2023）证明一个 100 万参数的 GPT 风格 transformer，每 token 约 966 秒（≈0.001 tok/s）。性能逐步提升：zkLLM（2024）在 GPU 上对 2048 token 输入的 LLaMA-2-13B 完成证明约需 15 分钟，即每个新 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 的 prover（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 上 1000 个 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 层的前馈块被替换为多个专家子网络和一个 router，router 为每个 token 只激活一小部分专家；我们的系统利用 MoE 结构来获得效率提升。其他架构（例如稠密模型）同样被广泛使用，其描述可能包含模型提供方希望保密的知识产权。事实上，也可以设想一个进一步隐藏模型架构的系统：证明方通过隐藏承诺同时承诺权重和架构（即推理的“可执行代码”），验证方的主张则是检查该已承诺的可执行代码在已承诺模型上的执行。
• 侧信道攻击。 协议目前的保证是：证明本身不泄露已承诺模型的权重信息。然而，所谓“侧信道攻击”，比如测量生成证明所需的时间，有可能泄露关于权重的信息。本次发布不覆盖这一问题。
• 更长的上下文。 系统目前能证明最长 1,024 个 token 的上下文上的推理。与聊天场景中累积的上下文相比，这相当短。理想情况下，上下文长度应能提升到前沿模型的完整上下文窗口（这类窗口通常有数十万到数百万个 token）。

Footnotes

1. 在我们的开源研究中，使用的是 Meta 的 Llama 4 Maverick（400B 参数），采用第三方在 Hugging Face 上公开的 4-bit 转换版本。本次发布不包含权重：读者需自行从 Hugging Face 下载，并遵守 Meta 的 Llama 4 许可证。本次发布中，我们公开由该模型计算得出的一些小体积内容，例如承诺 ID、校验和、性能数据以及部分参数设置（完整清单见 THIRD_PARTY.md）。我们鼓励读者自行验证我们的结果，也鼓励将这项工作适配到其他模型。跑通完整示例需要一台大型 GPU 机器，以及访问 Meta tokenizer 的权限。 ↩

2. 具体隐藏哪些信息取决于系统设计。在我们的工作中，权重是隐藏的，架构则不是。在后续工作中，我们计划连架构细节也一并隐藏。（原则上可以隐藏模型的全部细节，问题在于能以多高的效率做到。） ↩

3. 在 2026 年 10 月 19 日的更新中，我们还更改了目标名称：现在使用“推理验证”（inference verification），而不再用“可证明推理”（provable inference）。我们最初的目标是让 token 流的完整性获得高度保证，而这可以通过多种方式实现；“可证明推理”暗示的路径比我们认为必要的更窄。与该原型分开推进的，是我们在推理的密码学证明上的工作，它正是为 token 流提供高度保证的方式之一。 ↩

4. 模型的架构并未隐藏。进一步隐藏架构细节留待后续工作。 ↩