Anthropic 开源 FlashProve，给大模型推理加上密码学证明

你调用的模型，真的是服务商声称的那个吗？Anthropic 发布了可证明推理原型 FlashProve，尝试在不泄露权重、也不让用户重新运行模型的情况下，为这个问题提供密码学证明。以下是全文翻译。

大语言模型可证明推理的新进展

• 发布时间：2026年11月2日
• 团队：前沿红队（Frontier Red Team）

Roy Rinberg（Anthropic）、Alex Allain（Anthropic）；Alessandro Chiesa（EPFL、StarkWare）、Miranda Christ（MIT、RESI）、Rahul Dalal（Anthropic STEM Fellows Program、Succinct）、Giacomo Fenzi（EPFL）、Ben Mayer（Anthropic Fellows Program、MIT）、Guy Weissenberg（EPFL）

内容概要

当你和朋友面对面交谈时，有很多办法确认对方确实是本人：你能看到、听到对方，也能握手。但和 AI 模型交流时，你几乎没有这样的手段。如今，用户向模型提问，无法检查回答是否真的来自开发者声称正在提供服务的那个模型，还是路由服务为了节省成本而暗中换上的另一个模型，甚至是攻击者篡改 token 流后的产物。单凭输出判断并不可靠，即便回答质量很高也一样。推理的密码学证明可以解决这个问题：模型提供方先对某个模型作出密码学承诺，再证明每条回答都由该模型生成。这类证明的应用可以覆盖消费产品、内部安全等领域，也可以成为验证是否遵守 AI 发展节奏要求的一种工具。

具体来说，我们在一种名为 zkSNARK 的强大密码学证明上取得了进展。它凭借出色的隐藏性和效率，尤其适合可证明推理。本文主要通过一个我们称为 FlashProve 的系统，介绍其中的一部分进展。技术概要如下：

1. Claude 改进了用于推理的 zkSNARK，构建出一个明显快于此前开源系统的系统。对于一个大型模型——4000亿参数的混合专家模型 Llama 4 Maverick——在使用 4-bit 量化权重、预填充阶段采用整数运算的条件下，单张 H100 GPU 生成证明的速度约为每秒 110 个 token；每个 1024-token 请求对应的证明约为 19 MB。所需 GPU 时间约为使用常见开源库 vLLM 运行模型本身的 70—95 倍。此前的开源系统要慢几个数量级，详见第六节。Claude 找到了新方法，将密码学与安全文献中的前沿工具应用到这里，同时仍遵循密码学证明系统中成熟的设计原则。模型承诺值及后续推理证明都会隐藏模型权重；隐藏模型架构并不是本系统的目标。
2. Claude 很擅长优化，但它经常作出难以评估的决策，在大型复杂系统中尤其如此。为此，我们用形式化验证语言 Lean，为所声称的安全保证提供了可供审计的顶层命题。

今天，我们发布五项成果：

• 本文，概述系统及其潜在应用；
• 一份技术报告，介绍系统细节；
• 一份由 Claude 编写的协议规范文档；
• 可执行代码，包括一个证明器和两个验证器：用 C++ 编写的快速验证器，以及用 Lean 编写、经过正确性证明的验证器；
• 顶层数学命题的 Lean 证明，以及一个帮助审计 Lean 定理的交互式可视化工具。

我们以 Apache 2.0 许可证发布代码、Lean 证明和文档。[1] 这篇研究文章分享的是阶段性进展，而非一项已经完成的研究议程。我们公开这些工作，明确是希望其他人来审视、使用并改进它。

引言

如今，用户向 AI 模型发送请求时，无法确定生成回答的就是自己选择的那个模型。在日常使用中，用户往往主要关心输出，而不一定在意具体由哪个模型生成，因此这个问题未必那么紧迫。但有几类场景会需要这样的保证。例如，在模型发布前后进行测试的独立评估者，需要知道自己评估的模型就是实际提供服务的模型。通过第三方路由服务使用模型的客户，希望确认收到的 token 来自自己付费购买的那个模型。如果网络攻击者冒充某个模型并修改 token 流，用户也无法仅凭输出发现。

不过，验证模型回答并不容易。大多数前沿模型的权重不公开；即便用户能够拿到权重，要确认某条回答确实由这些权重对应的模型生成，也得运行模型，所需算力远超普通用户，甚至评估者能够承担的范围。

