Anthropic开源大模型验真工具FlashProve

你现在在网页或调用接口跟大模型聊天，根本没办法确认背后回复你的，到底是不是你指定的那个模型。

面对面跟真人沟通，你可以看对方的长相、听声音、握手确认身份。

但面对屏幕里的AI，你几乎没有任何手段核实对方的真实底细。

路由服务商为了压低成本，可能偷偷把后台换成便宜的小模型。

黑客可能在传输链路上做手脚，篡改返回的内容。

只看生成文本的质量，你完全无法识破这些替换。

就算厂商开源了模型权重，普通用户和审计机构也没有足够的算力把模型重新跑一遍来验真。

现在，密码学方案给出了解决路径。

来自Anthropic Frontier Red Team以及EPFL、MIT、StarkWare的研究团队，正式开源了一套名为FlashProve的系统。

技术报告：

它通过零知识简洁非交互式知识论证（zkSNARK），让模型服务商既能自证清白，又完全不会泄露商业核心的模型权重。

FlashProve不仅把这套方案做出来了，还把运行速度推到了前所未有的工程水准。

团队在Llama 4 Maverick上完成了系统验证。

这是一个参数量达4000亿的MoE（混合专家）模型，激活参数约170亿，使用4比特量化权重。

在单张英伟达H100 GPU加24核CPU的环境下：

FlashProve生成证明的速度达到了每秒110个Token。

针对1024个Token长度的请求，最终生成的证明文件大小只有约18.78 MB。

对比开源推理引擎vLLM运行同等任务的纯推理耗时，生成证明所消耗的GPU计算时间只有后者的70到95倍。

而在客户端这一侧：

用户验证证明不需要任何GPU，只要一台24线程的普通CPU电脑。

先下载大约6.5 MB的模型承诺文件。

随后验证一个请求的证明，在24线程下耗时仅需17秒，单线程也只要21秒。

以前的方案有多慢？

在机器学习零知识证明（zkML）领域，过去的性能数据让很多实用场景望而却步。

早期的系统证明卷积小网络都要数十秒。

后来扩展到Transformer架构：

证明1.17亿参数的GPT-2，每生成一个Token的证明需要159秒。

Modulus Labs证明15亿参数的GPT-2 XL，耗时超过90小时。

2024年的zkLLM在A100上证明130亿参数的LLaMA-2，批量速度只有每秒约2.5个Token。

此前唯一公开针对Llama 4 Maverick 4000亿模型的验证系统VerInf：

处理1000个Token需要在DGX Spark集群上跑14.3小时。

生成的证明体积高达93.6 GB。

光是验证这个证明，就要耗去将近一整天。

而FlashProve单张H100跑出每秒110个Token，证明体积压缩到19 MB以下，验证只需十几秒。

这项技术跨过了实用门槛，证明开销被压缩到两个数量级以内。

FlashProve是怎么做到的？

整套系统分为两个阶段：

离线阶段：

服务商把模型权重转换成一个短指纹，也就是密码学意义上的承诺。

模型权重完全隐藏在承诺背后。

这个离线计算每种模型只需跑一次，耗时约39分钟。

生成的承诺文件大小约6.5 MB，足够支持大约1600万次后续推理请求的验证。

在线阶段：

用户发送提示词，服务商返回结果，并随附一份证明文件。

这份证明向所有人宣告一个确定事实：

就是这个公布了承诺的模型，在输入该提示词后，精确生成了这串输出内容。

任何拿到证明的人，不需要知道权重，也不需要昂贵硬件，几秒钟就能核验真伪。

为了让庞大的计算塞进单卡，团队做出了几项关键工程设计：

第一，计算量只跟随实际激活的专家走。

4000亿参数的MoE模型，每个Token实际上只调用约170亿参数。

FlashProve的证明耗时严格与实际工作的170亿参数成正比，不会为闲置专家浪费算力。

同时，零知识特性确保了外界无法从中推断出究竟激活了哪些专家。

第二，后置批量证明。

团队没有选择边推理边出证明的实时模式，而是采用事后批量验证。

系统一次性并行读取生成好的完整文本，像预填充阶段一样高效处理。

一个批次的请求只需要解开一次权重承诺，大幅削减了重复开销。

