当你向一个 AI 模型发送请求，你凭什么相信回答确实来自你选择的那个模型？Anthropic 在官方研究博客中给出了一个直白的问题陈述：用户今天查询模型时，无法核实回复是否真的来自开发者声称正在响应的那个特定模型——而非被路由服务出于成本原因偷偷替换的模型，甚至被篡改了 token 流的攻击者。博客原文写道：”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.” 用户仅凭输出质量根本无法分辨——即使回答看起来足够好。

Anthropic 给出的回应是一个名为 FlashProve 的系统：用密码学中的 zkSNARK（零知识简洁非交互式知识论证）为大模型推理生成可验证的证明。项目以 Apache 2.0 许可开源，代码托管于 GitHub。据 Unite.AI 报道，仓库将 0.16.0 版标注为不再维护、不接受贡献的研究原型（research artifact）。据 Anthropic 博客，此前的开源系统慢数个数量级——同一个 Llama 4 Maverick（4000 亿参数 MoE 模型），此前已知唯一证明过同一模型的 VerInf 要以小时计，FlashProve 把它压到了单张 H100 每秒约 110 个 token。Anthropic 博客还提到，Attestable 公司已在 Gemma 4 31B 上实现 53–77 token/秒的可证明推理，但截至发文时尚未发布对应的开源库。FlashProve 公开了完整的证明器、验证器和 Lean 形式化证明。

该项目由 Anthropic 与多家机构的研究者合作完成。据博客署名，作者包括 Roy Rinberg、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）。

信任黑洞：API 推理的身份验证缺失

理解 FlashProve 的意义，需要先理解它试图解决的问题的严重性。

当前 AI 模型的商业交付在很大程度上通过 API 完成。用户发送 prompt，收到一串 token，整个过程是一个黑盒。Anthropic 在博客中列举了几个具体的威胁场景：路由服务出于成本考量，将请求偷偷转发给一个更便宜的模型；攻击者直接篡改 token 流。博客还提到了内部安全层面的风险——一个更强的模型可能顶替获授权的模型运行，并伪装成较弱的模型，以避开针对它的分类器和监控措施。在监管层面，Anthropic 指出，监管机构可能要求提供方只提供被认定为安全的模型，或确保硬件用于推理而非训练新的强大模型。这些场景并非纯粹的理论推演——在模型路由聚合服务日益普及的今天，用户实际上是在信任一条完全不透明的链路。

TechCrunch 在报道中进一步指出了第三方声明的验证问题：一个开发者可能声称其软件库已由前沿网络安全模型扫描过漏洞，一家公司可能声称其商业计划已获得某个特定模型的评估通过——用户如何验证这些声明？Anthropic 研究团队在博客中写道，仅从模型输出来判断是不可靠的，即使它产生了高质量的回复（”Judging from the model’s output alone is unreliable, even if it produces high-quality responses”）。

传统的验证方式是重新运行模型，但当权重是私有的、硬件需求巨大时，这对普通用户完全不可行。这就是 FlashProve 试图填补的空白：在不泄露权重的前提下，提供一种密码学级别的证明，证明特定输出确实来自特定模型。

方案拆解：zkSNARK 如何给推理「验明正身」

FlashProve 的核心是一种被称为 zkSNARK 的密码学证明系统。Anthropic 在博客中明确指出，选择 zkSNARK 是因为其”强隐藏性和效率特性”使其特别适合可证明推理场景。整个方案是纯软件实现，不依赖可信硬件（如 TEE/SGX），这是一个关键的设计选择。

协议分为两个阶段。

离线阶段：权重承诺。 模型提供方发布一个短承诺（commitment），这个承诺精确锁定一组特定的模型权重，但不泄露权重本身。据 Anthropic 博客，这个离线承诺步骤耗时约 39 分钟。承诺完成后，验证方需要下载一个约 6.5 MB 的承诺文件。TechCrunch 将这一机制类比为”密码学邮件签名”——让接收方确认消息确实来自其声称的发送者——但强调即使冒充者就是构建和运行模型的实验室本身，该系统也能提供防护。

在线阶段：逐请求生成证明。 对于每一条已完成的 prompt-response 对，系统生成一个证明，证明输出 token 确实是该承诺模型的输出。任何持有承诺、prompt 和回复的人，都可以在不接触权重的情况下验证这个证明。