可证明推理（provable inference，PI）的目标，是让算力有限、完全不知道权重的用户，也能验证某条回答是否来自所请求的模型。PI 一方面旨在提升客户对 AI 提供商的信任；另一方面，它能为独立评估者提供保证，让提供商证明自己履行了某些承诺和法律义务，因此也关系到如何控制前沿 AI 的发展节奏，以及 AI 监管。

实现 PI 的一种方式，是使用一种叫作零知识简洁论证的密码学对象：模型提供方在发送所声称的回答时，同时附上一份简短证明，比如几兆字节，让用户能够快速验证，理想情况下只需在 CPU 上花几秒钟。如果这条回答偏离了指定模型的计算结果，用户的检查就会失败。重要的是，密码学技术确保这份证明不会泄露模型权重的任何信息。

今天，我们发布 FlashProve：一个性能较高的开源可证明推理原型。对于 4000亿参数的混合专家模型 Llama 4 Maverick（4-bit 量化），单张 H100 GPU 生成证明的速度可超过每秒 100 个 token，每个 1024-token 请求的证明约为 19 MB。所需 GPU 时间约为常见开源库 vLLM 处理同样长度提示词的 70—95 倍。

此次发布包含可执行代码、Lean 形式化成果和协议的技术说明。我们有两个目标：一是加速并推动可证明推理的发展；二是展示零知识简洁论证用于可证明推理的实际可行性。

我们认为，这项进展对安全、控制 AI 发展节奏、为 AI 客户提供完整性保证，以及帮助审计者和监管者构建工具等，都具有重要意义。

AI 普及带来的信任挑战

人工智能不断发展，在数字基础设施和经济中的作用日益扩大，也带来了 AI 提供商必须回应的信任挑战。可证明推理工具有助于应对这些挑战。

PI 工具可以采用硬件方案、软件方案，或两者结合。这里，我们聚焦一种纯软件方案：名为 zkSNARK 的密码学工具，即零知识简洁知识论证。通俗地说，zkSNARK 让证明者能够用一张简短的“证书”，向验证者证明某次计算已经正确执行。关键在于，这张证书具有零知识性，除了计算正确性本身所蕴含的信息，不透露任何其他信息；同时它具有简洁性，验证速度相较被证明的计算具有指数级优势。

下面，我们介绍几类挑战，以及 zkSNARK 如何帮助应对。

挑战一：控制发展节奏

一些监管和控制 AI 发展节奏的提议，依赖于监测硬件及其使用方式。例如，可能要求提供商将硬件用于推理，而不是训练更强大的新模型。提供商可能通过提供更便宜的模型，或以预期之外的方式使用算力来作弊，从而腾出资源用于训练。监管者如何可靠地确认硬件确实用于推理？

zkSNARK 能提供的帮助：监管者可以要求提供商提交证书，覆盖某段时间内服务的推理请求。证书必须表明，这些请求的输出由所声称的模型生成。除非硬件确实在运行正确的模型提供服务，否则恶意提供商无法满足这一要求。借助 zkSNARK，监管者无需拥有提供商那样复杂的硬件配置，就能检查其声明是否有效；与此同时，提供商也能确保监管者不会得知专有模型信息。[2] 需要注意，这能验证硬件确实在提供推理服务，却不能证明硬件没有同时进行训练等其他工作。

挑战二：检测篡改

AI 模型越有价值，运行它们的服务器就越容易成为重点攻击目标。攻击者或失控的 Agent 可能入侵推理服务器，窃取权重、向用户提供恶意回答，例如把恶意软件送到用户电脑上，并将这些行为隐藏在正常回答之中。威胁也不一定来自外部。随着模型具备改进和部署自身的能力，一个更先进的模型可能取代获准运行的模型，伪装成较弱的模型，以规避原本适用于它的分类器和监控。在这两种情况下，问题都一样：公司如何确定服务器上实际运行的是哪些权重？Anthropic 在《前沿安全路线图》中设定了一个公开目标：“我们将在2026年9月30日前开发出可证明推理原型。这是一种可靠、可证明地为 AI 模型输出‘签名’的技术，使输出能够归属于一组特定的模型权重。”正如我们在 RSP 更新中所述，我们通过另一项相关但独立的项目实现了这一目标：该项目为推理流量签名，并在可信服务器上重新计算推理。本文的工作则以另一种方法追求同一目标。[3]

