Anthropic发布可证明推理研究进展，推出FlashProve系统，基于zkSNARK零知识证明技术，让模型提供方能够以密码学方式证明每条回复确实来自其声称的特定模型。该技术旨在解决用户无法验证AI响应来源的问题——路由服务可能出于成本考虑暗中替换模型，或攻击者篡改令牌流。技术指标方面：针对4000亿参数的混合专家模型Llama 4 Maverick，在4-bit量化权重下，单张H100 GPU的证明生成速度约为每秒110个token，每1024-token请求的证明大小约19 MB，开销为vLLM直接推理的70-95倍，而此前开源系统慢数个数量级。值得注意的是，Claude在zkSNARK优化中发挥了核心作用，找到了将密码学与安全领域前沿工具应用于推理证明的新方法。针对AI优化决策难以评估的问题，团队使用形式化验证语言Lean为声明的安全保证提供了可审计的顶层证明。本次共开源五项成果：博客文章、技术报告、协议规范文档、包含C++快速验证器与Lean可证明正确验证器的可执行代码，以及Lean数学证明和交互式可视化审计工具，均采用Apache 2.0许可证发布。
事件分析
该研究的核心看点在于将零知识证明从区块链领域迁移至大模型推理场景，FlashProve将400B级模型的证明开销压缩至直接推理的70-95倍，较此前开源实现提升数个数量级，首次逼近实用门槛。产业层面，模型路由与API转售市场长期存在暗中替换模型的信任黑洞，可验证推理为模型溯源、供应链安全和监管合规提供了密码学层面的技术底座。两个信号值得留意：一是Claude深度参与了核心密码学优化，显示前沿实验室正将AI智能体投入高难度工程研究；二是Lean形式化证明与代码同步开源，为AI生成代码结合形式化验证的工作流提供了范例。后续走向上，当前开销仍需降至个位数倍才可能规模化商用，证明体积、硬件适配性以及隐藏模型架构等方向仍有较大演进空间。
核心观点：当暗中替换模型成为API市场灰色地带，密码学证明正把AI可信度从商业承诺升级为可验证的数学事实。
原文链接：Hacker News
