Hacker News 5天前 · 2026-11-05 03:41:48 · 10 阅读

大模型可证明推理的进展

第 1 章：执行摘要

Roy Rinberg (Anthropic), Alex Allain (Anthropic)；Alessandro Chiesa (EPFL, StarkWare), Miranda Christ (MIT, RESI), Rahul Dalal (Anthropic STEM 学者计划, Succinct), Giacomo Fenzi (EPFL), Ben Mayer (Anthropic 学者计划, MIT), Guy Weissenberg (EPFL)

执行摘要

与朋友面对面交谈时，你可以通过看到他们、听到他们的声音或握手来确认对方身份。但与 AI 模型交互时，这种验证手段几乎为零。目前，用户无法核实响应确实来自开发者声称的那个特定模型，而非被路由服务出于成本考量悄悄替换的其他模型，甚至不是被篡改了令牌流的攻击者所操控。仅凭模型输出判断其来源不可靠，即便其生成的高质量回复。推理密码学证明解决了这一问题：它允许模型提供商提交特定模型，并证明每次响应均由该模型生成。此类证明可支持从消费级产品到内部安全等多种应用，并为验证 AI 合规性（如节奏要求）提供工具集。

具体而言，我们在一种强大的密码学证明类型——“zkSNARK”上取得了进展。凭借其强大的隐匿性和效率特性，zkSNARK 尤其适合可证明推理。在本文中，我们将通过一个名为 FlashProve 的系统分享部分进展。简要的技术总结如下：

Claude 在用于推理的 zkSNARK 方面取得了改进，构建了一个比现有开源系统快得多的系统。
1. 对于一个大型模型（Llama 4 Maverick，一个具有 400B 参数的专家混合模型），在 4 位量化权重和预填充阶段使用整数算术的条件下，单张 H100 GPU 能以约 110 tokens/秒的速度生成证明，每个 1,024 令牌的请求生成的证明大小约为 19 MB。这大约是 vLLM（一个常见的开源库）运行模型本身所需 GPU 时间的 70-95 倍。
2. 现有的开源系统要慢好几个数量级，详见第 6 节。Claude 找到了一些新颖的方式，将密码学与安全领域文献中的前沿工具应用到本系统中，同时遵循密码学证明系统由来已久的设计原则。对模型的承诺以及后续的推理证明会隐藏模型的权重，但隐藏模型架构并不是本系统的目标。
Claude 擅长优化，但它做出的决策往往难以评估，尤其是在大型复杂系统中。为此，我们用 Lean（一种形式化验证语言）为所声称的安全保障提供了可审计的顶层证明。

今天我们发布五个成果：

当前这篇博客文章，概述了我们的系统及其潜在应用；
一份技术报告，详细解释了系统原理；
一份（由 Claude 撰写的）协议规范文档；
可运行的代码，包括一个 prover 和两个验证器——用 C++ 编写的快速验证器，以及用 Lean 编写的可证明正确的验证器；
面向顶层数学命题的 Lean 证明，以及一个用于辅助审计的 Lean 定理交互式可视化工具。

我们的代码、Lean 证明和文档均以 Apache 2.0 许可证发布。¹这篇研究文章旨在分享阶段性进展，而非完整的研究计划。我们之所以明确公开，就是希望其他人能够审视我们的工作，取其所长并加以改进。

引言

当用户向 AI 模型发送请求时，目前无法确定生成响应的是否确为所选模型。在日常使用中，用户主要关心输出结果，而非具体由哪个模型生成，因此这一问题紧迫性较低。但在某些场景下，这种确定性至关重要。例如，在发布前后独立测试 AI 模型的评估者需确认所评估的正是被服务的模型；通过第三方路由服务使用模型的客户端，也需要确保所接收的 token 源自其付费的模型。此外，若网络攻击者在冒充特定模型的同时篡改了 token 流，用户仅凭输出内容无法察觉异常。

然而，实现模型响应的可验证性颇具挑战。大多数前沿模型的权重属于私有数据，即便用户能获取权重，验证某条响应是否由该模型生成也需实际运行模型，这对普通用户甚至评估者而言，算力成本都难以承受。

