Anthropic 发布 FlashProve，用密码学证明模型推理来源

Anthropic 于 2026 年 11 月 2 日发布 FlashProve：这是一个开源研究原型，使用密码学证明来表明某段语言模型回复来自已承诺的权重，同时不泄露这些权重。该公司报告称，对 Meta 的 Llama 4 Maverick，证明生成速度为每秒 110 个 token。

这项工作填补了托管式 AI 中的一个验证缺口。一个高质量的回答并不能证明是哪个模型生成了它：路由服务可能替换成另一个系统，评估者可能收到与预期测试不同的模型，或者攻击者可能篡改 token 流。当权重是私有的且硬件要求很高时，通过重新运行模型来检查对用户来说并不现实。

将回复绑定到隐藏权重

FlashProve 采用零知识简洁知识论证（zkSNARK），并且是纯软件设计，而不依赖可信硬件。在离线阶段，提供方发布一个简短的承诺，它标识某一组确切的权重，同时对这些权重保密。对于已完成的提示词与回复对，系统会生成一个证明，表明输出 token 是已承诺模型的输出。任何持有承诺、提示词和回复的人都可以在无法访问权重的情况下检查该证明。

其预期性质是完备性、可靠性、零知识和简洁性。诚实的证明应被接受，而证明一个虚假陈述则应需要破解被广泛相信的密码学假设。检查证明既不应泄露权重，也不应泄露中间计算值。该设计还隐藏了每个 token 运行了哪些混合专家子网络，尽管模型架构本身仍然可见。

该实现利用了 Maverick 的混合专家结构。证明方的工作量随每个 token 激活的约 170 亿参数扩展，而不是全部 4000 亿参数，同时仍然隐藏专家选择。分段权重从主机内存流式传输，使证明方能够装入一块 80 GB GPU，并搭配约 290 GB 主机内存。

Anthropic 描述了其在客户完整性检查、独立评估、监管工具以及执行已批准模型要求方面的可能用途。推理证书可以证明请求是由所声称的模型处理的，但它们无法证明同一硬件没有同时训练另一个模型。这一区别限制了此类证书在基于计算容量使用方式的合规要求方面所能证明的内容。

证明性能与推理开销

Anthropic 的评估使用了该模型公开可用的 4 位转换版本。一台配备一块 H100 和 24 个 CPU 核心的服务器在约 223 秒内证明了 24 条请求的一批，为每条请求生成 18.78 MB 的证明。离线承诺步骤耗时约 39 分钟。

在验证方面，客户端下载约 6.5 MB 的承诺，并在没有 GPU 的 CPU 上检查证明。Anthropic 测得，24 线程下验证耗时 17 秒，单线程下为 21 秒，其中包括离线阶段的检查。

这些测量将仅用 CPU 的检查过程与重得多的证明操作区分开来。在 Anthropic 与八块 H100 上运行 vLLM 的 FP8 推理进行的比较中，对于同一批次，证明所需的每 GPU 时间约为后者的 72 倍，在测试的最高 vLLM 负载下约为 94 倍。因此，与不生成证明地服务该模型相比，这种吞吐量伴随着相当大的成本。

形式化验证与实际限制

FlashProve 仓库包含一个证明方、一个快速的 C++ 验证器、一个较慢的 Lean 验证器、顶层数学陈述的 Lean 证明，以及一个交互式定理可视化工具，均以 Apache 2.0 许可证发布。它将 0.16.0 版本标注为不再维护的研究产物，且不接受贡献。

Lean 工作处理了随机预言机模型下的完备性、可靠性和零知识性。这些形式化陈述仍需人工审查，以确认它们表达了其预期的保证。Lean 验证器在形式上与可靠性定理相连，但用于日常使用的 C++ 验证器不带有形式化保证，而是通过与 Lean 验证器的一致性测试来检验。

该项目的已知限制文档记录，在人类指导下，AI 系统编写了几乎所有的软件、Lean 证明和文档，并运行了所报告的测试。目前尚无独立的安全审计，对权重隐藏和对抗性证明的测试仍然有限。

这些证明覆盖了贪心解码下权重的精确整数版本。浮点推理或采样解码可能偏离所证明的计算，而通用错误测试并不覆盖对抗性设计的提示词。上下文限制为 1,024 个 token，而时序和其他侧信道攻击不在保证范围内。与在推理同时进行证明相比，事后证明还引入了重新计算、延迟保证和非确定性。

要使可证明推理成为对已服务流量的常规检查，剩余工作集中在本次发布所暴露的缺口上：降低证明成本、覆盖限制更少的解码和更长的上下文，以及将快速实现更牢固地连接到形式化协议。