技术拆解 041｜FlashProve：Claude 写代码、Lean 兜底的零知识证明

背景与现象：你不知道回话的是不是你选的那个模型

2026 年 11 月 4 日，Anthropic 发布研究博客「Progress on provable inference for large language models」，公布了一个叫 FlashProve 的系统，同时开源五个工件：博客本身、技术报告、协议规范、可执行代码（一个证明器加两个验证器）、Lean 证明和一个定理交互可视化工具，代码、证明、文档全部 Apache 2.0 许可。配套仓库 anthropics/FlashProve 创建于 2026-10-30，截至 11 月 5 日拿到 781★，版本文件写着 0.16.0；博客的 HN 条目 155▲、77 条评论。

博客提出的问题很直白：用户向模型发请求时，没有任何办法确认回话的真是自己选的那个模型。路由服务可能为省钱悄悄换成便宜模型，攻击者可能篡改 token 流；从输出质量反推不可靠，回答再漂亮也证明不了自己的出身。独立评估机构需要知道评的就是线上跑的那个模型，走第三方路由的用户需要确认 token 真出自自己付钱买的那一个。

第二个拆解点是作者阵容和 Claude 在其中的角色。博客署名是学界加密码学创业圈的混编：Anthropic 两人，EPFL 三人，另有 MIT、StarkWare、Succinct、RESI 背景的研究者。更扎眼的是博客自述：「Claude 改进了推理用 zkSNARK」，构建出比既有开源系统快得多的系统；五个工件里的协议规范文档明确标注 Claude-written。Anthropic 同时自陈这种写法的风险和对策：Claude 擅长优化，但在大型复杂系统里的决策常常难以评估，对策是把声称的安全保证写成 Lean（形式化验证语言）里可审计的顶层命题。

README 首行是自我定位：「研究工件：不维护、不收贡献」。博客也明说这是中间进展，不是完成的研究议程，公开的目的就是让别人拿走改进。

架构与技术原理：commit、prove、verify 三步

FlashProve 的核心是 zkSNARK 式可证明推理，机制分三步（README 口径）。第一步 commit：服务商发布一个承诺 ID，绑定一组权重，权重本身保密，所有依赖权重的公开值都被掩码，只留 docs/what-is-not-hidden.md 声明的清单例外；设计目标写得很清楚，隐藏权重是目标，隐藏架构不是。第二步 prove：每条回复由服务商的 GPU 产出证明。第三步 verify：任何人用 C++ 验证器 cp_verify 在普通 CPU 上几秒核验「这条回复确实出自被承诺的模型」，全程不需要权重。

Lean 部分是仓库的另一半重心。本地 clone 统计共 30,902 个文件，其中 .lean 文件 29,563 个、.py 只有 185 个，总体积 723MB；目录含 prover、verifier、lean、paper（技术报告 PDF）、docs（19 篇）、guide（8 篇）、tests、toy、scales 等。lean/THEOREM.md 列出六个定理，全部针对同一套 committer / prover / verifier，对每个公开 setup 成立：sound（作弊方在 q 次哈希查询下骗过验证者的概率不超过约 q/2^124 + 2^-101，原文明注「这是界，不是安全级别」）；soundAndBinding（没人能把承诺开成另一组权重，除概率约 q/2^124 + 2^-100）；completeOnCanServe（可服务请求上诚实证明被误拒的概率不超过 2^-40）；zeroKnowledgeOnCanServe（在 2^64 次哈希查询与 688,127 条回复内泄露界不超过 2^-154，模拟器拿不到权重）；refusedHandsOutNoProof（被拒请求只能回空证明，但「拒得对不对」不在证明范围内）；repliesFit（688,127 条回复与表列数的一致性计数）。

两条边界值得点名，都是仓库自陈。其一，六个定理都要求「精确匹配」，而验证者并不检测这一点：服务商若在看到请求后更换公开文件策略，定理不覆盖。其二，测试套件全部使用合成权重，SUITE.md 原文自己说：通过的测试只说明程序对合成输入给出了预期答案，对可靠性与隐藏性说明不了更多。