Anthropic 博客明确列出了该协议追求的 4 个属性：完备性（诚实的证明应被接受）、健全性（伪造证明需要打破被广泛相信的密码学假设）、零知识性（验证过程不泄露权重或中间计算值）和简洁性。据 Anthropic 博客原文：”The verifier learns nothing about the weights, the intermediate values of the computation, or which experts ran at every layer. The model architecture (excluding the weights) is not hidden.” Unite.AI 报道进一步指出设计”conceals which mixture-of-experts subnetworks ran for each token”。这意味着即使架构公开，具体的专家路由决策和权重都被保护了。但 Anthropic 明确表示，隐藏模型架构本身不是该系统的目标。

性能账本：约 110 token/秒、约 19 MB 证明与 70–95 倍开销

密码学证明的核心矛盾始终是安全性与性能之间的权衡。FlashProve 的性能数据来自 Anthropic 官方博客，测试模型为 Llama 4 Maverick——Meta 的 4000 亿参数 MoE 模型，使用 4-bit 量化权重、整数算术进行 prefill。

证明生成速度： 据 Anthropic 博客，单张 NVIDIA H100 GPU 生成证明的速度约为 110 token/秒。这个数字对应的是 24 个请求的批处理场景。据 Anthropic 博客，一台配备 1 张 H100 和 24 个 CPU 核心的服务器，在约 223 秒内完成了 24 个请求的批量证明。

证明大小： 据 Anthropic 博客，每个 1024-token 请求的证明约为 19 MB（Unite.AI 报道的精确数据为 18.78 MB，与 Anthropic 博客的约 19 MB 一致，后者为近似值）。

验证速度： 验证方无需 GPU，在 CPU 上即可完成验证。据 Unite.AI 报道，使用 24 线程验证耗时约 17 秒，单线程约 21 秒，包含离线阶段的检查。

与直接推理的开销对比： 据 Anthropic 博客，与 vLLM（一个常用的开源推理库）在 8 张 H100 上运行 FP8 推理的对比：FlashProve 的证明生成所需的每 GPU 时间约为直接推理的 70–95 倍。据 Unite.AI 报道，在相同批次下约为 72 倍，在 vLLM 最高负载测试下约为 94 倍。

与此前方案的对比： 据 Anthropic 博客，FlashProve 比此前的开源方案快”数个数量级”（orders of magnitude）。博客第 6 节给出了具体对比：此前已知唯一证明过同一模型的 VerInf，处理 1000 个 token 需要 14.3 小时（在 DGX Spark 上），生成 93.6 GB 的证明，验证耗时近一天。FlashProve 在单张 H100 上以约 110 token/秒的速度证明同一模型，证明大小约 19 MB，验证仅需数秒。此外，据 Anthropic 博客转引，Attestable 公司在 Gemma 4 31B 上实现了 53–77 token/秒的可证明推理，但截至发文时未发布对应的开源库。

FlashProve 之所以能在这个规模上工作，关键在于它利用了 Maverick 的 MoE 结构。据 Anthropic 博客，证明器的工作量与每个 token 实际激活的约 170 亿参数成比例，而非全部 4000 亿参数——同时仍然隐藏了专家选择。分段权重从主机内存流式传输，使得证明器能在 1 张 80 GB GPU 加上约 290 GB 主机内存的配置下运行。

这些数字意味着什么？笔者判断，70–95 倍的开销在当前阶段排除了实时对话场景的应用。对每一条用户请求都生成证明，在大规模 API 服务中累积的额外支出将相当可观。但这个开销水平对于特定场景——离线审计、合规核验、高价值交易的事后验证——已经进入了可讨论的范围。

形式化验证与边界：Lean 证明了什么，没证明什么

FlashProve 的一个独特之处在于它附带了 Lean 形式化验证。Anthropic 在博客中坦承，Claude 在优化过程中”often makes decisions that are hard to evaluate, especially in large complex systems”，因此团队选择用 Lean 提供可审计的顶层安全声明。

开源发布的内容包括 5 个组件：一个证明器、一个快速 C++ 验证器、一个可证明正确的 Lean 验证器、顶层数学声明的 Lean 证明，以及一个交互式定理可视化工具。

但形式化验证的边界需要精确理解。据 Unite.AI 报道，Lean 工作在随机预言机模型下处理了完备性、健全性和零知识性。然而，形式化声明仍然需要人工审查，以确认它们确实表达了预期的保证。Anthropic 博客原文明确指出：”The paper and the fast executable code are derived from the Lean protocol, but we do not guarantee that all three (Lean, paper, code) match each other”。Lean 验证器与健全性定理之间有形式化的连接，但用于日常使用的 C++ 验证器没有形式化保证——它是通过与 Lean 验证器的一致性测试来验证的。

这是一个重要的区分：Lean 证明了数学层面的安全性声明，但从数学定理到实际运行的 C++ 代码之间，存在一个未被形式化覆盖的间隙。对于一个声称提供密码学级别保证的系统来说，这个间隙是审计者需要重点关注的。