zkSNARK 能提供的帮助：提供商可以要求服务器为每条回答附上有效的 zkSNARK。证明绑定到某个特定的权重承诺值，因此它证明的不只是“某个模型生成了回答”，而是“承诺的那个模型生成了回答”。入侵服务器的攻击者，或试图冒充另一模型的模型，要避免被发现，就必须为预期权重生成有效证明，而它们做不到。用户也可以收到这些证明，因为零知识性确保它们不泄露内部信息，简洁性则让验证成本很低；这限制了攻击者通过推理 API 所能实施的行为。

挑战三：文本来源

有时，人们希望证明自己确实投入了相当多的精力去理解或分析某件事。例如，开发者可能声称自己的软件库已经由前沿网络安全模型扫描过漏洞，公司可能声称商业计划已经得到某个合适模型的认可。用户如何验证这些说法？他们未必有运行模型的资源，或者没有相应的访问权限。即使公开聊天记录，也不能给出绝对保证：理论上，开发者可以伪造记录，使用更便宜的模型，或性能降级的版本，而不是前沿模型生成这些内容。更普遍地说，用户如何验证为自己提供服务的就是所选模型？

zkSNARK 能提供的帮助：提供商可以在每条回答后附上一份 zkSNARK，证明该输出是所声称的模型在给定输入上生成的。简洁性让用户无需专用硬件就能快速检查证书；零知识性则保证用户不会获知专有权重的任何信息。这可以补充现有用于验证回答来自哪个模型的机制。

例如，假设漏洞利用被频繁发现，那么在新代码发布之前，模型提供商可以向代码开发者提供一份“失败证明”（Proof-of-Failure）：证明自己确实让某个特定模型花费了至少 X 个 token，却没有达到某个特定结果。比如，某个模型在至少尝试了 100 万个 token 后，仍未在某份特定补丁中发现任何漏洞。

挑战四：模型审批

监管可能要求提供商只提供已被批准为安全的模型，而不能提供被认为存在网络安全或其他安全风险的模型。提供商可能有动机绕开要求，因为风险模型也许比竞争对手更强，或服务成本更低。监管者如何确保对外提供的只有获批模型？

zkSNARK 能提供的帮助：监管者可以要求提供商为回答附上 zkSNARK，以落实只能使用获批模型的要求。证明将每个请求绑定到实际使用的模型，因此使用未获批准的模型时，证明就无法通过验证。借助简洁性，监管者可以轻量地检查，而不必重新执行每个请求。

关于基于可信硬件的 PI，还需要说明一点。此前的工作常通过可信执行环境实现 PI。这类硬件方案提供隐私和认证，其基础是制造商能够生产抗篡改硬件。本研究聚焦纯软件的密码学方案，其安全性和隐私依赖于计算问题的困难性。即使硬件、操作系统等环境已被攻破，攻击者若不破解一个在计算上不可行的问题，也无法伪造证明。可信硬件与密码学相互补充，各有不同的保证和取舍，都会在应对上述信任挑战时发挥作用。

我们的系统 FlashProve

FlashProve 是面向大型混合专家（MoE）语言模型的可证明推理系统。更多细节见技术报告，这里介绍系统概况。

FlashProve 涉及两方：模型提供商，也就是证明者；以及用户，也就是验证者。系统分为两个阶段：

• 离线阶段，证明者发布模型权重的承诺值。这是一段简短的指纹，锁定一组确定的权重，同时让权重本身保持隐藏。后续的推理声明都将对照这个承诺值检查，也就是对照此阶段所承诺的模型权重。
• 在线阶段，验证者发出请求，也就是提示词及其对应的输出 token，证明者生成证明文件，证明以下命题：

对所承诺的模型执行计算，会生成这些输出 token。

任何持有承诺值、提示词和回答的人，都可以在没有权重、算力有限的情况下进行检查，并确认：用所承诺的权重处理这条提示词，确实会生成这些 token。

保证

证明文件满足以下“完备性”和“健全性”：

