核心观点 - Anthropic联合零知识证明领域学者开源密码学验真系统FlashProve，通过数学证明机制终结大模型API供应链中偷换模型、掺水降智的灰色操作，让开发者无需信任中心化机构即可验证每个Token是否由目标模型生成 [4][5] - 该系统所有代码、Lean证明、技术文档均以Apache 2.0协议开源，核心开发主力为Claude自身 [4][23] 行业痛点与背景 - 大模型API供应链长期存在挂羊头卖狗肉的暗箱操作，开发者支付顶配旗舰费用却可能获得缩水小模型服务，且无权重、无机房，后台被偷梁换柱也只能干瞪眼 [1][2][3] - 模型自报家门本身由后台生成，算力负载与采样配置的微小波动也会改变回答，用户难以获得钉死服务商的铁证 [5] - 更高级模型可能顶替获批弱模型上岗并伪装成弱模型躲避监控，形成安全隐患 [6] - 传统验真需获取权重自行重跑，但前沿模型权重是各家命根子，普通用户无力承担4000亿参数模型的机房成本 [7] FlashProve三步验真流程 - 第一步离线按手印：模型上线前服务商在单张H100上花约39分钟用零知识编码为权重生成唯一承诺ID并向全网公开，该ID如同权重数字DNA指纹，改一个参数即对不上，外界无法从指纹反推权重 [9] - 第二步在线开证明：每处理完一次对话请求，服务商GPU顺手生成约19MB密码学证明，证实输出确由按过手印的模型算出 [10] - 第三步客户端验真伪：用户或审计机构在普通CPU上运行验证程序cp_verify，17秒即可获得真或假判决，全程不需权重也不需GPU [11] 底层密码学引擎 - 底层引擎为zkSNARK零知识简洁非交互式知识论证，验证者随机抽查几处即以极高概率抓到破绽 [12][13] - 每个请求背后需跑约2000个sumcheck子协议将推理拆成可抽查形式 [14] - 安全性仅依赖哈希函数BLAKE2，不靠椭圆曲线等代数结构，被认为能扛住未来量子计算机攻击，该路线已在Starknet等以太坊二层网络久经实战 [15] 工程突破与性能表现 - 测试对象为Meta的Llama 4 Maverick，4000亿参数混合专家MoE模型，每个Token实际激活约170亿参数 [16] - 证明器工作量只与170亿真正干活参数成正比，省去95%以上无效陪跑；系统用零知识编码将路由选择藏进指示向量，验证器对所有专家加权求和，既省算力又保密内部运转路径 [17] - 模型4-bit量化后权重达232GB，单张H100显存仅80GB，团队将权重放主机内存分段送入GPU，流式读取逐段完成计算与证明，单张80GB显卡成功处理232GB权重 [18][20][21] - 单张H100实现5500倍加速 [16] AI自主工程范式 - 仓库中C++代码仅占1.4%，Python占1.3%，CUDA占0.9%，高达95.2%代码（足足398MB）全部用Lean 4数学证明语言写成 [22] - 从114页密码学论文、23页技术报告到C++与CUDA底层代码再到近400MB Lean形式化证明，几乎全部出自Claude之手；项目每次测试、运行、对比、推算和代码审校也全由AI包揽 [23][24] - 人类科学家只与AI敲定最顶层6条安全定义，省去审核上亿行中间推导的苦功，Lean 4编译器内核逐行核对每一步数学推导 [25][26] - 仓库README开篇写明专为Agent运行而建，附现成提示词与AGENTS.md规范 [29] 三条顶层安全定理 - 完备性：服务商老实按承诺权重跑模型，证明一定能通过核验，被误伤拒绝概率不到万亿分之一 [28] - 知识可靠性：服务商拿假模型冒充或偷改一个Token，造假蒙混过关概率不到2的100次方分之一，数学上等同于不可能 [28] - 零知识：客户端无论核验多少次，证明文件都不会泄露半点模型权重 [28] 行业范式意义 - FlashProve带来AI造系统、Lean保真伪的全新工程范式，人类定下公理边界，AI穷尽推理迷宫，数学给出终极审判 [31] - 面对近400MB证明代码、114页公式推导的密码学工程，碳基大脑阅读极限已被击穿，人类只死守6条顶层定理定义权，让AI攀登工程与数学绝壁，形式化验证器做铁面守门人 [31]