2026 年 11 月 2 日，Anthropic 发布 FlashProve：一个面向可证明推理（provable inference）的开源原型，让用户能核查一条模型回复确实来自提供方预先承诺的那组权重，而不是路由服务暗中换上的更便宜的模型，也不是攻击者篡改过的词元流。Anthropic 指出，仅凭输出本身无法判定这一点，哪怕输出看起来质量很高。随公告发布的材料包括可执行代码、技术报告、协议规范，以及在 Lean 证明助手中完成的机器核查数学证明，全部以 Apache 2.0 许可证发布。Anthropic 明确将该文定位为阶段性进展，而非完整的研究议程；代码仓库标注为不维护、不接受贡献的研究产物。[1][2]
系统分两个阶段。离线阶段，提供方发布对一组确切权重的密码学承诺：一个短小的指纹，锁定权重本身却不泄露权重内容。在所测模型上，计算承诺约需 39 分钟；验证方下载的承诺大小约 6.5 MB；一份承诺可覆盖约 1600 万次请求，之后提供方需要重新承诺。在线阶段在推理完成之后进行：提供方对一批已完成的请求生成证明文件，所证明的命题只有一条，承诺的模型在这个提示词上产生这些输出词元。任何人只要持有承诺、提示词和回复，就能在一台普通 CPU 上核查证明，无需权重，也无需提供方的硬件。[1]
这项主张由四条性质支撑。完备性：诚实提供方的证明会被接受。可靠性：伪造一份关于假命题的证明，难度等同于攻破被广泛信任的密码学假设；仓库给出的量化表述是，在 q 次哈希查询后，作弊的提供方未被识破的概率约为 q/2^124 + 2^-101。零知识：证明不泄露权重、中间计算值，也不泄露每一层实际运行了哪些专家，但模型架构本身不隐藏。简洁性：被证明的计算是 400B 参数模型在 H100 上的一次运行，证明却只有约 19 MB，数秒即可核查。其底层是一个 zkSNARK，与区块链二层网络所用的同类；构造方式是把交互式预言机证明（IOP）用哈希函数编译成密码学证明，Anthropic 指出这同时带来后量子安全性。[1][2]
评估使用 Llama 4 Maverick：一个 400B 参数的混合专家模型，每个词元实际激活约 17B 参数，采用其公开发布的 4 位权重。证明方运行环境为单块 H100、24 个 CPU 核心和约 290 GB 主机内存，权重按层分段流入，因此一块 80 GB GPU 即可胜任。每个请求是一个 1,024 个词元的窗口，每份证明检查一个词元。为一批 24 个请求生成证明约需 223 秒，折合约每秒 110 个词元，每份证明为 18.78 MB。验证在 24 个 CPU 线程上需 17 秒，单线程需 21 秒。对照测试是 vLLM 在八块 H100 上运行同一模型的 FP8 版本：按 GPU 时间计算，生成证明的开销约为普通推理的 72 倍，在最高负载下约为 94 倍。速度主要来自两个工程选择：证明方的工作量与实际运行的专家数成正比，而非与全部 400B 参数成正比；请求以批为单位在一次并行处理中完成证明，每批只打开一次权重承诺。[1]
最有意义的对照是与此前对同一模型的证明工作相比。VerInf 是 Anthropic 所知唯一先于此证明过 Llama 4 Maverick 的系统，其报告的速度约为每秒 0.02 个词元，证明 1,000 个词元需 14.3 小时，证明文件达 93.6 GB，验证需近一天。FlashProve 的每秒 110 个词元比它快约三个数量级，且证明小到数秒可验。Anthropic 同时谨慎指出，商业系统 Attestable 报告称可在单块 H100 上以每秒 53 至 77 个词元的速度证明一个 31B 稠密模型，但其未发布开源库。[1]
证明是事后（post-hoc）而非在线（in-line）生成的，Anthropic 明说了这一选择的代价：提供方需要对已完成文本重新计算，关于流量的保证会延迟到达，浮点非确定性也使精确匹配更困难。其声明的局限条件相当狭窄：证明覆盖的是已发布权重的精确整数版本、且在贪心解码下成立；来自浮点实现或采样解码的回复，可能在某个位置偏离被证明的计算。上下文上限为 1,024 个词元，远低于生产环境对话窗口。构造假定混合专家架构，且不隐藏架构。侧信道攻击（例如测量生成证明所需的时间）不在范围内。证明也不对答案的正确性、安全性或无偏性作任何断言；它证明的只是词元出自哪组权重，而非词元的质量。[1]
形式化验证在这次发布中分量很重，其边界同样被说得很清楚。Anthropic 在随机预言机模型下，用 Lean 陈述并证明了完备性、可靠性和零知识性，使协议的顶层主张可机器核查。随后它指出两个仍然存在的信任缺口。第一，形式化陈述是否准确表达了预期的保证，必须靠人工审计确认；为此提供了一个交互式可视化工具。第二，可执行代码必须与形式化定义的协议一致。就可靠性而言，关键只在验证器，而这里的区分非常明确：仓库附带一个 Lean 验证器，已被证明只接受可靠性定理所接受的证明，但它慢；日常推荐使用的 C++ 验证器没有任何形式化保证，不过 Anthropic 称它在全部测试中与 Lean 验证器的结论一致。零知识一侧则根本没有 Lean 证明方，因为证明过程太昂贵，无法以那种方式形式化；这一侧只能依靠对代码的审计。发布说明同样声明，Anthropic 不保证 Lean 协议、论文与快速代码三者完全一致。[1][2]
Anthropic 对这条路线与可信硬件的定位是并列而非取代。此前可证明推理的工作多用可信执行环境（TEE），其保证建立在制造商生产出防篡改硬件之上。FlashProve 是纯软件方案：安全性建立在计算困难性假设上，即便环境（包括硬件和操作系统）已被攻陷，对手仍无法在不解决不可行计算问题的前提下伪造有效证明。Anthropic 称两种方法互补，保证与取舍各不相同。它还提到，这项工作对应其《前沿安全路线图》中的一个目标，即在 2026 年 9 月 30 日前做出为推理流量签名的原型；Anthropic 称该目标已通过另一个相关项目达成（对流量签名并在可信服务器上重算推理），FlashProve 是以不同方法追求同一目标。[1]
[1]: Anthropic，《Progress on provable inference for large language models》，2026 年 11 月 2 日。https://www.anthropic.com/research/provable-inference [2]: anthropics/FlashProve，仓库 README，版本 0.16.0。https://github.com/anthropics/FlashProve
来源
核查或更正本页
- 更正
- 提交更正请求 · 在 GitHub 编辑源文件 · 更正政策
