Anthropic联合学者开源FlashProve：基于zkSNARK的大模型可证明推理系统，家用CPU 17秒验真
SmartHey11月4日消息，近日，Anthropic 联合零知识证明领域顶尖学者正式发布大模型可证明推理技术成果，并开源密码学验真系统 FlashProve。该系统以 zkSNARK 零知识简洁非交互式论证为核心，首次在不访问模型权重、无需复现完整推理的前提下，实现对大模型 API 输出结果的数学级可信验证，有效破解长期困扰行业的“套壳掉包”灰色难题——即服务商宣称调用高端模型，实则暗中替换为低性能或篡改版本模型。
测试表明，普通家用 CPU 仅需 17 秒即可完成一次完整核验，验真效率较传统黑盒测试方案最高提升 5000 倍；在超大规模场景下（如 4000 亿参数 MoE 模型），性能增益更达 5500 倍。项目全部代码、Lean 4 形式化证明库及配套技术文档均已基于 Apache 2.0 协议开源。
大模型 API 供应链中的信任缺失由来已久：部分服务商收取高价调用费，后台却路由至缩水模型；合规接入亦难防参数被静默篡改或推理过程遭干预。而模型权重作为厂商核心资产，开发者既无法获取，也无法通过提问测试或模型自述获得可验证证据，只能被动接受结果——甚至出现强模型伪装成弱模型以规避监管的风险。
FlashProve 构建了一条端到端的密码学验真链路，分为三大环节：
- 离线承诺（模型“按手印”）：模型上线前，服务商使用单张 H100 显卡，耗时约 39 分钟生成唯一公开承诺 ID，相当于模型权重的“数字 DNA 指纹”。该指纹对任意参数改动极度敏感，且不可逆推原始权重，兼顾安全性与知识产权保护；
- 在线证明（实时“开证”）：每次用户请求响应后，GPU 同步生成一份约 19MB 的密码学证明文件，确保证明输出内容严格源自指纹绑定的目标模型；
- 客户端核验（轻量“验真”）：开发者或审计方仅需运行本地验证程序（无需 GPU、不接触权重），即可在 17 秒内获得确定性真伪判定。
系统底层采用抗量子设计的 BLAKE2 哈希函数，不依赖椭圆曲线密码体系，理论可抵御未来量子计算机攻击。单次推理验证需执行约 2000 个 sumcheck 子协议，相关技术已在 Starknet 等主流零知识区块链网络中完成工程落地验证。
面对千亿级大模型的硬件瓶颈，FlashProve 实现多项关键突破：以 4000 亿参数 MoE 模型 Llama 4 Maverick 为测试基准，系统将计算开销精准锚定于实际激活的约 170 亿参数，剔除超 95% 的无效计算；针对 80GB 显存 H100 无法容纳 232GB 量化权重的难题，创新采用流式分段加载架构——权重驻留主机内存，按需分块送入 GPU 计算并即时释放显存，单卡即可完成全量证明生成。
尤为颠覆性的是：该项目95.2% 的仓库内容（近 400MB）为 Lean 4 编写的数学形式化证明，C++/Python/CUDA 等底层实现代码占比极低。配套产出包括 114 页协议论文、23 页技术报告，从算法设计、代码实现、测试验证到逻辑审校，大量工作均由 Claude 大模型协同完成。
为应对海量密码学代码人工审核不可行的现实，团队引入 Lean4 形式化验证工具链。人类专家仅需定义 6 条顶层安全公理，明确三大核心保障：完备性（合规模型几乎零误判）、知识可靠性（造假通过概率数学趋近于零）、零知识性（核验全程不泄露任何权重信息）。中间所有复杂推导交由 AI 自动生成，并经形式化编译器逐行逻辑校验，彻底规避人为疏漏引发的安全隐患。
项目 README 明确指出其面向 AI Agent 运行场景深度优化，已内置专用提示词模板与标准化运行规范。
业内评价认为，FlashProve 标志着一种全新 AI 工程范式的诞生：人类设定安全公理边界，大模型承担高密度工程与数学推导任务，形式化验证系统执行终极逻辑守门。在大模型 API 普及化、AI Agent 加速演进的当下，这种基于“数学铁律”的可证明推理能力，有望从根本上筑牢模型可信底座，为超级智能时代的安全契约提供关键技术支撑。