据 Unite.AI 报道，项目的 known-limits 文档还记录了几个关键事实：几乎全部软件、Lean 证明和文档都是 AI 系统在人类指导下编写的，测试也由其运行；目前没有独立安全审计（”There has been no independent security audit”）。

此外，当前系统还有几个关键的技术假设和限制。据 Anthropic 博客，FlashProve 目前仅适用于整数化（integer）模型——4-bit 量化权重、整数算术 prefill。这意味着浮点推理不在覆盖范围内。系统仅支持贪心解码（greedy decoding），不覆盖采样、温度调节等涉及随机性的解码策略。而在实际生产环境中，绝大多数 API 调用使用的是带温度参数的采样解码。

据 Anthropic 博客，协议目前只保证证明本身不泄露权重信息，但侧信道攻击（side channel attacks）——例如测量生成证明所需的时间——可能泄露权重信息。Anthropic 明确表示，这不在本次发布的范围内（”We consider this out of scope for this release”）。

据 Unite.AI 报道，推理证书可以证明请求由所声称的模型处理，但无法证明同一硬件没有同时在训练另一个模型。这个区分限制了此类证书在基于计算能力使用方式的合规要求中能够证明的范围。

TechCrunch 报道确认，目前没有在 Anthropic 或任何其他实验室部署该系统的计划。FlashProve 是一个研究原型，不是可用于生产的产品。

开源的信号：Apache 2.0 许可与行业影响

Anthropic 选择以 Apache 2.0 许可开源 FlashProve，这个决定本身就携带了大量信息。

Apache 2.0 允许商业使用、修改和再分发。Anthropic 在博客中明确表示：”This research post is meant to share intermediate progress, and not a completed research agenda. We are sharing this explicitly with the goal that others look at what we have done, take it, and improve it.”

这个开源决定的战略逻辑可以从几个层面理解。

降低审计门槛。 密码学系统的可信度取决于外部审计的深度。通过开源完整的证明器、验证器和 Lean 证明，Anthropic 邀请密码学社区对系统进行独立审查。这与密码学领域的传统一致——算法的安全性应该来自公开审查，而非保密。

建立行业标准的先发优势。 笔者判断，如果可证明推理最终成为行业标准或监管要求，率先定义协议框架的一方将拥有显著优势。Anthropic 通过开源 FlashProve，实际上是在提议一种技术标准。即使最终的生产系统与当前原型差异很大，核心的协议设计和安全假设很可能被后续工作继承。

对 API 信任体系的潜在重塑。 当前 AI API 市场的信任模型完全基于品牌声誉和服务条款——用户信任 Anthropic、OpenAI 等提供方不会偷换模型，但没有任何技术手段验证这一点。FlashProve 提供了一种从”基于信任”到”基于验证”的转变路径。如果证明开销降到可接受的水平，用户和监管机构可以要求提供方为关键请求附带推理证明。

对模型路由市场的合规压力。 模型路由聚合服务是 FlashProve 最直接的应用场景之一。这类服务在用户和底层模型提供方之间增加了一层不透明性——用户选择了某个模型，但路由服务可能出于成本优化将请求转发给另一个模型。Anthropic 博客描述的核心威胁场景之一正是路由服务出于成本原因偷偷替换模型（”one secretly substituted in by a routing service for cost reasons”）。如果可证明推理技术成熟，路由聚合服务将面临提供推理证明的市场压力。

监管核验的技术基础设施。 Anthropic 在博客中提到，此类证明”could contribute to a toolkit for verifying compliance with AI pacing requirements”。这暗示了一个更宏大的愿景：监管机构可以要求 AI 提供方为特定场景（如医疗、金融、安全）的推理附带密码学证明，确保使用的是经过审批的特定模型。

从原型到生产：距离有多远

据 Unite.AI 报道，仓库将 0.16.0 版标注为不再维护、不接受贡献的研究原型（research artifact）。这不是一个即将部署的产品。从原型到生产级系统，至少需要跨越以下几个工程和理论障碍。

解码策略的覆盖。 当前系统仅支持贪心解码。生产环境中的 API 调用绑定了温度、top-p、top-k 等采样参数，这些参数引入了随机性。笔者推测，为随机解码生成零知识证明可能需要处理可验证随机数生成（VRF）等额外的密码学原语，复杂度将显著增加，这是从原型到生产的最大理论障碍之一。

浮点推理的支持。 当前系统限于整数算术。虽然 4-bit 量化模型使用整数运算是合理的，但许多生产部署使用 FP16 或 BF16 精度。将 zkSNARK 扩展到浮点运算需要处理浮点数的非结合性等问题，这在密码学电路设计中是一个已知的难题。

