Anthropic 发布了可证明推理研究原型 FlashProve，面向大型混合专家（MoE）模型，用 zkSNARK 密码学证明帮助用户核验回答是否来自指定模型，同时隐藏模型权重。其代码、Lean 证明和文档以 Apache 2.0 许可开源。这项研究针对的是模型调用中的信任问题：仅凭回答内容，用户难以确认服务方实际运行的是否为其声称的模型。
FlashProve 分为离线和在线两个阶段。模型提供方先发布对权重的「承诺」，相当于锁定一组确切权重的指纹，随后为推理结果生成证明。持有承诺、提示词和回答的人，可以在不获取权重的情况下检查结果。
Anthropic 列出的潜在用途包括第三方模型评估、核验路由服务是否调用了用户选择的模型，以及检测输出被篡改。系统采用事后证明：读取已经完成的文本，批量生成证明，因此核验保障存在延迟。
测试使用 4 位量化的 Llama 4 Maverick。这是一个约 4000 亿参数的 MoE 模型，每个 token 约激活 170 亿参数。发布方自测显示，单块 H100 配合 24 个 CPU 核心，证明吞吐量约为 110 token/秒；每个 1024 token 请求对应的证明大小为 18.78 MB。
作为对照，Anthropic 使用 8 块 H100，通过 vLLM 运行同一模型的 FP8 版本。按 GPU 时间计算，24 个请求一批时，生成证明的开销约为普通推理的 72 倍，多次运行结果为 66 至 77 倍；在所测 vLLM 最高负载下，这一比值约为 94 倍。
验证端无需 GPU。据发布方测试，验证者需下载约 6.5 MB 的承诺，检查一份证明在 24 线程 CPU 上耗时 17 秒，单线程为 21 秒。每个模型的离线阶段耗时约 39 分钟，所得承诺可用于约 1600 万次请求，之后需要重新生成。
此次发布内容包括技术报告、由 Claude 撰写的协议规范、证明器、C++ 快速验证器、Lean 可证明正确验证器，以及顶层数学命题的 Lean 证明和交互式可视化工具。
Anthropic 表示，Claude 擅长优化，但其在复杂系统中的决策往往难以评估，因此团队用 Lean 提供可审计的顶层安全声明，涉及完备性、可靠性和零知识三项性质。不过，形式化证明并未消除所有信任缺口：发布方不保证 Lean 协议、论文和高性能代码三者完全一致，C++ 验证器也没有形式化保证。
FlashProve 仍是研究原型。它证明的是整数化模型在贪心解码下的结果，浮点实现或采样解码的回答可能与之不一致；当前支持的上下文最长为 1024 token。隐藏模型架构不是系统目标，通过证明耗时等信息进行的旁路攻击也不在本次发布的保障范围内。