• 诚实的证明会被接受（完备性）。诚实证明者生成的证明，会被验证者接受。
• 证明文件无法伪造（健全性）。对一个错误命题生成有效证明，在实践中是不可能的，相当于破解被广泛认可的密码学假设，因此验证者无需信任证明者。

一个知道模型权重、算力充足的验证者，也能仅凭重新计算实现完备性与健全性：用模型处理提示词，再检查结果是否与回答一致。接下来的两项性质，才是这个系统真正不简单的地方。

• 证明文件不泄露命题之外的信息（零知识性）。验证者无法得知权重、计算过程中的中间值，也不知道每一层运行了哪些专家。模型架构本身，不包括权重，并不隐藏。
• 证明文件小，检查成本低（简洁性）。被证明的计算，是在 H100 GPU 上运行一个 4000亿参数模型，量化版约为 232 GB；验证者收到的证明文件却只有约 19 MB，在 24 核 CPU 上几秒即可检查。审计者或硬件资源远少于提供商的用户，无需使用复杂的基础设施，就能检查证明文件。

评估

我们使用公开的 4-bit 权重，在 Llama 4 Maverick 上测量了协议实现。它是一个 4000亿参数的混合专家模型，每个 token 约使用 170亿参数。验证者的每个请求都是一个 1024-token 窗口，每份证明检查一个 token。证明者运行在配有单张 H100 和 24 个 CPU 核心的服务器上，验证者则运行在 CPU 上。

• 证明者。证明者运行在单张 H100、24 个 CPU 核心的服务器上。每个模型只需执行一次离线阶段，耗时约 39 分钟。出于技术报告中讨论的原因，得到的承诺值大约可用于 1600 万次请求，之后提供商需要重新作出承诺。在线阶段，以 24 个请求为一批时，证明者约需 223 秒，速度为每秒 110 个 token，每份证明为 18.78 MB。
• 验证者。验证者运行在客户端 CPU 上，不需要 GPU，只需获得权重承诺值。客户端先下载合计约 6.5 MB 的承诺数据，再为每次请求下载一份证明。包括离线阶段的检查在内，24 线程验证一份证明需 17 秒，单线程需 21 秒。

与普通推理的比较：我们在 8 张 H100 上，使用广泛采用的推理引擎 vLLM 运行同一模型的 FP8 版本。按 GPU 时间折算，证明一批 24 个请求，约需要 vLLM 同时处理这 24 个请求所需时间的 72 倍，不同运行中为 66—77 倍；在我们尝试的最高负载下运行 vLLM 时，这一倍数约为 94。

系统内部。FlashProve 的底层机制，是一种已用于点对点系统的 zkSNARK，例如以太坊等区块链上的 Starknet、Mantle 等 L2 网络。我们的 zkSNARK 遵循成熟的构建方式：先有一个称为交互式预言机证明（interactive oracle proof，IOP）的信息论对象，再依靠哈希函数将其编译成密码学证明，并且还能提供后量子安全性。我们的 IOP 使用前沿基础组件组装而成，包括带线性约束的编码邻近性测试、查找论证等工具，它们建立在编码理论和复杂性理论的技术之上。将这些部分组合成专门面向推理的 IOP，是一项精细的工作；构造细节见技术报告。

系统工程

FlashProve 得益于我们作出的一些架构决策，技术报告对此有详细讨论。这里列出几点：

• 证明者的工作量，与实际运行的专家数量成正比。在 MoE 模型中，每个 token 只使用 4000亿参数中的约 170亿，因此每个 token 的证明工作量与这约 170亿参数成正比，而不是全部参数；证明仍会隐藏具体选择了哪些专家。
• 请求在完成后批量证明。证明者像预填充阶段那样，在一次并行处理中读取已经完成的文本；每批只需打开一次权重承诺，而不是每个请求打开一次。
• 系统按单张 GPU 可容纳的目标设计。模型每层的权重被拆成若干分段，逐段完成层计算的证明。权重保存在普通内存中，按流式送入 GPU，因此单张 80 GB GPU 加上约 290 GB 主机内存就足够了。

事后证明与同步证明

将证明机制集成进推理服务器时，有两种选择：同步证明，也就是边推理边证明；或事后证明，也就是在计算结束后，对部分 token 生成证明。我们的系统采用后者。同步方案通常要求极快的速度，可能为了效率牺牲安全性；事后方案允许慢一些，未必需要作出同样的取舍。不过，事后证明也有限制，包括重新计算增加的复杂性、获得流量保证的延迟，以及固有的“非确定性”。技术报告进一步讨论了采用事后证明的动机及其影响。

