你没法确认对面是哪个模型——4000 亿参数的一次推理被压成 19 MB 收据，CPU 上 17 秒验完，代价是 70 到 95 倍算力
Progress on provable inference for large language models / FlashProve
11 月 2 日，Anthropic 的 Frontier Red Team 联合 EPFL、MIT 的几位密码学家放出了 FlashProve：一套开源系统，能为一个 4000 亿参数模型的每次推理生成一份约 19 MB 的密码学证明，你用一台普通电脑的 CPU、17 秒就能验完。验完你拿到的结论是：这串 token 确确实实是那组特定权重算出来的——不是路由服务为了省钱半路换了个便宜模型，也不是有人改过 token 流。而整个过程里，你对权重一无所知。它解决的那个问题平时根本没人提：你今天跟任何一个闭源模型说话，其实都没有任何技术手段确认对面是谁。答得好不代表身份对，答得差也可能只是被降级伺候了。
值得读有两层。第一层是数字：同一个 Llama 4 Maverick，此前唯一一份公开的推理证明要 14.3 小时才证完 1000 个 token，证明文件 93.6 GB，验一遍将近一天；FlashProve 在单张 H100 上做到 110 token/秒、证明 18.78 MB、验证 17 秒。这不是百分比的改进，是四个数量级。第二层更该慢慢读：这套系统的可执行代码有很大一部分是 AI 从 Lean 规范生成的，而作者处理这件事的办法比系统本身更值得抄——他们没有试图保证 AI 写的代码是对的，而是把它放在了「写错也动不了关键保证」的位置上。本栏今年写了十几篇 AI 交出成果的案例，这是第一篇把「怎么信 AI 交的活」直接变成架构问题来答的。
四种场合，你都需要一张「这是我本人」的凭据
博客里列了四种。一是测评：独立机构在发布前后测一个模型，必须确认它测的那个就是实际在服务的那个——这件事今天完全靠厂商自觉。二是防篡改：推理服务器是高价值目标，攻击者拿下一台之后可以偷权重、可以给特定用户回带恶意负载的答案，而这些答案就混在海量正常回复里；更麻烦的变体来自内部——当模型有能力改进和部署自己，一个更强的模型可以顶替被授权的那一版去跑，对外装成弱的那个，绕开本该管住它的分类器和监控。三是文本出处：有人说「这个库已经被前沿安全模型扫过漏洞了」，你没法核；作者顺手提了个有意思的构造——「失败证明」：厂商可以给开发者一份凭据，证明自己在某个指定模型上烧了至少一百万个 token 去找这个补丁的 bug，而且确实没找到。四是合规：如果监管要求只能上线通过审批的模型，厂商有动机偷跑未批准的版本，因为它可能更强或更便宜。第四条还牵着一条更野的线——Dario Amodei 那篇《我们必须给前沿踩刹车》设想过「要求厂商把算力用于推理而不是训练下一代」，而这类要求的死穴一直是没法核查。FlashProve 的答案是：监管方索要一段时间内的推理凭据，厂商没真在跑那个模型就交不出来，而监管方不必复制一套同等硬件，厂商也不用交出任何权重。但有个脚注必须一起读：它只能证明硬件在做推理，证不出旁边没在偷偷训练。
先给权重按个指纹，再为每次推理开一张收据
技术上用的是 zkSNARK——「零知识简洁知识论证」，一个证明者用很短的凭据，让验证者相信某个计算被正确执行了。它分两段。离线阶段，厂商对权重做一次「承诺」：把权重编码、哈希，公布一个很短的指纹，这个指纹唯一地钉死了一组权重，却不泄露权重本身。此后所有推理证明都相对这个指纹成立。在线阶段，每个请求产出一份证明，断言的句子只有一句：被承诺的那个模型，吃进这些输入 token，吐出的就是这些输出 token。四条性质撑着它：完整性（诚实的证明一定被接受）、可靠性（伪造一份假证明在计算上不可行，所以你完全不必信厂商）、零知识（证明不泄露权重、不泄露中间激活值，连每层激活了哪几个专家都看不出来）、简洁性（验证比重跑那个计算便宜几个数量级）。前两条其实靠一个「有权重、算力无限」的验证者自己重跑一遍就能拿到；后两条才是这件事成立的全部理由。安全基础选得很保守：整套东西只依赖哈希函数 BLAKE2 像随机函数这一个假设，不用椭圆曲线也不用格，顺带附带后量子安全性。配方是教科书级的三步：先构造一个信息论意义上的「交互式预言机证明」（IOP——证明者发很长的消息，验证者只随机抽查几个位置就能以高概率抓住谎话；报告里的比喻是，IOP 之于计算就像纠错码之于信息），再用 Merkle 承诺把长消息压掉，最后用 Fiat–Shamir 把来回交互折成一条消息。而这三步引用的奠基论文和教材，署名栏里就坐着作者本人。
110 token/秒 是怎么挤出来的，以及它仍然贵 70 到 95 倍
工程上做了三个取舍。第一，吃专家混合（MoE）架构的便宜：Llama 4 Maverick 有 128 个专家、4000 亿参数，但每个 token 只用到约 170 亿，证明者的工作量只跟真正跑了的那 170 亿成正比，而证明仍然藏住选了哪些专家。第二，事后批量证明，而不是边推理边证：响应先正常发给用户，证明随后在单独的服务器上靠重算生成，不占推理的关键路径，还能把一批请求并行证完——重算便宜得可以忽略，一次前向传播约等于 1 次推理，而证明本身要 70 到 95 倍，所以重算只给证明者加了 1% 到 1.5% 的活。第三，整个证明者塞进一张卡：232 GB 权重放在主机内存里按需流进 GPU，分段逐层证。数字是这样的：离线阶段每个模型跑一次约 39 分钟，一次承诺够用约 1600 万个请求；在线阶段一批 24 个请求耗时 223 秒，折合 110 token/秒。这个「110」要会读——它是吞吐，不是延迟。单个请求从所在批次开始到证明放出来要等约五分钟；改成一个一个证，58 秒能出一份，但吞吐掉到 17.6 token/秒。成本那一栏，他们用 vLLM 跑同一模型的 FP8 版做对照，按单卡折算，证明 24 个请求比直接跑完它们的 prefill 慢约 72 倍（多次测量 66 到 77 倍），最高负载下 94 倍。放进历史里看，这个倍数才是新闻：两年前 zkLLM 证一个 130 亿参数模型是 2.5 token/秒，今年同行评议的最好成绩 DeepProve 单机证 GPT-2 是 2.9 token/秒、Gemma 3 是 1.4 token/秒。作者的结论相当克制：开销大约两个数量级，比此前预期小得多。
把 AI 写的代码放在动不了关键保证的地方
密码学代码出名地脆，一个符号错了整套保证就空了。那凭什么信这份刚放出来的代码？答案是 Lean：协议本身，以及完整性／可靠性／零知识三条性质，全部写成形式陈述并给出机器可查的证明，主定理还带具体的误差上界。审计的对象于是从几百页推导缩成「几条定理的陈述说的是不是我想要的那件事」——他们估计一个专家花不了几个小时。真正聪明的一步在这儿：跑在 GPU 上的那份证明者代码是 AI 从 Lean 表示里生成的，并没有被证明与之等价；但这不影响可靠性。理由很干净：可靠性只取决于验证者。证明者代码里的错误，最坏结果是诚实的证明者说服不了验证者，或者无意泄露权重信息，但它没法让一份假证明通过检查——验证者只需要信自己。于是他们给了两个验证者：日常用的快速 C++ 版（无形式保证，但在所有测试上与 Lean 版判断一致），和一个慢得多、却被 Lean 证明「只接受可靠性定理允许的东西」的 Lean 版。这不是信任，是隔离。与之对照的是他们自己交代的另一件事：仓库里那份更长的协议规格说明书「是 AI 生成的，我们没有详细审阅」；而这份技术报告特意写明「由作者本人撰写」。限制也摊在明面上：只支持 1024 token 上下文，相对动辄几十万的真实对话窗口几乎是玩具；证明的对象是权重的整数量化版本，断言的是每个被检查的 token 为贪心解码的选择，浮点实现或带采样的回复可能在某处就对不上；架构不隐藏，旁路攻击不在范围内，证明者也还不支持多卡并行。最该记住的是事后证明的本性：它不防止你被喂到一个假答案，只保证篡改会被发现。作者自己点了出来——拿它防权重外泄，攻击者完全可以在证明失败发出警报之前，先用一个被改过的回复把关键比特传出去。
本文为 AKL AI Club 原创撰写的导读，不是原文翻译；著作权归原文作者所有。 篇目由编辑独立选取，来源均经人工核实。