智东西
编译 | 孙小雯
编辑 | 程茜
智东西 11 月 4 日消息，今天凌晨，Anthropic开源大模型可证明推理系统 FlashProve，详细技术报告于 11 月 2 日发布。服务商可通过该系统为模型回答生成密码学证明，用户无需获取模型权重或自行运行大模型，就能在 CPU 上核验输出是否符合指定模型的计算结果。
模型调用 API 的机制类似黑箱，发送提示词后，用户仅能查看生成的 Token，但无法验证为自己提供服务的是否为所选模型。此次开源的 FlashProve 旨在解决这一问题，上可抓 " 模型掉包 "，下可验 " 回答篡改 "，还可为监管机构提供监测服务商和企业 AI 使用合规性的渠道。
该模型一经发出，X 上的外网网友就火速贡献梗图。
X 上网友评论：FlashProve 揭开面具，旗舰模型竟是廉价模型（图源：X）
根据 Anthropic 公布的测试结果，FlashProve 已在 Meta 发布的 4000 亿参数模型 Llama 4 Maverick 上完成测试，使用单张 H100 GPU 生成证明，单个请求的证明文件约 19MB，用户端使用 24 线程 CPU 核验约需 17 秒，无需 GPU。
此前，开源系统 VerInf 也曾为 Llama 4 Maverick 生成证明。据其公布的测试结果，在单台 DGX Spark 上，为 1000 个 Token 的前向计算生成证明约需 14.3 小时，证明文件达 93.6GB，使用 20 个 CPU 核心核验约需 17.7 小时。
虽然两项测试的硬件与证明任务设置不同，但从各自公布的结果来看，FlashProve 的证明文件更小，用户端核验耗时也大幅缩短。
不过，FlashProve 目前仍是需要服务方配合的研究原型，生成证明的 GPU 时间开销约为普通推理的 70 — 95 倍。也有网友疑虑：谁会愿意为此高昂价格付费？
X 上网友的评论（图源：X）
FlashProve 的核心技术是零知识简洁非交互式知识论证（zkSNARK），即在不额外泄露模型权重信息的情况下，用户可以用较小文件、较低开销，独立核验推理过程的正确性。
证明系统的完备性、可靠性、简洁性与零知识性（图源：Anthropic）
Anthropic 此次同步公开了技术报告、协议规范、证明生成器、C++ 与 Lean 两种验证器以及用 Lean 编写的形式化证明。其中，代码、Lean 证明和文档均以 Apache 2.0 许可证开源。
Anthropic 透露，Claude 也参与了用于推理的 zkSNARK 技术优化。此次 FlashProve 的开源旨在展示当前可证明推理技术的阶段性进展，供其他研究者复现和改进。
FlashProve 开源主页（图源：Github）
开源地址：
https://github.com/anthropics/FlashProve
一、单张 H100 可批量生成 24 份证明，耗时不到四分钟
FlashProve 的运行分为离线准备和在线证明两个阶段，由模型服务方准备权重承诺、生成证明，再由用户通过验证器核验。
据技术报告介绍，离线阶段，服务方先对模型权重进行编码，生成密码学承诺。密码学承诺相当于为一组权重建立 " 指纹 "，后续证明均与这份承诺绑定，确保核验对应同一组权重。
FlashProve 离线准备流程（图源：Anthropic）
在线阶段，服务方根据输入和待检查输出，记录模型推理中的计算轨迹，包括矩阵乘法、取整、非线性运算等，再生成证明，说明这些运算使用了承诺中的权重，并按指定规则得到了相应输出。
用户持有权重承诺、输入、输出及对应证明，就可以通过验证器检查输出是否符合这组权重的计算结果。这份密码学证明同时具有零知识性（Zero knowledge）和简洁性（Succinctness）：前者使证明不额外泄露权重、中间计算值和专家选择等信息，后者让客户端以远低于自行运行模型的计算开销完成核验。模型架构本身不隐藏。
FlashProve 在线证明与核验流程（图源：Anthropic）
在 Llama 4 Maverick 测试中，离线准备耗时约 39 分钟，服务方保存约 2.15GB 文件。客户端首次下载权重承诺、离线证明及一个链接证明，共 6.24MB。这些准备工作可以复用，之后再为每个请求下载证明文件。
在降低证明开销方面，FlashProve 主要从模型结构、显存使用和批处理三方面进行优化。
Llama 4 Maverick 采用混合专家（MoE）架构，每个 MoE 层从 128 个路由专家中选择 1 个运行，另有 1 个共享专家。因此，每个 Token 约激活 4000 亿参数中的 170 亿。FlashProve 只在计算轨迹中记录实际运行的专家及其选择，使相应证明工作量随激活参数规模变化，同时核验路由器是否选对专家。
FlashProve 利用 MoE 稀疏激活减少证明计算，同时检查路由选择，并隐藏实际运行的专家（图源：Anthropic）
系统还将模型层和计算轨迹分段处理，约 232GB 权重保存在主机内存中，再逐段加载至 GPU。按公告披露，一张 80GB 显存的 GPU 配合约 290GB 主机内存，即可运行系统。
在批处理方面，FlashProve 一批最多可处理 64 个客户端请求。各请求的部分证明步骤在 GPU 上并发执行，整批请求共享用于核验权重承诺的查询数据，减少重复工作。
技术报告显示，研究团队在单张 H100 及 24 个 CPU 核心上测试了批处理效果，使用第三方公开的 4 比特权重，并将其转换为整数模型。每个请求包含 1024 个 Token 的窗口，主测试每份证明只检查紧随提示词之后的一个输出 Token，确认它是已承诺模型在该位置得分最高的选择。测试以 128 位安全强度为目标。
逐个处理请求时，生成一份证明约需 58 秒；每批处理 24 个请求时，总耗时约 223 秒。按请求窗口中的全部 Token 统计，证明生成的处理吞吐由每秒 17.6 个 Token 提高至 110 个 Token。
研究团队还测试了检查回复中每个 Token 的情况，证明生成耗时未出现可测差异。若只统计该测试中被检查的回复 Token，吞吐约为每秒 39.1 个 Token。
二、防止模型被 " 掉包 "、输出遭篡改，四类情形分别怎么验？
Anthropic 在公告中提出，模型服务中有几类难以核实的情况。例如，开发者声称用前沿模型检查过软件漏洞，但聊天记录不足以证明实际调用的是哪款模型；推理服务器遭到入侵后，攻击者还可能将恶意内容混入正常回答。
Anthropic 设想，FlashProve 可通过密码学证明，辅助确认模型有没有被 " 掉包 "、回答有没有被篡改、服务商是否使用通过安全审批的模型，以及企业是否执行了申报的推理任务。
第三方 API 客户和独立评测者可以据此核对实际使用的模型，监管机构则可检查服务商是否遵守模型使用要求。对于要求企业将硬件用于推理、而非训练更强模型的政策提案，监管机构还可要求企业提交某段时间的推理证明，辅助管控 AI 发展节奏。但这些证明只能说明相关推理确实发生，不能排除企业同时训练其他模型。
此外，模型未能取得指定结果时，服务方也可以证明相应尝试确实发生过。Anthropic 在公告中举例设想，代码发布前，服务方可以提供 " 未取得指定结果的证明 "：例如证明某款模型针对指定补丁尝试了至少 100 万 Token，仍未发现漏洞。
三、证明耗时仍为普通推理数十倍，三方面限制尚待解决
要将上述核验方式用于实际服务，FlashProve 还面临证明生成开销、验证范围和安全实现三方面限制。
限制一：生成证明开销高，事后核验存在延迟
相比直接运行模型，生成密码学证明需要更多算力。技术报告显示，研究团队在 8 张 H100 上，通过 vLLM 运行同一模型的 8 位浮点（8-bit floating point，FP8）版本进行对照。
按每张 GPU 折算，FlashProve 为 24 个请求生成证明的 GPU 时间开销约为 vLLM 处理相同请求的预填充（Prefill）阶段所用 GPU 时间的 72 倍；在测试的最高负载下约为 94 倍。
为避免用户等待证明生成，FlashProve 采用事后证明（Post-hoc proving）方式，先返回回答，再由独立硬件根据完整记录重新计算、生成证明。
但事后核验存在延迟，用户可能在发现篡改前就收到恶意回答；已经通过回答泄露的信息，也无法撤回。
FlashProve 采用事后方案，先返回回答，再生成证明，核验结果存在延迟（图源：Anthropic）
限制二：上下文最长 1024 个 Token，计算方式差异影响核验
FlashProve 目前支持的上下文最长为 1024 个 Token，而前沿模型的窗口通常达到数十万乃至数百万 Token，长对话等场景仍难以覆盖。
此外，FlashProve 验证的是整数模型（Integer model）在指定位置选择得分最高 Token 的结果。实际服务采用浮点推理（Floating-point inference）或采样解码（Sampled decoding）时，可能产生不同输出。因此，发现输出不一致时，还需区分计算方式差异与回答篡改。
浮点模型回答 " 煮 7 分钟 "，整数模型选择 " 煮 8 分钟 "（图源：Anthropic）
限制三：实际代码和批量处理的安全性尚未得到完整证明
技术报告显示，高性能可执行代码尚未获得与 Lean 协议同等的形式化安全保证。因为现有证明针对 Lean 描述的协议，而实际运行的 GPU 和 CPU 代码由 AI 据此生成，两者的等价性尚未得到证明。
此外，批量处理请求时的零知识性（Zero knowledge）尚未完成形式化证明（Formal proof）。目前，已完成的相关证明只覆盖逐个请求处理的情形，尚未扩展至多个请求共同处理的情况。
Lean 协议、形式化证明与可执行代码的关系（图源：Anthropic）
结语：FlashProve 补齐推理核验，有望增强企业客户信任
模型身份核验已吸引多家公司入局。今年 2 月 3 日，美国 AI 隐私服务商 Tinfoil 介绍了 Modelwrap 方案，通过安全硬件与权重承诺核验模型身份。今年 8 月，以色列 AI 安全公司 Attestable 公开了面向大模型的零知识推理证明方案，目前公布的测试结果已覆盖 Gemma 4 31B。
Anthropic 推进这项研究，也有自身的安全考虑。该公司此前在安全路线图中提出，要确认模型输出对应的是指定权重，降低攻击者入侵后修改模型的风险。此次开源 FlashProve，就是尝试通过纯软件的密码学方案解决这一问题。
对企业客户来说，付费调用的模型有没有被替换、评测时的版本和实际服务是否一致，都会影响采购和使用决策。如果后续能降低证明开销、接入实际服务，FlashProve 就能让客户和评测者多一种独立核验的手段。这也有望成为 Anthropic 争取企业客户的一项优势，尤其是对服务可靠性和审计有较高要求的客户。
来源：Anthropic