通过形式化验证建立可信性

密码学代码出了名地脆弱、容易出错。用户凭什么信任我们今天发布的代码？

答案是形式化验证：我们用 Lean 证明助手描述协议及期望的安全性质，并以机器可检查的形式证明这些性质，保证其正确性，编译器错误除外。我们针对三项顶层性质：

1. 完备性：如果命题正确，生成的证明会被验证者接受。
2. 健全性：任何伪造证明都会被验证者拒绝，仅允许可忽略不计的概率例外。
3. 零知识性：除了验证者从回答本身能够推断出的内容，证明不会泄露模型权重的任何信息。[4]

这些性质在所谓的随机预言机模型中表述。这是一种从信息论角度分析依赖哈希函数的密码学协议的方法。

形式化验证仍留下两处重要的信任缺口。首先，必须审计形式化命题，确认它们准确表达了原意。这需要人工完成，尽管负担比审计证明小得多；我们提供了交互式可视化工具来辅助这项工作。

其次，必须审计可执行代码，确认它与已经证明安全性质的形式化协议一致。如何更好地辅助审计，取决于具体性质：健全性只依赖验证者，零知识性只依赖证明者，而完备性取决于双方交互。

• 对于健全性，我们只需验证者代码正确即可。拥有“证明”的全部价值，就在于只要信任验证者，就可以完全不信任证明者。除 C++ 验证器外，我们还提供可执行的 Lean 验证器。Lean 验证器更慢，但 Lean 证明了它只会接受健全性定理中的验证器所接受的证明。不过，日常使用仍应选择 C++ 验证器：它没有形式化保证，但在我们的测试中，对每份证明的判断都与 Lean 验证器一致。
• 对于完备性，威胁模型不假设对抗性攻击，证明者和验证者都是诚实的。因此，有了 Lean 验证器，我们就可以通过标准软件测试，对诚实证明者能否生成会被接受的证明建立信心：先让证明者为一个正确命题生成证明，再用 Lean 验证器检查。
• 对于零知识性，我们只需证明者正确即可。然而，证明者不同于验证者，它是一项昂贵的计算过程，运行 Lean 证明器并不现实。我们在这里没有提供额外的辅助措施：我们预计，任何希望隐藏所服务模型权重的证明方，都有足够资源开展细致的 Agent 安全审计和／或人工安全审计，确认其实现与 Lean 证明器等价。

已有工作

实现可证明推理，是通常被称为“zkML”的一系列研究的目标。早期工作如 SafetyNets（2017）验证了一个包含两层卷积的 MNIST 卷积网络和一个小型全连接语音模型；zkCNN（2021）推进到 1500万参数的 VGG-16，每份证明耗时 88.3 秒；Kang 等人（2022）则证明了在全分辨率 ImageNet 上运行的 MobileNet v2。

随后出现了 Transformer 的证明：ZKML 对 1.17亿参数 GPT-2 的证明，每个 token 约需 159 秒，约合每秒 0.006 个 token；Modulus Labs 的 15亿参数 GPT-2 XL 则需要超过 90 小时。EZKL（2023）证明了一个 100万参数的 GPT 风格 Transformer，每个 token 约需 966 秒，约合每秒 0.001 个 token。性能逐步改善：zkLLM（2024）在 GPU 上为 LLaMA-2-13B、2048-token 输入生成证明约需 15 分钟，若按新增 token 计，约为每秒 0.001 个；按批量计，约为每秒 2.5 个 token。2025年，zkGPT 将 GPT-2 的证明时间降至 21.8 秒，约合每秒 0.05 个 token；zkPyTorch 在单个 CPU 核心上证明 Llama-3 8B，每个 token 约需 150 秒，约合每秒 0.007 个 token；ZKTorch 证明 GPT-J（60亿参数）约需 20 分钟，约合每秒 0.001 个 token。VerInf 对 Llama 4 Maverick，也就是我们所证明的同一个 4000亿参数 MoE 模型，速度约为每秒 0.02 个 token。DeepProve 是目前经过同行评审的前沿方案，它只需一次前向计算，就能认证整个生成序列。在单机上，它对 GPT-2 可达每秒约 2.9 个 token，对 Gemma 3 可达每秒 1.4 个 token，分布式部署可达每秒 31 个 token。SASH 的证明器（2026）在单张 H100 上证明 Llama 3.1 8B，速度约为每秒 1.25 个 token。

