--- layout: post.njk source: https://yage.ai/share/anthropic-flashprove-provable-inference-20261108.html web_feed: articleId: cmw8gz6t20000yhedh84dltgn feedSourceId: webfeed_yage_ai guid: https://yage.ai/share/anthropic-flashprove-provable-inference-20261108.html sourceUrl: https://yage.ai/share/anthropic-flashprove-provable-inference-20261108.html speaker: yage.ai title: |- Anthropic 开源大模型验钞机 FlashProve：为什么它能抓死中转站换模型，却管不了官方降智 date: '2026-11-08' summary: Anthropic 开源了 FlashProve，一个可证明推理原型，它能通过零知识证明技术，让用户在不拥有模型权重和显卡的情况下，从数学上验证大模型回答的来源，从而抓包中转站的掉包行为，但目前无法监管大厂的暗中降智。FlashProve 的工作流程包括服务商离线打封条生成公开权重指纹，以及用户在普通 CPU 上对证明文件进行验证。尽管生成证明消耗算力巨大，但通过优化策略，FlashProve 实现了单卡上的高速度，并能通过将证明服务器与线上推理分离来提升并行吞吐。文章指出，尽管数学上难以造假，但线上浮点数和证明器整数模型之间的误差、隐藏思维链的限制以及权重指纹的更换周期等因素，使得该工具目前无法完全检测大厂的暗中降智。 area: tech-engineering category: ai-application tags: - ai-application - zero-knowledge-proof - model-verification - flashprove - model-security people: [] companies_orgs: - Anthropic - Meta products_models: - Llama 4 Maverick - Claude media_books: [] draft: true status: evergreen --- 日常使用大模型 API 或者官方订阅，我们经常会怀疑两件事。第一是第三方中转站为了节省成本，可能把最好的模型换成了次好的或者阉割版。第二是大公司为了节省成本，可能在算力高峰期偷偷降级。但这两件事情以前都没有人能举证，因为光从结果上看无法确定是不是同一个模型，同时因为闭源拿不到模型权重，普通人手里也没有那几百张显卡去重跑复现。 11 月 2 日，Anthropic 开源了可证明推理原型 FlashProve，相当于给 AI 造了一台数学验钞机。哪怕你看不见权重，没有显卡，只要用普通的 CPU 花 17 秒，就可以从数学上验证这段回答到底是哪个模型算出来的。但看完同时发布的 23 页技术报告，你会发现这个验钞机可以抓包中转站掉包，却无法监管大厂自己的暗中降智。 ## 不交出商业机密的模型权重，怎么向用户自证清白 许多开发者看到的第一反应是怀疑：如果权重不能公开，普通电脑又没有显卡，凭什么普通处理器可以检测出远端服务器是否在算假账？FlashProve 引入了零知识证明，这是一种不暴露商业机密权重、但从数学上可以证明计算过程没有做假的技术。整个防伪的流程可以分为两步。 第一步，服务商离线打封条。他们在自己的程序里把几千亿个权重参数跑 39 分钟后，得到一个大约 6 MB 的公开权重指纹。只要改动一个参数，算出来的指纹就会完全不同，但它本身不会泄露权重内容。 第二步是随结果开收据。处理请求时，服务商把模型每一层的算术结果和选词过程打包成一份约 19 MB 的证明文件。用户拿到这张防伪收据后，在 24 核处理器上跑 17 秒验证程序，就能抽查完里面的数学咬合关系。一旦哪一步换了权重或跳过了计算，收据里的数字链条就会断裂。 这时候，中转站事后补票的伎俩就无效了。比如中转站平时用小模型糊弄用户，吐出的答案是甲。到抽查要证明时，它再去用真模型补算出证明。这在数学上是走不通的，因为证明文件绑定了输入提示词、权重指纹和唯一输出之间的对应关系。真模型算出来的回答乙即便和回答甲只差一个标点，也生成不出指向回答甲的合法证明。如果中转站偷偷截断长提示词，或在后台塞了一句要求简短回答的隐藏指令，用户用原始提示词去跑验证程序，从第一层运算开始就会报错。 当然，开这张数学收据不便宜。生成一份证明消耗的算力比直接使用开源推理引擎 vLLM 进行普通推理高 70 到 95 倍。日常对话不可能每个句子都开发票，它的主要用法是在事后进行抽查。只要买方或评测机构在合同中保留一小部分事后的抽查权，中转站事先不知道哪些请求会受到抽查。一旦造假在抽查里败露，就会留下铁证，偷换模型省下的电费抵不上违约代价。 FlashProve 两步验真机制与中转站事后补票露馅过程 ## 以前算一份证明要十几个小时，为什么现在一张显卡就能跑动 即便比一般的推理慢了近百倍，FlashProve 仍然是一个非常难实现的工程。Anthropic 这次选用 Meta 开源的模型 Llama 4 Maverick 作为基准模型；在之前的开源系统中，只有 VerInf 在这个模型上做过证明，在高端算力机上要花 14.3 小时才能跑完单次基准证明，整个证明文件大小 93.6 GB，验证一次还要花接近一天时间。 相比之下，FlashProve 用单卡把同款模型的证明速度推到了每秒 110 个词元，速度和文件大小都改善了大约 5000 倍。能在单卡上达到这样的速度，团队主要做了两个顺应硬件的工程取舍。 第一个策略是顺应混合专家模型的稀疏性，只证明真正用到的那一部分参数。这个模型共有 4000 亿个参数，但每层有 128 个路由专家，每次处理一个词元时只会激活一个路由专家和共享专家，因此只有 170 亿个参数真正参与了运算。 FlashProve 生成证明文件时，只把实际运行的那一个专家的计算过程写进收据，同时用密码学遮掩把具体选了几号专家藏起来。证明器的工作量直接跟着激活参数走，省掉了九成以上的陪跑计算。再配合把 232 GB 模型权重放在主机普通内存里、按层分段流式读入 80 GB 显卡显存的做法，单张显卡就能装下整套流程。 第二个取舍是放弃边吐字边证明，改成等整段话写完后再一次性并行重算。大模型线上推理分两步：第一步叫预填充，是模型一次性读完输入提示词的阶段，主要吃显卡算力；第二步叫解码，是模型一个字一个字往外吐回答的阶段，主要卡在显存带宽上。如果边吐字边生成证明，不仅会和线上推理抢显存带宽，而且会让串行吐字的速度卡死。 FlashProve 干脆分头处理：线上服务器先照常给用户返回答案，证明服务器则在后台拿整个对话历史把结果重算一遍。因为整段回答已经生成，证明服务器可以用提示词加回答当做一个完整的预填充一次性并行计算，还可以把 24 个请求聚合成一批，整个批次只拆包一次权重指纹。重算一遍模型只占证明总开销的 1% 到 1.5%，但带来了并行吞吐的大幅提升。 在技术报告中，他们详细解释了上面那个跑分速度是怎么算出来的。虽然证明器可以检验任意多个词元，但它必须对整个 1024 词元窗口的输入和输出进行计算。因此，官方基准测试默认只检验紧跟在提示词之后的第一个词元，再用整个窗口内所有词元的数量来折算速度。如果启用全检模式，对每一个回复词元都做检验，总时间几乎不变，但只按实际检验的回复词元数量来算，有效速度就变成了每秒 39.1 个词元。 ## 既然数学上没法造假，为什么还是抓不住大厂自己的暗中降智 理解了这套机制以后，很多开发者最想知道的是：能不能用这个验钞机去测测 Anthropic 本身，看在算力高峰期 Claude 有没有变傻？不过技术报告的三处技术细节说明，目前还做不到。 第一个坑是线上浮点数和证明器整数模型天然有误差。生产环境为了兼顾精度和速度都跑 FP8 这种浮点数。但显卡跑浮点数加法不满足结合律，不同批次大小或者不同芯片算出来的分数会有微小抖动，没法直接做数学证明。为了绕过死结，FlashProve 证明的是一套转成整数的影子模型。 问题是，即使官方完全诚信，线上浮点数模型输出的词元和事后整数模型计算的词元，本身就会在某些得分相近的词元上产生差异。报告附录采用的方法是再做一层基于近似平局的统计检测，如果差异的词元在整数模型里恰好是得分很接近第一的亚军或季军，就认为是正常的浮点误差。这样的设计天然允许一定程度的精度损失。 第二道门槛是协议锁死了选词方式和 1024 词元的短窗口，管不住隐藏思维链预算。为了让重算结果固定，协议要求模型每次必须选得分最高的词元（贪心解码），相当于把采样温度锁死为 0。平时我们使用 Claude 写代码或做推理，上下文动辄几十万词元。而且高峰期降智往往不在于换了底层权重，而是服务端压低了隐藏思考过程允许消耗的词元上限，或在超长上下文里做了截断。只要隐藏思维链不完整公开并纳入证明，短窗口就够不着这些地方。 第三道门槛是权重指纹每 1600 万次请求就得更换。为防止外界搜集大量证明文件反推权重，每个离线权重指纹至多支撑约 1600 万次请求，到期需重算。对一线大厂而言，这点额度几个小时就能耗尽。如果官方借着日常小版本更新直接发布一串全新的根指纹，密码学只能保证你今天调的是新指纹对应的模型，却无法担保新指纹背后的模型没有比上个月那版缩水。 线上浮点模型与证明器整数影子模型的双轨误差及放行窗口 ## 用 Claude 写的代码来审计 AI，它真正的落点在哪 除了算法边界以外，这个版本号为 0.16.0 的原型还有一个有趣的实现细节。防伪协议的底层数学规则非常繁琐，如果直接手写底层 C++ 代码，人类密码学家很难靠肉眼排查里面有没有安全漏洞。所以团队索性反其道而行之，先用一种用来检查数学推理的编程语言 Lean，把核心防伪规则写成一份数学母本。这种语言的编译器就像一个铁面无私的阅卷机器一样，只要编译通过，就能在数学逻辑上锁定顶层防伪定理没有漏洞。 然后，他们又让 Claude 根据这个数学母本自动翻译出显卡上运行的 C++ 证明器、处理器上运行的 C++ 快速验证器，甚至 FlashProve 开源代码仓库中的长版协议规范文档也是用 Claude 翻译生成的。人类作者在报告中坦言，长版协议文档尚未仔细审阅，C++ 代码与 Lean 数学母本是否完全一致也未完成证明。这就让人疑惑了：用一套 AI 翻译出来的、作者都没彻底审完的代码来抓作弊，万一 Claude 翻译错了怎么办？ 但为什么他们敢这么干呢？这其实是把服务商机房里的证明器跟用户电脑里的验证器职责分开，把翻译出错可能带来的三种后果给彻底切割开了。第一种错误是，服务商机房里的 C++ 证明器翻出了算术漏洞，导致真模型算出来的收据过不了检验。这种不涉及黑客作弊，用正常的请求跑一遍软件测试，看收据能不能验过，当场就能抓出来。 第二种错误是证明器在批处理模式或 C++ 翻译过程中漏掉了随机掩护，导致收据不小心暴露了模型权重的某些信息。目前团队在 Lean 母本里只证明了单条请求不会泄露权重，批处理模式下的防泄露证明还没写完，而且证明器要处理几千亿参数的模型，计算量非常大，无法直接使用 Lean 母本进行运算。但是，如果权重发生泄露，只会对服务商自身的商业机密造成影响，而不会对用户造成收到虚假回答的伤害。这个开源 demo 使用的是 Meta 公开的开源权重，所以不用担心权重泄露的问题。如果未来有厂商希望使用这个工具保护自己的闭源模型，就需要补全证明并聘请安全专家来检查证明器的代码。 第三种且用户唯一关心的风险是：服务商能否利用代码的缺陷来伪造一个假的收据欺骗用户？这种情况是不会发生的。因为决定收据是否真实的标准，完全由用户的电脑上的验证器说了算。只要用户使用的验证器本身是正确的，即便服务商那边的证明器写得再烂，也无法产生能欺骗用户的假收据。那万一用户手里的 C++ 快速验证器本身有错误怎么办？考虑到验证器的计算量很小，团队提供了双重保障：除了 C++ 快速验证器，他们还把通过数学检查的 Lean 母本直接编译成一个纯 Lean 的慢速验证器。在正常抽检的情况下使用 C++ 快速验证器，同时在测试集上确认它与 Lean 验证器结果相同；如果遇到正式的合规审计、法律诉讼或者对 C++ 翻译的担忧，审计方完全可以跳过 C++ 版本，直接使用纯 Lean 的慢速验证器。这样就能规避 AI 翻译可能产生的错误。 而在研究博客的脚注中还提到了 Anthropic 自己的内部路线。他们在安全路线图中曾提到要在今年 9 月 30 日之前实现验证推理流量的原型系统。但在脚注中又透露，内部其实已经用了一个更简单的方案提交了答卷：直接在推理流量上加签，在受信任的内部服务器上重复跑一遍，就能防范黑客入侵自家服务器或窃取权重。 理解了这两条路线各自的分工，就能理解 FlashProve 的真实定位。高额的算力成本决定了它不太可能成为一个普通用户每次聊天都能用到的实时开关，而更像一个悬在算力托管商、中转平台和刷榜方头顶的事后抽检工具。一旦买方或者评测机构掌握了随时对一小批历史请求发起事后验算的能力，黑盒接口时代全凭服务商良心的博弈规则就发生了改变。