可证明推理（Provable Inference, PI）旨在让算力有限且不知晓权重信息的用户，也能验证响应是否来自指定模型。PI 的动机在于增强用户对 AI 提供商的信任。同时，由于它能为独立评估者提供保证，并让提供商证明其遵守了特定承诺及法律义务，因此 PI 还对 AI 前沿发展的节奏及监管具有深远影响。

实现 PI 的一种方式是借助一种名为零知识简洁论证的密码学对象：模型提供商在发送目标响应的同时，还附带上一个简短的证明（例如几兆字节大小），用户可在短时间内（理想情况下，在 CPU 上仅需几秒）完成验证。若目标响应与指定模型不符，用户的验证将失败。关键在于，密码学技术确保了该证明不会泄露任何关于模型权重的信息。

今天，我们正式发布 FlashProve：一个开源的可验证推理高性能原型。在一个 4000 亿参数的混合专家模型（Llama 4 Maverick，4-bit 量化）上，我们展示了单张 H100 GPU 能以超过 100 tokens/秒的速度生成证明，每个 1024 token 请求的证明大小约为 19 MB（GPU 耗时约为开源推理库 vLLM 处理同长度 prompt 的 70-95 倍）。

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

我们相信这一进展具有深远的安全意义：无论是为 AI 发展设定节奏、为 AI 用户提供完整性保障，还是为审计者和监管者提供工具支持等方面。

AI 普及带来的信任挑战

人工智能的发展及其在数字基础设施和经济中日益重要的作用，带来了 AI 服务商必须应对的信任挑战。借助可验证推理（Provable Inference，PI）工具，可以更好地应对这些挑战。

PI 工具既可以是硬件方案、软件方案，也可以是两者结合。本文聚焦纯软件方案：一种名为 zkSNARK（zero-knowledge succinct argument of knowledge，零知识简洁知识论证）的密码学工具。通俗地说，zkSNARK 是一种让证明者（prover）通过简短的“证书”说服验证者（verifier）某项计算已被正确执行的系统；关键在于，这份证书具有零知识性——除了“计算正确”这一事实本身，它不泄露任何其他信息；同时还具有简洁性——验证证书比执行原计算要快指数倍。

下面我们列举几个挑战，并说明 zkSNARK 如何帮助应对。

挑战一：节奏控制

目前，一些关于监管和控制节奏AI 发展的提议，都依赖于监控硬件及其使用情况。例如，可能会要求服务提供商将硬件专门用于推理，而非训练强大的新模型。提供商可能会试图作弊，比如通过提供成本较低的模型，或以意想不到的方式使用计算资源，从而腾出算力用于训练。监管者该如何可靠地确保硬件确实被用于推理？

zkSNARK 如何助力： 监管者可以要求提供商提供一份证明，涵盖特定时间段内服务的推理请求。该证明必须显示这些请求确实由声称的模型生成。恶意提供商无法完成此要求，除非其硬件真的在运行指定的模型。借助 zkSNARK，监管者可以在不依赖提供商可能拥有的复杂硬件设施的情况下，验证提供商声明的有效性；同时，提供商也能得到保证，即监管者不会获知其专有模型信息。² 需要指出的是，虽然这能验证硬件正在执行推理任务，但并不能证明硬件没有在“暗中进行训练”。

挑战 2：篡改检测

随着 AI 模型的价值不断提升，运行它们的服务器也成了攻击者的重点目标。攻击者或不怀好意的内部人员可能攻破推理服务器，窃取模型权重、向用户返回恶意响应（比如往用户电脑上投送恶意软件）等等，而且可以混在真实响应中不留痕迹。威胁未必来自外部。随着模型逐渐具备自我改进和自主部署的能力，一个更先进的模型完全可能顶替被授权运行的那个模型，把自己伪装成较弱的模型，从而规避针对它的分类器和监控手段。两种场景指向同一个问题：公司如何确定服务器上实际运行的究竟是哪些权重？Anthropic 在前沿安全路线图中设定了一项公开目标，要做出一个验证推理流量的原型：“我们将在 2026 年 9 月 30 日前开发出可证明推理（provable inference）的原型，这项技术可以可靠且可证明地‘签注’ AI 模型的输出，使输出能够归因到特定的模型权重。”正如我们的 RSP 更新中所说，我们通过一个独立但相关的项目实现了这一目标：对我们的推理流量进行签注，并在可信服务器上重新计算推理；本篇博文的工作则是用另一种方法追求同一个目标。³