证明开销的进一步压缩。 70–95 倍的开销意味着，如果直接推理一个请求的 GPU 成本是 X，生成证明的成本是 70X–95X。即使只为 1% 的高价值请求生成证明，这也是一笔可观的额外支出。笔者判断，要进入大规模商业应用，证明开销需要大幅下降——这一粗略估计基于当前推理成本本身已经不低的现实，具体阈值取决于应用场景的价值密度，可能需要密码学证明系统本身的根本性改进，或者专用硬件加速。

证明大小的优化。 每个 1024-token 请求约 19 MB 的证明，对于需要存储和传输大量证明的场景（如监管审计）来说，存储成本不可忽略。如果一个 API 服务每天处理数百万请求，全量证明的存储需求将以 TB 级增长。

C++ 验证器的形式化保证。 如前所述，实际使用的 C++ 验证器没有形式化保证，Anthropic 博客明确表示不保证 Lean、论文和代码三者完全一致。对于一个声称提供密码学级别安全性的系统，这个间隙需要被弥合——要么通过形式化验证 C++ 代码，要么通过从 Lean 验证器自动生成高效的可执行代码。

端到端的信任链。 即使推理过程被证明正确，还有一些 FlashProve 不覆盖的信任问题。据 Unite.AI 报道，推理证书无法证明同一硬件没有同时在训练另一个模型。此外，承诺阶段本身需要信任——谁来验证发布的承诺确实对应了声称的模型？如果一个提供方发布了一个声称是某模型的承诺，但实际上承诺的是另一个模型，用户如何知道？这需要额外的治理机制，比如第三方审计或多方承诺协议。

Claude 在 FlashProve 中的角色

Anthropic 博客中有一个容易被忽略但意义深远的细节：Claude 在 FlashProve 的优化中发挥了重要作用。博客原文称”Claude has produced improvements on zkSNARKs for inference, building a system that is substantially faster than prior open-source systems”，并指出”Claude found novel ways to apply state-of-the-art tools in the cryptography and security literature”。同时，项目的 known-limits 文档记录，几乎全部软件、Lean 证明和文档都是 AI 系统在人类指导下编写的。

这意味着 Anthropic 在用 AI 模型进行密码学系统的工程优化，而正是因为 AI 在复杂系统中”often makes decisions that are hard to evaluate”，团队才引入了 Lean 形式化验证作为对冲。这构成了一个有趣的递归结构：AI 参与构建了一个用于验证 AI 输出真实性的系统，而这个系统本身的正确性又需要形式化方法来验证——且目前尚未经过独立安全审计。

笔者判断，这个细节透露了 Anthropic 对 AI 辅助研究的一种方法论态度——让 AI 做它擅长的大规模优化工作，但用形式化方法约束其输出的正确性。这种”AI 生成 + 形式化验证”的范式，若能经受住独立审计的检验，可能在密码学、编译器、硬件设计等对正确性要求极高的领域具有更广泛的适用性。

从「你说是就是」到「密码学说了算」

FlashProve 的跨越在于：同一个 4000 亿参数的模型，证明从以小时计、以 GB 计，压到了每秒约 110 个 token、约 19 MB。证明速度、证明大小和验证时间同时实现了数个数量级的改善。

但 70–95 倍的开销、仅支持贪心解码和整数模型的限制、C++ 验证器缺乏形式化保证、侧信道攻击未纳入防护范围、尚无独立安全审计，这些都清晰地标定了从原型到生产的距离。Anthropic 自己也坦诚这是”intermediate progress”而非完成的研究议程。

真正的影响可能不在于 FlashProve 本身是否会被部署，而在于它打开的可能性空间。当密码学证明推理的技术可行性在全尺寸模型上被验证后，围绕 API 信任、模型路由透明度和监管核验的讨论就从”是否可能”转变为”何时可行”和”谁来推动”。Anthropic 以 Apache 2.0 开源的决定，实际上是在邀请整个行业——包括竞争对手、学术界和监管机构——共同回答这些问题。

在一个 AI 模型越来越多地被用于高风险决策的世界里，”这个回答真的来自你声称的那个模型吗”不再是一个可以忽略的问题。FlashProve 给出了一个可以公开检验的工程原型答案——尽管距离生产部署仍有相当距离。

主题分类：技术突破

参考资料

  1. Progress on provable inference for large language models — Anthropic Research, 2026-11-02
  2. Anthropic Releases FlashProve for Cryptographic AI Inference Proofs — Unite.AI, 2026-11-02
  3. Anthropic is working on a system to prove AI models’ identity — TechCrunch (Russell Brandom), 2026-11-03