近期，商业项目也取得了令人印象深刻的数字：Attestable 在单张 H100 上证明 Gemma 4 31B，可达每秒 53—77 个 token；截至本文写作时，Attestable 尚未发布相应的开源库。

这些数字展现了过去几年可证明推理的迅猛进展，也应该改变我们对零知识证明能力边界的原有判断。

• 2024年，zkLLM 在单张 A100 上证明 130亿参数模型，速度约为每秒 2.5 个 token。我们所知此前唯一针对 Llama 4 Maverick 的证明来自 VerInf：据其报告，在 DGX Spark 上证明 1000 个 token 需要 14.3 小时，证明文件为 93.6 GB，验证耗时接近一天。
• FlashProve 在单张 H100 上证明同一个模型，可达每秒 110 个 token；证明文件为 19 MB，几秒即可验证。Attestable 则独立报告，其对一个 310亿参数稠密模型的速度为每秒 53—77 个 token。

我们相信，这些进展应该能够迁移到更多模型与架构，形成灵活而强大的工具。相较原生计算，额外开销大致为两个数量级，我们测得约 70—95 倍，远低于此前的预期。

局限

此次发布的是研究原型，存在以下技术局限：

• 快速可执行代码没有形式化保证。我们提供协议的 Lean 实现，包括可执行的“慢速”Lean 验证器，以及在 Lean 中证明的安全性质。论文与快速可执行代码均从 Lean 协议推导而来，但我们不保证三者——Lean、论文和代码——完全一致。
• 证明针对的是采用贪心解码的整数模型。我们证明的是公开权重的一个精确整数版本，每份证明断言所检查的 token 是该模型按贪心方式选出的结果。来自浮点实现或采样解码的回答，可能在某个位置出现偏差，从而不再与所证明的计算精确匹配。一般预期以及实证测试都表明，整数版本与真实浮点推理之间的误差率较小，即便考虑浮点计算的非确定性也是如此；但这不涵盖经过对抗性设计的提示词。
• 隐藏架构。我们的系统假设所服务的模型采用混合专家架构：每个 Transformer 层的前馈模块被多个专家子网络和一个路由器替代，路由器为每个 token 仅激活一小部分专家。系统利用这种 MoE 结构提高效率。稠密模型等其他架构也被广泛使用，架构描述中可能包含提供商希望保密的知识产权。的确，我们也可以设想一个进一步隐藏模型架构的系统：证明者通过隐藏承诺，同时承诺权重与架构，也就是用于推理的“可执行代码”；验证者所检查的命题，则是在所承诺模型上执行这份已承诺代码的结果。
• 侧信道攻击。协议当前保证的是，证明本身不会泄露所承诺模型的权重信息。然而，测量生成证明所需时间等“侧信道攻击”，仍可能泄露权重信息。此次发布不处理这一问题。
• 更长的上下文。系统目前可证明的推理上下文长度最多为 1024 个 token。相较聊天场景中累积的上下文，这相当短。理想情况下，应将其扩展到前沿模型的完整上下文窗口，这些窗口通常可达数十万到数百万个 token。

脚注

[1] 在这项开源研究中，我们使用了 Meta 的 Llama 4 Maverick（4000亿参数），具体为 Hugging Face 上由第三方公开转换的 4-bit 版本。此次发布不包含权重，读者需要自行从 Hugging Face 下载，并遵守 Meta 的 Llama 4 许可证。我们分享的是由模型计算得到的一些小型产物，例如承诺 ID、校验和、性能数据及部分参数设置，THIRD_PARTY.md 列出了完整清单。我们鼓励读者自行验证结果，并将工作适配到其他模型。运行完整示例需要大型 GPU 机器，以及对 Meta 分词器的访问权限。

[2] 具体隐藏哪些信息，取决于系统设计。在我们的工作中，隐藏的是权重，而非架构。未来我们计划同时隐藏架构细节。原则上，可以隐藏模型的全部细节；问题是能够做到多高的效率。