zkSNARKs 能提供什么帮助：服务提供方可以要求服务器对每一条响应都附带有效的 zkSNARK 证明。证明与权重的特定承诺绑定，因此它证明的不只是“某个模型”生成了响应，而是那个“已承诺的模型”生成了响应。无论是攻破服务器的攻击者，还是顶替其他模型运行的模型，想要不被发现，就必须为预期权重生成有效证明——而这做不到。用户也可以拿到这些证明：得益于零知识性，证明不会泄露内部信息；得益于简洁性，验证成本也很低。这样一来，攻击者通过推理 API 能干的事情就大大受限了。

挑战 3：文本溯源

人们可能希望证明，在理解或分析某事物上确实投入了大量精力。例如，开发者可能会声称其软件库已经过前沿网络安全模型的安全扫描，或者公司可能会称其商业计划已获相关模型的批准。用户该如何验证这些声明？用户可能缺乏自行运行该模型的资源（或没有相应的权限）。即便公开聊天日志也无法提供绝对保证：理论上，开发者可以伪造这些日志，使用更便宜或降级版本的模型来生成，而非声称的前沿模型。更普遍的问题是，用户如何确认自己接受服务的是其选定的模型？

zkSNARKs 如何提供帮助：服务方可以在每个响应附带一个 zkSNARK，以证明该输出确实由声称的模型针对给定输入生成。简洁性让用户无需专用硬件即可快速验证此证书，而零知识特性则确保用户不会获知专有模型的权重信息。这与现有的验证机制相辅相成，用于确认生成响应的具体模型。

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

挑战 4：模型审批

法规可能要求服务方仅部署经批准的安全模型，而非被判定存在网络安全或安全隐患的模型。由于高风险模型可能在性能上优于竞争对手或部署成本更低，服务方可能有动机规避此规定。监管机构如何确保仅部署经过批准的模型？

zkSNARKs 能帮上什么忙：监管方可以要求模型提供商在每次响应中附上 zkSNARK，以确保其确实使用的是经批准的模型。证明会把每个请求与所用模型绑定在一起，因此如果提供商偷偷用了未经批准的模型，证明就无法通过验证。借助 zkSNARK 的简洁性，监管方可以轻量级地完成校验，无需重新执行每个请求。

关于基于可信硬件的可证明推理。以往的研究通常依赖可信执行环境（trusted execution environments）来实现 PI。这类方案基于硬件，其隐私保护和远程证明能力依赖于制造商提供防篡改硬件。我们的研究则聚焦于纯软件的密码学方案，其安全性和隐私性建立在计算难题的困难性之上。即便运行环境（硬件、操作系统等）被攻破，攻击者也无法在不高破计算上不可行的问题的情况下伪造有效证明。可信硬件与密码学是两种互补的路线，各有不同的保证与权衡，二者都将在应对上述信任挑战中发挥作用。

我们的系统：FlashProve

FlashProve 是一个面向大规模 Mixture-of-Experts（MoE）语言模型的可证明推理系统。更多细节见我们的技术报告，这里只做概要介绍。

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

在离线阶段，证明者发布一份针对模型权重的承诺（commitment）——一个简短的指纹，用来锁定某一确切的权重版本，同时不暴露权重本身。之后的推理声明都将对照这份承诺来核验，也就是说，核验依据正是这一阶段所承诺的模型权重。
在在线阶段，收到验证者的请求（即提示词和对应的输出 token）后，证明者会生成一份证明文件，证明以下命题：

被承诺的模型在求值时确实生成了这些输出 token。

任何持有承诺、提示词和回复的人都可以进行核验——不需要拿到权重，也不需要强大的算力——即可确信：被承诺的权重在处理这个提示词时，生成的正是这些 token，不多不少。

安全性保证

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

诚实的证明文件会被接受（完备性）。诚实证明方生成的证明能够通过验证方的检验。
证明文件无法伪造（可靠性）。生成虚假命题的有效证明在实际上是不可能完成的任务（即等同于打破被广泛认可的密码学假设），因此验证方无需信任证明方。

