新智元报道
新智元报道
大模型API供应链长期存在“挂羊头卖狗肉”的灰色地带：用户支付顶配旗舰费用，后台可能仅运行缩水模型或转售路由。由于缺乏权重和机房访问权限，开发者难以验证模型真实性。
近日，Anthropic联合零知识证明领域专家公布重大突破，正式开源密码学验真系统FlashProve。该系统为每条模型生成内容赋予数学级“出生证明”，无需信任中心化机构或获取权重代码，即可验证输出是否由指定模型生成。
即便使用普通家用CPU，仅需17秒即可通过纯数学方式精准验证每个Token的来源，彻底杜绝模型偷换与篡改。值得一提的是，FlashProve的核心代码主要由Claude自身生成，所有代码、Lean证明及技术文档均基于Apache 2.0协议开源。
项目地址：https://github.com/anthropics/FlashProve
传统验证方式依赖用户提问试探或自行重跑模型，前者易受采样波动影响，后者则因算力成本高昂且权重保密而不可行。更严峻的是，高级模型可能伪装成弱模型以规避监管。
FlashProve基于zkSNARK（零知识简洁非交互式知识论证）技术，将验真流程拆解为三个闭环步骤：
第一步：离线“按手印”。
模型上线前，服务商在单张H100上耗时约39分钟，利用零知识编码为模型权重生成唯一的承诺ID并公开。该ID如同数字DNA指纹，任何参数修改都会导致不匹配，且无法逆向推导权重信息。
第二步：在线“开证明”。
处理对话请求时，服务端GPU同步生成约19MB的密码学证明，证实输出结果确由已备案权重的模型计算得出。
第三步：客户端“验真伪”。
用户或审计机构获取回答后，在普通CPU上运行验证程序cp_verify，17秒内即可完成真假判决，全程无需权重文件或GPU支持。
该系统安全性依赖哈希函数BLAKE2，具备抗量子攻击能力。每个请求背后运行约2000个sumcheck子协议，验证者通过随机抽查即可高效识别破绽。
团队以Meta Llama 4 Maverick（4000亿参数MoE模型）进行测试，每Token实际激活约170亿参数。FlashProve针对这一特性优化，证明器工作量仅与激活参数成正比，节省超过95%的无效计算。
为保护模型隐私，系统通过零知识编码将路由选择隐藏于指示向量中，验证器对所有专家进行加权求和，既保障算力效率又防止通过激活模式反推权重。
针对4-bit量化后权重达232GB而单张H100显存仅80GB的挑战，团队采用流式处理方案：权重存放于主机内存，分段送入GPU进行计算与证明。每次仅读取片段权重，完成后立即在显存中执行编码、哈希与归约，仅保留必要数据传递至下一段。
凭借这种“分段消化”机制，单张80GB显卡成功承载232GB庞然大物，实现高效验真。
FlashProve的代码构成极具颠覆性：C++、Python和CUDA代码占比不足4%，高达95.2%的代码（约398MB）由Lean 4数学证明语言编写。
从114页密码学论文、23页技术报告到底层代码及形式化证明，绝大部分工作由Claude完成。测试、运行、对比及代码审校均由AI包揽，人类专家仅负责制定顶层安全定义。
鉴于密码学代码的高敏感性，Anthropic引入Lean 4作为验证核心。每一步数学推导均需通过编译器内核逐行核对，确保无误。
人类科学家确立了六条顶层安全定义，其中核心包括：
完备性：诚实执行生成的证明必能通过核验，误拒概率低于万亿分之一。
知识可靠性：伪造模型或篡改Token蒙混过关的概率低于2的100次方分之一，数学上视为不可能。
零知识：验证过程不泄露任何模型权重信息。
只要顶层定理成立，Lean 4内核即自动保障近400MB中间推导的正确性。项目README明确标注“专为Agent运行而建”，提供现成提示词与规范，标志着开发模式的转变。
FlashProve确立了“AI造系统、Lean保真伪”的工程新范式。面对超出人类阅读极限的复杂密码学工程，人类专注于定义公理边界，AI负责攀登工程与数学绝壁，形式化验证器担任守门人。
这一模式不仅解决了大模型信任危机，也为通往超级智能之路提供了硬核的安全契约。
参考资料：
https://x.com/AnthropicAI/status/2117707052948898271
https://www.anthropic.com/research/provable-inference
编辑：摩西 桃子
