Anthropic 发布 FlashProve，为 AI 推理提供密码学证明

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

这项工作旨在弥补托管式 AI 中的验证缺口。答案质量再高，也无法证明究竟由哪个模型生成：路由服务可能会换用另一个系统，评估者可能收到的不是原定用于测试的模型，攻击者也可能篡改词元流。由于权重是私有的，且硬件要求相当高，用户要通过重新运行模型来核验并不现实。

将回复绑定到隐藏权重

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

该设计旨在实现完备性、可靠性、零知识性和简洁性。诚实生成的证明应当能够通过验证；而要让虚假陈述通过验证，则必须攻破广泛被认为成立的密码学假设。核验证明不应泄露权重或中间计算值。该设计还会隐藏每个词元对应运行了哪些混合专家子网络，但模型架构本身仍然是可见的。

该实现利用了 Maverick 的混合专家结构。证明者的工作量随每个词元激活的约 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 将其与运行 vLLM、使用八块 H100 进行的 FP8 推理作比较时，对于同一批请求，生成证明所需的每 GPU 时间约为推理的 72 倍；在测试过的 vLLM 最高负载下，这一数字约为 94 倍。因此，与不带证明的模型服务相比，这种吞吐能力伴随着相当高的成本。

形式化验证与实际限制

FlashProve 代码库包含证明者、快速的 C++ 验证器、较慢的 Lean 验证器、针对顶层数学命题的 Lean 证明，以及交互式定理可视化工具，并采用 Apache 2.0 许可证。该项目将 0.16.0 版本标注为不再维护的研究成果，且目前不接受贡献。

Lean 相关工作在随机预言机模型下处理了完备性、可靠性和零知识性。要确认形式化陈述确实表达了预期保证，仍需人工审查。Lean 验证器已在形式上与可靠性定理建立联系；而原本供日常使用的 C++ 验证器没有形式化保证，项目改为测试它是否与 Lean 验证器的结果一致。

该项目的已知限制文档记载，几乎所有软件、Lean 证明和文档均由人类指导下的 AI 系统编写，报告中的测试也由这些系统运行。项目尚未接受独立安全审计，对权重隐藏和对抗性证明的测试仍然有限。

这些证明针对贪心解码下权重的精确整数版本。浮点推理或采样解码可能偏离被证明的计算过程，而通用错误测试并未涵盖专门设计的对抗性提示。上下文长度限制为 1,024 个词元，计时攻击及其他侧信道攻击也不在保证范围内。与在推理过程中同步生成证明相比，事后生成证明还会带来重复计算、保证延迟和非确定性。

要让可证明推理成为对实际服务流量进行常规检查的手段，后续工作主要集中在此次发布所暴露的几个不足上：降低证明成本、支持限制更少的解码方式和更长的上下文，以及让快速实现与形式化协议更加紧密地衔接。