仅具备完备性和可靠性是可以通过一个拥有强大算力且知晓模型权重的验证方来实现的（即对提示执行模型推理，并检查结果是否与响应匹配）。接下来的两个属性才是使该系统非平凡的关键。

证明文件不泄露命题以外的信息（零知识）。验证方对权重、计算过程中的中间值或每层激活的专家模型一无所知。除权重外，模型架构并非隐藏信息。
证明文件小巧且校验成本低（简洁性）。被证明的计算涉及在 H100 GPU 上运行一个拥有 4000 亿参数（量化版本约占 232 GB）的模型，而验证方仅需接收一个约 19 MB 的证明文件，在 24 核 CPU 上几秒钟即可完成校验。审计员或硬件资源远少于提供方的用户，无需依赖复杂的基础设施即可检查证明文件。

评估

我们在 Llama 4 Maverick 上测试了该协议的实现（这是一个 4000 亿参数的混合专家模型，每个 token 仅使用约 170 亿参数），使用的是公开可用的 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 秒）。

与普通推理的对比：我们在 8 个 H100 上运行了广泛使用的推理引擎 vLLM（使用同一模型的 FP8 版本），发现按单 GPU 计算，对 24 个请求生成证明的耗时约为 vLLM 同时处理这 24 个请求的 72 倍（多次运行的结果在 66 到 77 倍之间）；当 vLLM 以我们测试的最高负载运行时，这一差距约为 94 倍。

系统内部。FlashProve 的底层机制是一种 zkSNARK，与点对点系统中部署的类型相同（例如以太坊等区块链上的 L2 网络，如 Starknet 或 Mantle）。我们的 zkSNARK 采用成熟的技术路线构建：先构造一个名为交互式预言机证明（IOP）的信息论对象，再借助哈希函数将其编译为密码学证明（甚至具备后量子安全性）。我们的 IOP 由最先进的组件组装而成，使用了带线性约束的码邻近性测试和 lookup argument 等工具，这些技术源自编码理论和复杂度理论。将这些组件组合成面向推理的定制化 IOP 是一项精细的工作，具体构造细节见技术报告。

系统工程

FlashProve 受益于我们的架构设计，相关细节见技术报告。本文重点阐述其中几点：

验证者的计算量与实际运行的专家模型成正比。在 MoE 模型中，一个 token 仅使用 400B 参数中的约 17B，验证者每 token 的工作量与这 17B 成正比，而非全部参数（且证明过程会隐藏实际选中的专家）。
请求采用事后批量验证。验证者通过单次并行路径读取已生成的文本（类似 prefill 阶段），每个批次只需解开一次权重承诺，而非每个请求解开一次。
系统设计为适配单块 GPU。每层模型权重被切分为若干段，逐段进行验证。权重保存在普通内存中按需流入，因此一块 80 GB GPU 加上约 290 GB 主机内存即可满足需求。

事后验证与内联验证

将验证机制集成到推理服务器时，有两种选择：内联验证（随推理同步进行）或事后验证（对部分 token 在事后进行验证）。我们的系统采用后者。内联方案要求极低延迟，可能在安全与效率间做出妥协；事后方案允许更高延迟，无需承受这种权衡。不过，事后验证也有局限：增加了重新计算的复杂度、获取流量保障存在延迟，且存在固有的“非确定性”。关于事后验证的动机与影响，我们将在技术报告中详细说明。

基于形式化验证的可信性

密码学代码以脆弱且易错著称。用户如何信任我们今日发布的代码？

答案是形式化验证：我们使用 Lean 证明助手来指定协议和所需的安全属性。我们以机器可检查且保证正确（仅限编译器错误除外）的形式证明这些属性。我们聚焦于以下三个顶层属性：

完备性：若陈述正确，验证者将接受生成的证明。
可靠性：任何伪造的证明都会被验证者拒绝（除非出现可忽略不计的小概率）。
零知识：证明不会泄露模型权重的任何信息，验证者能获知的仅限于从响应本身推断出的内容。⁴

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

形式化验证仍留下两个重要的信任缺口。第一，形式化陈述必须经过审计，确保它们与实际意图一致。这一步只能靠人工完成（尽管比审计证明轻松得多）；我们提供了一个交互式可视化工具来辅助这项工作。

