调用云端大模型 API 的开发者，心里大多悬着块石头。你按旗舰模型的价格付费，却无法确认云端厂商有没有在流量高峰期偷偷把模型换成廉价的蒸馏版；安全公司宣称代码库经过了前沿模型扫描，客户也拿不到任何数学凭证。2026 年 11 月 2 日，Anthropic 发布了一套名为 FlashProve 的可证明推理原型系统与 23 页技术规范，试图给大模型的每次回答打上类似 DKIM 邮件签名的密码学防伪标。
想法很丰满，但连 Anthropic 自己都在博客里坦承，目前在内部或任何其他实验室均无部署计划。翻开 GitHub 上采用 Apache 2.0 协议开源的 0.16.0 版本代码库，它被明确标注为不维护的研究产物且不接受外部贡献。把纯密码学塞进百亿参数大模型，需要付出 70 至 95 倍 的算力代价和严苛的推理阉割，这套防伪体系离走出实验室还隔着一道商业鸿沟。
拆穿 110 tokens/秒：连 Anthropic 都不敢上线的算力账单
如果只看表面宣传，FlashProve 像是一件趁手的轻兵器。厂商预先用约 39 分钟离线生成一次模型权重的密码学承诺（即不暴露商业私有权重的指纹），就能支撑约 1600 万次请求后再重新承诺；用户在本地无需 GPU，就能核验某段文字是否出自该模型。
但算力账单立刻暴露了它无法上线的真相。Anthropic 的基准测试根本没用自家的 Claude，而是基于 4-bit 整数权重的开源模型 Llama 4 Maverick（总参数 400B，每 token 激活约 17B），跑在单张 80GB H100 GPU 加 24 核 CPU 上。与跑在 8 张 H100 上的 vLLM（FP8 权重）相比，FlashProve 的每 GPU 时间开销高達 70 至 95 倍——在批处理大小（batch size）为 24 时精确开销为 71.4 倍，对比最高测试负载则达到 93.0 倍，处理完一个 24 请求的批次要花掉约 223 秒。
更隐蔽的落差藏在吞吐量口径里。报告大字宣传的 110 tokens/秒（batch 24 下精确值为 111.23±0.92 tokens/秒），统计的其实是输入的上下文预填充（prefill）token 数，而且每个证明只校验 1 个预测出的 token。如果要老老实实校验模型回复里的每一个词，吞吐量会直接跌到 39.1 checked tokens/秒。
对客户端而言，这同样算不上轻量。每验证一次请求，用户得先下载一个 18.78 MB 的证明文件；用 C++ 验证器在 24 线程 CPU 上跑完需要 17 秒（单线程 21 秒）。如果追求真正的数学安全定理保障，改用 Lean 验证器去核验一个完整合成证明，耗时高达 24 分钟。没有任何一家商业 API 厂商能在亏损 70 倍算力的前提下，让用户等上十几秒去收一份近 19MB 的防伪回执。
被阉割的推理与分裂的代码：数学证明撞上工程现实
算力贵只是第一重障碍，更大的麻烦在于密码学喜欢绝对的确定性，而现代大模型天然是充满随机与近似的黑箱。
日常调用的商业大模型依赖浮点数运算，并靠温度（temperature）随机采样来保持回答的多样性，即便输入相同提示词，底层 GPU 硬件的浮点误差和动态路由也会让输出产生微小偏移。但 FlashProve 的精确匹配证明，只能死死锁住 1,024 tokens 上下文窗口内的 4-bit 整数模型，以及每次永远只选最高概率词的贪婪解码（greedy decoding），完全不支持带随机种子的采样解码和浮点数推理。
密码学要求毫厘不爽的确定性，而商业大模型活在浮点近似与随机采样里。
为了兼容真实服务里的微小差异，Anthropic 引入了一种叫 clipped-gap 的宽松验收策略。但这直接撕开了安全防线：当模型输出的词表得分较为平缓或阈值设得较宽时，该策略会放行大量非精确输出；更危险的是，宽松模式与严格精确模式在程序里同样返回退出码 0。下游开发者在集成时只要稍一疏忽没去解析策略字段，就会把放水后的结果当成数学级担保。
代码库文档还揭开了形式化验证与工程实现的脱节：
- 数学担保的断层.Lean 形式化证明只覆盖了协议定义和慢如蜗牛的 Lean 验证器，而真正跑进 17 秒的 C++ 验证器和底层 CUDA 证明器，并没有形式化等价保证。
- 权重隐私的敞口.对外宣传中津津乐道的零知识（不泄露模型权重）定理，仅在理论上覆盖了单次运行的 Lean 证明器，并未覆盖实际程序运行的批处理（batch）模式，且明确排除了时序侧信道攻击；工程级的权重隐藏目前只是研究者的预期，而非已证实的数学结论。
- 审计与复现缺失.GitHub 仓库缺失了原始运行记录、测量脚本和基准测试提示词；截至 2026 年 11 月 4 日，尚无任何独立第三方安全审计，所有测试与审查均由 Anthropic 内部团队完成。
- 风险.密码学承诺只能证明某次输出与某组已承诺的权重一致，却无法证明这组权重就是对外宣称的商业旗舰模型；若缺少外部权威机构的身份锚定，厂商依然能用小模型生成指纹并贴上旗舰标签。
信数学还是信英伟达：防伪暗战的现实出路
把视线拉回整个行业，为大模型验明正身目前有两条截然不同的技术路线在赛跑。一条是以英伟达 H100 机密计算为代表的硬件可信执行环境（TEE），另一条就是以 FlashProve 和零知识机器学习（zkML）为代表的纯密码学证明。
对于金融审批、网络安全扫描以及 AI 评测机构来说，弄清这两条路线的边界直接关系到采购与合规决策。FlashProve 的优势是不必信任 GPU 硬件厂商和云机房环境，但它除了算力贵得离谱，还不保护用户输入的提示词隐私。相比之下，硬件 TEE 性能损耗很小，能同时保护模型权重与用户数据，只是把信任根交给了芯片厂商的固件，且单纯的硬件证明需要上层可信应用配合才能绑定具体模型身份。
这并不意味着 Anthropic 做了一件无用功。在密码学与去中心化算力社区眼里，FlashProve 第一次将密码学可验证推理推向了 400B 总参数（17B 激活）的混合专家（MoE）大模型规模，其结合交互式预言机证明（IOP）、编码接近度测试与查找论证的架构，立起了一座重要的学术基线。
- 建议.高敏行业客户短期内切勿指望纯密码学防伪落地，采购审计仍需依赖硬件 TEE 机密计算与严格的合同罚则。
接下来真正值得紧盯的变量有三个：外部密码学学者对那套 Lean 形式化证明的独立审计结果、针对批处理模式权重泄露风险的实战攻击测试，以及学界能否在未来两三年内把 70 倍的算力开销压缩到 10 倍以内。在此之前，想在本地电脑上戳穿云端大模型的偷工减料，依然是一场昂贵的幻觉。