第 01 章：执行摘要
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 在用于推理的 zkSNARK 上取得了改进，构建出一个比以往开源系统快得多的系统。
- 对于一个大模型（Llama 4 Maverick，400B 参数的专家混合模型），在 4 比特量化权重、预填充阶段使用整数运算的情况下，单块 H100 GPU 生成证明的速度约为 110 tokens/秒，每 1,024-token 请求的证明大小约为 19 MB。这大约是在 vLLM（一个常用开源库）上运行模型本身所需 GPU 时间的 70-95 倍。
- 以往的开源系统要慢几个数量级，我们在第 6 节中对此进行了讨论。Claude 找到了新颖的方式来应用密码学与安全文献中最先进的工具，同时依赖密码学证明系统成熟的设计原则。对模型的承诺以及随后的推理证明会隐藏模型权重；隐藏模型架构并不是本系统的目标。
- Claude 擅长优化，但常常做出难以评估的决策，尤其是在大型复杂系统中。为应对这一点，我们针对所声称的安全保证，在 Lean（一种形式化验证语言）中提供了顶层可审计的陈述。
今天我们发布五项成果：
- 当前这篇博客文章，概述我们的系统及其潜在应用；
- 一份技术报告，详细解释我们系统的细节；
- 一份（由 Claude 撰写的）协议规范文档；
- 可执行代码，其中包括：一个证明器和两个验证器——一个用 C++ 编写的快速验证器，以及一个用 Lean 编写的可证明正确的验证器；以及
- 针对顶层数学陈述的 Lean 证明，以及一个用于辅助审计的 Lean 定理交互式可视化工具。
我们以 Apache 2.0 许可证发布代码、Lean 证明和文档。这篇研究文章旨在分享阶段性进展，而不是一份已完成的研究议程。我们之所以明确分享这些内容，是希望其他人查看我们所做的工作，将其采纳并加以改进。
引言
当用户向 AI 模型发送请求时，如今他们无法确定自己所选定的模型就是实际生成响应的那个模型。对于日常使用而言，用户通常更关心输出结果，而不一定在意是哪个具体模型产生了结果，因此这一问题并不算紧迫。但在若干场景中，这种保证会很有用。例如，在模型发布前后对其进行测试的独立评估者需要知道，他们正在评估的模型就是实际提供服务的模型。通过第三方路由服务使用模型的客户希望得到保证：他们获得的 token 来自他们付费购买的那个模型。而如果网络攻击者冒充某个给定模型并篡改 token 流，用户仅凭输出根本无法察觉。
然而，实现模型响应的可验证性颇具挑战。大多数前沿模型的权重是保密的，而且即便用户能够访问权重，要检查某个给定响应是否由拥有这些权重的模型产生，也需要运行该模型，而这所需的计算资源远远超出一个典型用户（甚至评估者）所能承受的范围。
可证明推理（provable inference，PI）的目标是：让计算资源有限、且对权重一无所知的用户，能够验证某个响应确实来自所请求的模型。PI 的动机既包括提升客户对 AI 提供商的信任，也因为它可以为独立评估者提供保证，并让提供商能够证明自己正在履行某些承诺和法律义务——因此它也对把控 AI 发展前沿以及 AI 监管具有意义。
实现 PI 的一种方式是通过一种名为零知识简洁论证（zero-knowledge succinct argument）的密码学对象：模型提供商在发送所声称的响应时，同时附带一个简短的证明（比如几兆字节），用户能够快速验证该证明（理想情况下，在 CPU 上几秒内完成）。如果所声称的响应偏离了指定模型，用户的检查就会失败。重要的是，密码学技术确保该证明不会泄露任何关于模型权重的信息。
今天，我们发布 FlashProve：一个开源的高性能可证明推理原型。对于一个 400B 参数的混合专家模型（Llama 4 Maverick，4 比特量化），我们展示：单块 H100 GPU 生成证明的速度超过 100 tokens/秒，每 1,024 token 请求的证明大小约为 19 MB（约为常见开源库 vLLM 处理同样长度提示所需 GPU 时间的 70–95 倍）。
本次发布包含可执行代码、Lean 形式化以及协议的技术说明。我们的目标有两方面：(i) 加速并促进可证明推理的发展；(ii) 证明零知识简洁论证在可证明推理中是实用的。
我们相信，这一进展对安全性、把控 AI 发展节奏、为客户提供完整性保证、为审计者和监管者提供工具等方面都具有重要意义。
AI 扩散中的信任挑战
人工智能的发展及其在我们的数字基础设施和经济中日益重要的作用，带来了 AI 提供方必须回应的信任挑战。借助可证明推理（provable inference，PI）工具，有助于应对这些以及其他挑战。
可证明推理工具包括硬件方案、软件方案，或两者的结合。这里我们聚焦于纯软件方案：一种称为「zkSNARK」（零知识简洁知识论证，zero-knowledge succinct argument of knowledge）的密码学工具。通俗地说，zkSNARK 是一个系统，允许证明者通过一份简短的「证书」让验证者相信某个给定计算被正确执行；关键在于，该证书是零知识的，即除了计算正确性所隐含的信息之外不泄露任何信息，并且是简洁的，即验证它比被证明的计算本身呈指数级地更快。
下面我们概述若干挑战，以及 zkSNARK 如何帮助应对这些挑战。
挑战 1：节奏把控
一些关于监管和把控 AI 发展的提议，依赖于对硬件及其使用方式的监控。例如，可能要求某个提供方将其硬件专用于推理，而不是用于训练一个强大的新模型。该提供方可能试图作弊，例如提供更便宜的模型，或以意料之外的方式使用算力，从而腾出资源用于训练。监管者如何可靠地确保硬件被用于推理？
zkSNARK 如何提供帮助：监管者可以要求提供方提交覆盖某段时间内所服务推理请求的证书。证书必须表明这些请求是由所声称的模型生成的。恶意提供方除非其硬件确实在服务正确的模型，否则无法满足这一要求。使用 zkSNARK，监管者无需具备提供方可能拥有的复杂硬件配置，就能验证提供方的主张是否有效；同时，提供方也得到保证：监管者不会获知专有的模型信息。我们注意到，尽管这验证了硬件正在服务推理，但它并不能证明硬件没有在做别的事，例如在暗中进行训练。