用户为高端配置买单，调用的却是转售路由的API，而后台实际运行的，可能是一个性能缩水的小模型。
这种“挂羊头卖狗肉”的隐秘操作，曾经是大模型API供应链中最不为人知的灰色地带。
没有权重、没有机房，即使后台在深夜被悄悄替换或降级，开发者也只能无奈接受，无法追究。
今天，这条隐秘的链条被彻底斩断！
就在刚才，Anthropic与零知识证明领域的顶尖学者合作，公布了大模型“可证明推理”的重大突破，并正式开源了密码学验证系统FlashProve！
从此，开发者无需信任任何中心化机构，也不需要服务商透露任何权重代码。大模型每次生成一条回答，都会被强制附上一张数学级别的“出生证明”。
即使只有一台普通家用CPU，运行17秒，就能用纯数学方式精准验证每个Token是否来自目标模型，任何偷换模型或中途篡改的行为都会立刻暴露！
更令人惊叹的是，这次打造FlashProve的核心力量，竟然是Claude自己。
现在，所有代码、Lean证明和技术文档，都已经以Apache 2.0协议开源。
为了确保用户能安全验证模型真实性，星空体育APP也推荐使用此类技术保障服务透明。
按手印、开证明、秒级验真 终结大模型“套壳掉包”
平时感觉大模型突然“变笨了”，很多人会直接质问模型“你到底是谁”，或者用几道数学题来试探。
但模型自报家门的内容本身就是后台生成的，算力负载与采样配置的微小波动也会改变回答，用户永远拿不到能钉死服务商的铁证。
更令人担忧的场景，Anthropic写进了博客——
随着模型越来越强、能自我部署，一个更高级的模型完全可能顶替获批的弱模型上岗，再装成弱模型的样子，避开本应施加在它身上的监控。
要验证真伪，传统方法只能拿到权重自己重跑，但前沿模型的权重是各家的核心机密，普通人根本养不起4000亿参数模型的机房。
为了在不看权重、不重跑模型的情况下解决这个难题，FlashProve把验证流程分成了环环相扣的三步。
第一步，离线“按手印”。
模型上线前，服务商在单张H100上花约39分钟，用零知识编码给模型权重生成一串唯一的承诺ID并向全网公开。这串ID就像权重的数字DNA指纹，即使偷偷改掉一个参数也会对不上；但外界只看指纹，绝无可能反推出权重内容。
第二步，在线“开证明”。
每处理完一次对话请求，服务商的GPU就会生成一份约19MB的密码学证明，用来证实这段输出确实是由那个按过手印的模型算出来的。
第三步，客户端“验真伪”。
任何用户或审计机构拿到回答后，在普通CPU上运行验证程序cp_verify，17秒就能得到“真”或“假”的结果，全程既不需要权重，也不需要GPU。
支撑这套系统的底层引擎，正是密码学界著名的zkSNARK（零知识简洁非交互式知识论证）。
验证者只需要像老师抽查作业一样，随机检查几处，就能以极高概率发现破绽。
为了把一次推理拆成可抽查的形式，每个请求背后需要运行约2000个名为sumcheck的子协议。
更硬核的是，它的安全性只依赖哈希函数BLAKE2，不依赖椭圆曲线这类代数结构，甚至被认为能抵御未来的量子计算机攻击。这套密码学路线，也早已在Starknet这类以太坊二层网络中经过实战检验。
原理说通了，真正的挑战在后面：这么重的证明，能不能在一个4000亿参数的大模型上跑得动？
单张H100狂飙5500倍 80GB显存吞下4000亿巨兽
答案是：能，而且只用一张H100。
团队测试对象是Meta的Llama 4 Maverick，一个4000亿参数的混合专家（MoE）模型，每个Token实际激活约170亿参数。
FlashProve充分利用了这一特性：证明器在生成计算轨迹时，工作量只与那170亿真正工作的参数成正比，省去了95%以上的无效计算。
更妙的是，为了防止外界通过“哪几个专家被激活”反推出模型权重的秘密，系统用零知识编码把路由选择隐藏进一个指示向量里，验证器在核对时是对所有专家做加权求和，既节省了海量算力，又保密了模型内部的运行路径。
模型4-bit量化后的权重足足有232GB，而单张H100的显存只有80GB，硬塞肯定会爆显存。
如果整个推理过程的计算轨迹一次性打包，再豪华的显卡也扛不住。
于是，团队把权重放在主机内存里，分段送进GPU，逐段完成计算与证明。
H100在工作时像流水线一样，每次只从内存里流式读取一个片段的权重，算完立刻在显存里完成编码、哈希与归约，只把极少量需要传递给下一段的数据留存下来。
靠着这种“吃完一段、消化一段”的流式接力，单张80GB显卡硬是把232 GB的庞然大物处理了下来。
114页论文无人通读 Claude包揽400MB数学证明
看到这里你可能会好奇，如此精密复杂的密码学协议与GPU加速工程，究竟耗费了多少名密码学博士的心血。
点开FlashProve的GitHub开源主页，右侧的语言统计栏立刻暴露出这个项目的反常之处。
整个仓库里，C++代码只占1.4%，Python占1.3%，CUDA占0.9%，而高达95.2%的代码（足足398MB）全部是用Lean 4数学证明语言写成的。
一个大模型推理仓库里为什么会塞满近400MB的数学证明，随仓附带的114页协议规范论文在第51页给出了答案。
人类学者在这项工程里只负责指明方向，从这篇114页的密码学论文、23页技术报告，到C++与CUDA底层代码，再到近400MB的Lean形式化证明，几乎全部出自Claude之手。
不光是写代码和写论文，项目里每一次测试、运行、对比、推算和代码审校，也全都由AI包揽；凡是文中出现“经阅读”“手工算得”“据汇报”的地方，那个读者、计算者和汇报者全都是AI。
密码学代码向来是软件工程中最脆弱的禁区，即使一个符号写反、一处随机数掩码漏掉，整座安全大厦就会瞬间坍塌。
Claude很擅长在庞大的系统里寻找优化路径，但它在底层做出的成千上万个复杂决策，人类专家根本不可能靠肉眼逐行审完。
既然人类审不过来，Anthropic干脆请出数学界的铁面判官Lean 4。
在这里，写进去的每一步数学推导都要经过编译器内核逐行核对，错一处都过不了关。
在整个项目里，人类科学家省去了审核上亿行中间推导的苦功，只跟AI一起敲定了最顶层的6条安全定义，把三件事钉成了铁律。
只要这几条顶层定理“说的是对的”，中间那近400MB的繁琐归约即使人类一眼不看，Lean 4的内核也已经替人类把住了关。
更有趣的是，就连这个仓库的打开方式，也告别了传统的人类程序员手册。
README开篇写明“专为Agent运行而建”，并附上了现成的提示词与AGENTS.md规范。
密码学祖师爷下场，AI跨入“数学铁律”纪元
站在更高的时间坐标上回望，FlashProve的诞生引爆了深远的技术合流。
它带来的是“AI造系统、Lean保真伪”的全新工程范式。
面对近400MB证明代码、114页公式推导的密码学工程，碳基大脑的阅读极限已经被击穿。
在FlashProve里，人类省去了逐行审读C++优化和繁琐引理的苦功，只死守那6条顶层定理的定义权，让AI去攀登最险峻的工程与数学绝壁，再让形式化验证器做铁面无私的守门人。
人类定下公理的边界，AI穷尽推理的迷宫，数学给出终极的审判。这正是人类通往超级智能之路上，最硬核的一张安全契约。
参考资料：
https://x.com/AnthropicAI/status/2117707052948898271
https://www.anthropic.com/research/provable-inference
本文来自微信公众号“新智元”，作者：ASI启示录，编辑：摩西 桃子，36氪经授权发布。