Anthropic 开源 FlashProve，可在普通 CPU 上验证回复出自哪个模型
Anthropic just open-sourced FlashProve, which lets you check which AI model actually wrote a reply
Anthropic 开源 FlashProve，让服务器能以数学方式证明某条回复来自指定模型，验证可在普通 CPU 上完成。在 Meta 的 Llama 4 Maverick（400B 参数）上，单张 Nvidia H100 以 110 tokens/秒生成证明，每份约 19MB，普通 CPU 约 17 秒校验一份；此前唯一已知能证明该模型的 VerInf 生成 93.6GB 证明，校验耗时接近一天。该系统由 Claude 构建，因代码难以审计，其安全保证在 Lean 4 中以数学方式证明。
推荐理由
AI 评分 72
原文给出了证明体积和校验耗时的对比数字，读者可据此判断可验证推理在部署中的可行性。
主题
查看原帖Anthropic 新研究：大语言模型可证明推理方面的进展。 在此，我们推出 FlashProve。基于成熟的密码学技术，FlashProve 让开发者能够验证某条回复是否来自某个给定的 AI 模型。相比此前用于此目的的开源方法，它的效率大幅提升。 这些证明有着广泛的应用场景。例如，它们可以增加攻击者劫持聊天内容的难度，或让安全评估人员能够验证他们所测试的模型与向客户提供服务的模型是同一个。 完整报告见此处：https://t.co/OIZWPb6QZa 可证明推理的进一步进展，很可能成为提升 AI 部署信任度的重要组成部分。为此，我们开源了 FlashProve 的代码，见此处：https://t.co/7ky3Ir8V06 我们感谢我们的合作者：Alessandro Chiesa、@GiacomoFenzi、@gwberg95、@miranda__christ、Rahul Dalal（https://t.co/pjWKLHWXyz）以及 Ben Mayer（@transmissions11）。
查看原文
New Anthropic research: progress on provable inference for large language models. Here, we introduce FlashProve. Building on established cryptographic techniques, FlashProve allows developers to verify whether a given response came from a given AI model. It’s substantially more efficient than prior open-source methods for doing so. These proofs have a range of applications. They can, for instance, make it harder for attackers to hijack a chat, or enable safety evaluators to verify that the model they’re testing is the same one being served to customers. For our full write-up, see here: https://t.co/OIZWPb6QZa Further progress in provable inference will likely be an important part of improving trust in AI deployment. To that end, we're open-sourcing FlashProve’s code, here: https://t.co/7ky3Ir8V06 We’re grateful to our collaborators: Alessandro Chiesa, @GiacomoFenzi, @gwberg95, @miranda__christ, Rahul Dalal (https://t.co/pjWKLHWXyz) and Ben Mayer (@transmissions11).
正文
Anthropic just open-sourced FlashProve, which lets you check which AI model actually wrote a reply
checkable on an ordinary CPU.
e.g. if you pay for a top AI model through a reseller, you can’t check whether it quietly served a cheaper one. Anthropic’s FlashProve lets the server prove mathematically which model answered.
Anthropic tested it on Meta’s Llama 4 Maverick, a large 400B-parameter open model, where a single Nvidia H100 GPU produced proofs at 110 tokens/second, each about 19MB.
A regular CPU checks each proof in about 17 seconds, while VerInf, the only earlier system known to prove this model, made 93.6GB proofs that took almost a day to check.
Claude built the system, and because its code is hard to audit, the security guarantees are mathematically proved in Lean 4, a proof-checking language,