第二，可执行代码必须经过审计，确保它与已证明安全性质的形式化协议一致。如何最好地辅助这项工作取决于具体性质，因为可靠性只取决于验证者，零知识只取决于证明者，而完备性取决于两者的交互。

对于可靠性，我们只需要验证者代码是正确的（“证明”的全部价值就在于：只要信任验证者，就可以完全不信任证明者）。我们在 C++ 验证者之外还提供了一个可执行的 Lean 验证者。Lean 验证者运行较慢，但 Lean 可以证明它只会接受我们的可靠性定理中验证者所接受的内容。不过，日常使用的还是 C++ 验证者：它没有形式化保证，但在我们的所有测试中都与 Lean 验证者的判定结果一致。
对于完备性，威胁模型不假设存在对抗性攻击（证明者和验证者都是诚实的）。因此，通过标准软件测试即可借助 Lean 验证者建立信心，确认诚实的证明者能够产生可被接受的证明：先在正确的陈述上运行证明者，再用 Lean 验证者验证产生的证明。
零知识证明只需要证明方（prover）具备正确性。但不同于验证方，证明方是一个高开销的流程，直接运行 Lean 证明器并不现实。本文未提供具体实现方案：我们认为，任何希望隐藏模型权重的证明方，都拥有足够的资源进行细致的代理式（agentic）和/或人工安全审计，以确保其证明与 Lean 证明器的等效性。

局限性

本次发布属于研究原型，存在以下技术局限：

快速可执行代码没有形式化保证。我们提供了该协议的 Lean 实现（包括一个可执行的“慢速” Lean 验证器），并在 Lean 中证明了相关安全属性。论文和快速可执行代码均衍生自 Lean 协议，但我们并不保证三者（Lean、论文、代码）完全一致。
证明针对的是贪心解码下的整数模型。我们证明的是已发布权重的精确整数版本，证明声明每个检查的 token 都是该模型的贪心选择。来自浮点实现的响应或采样解码，可能在某一位点偏离，导致不再与已证明的计算精确匹配。通常预期且经过实证测试，整数版本的误差率在通用情况下（即使考虑浮点计算的非确定性）与真实浮点推理相比很小，但这并不涵盖对抗性设计的提示词。
架构隐藏。我们的系统假设所服务的模型采用 Mixture-of-Experts (MoE) 架构，其中每个 Transformer 层的前馈模块被替换为多个专家子网络和一个 router，该 router 仅为每个 token 激活少量专家，我们的系统利用这种 MoE 结构来实现效率提升。其他架构，如 dense 模型，也被广泛使用，其描述可能包含模型提供商希望保密的知识产权。事实上，还可以设想一种进一步隐藏模型架构的系统：prover 通过隐藏承诺提交权重和架构（即可用于推理的“可执行代码”），而 verifier 的声明则关于在承诺模型上检查该承诺可执行代码的执行情况。
侧信道攻击。当前协议只保证证明本身不会泄露已提交模型的权重信息。但“侧信道攻击”——比如测量生成证明所耗费的时间——仍可能间接泄露权重的相关信息。我们认为这超出了本次发布的范围。
更长的上下文。系统目前可证明的推理上下文长度上限为 1,024 个 token，与聊天场景中累积的上下文相比相当短。理想情况下，这一长度应能扩展到前沿模型的完整上下文窗口（通常为数十万到数百万 token）。

脚注

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

02具体隐藏哪些信息取决于系统设计。在我们的工作中，我们隐藏了权重，但未隐藏架构。在后续工作中，我们计划连架构细节也一并隐藏。（原则上隐藏模型的全部信息是可行的，问题在于效率如何。）

03在 2026 年 10 月 19 日的更新中，我们还更改了目标名称：现在使用“推理验证”（inference verification）而非“可证明推理”（provable inference）。我们最初的目标是让 token 流的完整性具备高度保障，而实现这一点有多种途径，“可证明推理”一词暗示的方法比我们认为必要的范围更窄。除该原型外，我们还在推进基于密码学证明的推理验证，这是实现 token 流高度保障的途径之一。

04模型架构并未隐藏。隐藏架构细节留待后续工作完成。

原始来源： Hacker News