在当前的AI交互中，用户难以确认屏幕背后是否真的是指定的模型。路由服务商可能为降低成本替换为廉价小模型，黑客也可能篡改传输内容。由于仅凭生成文本无法识破替换，且普通用户缺乏算力重新运行开源权重进行验真，信任危机日益凸显。
针对这一痛点，来自Anthropic Frontier Red Team以及EPFL、MIT、StarkWare的研究团队正式开源了名为FlashProve的系统。该技术基于零知识简洁非交互式知识论证（zkSNARK），使模型服务商能在不泄露核心权重的情况下自证清白。
技术报告：
性能突破：单卡H100实现高效验证
FlashProve不仅在理论上可行，更在工程性能上实现了重大突破。团队在参数量达4000亿的MoE模型Llama 4 Maverick（激活参数约170亿，4比特量化）上完成了系统验证。
服务端表现
在单张英伟达H100 GPU加24核CPU的环境下：
- 生成证明速度：每秒110个Token。
- 证明文件大小：针对1024个Token长度的请求，证明体积仅约18.78 MB。
- 开销对比：生成证明消耗的GPU计算时间仅为同等任务纯推理耗时（基于vLLM引擎）的70到95倍。
客户端表现
用户验证无需GPU，仅需一台24线程的普通CPU电脑：
- 前置下载：约6.5 MB的模型承诺文件。
- 验证耗时：24线程下仅需17秒，单线程也只需21秒。
技术演进：从不可用到实用化
回顾机器学习零知识证明（zkML领域）的发展历程，此前的性能瓶颈严重阻碍了实际应用：
- 早期系统：证明小型卷积网络需数十秒。
- GPT-2（1.17亿参数）：每Token证明耗时159秒。
- GPT-2 XL（15亿参数）：Modulus Labs方案耗时超90小时。
- LLaMA-2（130亿参数）：2024年的zkLLM在A100上批量速度仅约每秒2.5个Token。
- Llama 4 Maverick（4000亿参数）：此前的VerInf系统处理1000个Token需在DGX Spark集群运行14.3小时，证明体积高达93.6 GB，验证需近一整天。
相比之下，FlashProve将证明开销压缩了两个数量级，证明体积控制在19 MB以下，验证时间缩短至十几秒，真正跨过了实用门槛。
核心原理：离线承诺与在线证明
FlashProve系统分为离线和在线两个阶段，并通过多项关键工程设计实现单卡高效运行。
两阶段流程
离线阶段：服务商将模型权重转换为密码学承诺（短指纹）。该计算每种模型仅需执行一次，耗时约39分钟，生成约6.5 MB的承诺文件，可支持约1600万次后续推理请求的验证。权重完全隐藏于承诺之后。
在线阶段：用户发送提示词，服务商返回结果及证明文件。该证明声明特定承诺模型在给定输入下精确生成了对应输出。任何人均可在不知晓权重、不使用昂贵硬件的情况下，于数秒内完成核验。
关键工程技术
1. 按需计算：证明耗时仅与实际激活的专家参数（约170亿）成正比，不为闲置专家浪费算力。零知识特性确保外界无法推断具体激活了哪些专家。
2. 后置批量证明：采用事后批量验证模式，一次性并行处理完整文本，类似预填充阶段。一个批次请求只需解开一次权重承诺，大幅降低重复开销。
3. 单GPU内存流式处理：将权重切分分段，按需逐段证明。权重主体常驻约290 GB主机内存，动态送入80 GB显存的单张H100，避免了多卡集群的通信瓶颈。
4. 底层数学结构：基于多项式交互式预言机证明（IOP），结合哈希函数编译，采用代码邻近度测试与查找论证等工具。不依赖传统可信设置，具备抗量子计算特性。
安全保障：形式化验证消除黑盒风险
鉴于密码学工程易存隐藏漏洞，且AI生成的优化代码难以人工审计，团队引入形式化验证语言Lean对整个协议和安全属性进行了严密描述。系统在随机预言机模型下满足三大核心定理：
- 完备性：诚实证明者生成的证明必被接受。
- 可靠性：伪造虚假结果的证明在密码学意义上无法通过验证。
- 零知识性：证明文件不泄露任何权重数值或专家激活路径。
开源交付物中不仅包含高性能C++验证器，还包含由Lean编写并通过定理证明的验证器，供用户机器级确认安全性。
应用场景：重建AI信任机制
FlashProve不仅是防伪工具，更解决了AI落地中的关键信任断点：
- 算力监管与合规：监管方可通过抽查零知识证明，远程核实厂商是否将算力用于指定推理任务而非违规训练下一代模型，且无需触碰商业机密。
- 服务器防篡改：若推理服务器被入侵或高能力模型试图替换低能力模型以规避监管，因无法生成合法的权重承诺证明，篡改行为将立即暴露。
- 文本溯源与责任认定：企业可附带证明确认代码或方案确经特定大模型审核。服务商甚至可提供“失败证明”，证实已耗费资源进行漏洞挖掘但未发现缺陷。
- 合规模型强制上岗：通过绑定每次请求与合规模型身份，从机制上杜绝使用未审核模型的情况。
当前局限与展望
团队指出，FlashProve目前仍为研究原型，存在以下边界限制：
- 确定性流程限制：系统基于整数算术和贪婪解码。虽然多数情况下与浮点运算输出一致，但在对抗性提示词下，浮点系统的随机采样输出可能与整数证明不对齐。
- 架构信息未隐藏：当前仅隐藏权重数值，模型网络架构公开。若需保密架构，需升级系统将其一并作为承诺目标。
- 侧信道风险：证明内容本身安全，但生成证明的时间微差等侧信道数据理论上仍可能泄露信息，当前版本未作防御。
- 上下文长度受限：单次支持最大1024个Token，远低于前沿模型的长文本需求。
- 代码等价映射：快速运行的C++代码与Lean规范之间尚未实现全自动机器级等价映射，快速程序仍需依赖人工审查。
开源资源
该项目核心成果已依照Apache 2.0协议公开发布，包括：
- 技术报告全文及协议设计文档；
- 完整可执行代码（含证明者、C++快速验证器、Lean形式化验证器）；
- Lean形式化证明源码及定理可视化交互审计工具。
source：
https://www.anthropic.com/research/provable-inference
--end--