FlashProve 官方博客题图（图源：Anthropic）
先介绍下主角：Anthropic 是 Claude 系列大模型背后的美国 AI 公司，一向把 AI 安全当作招牌。这次它开源的不是新模型，而是一个"给 AI 回答验明正身"的工具。
Anthropic 发布研究博文，开源 FlashProve：一个可证明推理（provable inference）的原型系统。它要解决的问题很朴素——你调用一个 AI 接口，怎么确定回答你的真是对方宣称的那个模型，而不是被中间商为了省钱偷偷换成的便宜模型，或者被黑客篡改过的输出？
官方博客
https://www.anthropic.com/research/provable-inference
GitHub 仓库
https://github.com/anthropics/FlashProve
它是怎么做到的？三步走
1. 先"按手印"。模型提供方一次性公布一个对模型权重的承诺（commitment），可以理解为一枚短短的"指纹"：它锁死了某一套确定的权重，但从指纹反推不出权重本身。
2. 每条回答附一张"证明"。之后每生成一条回复，提供方的 GPU 都会额外算出一份密码学证明，证明"这段输出确实是那套被锁定的权重算出来的"。
3. 谁都能验。任何手里有指纹、提示词和回复的人，都能在普通 CPU 上检查这份证明，不需要权重，也不需要 GPU。造假的回复过不了关；证明本身也不泄露权重信息。
背后的技术是一种叫"零知识简洁论证"的密码学工具：证明很小、验证很快，而且除了"计算是对的"之外什么也不透露。博客还提到，它基于哈希函数构建，具备抗量子特性。
FlashProve 仓库 README 首页（截图：GitHub）
跑得多快？官方实测数字
以下数字均来自 Anthropic 博客。测试模型是 Meta 的 Llama 4 Maverick（4000 亿参数的混合专家模型，每个 token 激活约 170 亿参数），使用公开的 4-bit 量化版本（约 232 GB）：
证明速度：一张 H100 加 24 核 CPU，一批 24 个请求约 223 秒证完，折合约 110 token/秒。
证明大小：每个 1024 token 的请求约 19 MB（实测 18.78 MB）。
验证成本：客户端先下载约 6.5 MB 的承诺数据，验证一份证明在 24 线程 CPU 上约 17 秒，单线程约 21 秒。
一次性承诺：每个模型做一次，约 39 分钟，之后大约可用于 1600 万个请求，再重新承诺。
代价：和在 8 张 H100 上用 vLLM 跑 FP8 版同一模型相比，按每张 GPU 算，证明耗时约是正常推理的 72 倍（多次测量 66–77 倍），在 vLLM 最高负载下约 94 倍，也就是官方说的 70–95 倍。
这个代价不小，但对比前人是数量级的进步：博客提到，此前唯一证明过同款 Maverick 模型的开源系统 VerInf，1000 个 token 要 14.3 小时、证明 93.6 GB、验证将近一天。
能塞进单卡，靠的是几个设计：请求事后成批证明（像预填充一样一次并行读完文本）；权重按层切段、放在主机内存里流式送入，一张 80 GB 显卡配约 290 GB 内存就够；同时利用混合专家结构，只为实际激活的专家干活。
上手：三行命令验一份证明
我们克隆了仓库（版本 0.16.0）。它被定位为研究产物：不维护、不接受贡献。整体分为 prover（CUDA 证明器）、verifier（C++ 快速验证器 cp_verify）、lean（Lean 4 形式化证明与慢速验证器）几部分，另有 toy 目录可在 CPU 上跑玩具证明。README 给出的最简单路线是：只需 g++ 13+、不到 2 GB 内存，编译验证器后检查仓库自带的示例证明，最后一行输出 YES 就算通过。
README 中的验证器编译与验证命令（代码摘自 FlashProve 仓库，中文注释为本文所加）
注意一个细节：README 特别强调，承诺 ID 必须从你信任的渠道拿，不能从被检查的服务器或随证明发来的文件里取，否则"指纹"本身就可能是假的。另外仓库自带的示例是合成权重的小模型，只能说明验证器能用；要跑真正的 Maverick 证明，需要 H100 和三百多 GB 内存。
有意思的是，README 开头还专门写了一段"给智能体看的说明"：编译、运行、核对结果这些繁琐活，官方建议直接交给编程智能体来做。
为什么还要 Lean 形式化？
博客坦言，这套系统大量由 Claude 参与设计和优化，而 AI 做出的复杂工程决策往往难以审查。所以团队用 Lean（一种形式化验证语言）写下顶层安全性质并给出机器可检查的证明，覆盖三件事：完备性（诚实的证明会被接受）、可靠性（拿不是该模型的输出蒙混过关几乎不可能）、零知识（证明不泄露权重）。
Lean 中的可靠性定理 sound（代码摘自 FlashProve 仓库 lean/AtFullSide/Face/TheSixLines.lean）
按 README 的说法，作弊者在 q 次哈希查询内蒙混过关的概率约不超过 q/2^124 + 2^-101。仓库同时提供两个验证器：Lean 写的慢速验证器有形式化保证；日常用的 C++ 快速验证器没有形式化保证，只是在所有测试中和 Lean 版结论一致。
官方自己承认的局限
证的是"整数版、贪心解码"的模型。如果实际服务用浮点运算或采样解码，输出可能在某处偏离，就不再严格匹配被证明的计算。
只藏权重，不藏架构。模型结构是公开的，而且目前依赖混合专家架构来提速。
三方不保证一致。论文、Lean 协议和快速代码之间，官方不保证完全对应；侧信道攻击（比如通过证明耗时推测权重）也不在本次范围内。
据报道称，仓库的已知局限文档还写明，几乎所有代码、Lean 证明和文档都是在人类指导下由 AI 系统完成，目前尚无独立安全审计。
Anthropic 为什么做这个？
除了让用户放心，博客更看重的是安全：如果推理服务器被攻破，攻击者可能偷换输出、投放恶意内容；更远一点，一个更强的模型甚至可能冒充较弱的模型来逃避监控。要求服务器每条回复都附证明，这些手段就藏不住了。
Anthropic 此前在《前沿安全路线图》中定下目标：2026 年 9 月 30 日前做出"可证明推理"原型。博客说明，这个目标已通过另一个相关项目达成——它对 Anthropic 的推理流量做签名，并在可信服务器上重新计算推理；FlashProve 是用密码学证明走的另一条路，属于阶段性研究成果，官方希望其他人拿去继续改进。
安全研究者 Steve Weis 在 X 上转发该发布（图源：X @sweis）
一句话看点
70–95 倍的代价还不便宜，但"让每条 AI 回答都能被验明正身"第一次在 4000 亿参数级模型上跑到了每秒百 token 量级，而且全套代码、论文和 Lean 证明都以 Apache 2.0 协议开源了。
相关链接
Anthropic 官方博客
https://www.anthropic.com/research/provable-inference
GitHub 仓库
https://github.com/anthropics/FlashProve
技术报告（PDF）
https://github.com/anthropics/FlashProve/blob/main/paper/paper.pdf
Steve Weis 原帖
https://x.com/sweis/status/2117485473497309299
