让大模型推理过程可被密码学证明

当用户与朋友面对面交谈时，可以通过视觉、声音乃至握手来确认对方身份。但当用户与 AI 模型交互时，几乎没有任何等效手段。现有系统中，用户无法核实响应是否真的来自开发者声称的特定模型，路由服务可能出于成本考量悄然替换模型，攻击者也可能在不被察觉的情况下篡改 token 流。仅凭输出质量判断并不可靠，即便响应看起来完全正常。

为解决这一问题，Anthropic 联合 EPFL、MIT 等机构的研究者开发了 FlashProve 系统，其核心是一种名为 zkSNARK 的密码学证明机制。该机制允许模型提供方对特定模型做出承诺，并为此后每次推理生成简短的密码学证明，用户无需掌握模型权重、也无需运行模型本身，即可在本地快速验证响应的真实性。证明过程同时保护模型权重不被泄露，但不隐藏模型架构。

在性能层面，FlashProve 取得了显著突破。针对 4-bit 量化的 Llama 4 Maverick（400B 参数混合专家模型），单张 H100 GPU 可实现每秒超过 100 个 token 的证明生成速度，每 1024 个 token 请求对应约 19 MB 的证明文件。与此前开源系统相比，FlashProve 的速度提升幅度达到数个数量级，但与直接运行模型的 GPU 时间相比，仍需约 70 至 95 倍的额外开销，这也是后续优化的主要方向。

值得关注的是，本次研究中 Claude 本身参与了系统的优化工作，找到了将密码学与安全领域前沿工具应用于推理证明的新方法。然而研究团队也坦承，AI 在大型复杂系统中的决策有时难以评估。为此，团队在形式化验证语言 Lean 中提供了顶层可审计声明，并附有交互式可视化工具，以便外部审计人员核查安全保证的数学基础。

可验证推理的应用场景远不止于技术层面。独立评估机构在模型发布前后进行测试时，需要确认所评估的模型与实际部署的模型一致；通过第三方路由服务使用模型的企业客户，需要保证所付费的 token 确实来自指定模型；监管机构和合规审计人员也可借助此类工具，验证 AI 提供方是否遵守相关承诺与法律义务。研究团队认为，FlashProve 可成为 AI 发展节奏管理与监管工具箱的重要组成部分。

Anthropic 明确将本次发布定位为阶段性进展而非完整研究成果，代码、Lean 证明及文档均以 Apache 2.0 协议开源，并公开邀请外部研究者在此基础上继续推进。团队发布了五项配套成果：当前博客文章、技术报告、协议描述、包含证明器与验证器的可执行代码，以及 Lean 形式化证明与交互式可视化工具。这种开放姿态体现了 Anthropic 在 AI 安全基础设施领域寻求广泛协作的意图。

要点

• FlashProve 利用 zkSNARK 密码学证明技术，让用户无需访问模型权重即可验证 AI 响应是否来自声称的特定模型，从根本上解决了推理过程的信任验证问题。
• 在 400B 参数的 Llama 4 Maverick 模型上，单张 H100 GPU 可实现每秒超过 100 个 token 的证明生成，比此前开源系统快出数个数量级，但仍有约 70-95 倍于直接推理的额外 GPU 开销。
• 系统在保护模型权重隐私的同时生成可验证证明，适用于独立评估、第三方路由服务审计及 AI 监管合规等多种场景。
• 团队在 Lean 形式化验证语言中提供了顶层安全声明及交互式可视化工具，以应对 AI 辅助优化在复杂系统中决策难以评估的风险。
• 全部代码、Lean 证明及文档以 Apache 2.0 协议开源，Anthropic 明确邀请外部研究者在此基础上继续改进，定位为阶段性进展而非终态成果。