Anthropic 开源 FlashProve 研究原型：用密码学证明回答来自指定模型

要证明的是计算来源，而不是答案是否正确

Anthropic 11 月 2 日公开 FlashProve 研究，关注一个模型服务中的信任问题：用户收到回答时，怎样核对真正执行计算的权重与服务商声称的模型一致。仅凭回答风格或质量猜模型，并不能提供这样的保证。

FlashProve 的目标是让提供方给出可验证的密码学证明，用户不必获得模型权重或重新运行整个模型，就能检查约定的输入、输出与权重承诺是否对应。它证明计算关系，不证明回答内容客观正确，也不能把通过验证理解成模型没有幻觉。

提供方先承诺权重，再为推理结果生成证明

研究把流程分为离线和在线阶段。离线阶段由提供方发布一个绑定特定权重的简短承诺，权重本身保持隐藏；在线阶段则围绕输入与输出生成证明，验证方利用承诺、提示和回答检查指定计算是否成立。

这意味着方案需要提供方参与，先有可信对应的权重承诺，再有可核验的证明文件。它不是只向陌生 API 问几道题就自动识别后台模型的工具，也不能从一个没有承诺和证明的普通聊天记录中，补造出相同等级的密码学保证。

开源材料覆盖协议、执行代码和 Lean 形式化工作

Anthropic 发布的材料包括技术报告、协议说明、执行代码、证明器和验证器，以及 Lean 证明和帮助审计的交互可视化工具。官方表示，代码、Lean 证明与文档采用 Apache 2.0 许可，并邀请其他研究者继续检查和改进。

许可范围需要与测试所用模型分开。研究使用 Meta 的 Llama 4 Maverick 量化权重，权重不包含在此次发布中，读者需要按相应模型条款另行获取。开源证明代码不意味着测试模型本身也改成 Apache 2.0，更不代表无需计算资源即可完整复现。

证明生成仍明显比普通推理昂贵

官方实验围绕四千亿参数的 Llama 4 Maverick MoE 模型，使用四位量化权重及特定整数计算路径。论文网页报告了单张 H100 上的证明生成表现，同时明确相对于 vLLM 普通推理仍存在显著 GPU 时间开销，不能把证明吞吐当成聊天服务的推理速度。

这类比较依赖量化方式、批量、上下文及验证对象，不能抽出一个速度数字后推广到所有模型。本文没有复现实验，也不将不同模型、硬件或早期系统的结果拼成独立性能榜单；读者应沿原研究的实验条件和技术报告核对成本。

整数模型、贪心解码与短上下文构成当前边界

研究明确，此次证明针对权重的精确整数版本，并核验所检查 Token 是否是该模型的贪心选择。浮点实现或采样解码的回答可能偏离这个计算路径，因此不能直接把原型的保证套到所有商用服务的实际输出。

当前系统验证的上下文长度上限为一千零二十四 Token，远短于许多真实长对话。研究还不隐藏模型架构，侧信道攻击也不在本次保证范围。这些限制不否定原型价值，但决定了它距离广泛接入现有生产模型还有工程与研究工作。

形式化证明也不能替代对实现和假设的审计

Anthropic 同时提供 Lean 验证器与较快的 C++ 验证器，并指出快速执行代码不具备同等形式化保证。形式化陈述是否准确表达目标、执行代码是否与协议对应，仍存在需要审查的信任环节，不能简单写成全部代码已被数学证明绝无漏洞。

因此，这次公布的是可证明推理的阶段性研究成果，而不是 Anthropic 已经给每次 Claude 回复附上证明的产品公告。对使用模型网关和第三方路由的开发者来说，它提供了一条更强的完整性验证方向，但实际采用仍要等待模型支持、承诺分发、证明成本和审计流程共同成熟。

继续阅读