Anthropic亲手终结「套壳AI」！17秒扒下假模型头套，验身速度快5000倍

掏的是顶配旗舰的钱，调的是转售路由的API，后台真正干活的却可能是缩水的小模型——这种大模型API供应链的暗箱操作，如今被Anthropic斩断。Anthropic联手零知识证明领域学者，公布大模型「可证明推理」突破，开源密码学验真系统FlashProve。开发者无需信任中心化机构，也无需服务商交出权重代码，模型每生成一条回答都会被附上一张数学级「出生证明」。普通家用CPU跑17秒，就能用纯数学方式验证每个Token是否出自目标模型，偷换模型、半路篡改将当场现形。所有代码、Lean证明、技术文档均以Apache 2.0协议开源。

传统验真需拿到权重重跑，但前沿模型权重是各家命根子，普通人也养不起4000亿参数模型的机房。FlashProve把验真拆成三步：第一步离线「按手印」，模型上线前服务商在单张H100上花约39分钟，用零知识编码给权重生成唯一承诺ID并公开，类似数字DNA指纹，改一个参数都对不上，外界也无法反推权重；第二步在线「开证明」，每处理一次请求，GPU顺手生成约19MB密码学证明，证实输出由按过手印的模型算出；第三步客户端「验真伪」，用户或审计机构在普通CPU上运行cp_verify，17秒拿到真或假判决，全程不要权重和GPU。

底层引擎是zkSNARK，验证者随机抽查几处即可以极高概率抓到破绽。每个请求背后要跑约2000个sumcheck子协议。其安全性只依赖哈希函数BLAKE2，不靠椭圆曲线，被认为能扛量子攻击，该路线已在Starknet等以太坊二层网络实战。

难关在于能否在4000亿参数模型上跑动。团队测试Meta的Llama 4 Maverick，4000亿参数MoE模型，每Token激活约170亿参数。FlashProve让证明器工作量只与170亿干活参数成正比，省去95%以上无效陪跑；并用零知识编码把路由选择藏进指示向量，验证器对所有专家加权求和，既省算力又保密内部路径。模型4-bit量化后权重达232GB，单张H100显存仅80GB。团队把权重放主机内存，分段送进GPU，流式读取、算完即编码哈希归约，只留少量数据传递，单张80GB显卡啃下232GB庞然大物。

FlashProve的GitHub仓库中，C++占1.4%，Python占1.3%，CUDA占0.9%，高达95.2%的代码（约398MB）用Lean 4数学证明语言写成。随仓附带的114页协议规范论文第51页给出答案：从论文、技术报告到底层代码再到近400MB Lean形式化证明，几乎全部出自Claude之手；每一次测试、运行、对比、推算和代码审校也由AI包揽。密码学代码极脆弱，一个符号写反即坍塌，人类专家无法逐行审完Claude的成千上万个底层决策，于是请出Lean 4，每一步数学推导经编译器内核逐行核对。人类科学家只与AI敲定最顶层6条安全定义：完备性——老实跑模型生成的证明一定能通过，误伤概率不到万亿分之一；知识可靠性——假模型冒充或偷改一个Token，蒙混概率不到2的100次方分之一，数学上等同于不可能；零知识——核验多少次都不泄露权重。只要顶层定理正确，近400MB中间归约即使人类不看，Lean 4内核也已把住关。仓库README写明「专为Agent运行而建」，附有提示词与AGENTS.md规范。

FlashProve带来「AI造系统、Lean保真伪」的新工程范式：人类省去逐行审读C++优化和繁琐引理的苦功，只死守6条顶层定理的定义权，让AI攀登工程与数学绝壁，再让形式化验证器做守门人。人类定下公理边界，AI穷尽推理迷宫，数学给出终极审判。