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

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)

Executive summary

When you talk to a friend in person, you have many ways to know it is really them: you can see them, hear them, shake their hand. When you talk to an AI model, you have almost none. A user querying a model today cannot check that the responses came from the specific model that a developer claims is responding, as opposed to one secretly substituted in by a routing service for cost reasons, or even by an attacker who has tampered with the token stream. Judging from the model’s output alone is unreliable, even if it produces high-quality responses. Cryptographic proofs of inference solve this problem: they let a model provider commit to a model and then prove that each response was produced by that model. Such proofs could enable applications ranging from consumer products to internal security, and could contribute to a toolkit for verifying compliance with AI pacing requirements.

Specifically, we have made progress on a powerful type of cryptographic proof known as a “zkSNARK”, which is uniquely fit for provable inference (owing to its strong hiding and efficiency properties). In this post, we share some of that progress, primarily through a system we call FlashProve. A brief technical summary is as follows:

· Claude has produced improvements on zkSNARKs for inference, building a system that is substantially faster than prior open-source systems.

For a large model (Llama 4 Maverick, 400B-parameter mixture of experts), a single H100 GPU generates proofs at around 110 tokens/second, with a proof size of ~19 MB per 1,024-token request, when in 4-bit quantized weights, using integer arithmetic in prefill. This is ~70-95x the GPU time of running the model itself on vLLM, a common open-source library.

· Prior open-source systems are orders of magnitude slower, as we discuss in section 6. Claude found novel ways to apply state-of-the-art tools in the cryptography and security literature, while relying on well-established design principles for cryptographic proof systems. The commitment to the model, and subsequent inference proofs, hide the weights of the model; hiding the architecture of the model is not a goal of this system.

· Claude is good at optimization, but often makes decisions that are hard to evaluate, especially in large complex systems. We counter this by providing top-level auditable statements in Lean (a formal verification language) for the claimed security guarantees.

Today we are releasing five artifacts:

· The current blog post, which outlines our system and its potential applications;

· A technical report explaining the details of our system;

· A (Claude-written) protocol specification document;

· 可执行代码，包含：一个证明者（prover）和两个验证者（verifiers），一个是用 C++ 编写的快速验证者，另一个是在 Lean 中证明正确的验证者；以及

· 顶层数学陈述的 Lean 证明，以及 Lean 定理的交互式可视化工具，以辅助审计。

我们在 Apache 2.0 许可证下发布了我们的代码、Lean 证明和文档。1 本研究文章旨在分享阶段性进展，而非一项已完成的研究议程。我们明确分享这些内容的目的，是希望其他人能够审阅我们的工作、拿去使用并加以改进。

Introduction

当用户向 AI 模型发送请求时，他们目前无法确切知道他们选择的模型就是生成该响应的模型。对于日常使用而言，用户主要关心的是输出结果，而不一定是哪个特定模型产生了该结果，因此这是一个不太紧迫的问题。

但在几种情况下，这种保证将非常有用。例如，在模型发布前后对其进行测试的独立评估人员需要知道他们正在评估的模型就是正在提供服务的模型。通过第三方路由服务使用模型的客户希望确信这些 Token 来自他们付费购买的模型。

如果网络攻击者在伪装成给定模型的同时修改了 Token 流，用户单从输出结果是无法检测出来的。

然而，实现模型响应的验证具有挑战性。大多数前沿模型的权重都是保密的，并且即使常用户能够访问这些权重，检查给定的响应是否由具有这些权重的模型产生，也需要运行该模型，这需要普通用户（甚至评估人员）无法承受的计算资源。

可证明推理（Provable Inference, PI）的目标是使计算资源有限且没有任何权重信息的的用户能够验证响应是否来自请求的模型。PI 的推动力不仅来自增强客户对 AI 提供商信任的愿望，而且由于它可用于向独立评估人员提供保证，并允许提供商证明他们正在履行某些承诺和法律义务，它对推进前沿 AI 发展和 AI 监管也具有重要意义。

实现 PI 的一种方法是通过称为零知识简洁论证（zero-knowledge succinct argument）的密码学对象：模型提供商随声称的响应一起发送一个简短的证明（例如几兆字节），用户可以快速验证（理想情况下，在 CPU 上几秒钟内完成）。

如果声称的响应与指定的模型不符，用户的检查将失败。重要的是，密码学技术确保了证明不会泄露关于模型权重的任何信息。

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

此次发布包含可执行代码、Lean 形式化描述以及协议的技术说明。我们的目标有两个：（i）加速并促进可证明推理的发展；（ii）证明零知识简洁论证对于可证明推理是切实可行的。

我们认为，这一进展对安全性、AI 发展的节奏、为 AI 客户提供完整性保证、促进审计人员和监管人员的工具开发等方面具有重要意义。

AI 扩散中的信任挑战

人工智能的发展及其在数字基础设施和经济中日益增长的作用，引发了 AI 提供商必须回应的信任挑战。通过依赖可证明推理（PI）工具，可以促进解决这些以及其他挑战。

PI 工具包括硬件方法、软件方法或两者的结合。在这里，我们专注于纯软件方法：一种被称为“zkSNARK”（零知识简洁知识论证）的加密工具。非正式地说，zkSNARK 是一种系统，允许证明者通过一个简短的“证书”来让验证者确信给定的计算已正确执行；

关键在于，该证书是零知识的，即除了计算正确性所暗示的信息外不泄露任何信息，并且是简洁的，即验证速度比被证明的计算快指数级。

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

挑战 1：节奏控制

一些监管和节奏控制 AI 发展的提案依赖于监控硬件及其使用方式。例如，可能要求提供商将硬件用于推理，而不是用于训练强大的新模型。提供商可能会通过提供更便宜的模型或以意想不到的方式使用计算资源来作弊，从而为训练释放资源。监管机构如何能……