关键数据：110 tok/s、93 倍代价和六个概率界

性能数字全部来自仓库 guide/performance.md 与 README，官方自报口径，暂无独立复现。

跑的对象：Llama 4 Maverick 全尺寸（400B 参数 MoE），用第三方公开的 4-bit 转换（下载 232GB），1,024-token 上下文窗口，单张 H100 80GB。速度：prefill 批 24 时 111.23±0.92 tokens/s，README 约称 110；批 1 只有 17.41；批 64 能到 123.31，但仓库自己标注 80GB 卡上批 64 不可靠，显存顶到 80,629/81,559 MiB，合成权重下 8 次尝试的 CUDA 调用全部失败。

代价同样是仓库自陈：每 GPU 计，比 vLLM 原生 prefill 慢 93.0 倍（最高负载对局）、比 vLLM 批 24 慢 71.4 倍，而且这是「算出来的、最好情况」，不含启动与承诺时间，基线机还是 8×H100 跑 FP8。

证明与存储体积：单个证明平均 18.78MB；客户端每个承诺一次性下载 6.24MB；服务商每个承诺要保存 2.15GB。承诺耗时约 39 分钟，一次承诺可以多次使用；服务商主机内存要 330GB 起、磁盘 245GB。验证成本是整套系统里最不对称的数字：cp_verify 单线程约 21 秒、内存至多 3.53GB、无需 GPU；Lean 版「可证正确验证器」核一个全尺寸证明约 24 分钟、内存至多 14.13GB。

仓库对自己的短板交代得相当老实：启动耗时 68-79 秒；把承诺成本摊进前 1,000 个请求后稳态速率 88.81 tok/s，没达到自设的 100 tok/s 目标，performance.md 直接承认不达标。

影响与意义：把「哪个模型说的」变成可检查的属性

第一，合规与审计场景。博客明说 zkSNARK 可以作为验证 AI 节奏合规要求的工具：监管方要求服务商提供覆盖某段时间推理请求的证书，服务商除非硬件真在跑宣称的模型，否则伪造不出来，同时监管方拿不到专有权重信息。HN 一条高赞评论是同一个意思：在合规审计、代理链、监管场景里，「哪个模型说的」本身就是关键属性。

第二，聚合路由的信任问题。有评论指出 OpenRouter 这类聚合器会把请求路由到别的模型，这套机制能抓住；另一条给了更具体的欺诈场景，某些市场的 Claude 转售商承诺提供访问、实际偷换模型，可证明推理防的就是这类事。还有人提到传闻某些主机上的同名模型表现明显更差、疑跑未公开的量化版（评论者自认 rumour），问这套能否抓到。

第三，开源权重模型同样能拿它自证。一条读过仓库文档的高赞评论指出：用公开权重做承诺、公布种子，任何人都能从 Hugging Face 文件重算承诺，核对服务商跑的是不是宣称的 checkpoint 和量化位宽。也就是说这套机制不只服务闭源厂商，反而先给了社区一个自查工具。

第四，Claude 写密码学代码加 Lean 兜底这件事的方法论意义，可能不小于系统本身。把「难以评估的 AI 决策」翻译成形式化语言里可审计的顶层命题，让机器证明替人复核机器写的代码，这是 AI 参与关键基础设施开发时一个可复用的工程范式（这是我的判断）。

争议与风险：PR 动作，还是真空白的填补

HN 评论区声量最大的是讽刺。最高赞评论认为这是一次 PR 动作，有网友翻出此前报道，指认同一家公司曾因把 ML 相关请求静默路由到较弱模型上新闻（评论者指认，未经独立核实）。但反驳同样高赞：被偷换模型恰恰是用户最常见的抱怨，而且此前根本不存在任何验证机制，这套若能做成，意义重大。