第三，单GPU内存流式处理。

每层的权重被切分成若干分段，按需逐段证明。

权重主体常驻在约290 GB的主机内存中，动态送入80 GB显存的单张H100，避免了多卡集群的通信瓶颈。

底层数学结构上，FlashProve基于多项式交互式预言机证明（IOP），结合哈希函数进行编译。

它采用了代码邻近度测试与查找论证等现代密码学工具，不依赖传统可信设置，且具备抗量子计算特性。

用形式化验证解决密码学黑盒

密码学工程极易出现隐藏漏洞。

在FlashProve开发过程中，Claude协助完成了大量优化，但AI生成的复杂优化代码往往难以依靠人工轻松审计。

为了确保安全根基，团队引入了形式化验证语言Lean：

对整个协议和安全属性进行了严密的形式化描述。

证明在随机预言机模型下满足三个核心定理：

完备性：诚实证明者生成的证明一定会被验证者接受。

可靠性：伪造虚假结果的证明，在密码学意义上不可能通过验证。

零知识性：证明文件除了证明计算正确，不会泄露任何权重数值或专家激活路径。

开源交付物中，除了常规的高性能C++验证器，还包含了一个完全由Lean编写并通过定理证明的验证器。

用户可以用这个形式化验证器，机器级地确认自身安全不受损害。

为什么大模型需要证明推理？

这项技术不仅仅是一个防伪工具，它直击当前AI落地过程中的几个重大信任断点：

计算调配监控与发展节奏管控：

监管如果要求厂商把算力用于推理而非违规训练下一代超级模型。

厂商不能偷偷用小模型应付用户，把算力挪去训练。

监管方可以通过抽查零知识证明，远程核实算力是否确确实实跑在指定推理任务上，同时不必触碰厂商的商业模型秘密。

服务器防篡改与恶意自替换：

一旦推理服务器遭受外部入侵，或者未来高能力模型试图暗中替换掉低能力模型来规避行为监管。

没有正确的权重承诺，任何被替换的模型都无法生成合法的证明，篡改行为会当场暴露。

文本来源溯源与失败证明：

企业对外宣称某份代码已经通过前沿大模型的安全扫描，或者某份商业方案已经通过顶级模型审核。

客户可以通过附带的证明确认此话当真。

甚至，服务商可以给出失败证明，向客户证实自己确实耗费了数百万Token进行漏洞挖掘，但该模型确实没有找到缺陷。

合规模型上岗保障：

监管要求特定场景必须使用经过安全备案的合规模型。

挂载证明能够强制绑定每次请求与合规模型身份，从机制上杜绝偷跑未审核模型。

当前局限

团队明确指出，FlashProve目前仍然是一个研究原型，存在若干边界限制：

首先，系统证明的是基于整数算术和贪婪解码的确定性流程。

实际大模型推理通常依赖浮点数并包含随机采样。

虽然整数运算与浮点运算在绝大多数情况下输出一致，但面对对抗性诱导提示词时，浮点系统的随机输出可能无法对齐这里的整数证明。

其次，架构信息并未隐藏。

当前系统只隐藏权重数值，但模型的网络架构对外界是完全公开的。

如果厂商需要连同模型结构一起保密，系统需要升级为将架构和权重一并作为承诺目标。

第三，侧信道分析未被覆盖。

证明内容本身不泄露权重，但生成证明所耗费的时间微差等侧信道数据，理论上仍可能带来信息外泄风险，当前版本未作防御。

第四，上下文长度受限。

目前系统单次支持的最大上下文长度为1024个Token，远低于当前前沿模型数十万乃至数百万Token的长文本需求。

最后，快速运行的C++代码与精细的Lean规范之间，目前尚未实现全自动机器级代码等价映射，日常使用的快速程序依然需要依赖人工审查代码实现。

开源清单

目前，该项目的所有核心成果已经依照Apache 2.0协议全部公开发布。
包括：

技术报告全文；

协议设计文档；

包含证明者、C++快速验证器、Lean形式化验证器的完整可执行代码；

Lean形式化证明源码以及定理可视化交互审计工具。

source：

https://www.anthropic.com/research/provable-inference