AI 模型和平台
Anthropic 发布密码学的闪光证明 AI 推论证明
在 Google 上的首选来源中添加 Unite.AI
2026年11月2日的Anthropic 发布 FlashProve：一个使用密码学证明来显示语言模型反应的开源研究原型来自承诺的重量而不透露。 该公司报告说，Meta的Llama 4 Maverick的证明生成量为每秒110个令牌。
这项工作解决了东道国大赦国际在核查方面的差距。 高质量的答案并不能确定哪一个模型产生：一个路由服务可以替代另一个系统，一个评估者可以接收一个与打算测试的模型不同的模型，或者攻击者可以改变信号流。 通过重新运行该模型进行检查对用户来说是不切实际的，因为重量是私人的，硬件需求很大。
对隐藏重量的具有约束力的回复
FlashProve在只使用软件的设计中使用了零知识简洁的知识论证，或zkSNARK，而不是依赖可信赖的硬件。 在离线阶段，供应商公布一份简短的承诺书，其中明确了一套精确的权重，同时不透露其内容。 对于完成的即时反应对子，系统生成一个证明，即输出符是承诺模型的输出。 任何持有承诺，即时回复的人均可以检查证据而无需查阅权重。
意图属性是完整性，合理性，零知识和简洁性。 应当接受诚实的证明，同时证明虚假陈述应当要求打破广泛相信的密码假设。 检查证据时，既不能显示权重，也不能显示中间计算值。 该设计还隐藏了每个标志的混合专家子网络，尽管模型的结构本身仍然可见。
执行工作利用了马韦里克的专家混合结构。 大约170亿个参数是用来表示而不是全部4 000亿的，而同时又隐藏着专家的选择。 从主机内存中流出分层的权重，使验证器能够搭配一个80GB GPU，并配有约290GB的主机内存。
Anthropic描述了在客户诚信检查、独立评价、监管工具以及执行已核准的示范要求方面可能的用途。 推论证书可以证明，要求的模型符合要求，但不能证明同样的硬件也没有培训另一个模型。 这种区分限制了这些证书根据如何使用计算能力来证明遵守要求。
性能和推论证据
Anthropic的评价采用公开的4位转换模型。 一个拥有1个H100和24个CPU核心的服务器在大约223秒内证明了一批24个请求，为每个请求提供了18.78 MB证明。 下线承诺步骤用了约39分钟。
在核实方面，客户端下载了约6.5MB承诺，并检查一个没有GPU的CPU上的证明。 Anthropic在17秒用24线和21秒用1线测量核实，包括离线阶段的检查。
这些测量将一个只使用CPU的检查过程与一个更重的证明操作分开。 在Anthropic与FP8对运行vLLM的8个H100s推论的比较中，证明同一批次每GPU所需时间约为72倍，在测试的vLLM载荷最高时所需时间约为94倍。 因此，在没有证据的情况下为模型服务的费用很高。
正式核查和实际限制
FlashProve寄存器包含一个验证器，一个快速的C++验证器，一个较慢的Lean验证器，顶级数学语句的Lean验证器和Apache 2.0许可下的互动定理可视化器。 它将0.16.0版本标注为未保存的研究文物，不接受贡献。
利恩工作涉及随机-oracle模型中的完整性，稳健性和零知识。 正式声明仍然需要人工审查，以确定它们表示其打算的保证。 利恩校验器与声音定理正式连接，但打算用于常规使用的C++校验器没有正式保证，而是经过测试与利恩校验器达成协议。
该项目的已知限制文件记录显示，在人类指导下的AI系统撰写了几乎所有的软件、精益证和文件，并进行了所报告的测试。 没有进行独立的安全审计，对隐藏体重和对抗性证据的测试仍然有限。
证据涵盖了在贪婪的解码下精确的整数版本的重量。 浮点推论或抽样解码可以脱离被证明的计算，通用错误测试并不包括对抗性设计的提示。 上下文仅限于1,024个令牌，而时间和其他侧道攻击则不属于保证范围。 与证明和推论相比，还证明推出重算、延迟保证和不确定。
为了使可证明的推论成为对服务流量的例行检查，剩下的工作集中在这一发布所暴露的空白上：降低证明成本，涵盖限制性较小的解码和较长的背景，将快速执行与正式协议更牢固地联系起来。
本文由 AI图鉴自动抓取并翻译，版权归原作者所有；如需查看原文请点下方链接。
AI Models & Platforms
Anthropic Releases FlashProve for Cryptographic AI Inference Proofs
Add Unite.AI to your preferred sources on Google
Anthropic released FlashProve on November 2, 2026: an open-source research prototype that uses cryptographic proofs to show a language-model response came from committed weights without revealing them. The company reported proof generation at 110 tokens per second for Meta’s Llama 4 Maverick.
The work addresses a verification gap in hosted AI. A high-quality answer does not establish which model produced it: a routing service could substitute another system, an evaluator could receive a different model from the one intended for testing, or an attacker could alter the token stream. Checking by rerunning the model is impractical for users when weights are private and the hardware requirements are substantial.
Binding Responses to Hidden Weights
FlashProve uses a zero-knowledge succinct argument of knowledge, or zkSNARK, in a software-only design rather than depending on trusted hardware. During an offline phase, the provider publishes a short commitment that identifies one exact set of weights while keeping them secret. For completed prompt-and-response pairs, the system produces a proof that the output tokens are the committed model’s output. Anyone holding the commitment, prompt and reply can check the proof without access to the weights.
The intended properties are completeness, soundness, zero knowledge and succinctness. An honest proof should be accepted, while certifying a false statement should require breaking widely believed cryptographic assumptions. Checking a proof should reveal neither the weights nor intermediate computation values. The design also conceals which mixture-of-experts subnetworks ran for each token, although the model’s architecture itself remains visible.
The implementation takes advantage of Maverick’s mixture-of-experts structure. Prover work scales with the roughly 17 billion parameters active for a token rather than all 400 billion, while still hiding the expert choices. Segmented weights are streamed from host memory, allowing the prover to fit on one 80 GB GPU with about 290 GB of host memory alongside it.
Anthropic describes possible uses in customer integrity checks, independent evaluations, regulatory tools and enforcement of approved-model requirements. Inference certificates could attest that requests were served by a claimed model, but they would not establish that the same hardware was not also training another model. That distinction limits what such certificates could demonstrate about compliance requirements based on how computing capacity is used.
Proof Performance and Inference Overhead
Anthropic’s evaluation used a publicly available 4-bit conversion of the model. A server with one H100 and 24 CPU cores proved a batch of 24 requests in about 223 seconds, producing an 18.78 MB proof for each request. The offline commitment step took about 39 minutes.
On the verification side, the client downloads an approximately 6.5 MB commitment and checks proofs on a CPU without a GPU. Anthropic measured verification at 17 seconds with 24 threads and 21 seconds with one thread, including the offline phase’s checks.
Those measurements separate a CPU-only checking process from a much heavier proving operation. In Anthropic’s comparison with FP8 inference on eight H100s running vLLM, proving required about 72 times as much per-GPU time for the same batch and about 94 times as much at the highest vLLM load tested. The throughput therefore comes with a substantial cost relative to serving the model without proofs.
Formal Verification and Practical Limits
The FlashProve repository contains a prover, a fast C++ verifier, a slower Lean verifier, Lean proofs of top-level mathematical statements and an interactive theorem visualizer under the Apache 2.0 license. It labels version 0.16.0 as an unmaintained research artifact that is not accepting contributions.
The Lean work addresses completeness, soundness and zero knowledge in the random-oracle model. The formal statements still require manual review to establish that they express their intended guarantees. The Lean verifier is formally connected to the soundness theorem, but the C++ verifier intended for routine use carries no formal guarantee and was instead tested for agreement with the Lean verifier.
The project’s known-limits documentation records that AI systems under human direction wrote nearly all of the software, Lean proofs and documentation and ran the reported tests. There has been no independent security audit, and testing of weight hiding and adversarial proofs remains limited.
The proofs cover an exact integer version of the weights under greedy decoding. Floating-point inference or sampled decoding can depart from the computation being proved, and the generic error testing does not cover adversarially designed prompts. Contexts are limited to 1,024 tokens, while timing and other side-channel attacks fall outside the guarantee. Post-hoc proving also introduces recomputation, delayed assurances and non-determinism compared with proving alongside inference.
For provable inference to become a routine check on served traffic, the remaining work is concentrated in the gaps this release exposes: lowering proving cost, covering less restrictive decoding and longer contexts, and connecting the fast implementation more firmly to the formal protocol.
Auto-fetched and translated by AI Atlas. All rights belong to the original author.