价值争论更深一层。有人认为它证明的属性「算是底线要求」：不过告诉你没被换成便宜模型、没被中间人，除此之外没提供多少有用信息；有人先以为要证明「输出正确」，发现只证明「用的哪个模型」，直言若本就不信任服务商，游戏早结束了。反方回应：客户关心输出正确，厂商关心输出出自自家模型，这套解决的是后者；还有评论预测它最终会被用作针对廉价路由的 FUD（此为评论者的动机推测）。我的看法：两边其实不冲突，「输出正确」和「输出出自宣称的模型」是两个独立的验证问题，前者远未解决，后者目前恰好只有密码学这一条可行路径（这是我的判断）。

技术风险有三条硬边界。其一，精确匹配问题：六个定理都要求公开文件与承诺精确一致，而验证者不检测，服务商看到请求后更换策略就落在保证范围之外，这是仓库自陈的已知缺口。其二，部署门槛：GPU 栈要求 x86-64 Linux 4.14+、带 SHA 扩展的 CPU、独占一张 H100 80GB、CUDA 13.2 Update 2（明确不支持更新的工具包），真模型路线还要 330GB 内存和 245GB 磁盘，个人和小团队基本摸不到。其三，所有性能数字均为官方自报、无第三方复现，93 倍的减速也意味着短期内它更像审计工具，而不是能常开的生产特性。

结论与展望：仓库本身就是第二个实验

核心一句话：FlashProve 用 zkSNARK 把「这条回复出自被承诺的权重」变成任何人在普通 CPU 上几十秒能核的命题，代价是自报 70-95 倍的 GPU 时间和 330GB 内存级的部署门槛；同时它用 29,563 个 Lean 文件，把「Claude 写的密码学代码可信吗」这个问题翻译成六个可审计的定理。

值得单独点一个现象：README 有一节「Built to be run by an agent」，作者预设读者把自己的 coding agent 指向这个仓库，给了一段可直接粘贴的指令文本，并把验证路线按硬件分成四条：路线 1 只要 Linux 加 g++13、2GB 内存，1-2 分钟构建、2 秒核验存量证明；路线 2 在 CPU 上跑玩具证明约 1 分钟；路线 3 的八层合成小模型需要 H100 全套栈，构建约 29 分钟；路线 4 才是真 Llama 4 Maverick，耗时以小时计。安全姿态也是配套的：全程禁止 root/sudo，沙箱用 Landlock。这些设计本身就是一场「让 agent 安全运行陌生仓库」的实验，仓库文档的第一读者可能正在从人变成 agent。

后续值得盯两件事。一是 README 声明不维护、不收贡献，博客呼吁别人拿走改进，Apache 2.0 的五个工件大概率由学界和密码学创业圈接着做，能否出现独立复现的实现，是比星标更硬的验证。二是精确匹配边界会不会被补上，这决定这套机制能否从审计场景走进常开的生产流程。

我的结论一句话：FlashProve 值得拆，不是因为它已经解决了推理信任问题（它没有，官方自己也承认只是中间进展），而是它把两件此前只能靠嘴保证的事变成了可证明的命题：模型的身份，和 AI 写的密码学代码的正确性。前者指向推理市场的信任底座，后者指向 AI 编程时代的质量保证方式。

参考来源

• Anthropic 研究博客「Progress on provable inference for large language models」：anthropic.com/research/provable-inference（2026-11-04 发布；Claude 相关表述均为博客自述口径）
• HN 条目：story 50368626（155▲ / 77 评论，2026-11-05 快照）
• 仓库：github.com/anthropics/FlashProve（781★ / Apache 2.0 / created 2026-10-30 / VERSION 0.16.0，2026-11-05 快照）
• 本地浅 clone 核对（2026-11-05 实测，未运行任何仓库代码）：README.md、guide/performance.md、lean/THEOREM.md、SUITE.md、docs/、AGENTS.md；30,902 文件 / 723MB 为本地统计
• HN 评论池：hn-provable.json（47 条存证，正文全部转述，未直引）

署名：永亮