[3] 在2026年10月19日的更新中，我们也修改了这一目标的名称：现在使用“推理验证”（inference verification），而不是“可证明推理”（provable inference）。我们最初希望对 token 流的完整性获得高度保证，而实现这一目标有多种方式；“可证明推理”暗示的路径比我们认为必要的更窄。除那个原型外，我们也在推进推理的密码学证明，这是对 token 流获得高度保证的其中一种方法。

[4] 模型架构并未隐藏。进一步隐藏架构细节，留待未来工作。

参考链接

• 原文：https://www.anthropic.com/research/provable-inference
• Read the technical report：https://www.anthropic.com/document/flashprove-technical-report
• Frontier Red Team：https://www.anthropic.com/research/team/frontier-red-team
• technical report：https://www.anthropic.com/document/flashprove-technical-report
• protocol specification：https://github.com/anthropics/FlashProve/blob/main/paper/paper.pdf
• Executable code：https://github.com/anthropics/FlashProve
• prover：https://github.com/anthropics/FlashProve/tree/main/prover
• fast verifier：https://github.com/anthropics/FlashProve/tree/main/verifier
• provably correct verifier：https://github.com/anthropics/FlashProve/tree/main/tools/lean-verify
• Lean proofs：https://github.com/anthropics/FlashProve/tree/main/lean
• interactive visualizer：https://github.com/anthropics/FlashProve/blob/main/lean/STATEMENTS.html
• trust challenges：https://arxiv.org/abs/2004.07213
• regulate：https://thefuturesociety.org/international-ai-verification
• pace：https://darioamodei.com/post/we-must-pace-the-frontier
• monitoring hardware and how it is used：https://arxiv.org/abs/2402.08797
• devote its hardware to inference：https://arxiv.org/abs/2506.15867
• prime targets：https://www.rand.org/pubs/research_reports/RRA2849-1.html
• compromise an inference server：https://www.wiz.io/blog/nvidia-triton-cve-2025-23319-vuln-chain-to-ai-server
• hiding among genuine responses：https://arxiv.org/abs/2511.02620
• Frontier Safety Roadmap：https://www.anthropic.com/responsible-scaling-policy/roadmap
• public goal：https://www.anthropic.com/responsible-scaling-policy/roadmap
• cheaper one：https://arxiv.org/abs/2504.04715
• degraded version：https://kimi.com/blog/kimi-vendor-verifier
• their chosen model：https://arxiv.org/abs/2410.20247
• existing mechanisms：https://arxiv.org/abs/2511.20621
• serve only models approved as safe：https://arxiv.org/abs/2307.03718
• only approved models are served：https://arxiv.org/abs/2507.15916
• Llama 4 Maverick：https://huggingface.co/meta-llama/Llama-4-Maverick-17B-128E-Instruct
• vLLM：https://vllm.ai/
• L2 networks：https://l2beat.com/layer2s/summary?filters=%7B%22ProofSystem%22%3A%7B%22values%22%3A%5B%22Validity%22%5D%7D%7D
• Starknet：https://www.starknet.io/
• Mantle：https://www.mantle.xyz/
• SafetyNets：https://proceedings.neurips.cc/paper_files/paper/2017/file/6048ff4e8cb07aa60b6777b6f7384d52-Paper.pdf
• zkCNN：https://eprint.iacr.org/2021/673
• Kang et al：https://arxiv.org/abs/2210.08674
• ZKML’s GPT-2：https://ddkang.github.io/papers/2024/zkml-eurosys.pdf
• Modulus Labs’：https://medium.com/@CountableMagic/chapter-14-the-worlds-1st-on-chain-llm-7e389189f85e
• zkLLM：https://arxiv.org/abs/2404.16109
• zkGPT：https://eprint.iacr.org/2025/1184.pdf
• zkPyTorch：https://eprint.iacr.org/2025/535
• ZKTorch：https://arxiv.org/abs/2507.07031
• VerInf：https://github.com/JamesPetrie/VerInf
• DeepProve：https://eprint.iacr.org/2026/1112
• SASH's prover：https://www.aisafety.sg/research/what-proving-llm-inference-actually-costs-research-note
• Attestable：https://attestable.com/blog/proving-llms-scale