资源

能帮助读者核查 AI 系统声明的论文、规范、工具与报告,可信执行环境相关条目排在最前。收录不代表背书。“链接核查于”注明我们最近一次打开该链接的日期。

阅读路径

从 TEE 读起

先了解远程证明的基本概念:机器签署一份记录,写明自己加载了哪些软件,供他人核查。然后再看 CPU 和 GPU 平台,经远程证明的 AI 服务就运行在这些平台上。

  1. RFC 9334: Remote ATtestation procedureS (RATS) Architecture定义了证明方、验证方和依赖方这三个角色,后面各篇文献都以它们为前提。
  2. Intel TDX Demystified: A Top-Down Approach由 Intel 以外的研究人员讲解 TDX 隔离整台虚拟机的设计。
  3. AMD SEV-SNP: Strengthening VM Isolation with Integrity Protection and MoreSEV-SNP 针对恶意的虚拟机监控器(hypervisor,即管理虚拟机的软件)增加了哪些防护,AMD 又把哪些威胁排除在防护范围之外。
  4. Arm Confidential Compute ArchitectureArm 的 Realm 如何按设计把工作负载与虚拟机监控器隔开,而调度仍由后者负责。
  5. Confidential Computing on NVIDIA H100 GPUs for Secure and Trustworthy AIGPU 如何纳入信任边界,以及 NVIDIA 不加密哪部分显存。
  6. Private Cloud Compute Security Guide一套完整的服务设计,附带研究环境,外界可以在其中运行并检查节点软件。

TEE 的保护在哪里止步

已公开的攻击显示了隔离与远程证明在哪些情况下会失效。其中多数攻击需要物理接触服务器。

  1. TEE.fail: Breaking Trusted Execution Environments via DDR5 Memory Bus Interposition一种物理攻击:提取密钥以伪造 TDX 证明报告(quote),并表明 GPU 证明报告可以从其他机器“借用”。
  2. BadRAM: Practical Memory Aliasing Attacks on Trusted Execution Environments研究人员用不到 10 美元的设备改动内存条,为植入后门的 SEV-SNP 虚拟机重放了正常虚拟机的度量值。
  3. Battering RAM: Low-Cost Interposer Attacks on Confidential Computing via Dynamic Memory Aliasing插入器装在处理器与内存之间,先通过启动检查,之后在已打全补丁的系统上攻破 SEV-SNP 的远程证明。
  4. Proof of Cloud: Data Center Execution Assurance for Confidential VMs一项应对提案:把远程证明与可信数据中心里的某台机器绑定。
  5. Machine Learning with Confidential Computing: A Systematization of Knowledge一篇综述:TEE 能为机器学习任务提供什么,不能提供什么。

私密 AI 服务:服务商的自述

这里是服务商对自身设计的描述,应当作服务商的声明来读,并留意每种设计让外界能核查什么。

  1. Private Cloud Compute: A new frontier for AI privacy in the cloudApple 对云端 AI 提出的要求:用户设备要能够核验它。
  2. Building Private Processing for AI tools on WhatsAppMeta 为 WhatsApp 设计的方案,上线前经过了 Trail of Bits 的审计。
  3. Private AI Compute: our next step in building private and helpful AIGoogle 的平台,其中大部分远程证明核查在 Google 内部完成。
  4. Confidential Inference via Trusted Virtual Machines一份早期设计:只有一个经过远程证明的小型加载器能解密提示词和权重。
  5. Azure AI Confidential Inferencing: Technical Deep-DiveMicrosoft 规划中的设计:密钥服务只把解密密钥释放给通过远程证明的 GPU 虚拟机。
  6. RFC 9458: Oblivious HTTP几项服务借助这一中继协议,对服务器隐藏客户端的网络地址。

与 TEE 相比的其他核查方法

签名、审计、重新执行和数学证明要求你信任的参与方,都与 TEE 不同。每种方法可以先读一到两篇。

  1. Sigstore签名与公开日志:签名方担保的是什么。
  2. Black-Box Access is Insufficient for Rigorous AI Audits审计:为什么访问深度决定了审计能发现什么。
  3. TOPLOC: A Locality Sensitive Hashing Scheme for Trustless Verifiable Inference重新执行:为模型的中间计算值(激活值)生成的指纹,能容忍不同 GPU 型号之间的差异。
  4. Verde: Verification via Refereed Delegation for Machine Learning Programs带仲裁方的重新执行:把服务商之间的争议缩小到单个算子。
  5. zkLLM: Zero Knowledge Proofs for Large Language Models数学证明:一套零知识证明系统,可让他人在看不到模型权重的情况下,核查模型是否正确算出了输出。作者将其用于 130 亿参数的模型。
  6. A Survey of Zero-Knowledge Proof Based Verifiable Machine Learning数学证明:零知识机器学习的现状,以及制约它的因素。

显示 170 项,共 170 项

机密计算与远程证明 27

需要信任:芯片厂商与被度量的软件

架构与标准 5

  • RFC 9334: Remote ATtestation procedureS (RATS) Architecture

    IETF · 2023 · 规范 链接核查于 2026年10月20日

    简介

    IETF 的信息类 RFC,定义了远程证明中的角色与消息。角色包括证明方、验证方和依赖方;消息包括证据、背书、参考值和证明结果。

  • Confidential Computing Consortium

    Linux Foundation · 2019 · 机构 链接核查于 2026年10月20日

    简介

    Linux 基金会旗下的社区,致力于加快可信执行环境(TEE)技术的采用。它还维护这些技术的开源项目和远程证明规范。

  • RFC 9458: Oblivious HTTP

    IETF · 2024 · 标准 链接核查于 2026年10月20日

    简介

    IETF 标准轨道协议:由中继转发加密的 HTTP 请求。服务器看不到客户端的 IP 地址,中继也看不到请求内容。Apple 和 Meta 通过第三方 OHTTP 中继转发 AI 请求,以阻碍针对特定用户的攻击。

  • Caliptra

    CHIPS Alliance (Linux Foundation) · 2022 · 项目 链接核查于 2026年10月20日

    简介

    一种信任根模块,供芯片厂商集成到数据中心的 CPU、GPU 等片上系统(SoC)中。它提供设备身份、度量启动和远程证明能力。其规范、硬件设计(RTL)、ROM 和固件均已开源。AMD、Google、Microsoft 和 NVIDIA 于 2022 年在开放计算项目(OCP)峰会上联合发布了这一项目。

  • RFC 9711: The Entity Attestation Token (EAT)

    IETF · 2025 · 标准 链接核查于 2026年10月20日

    简介

    IETF 标准轨道规范,规定证明证据和证明结果的格式,以 CBOR Web Token(CWT)或 JSON Web Token(JWT)承载。它定义了一组常用声明,例如表明证据足够新的随机数(nonce)、通用实体标识(UEID)、硬件制造商以及软件名称和版本。它沿用 RFC 9334 的 RATS 架构。

CPU TEE 3

  • AMD SEV-SNP: Strengthening VM Isolation with Integrity Protection and More

    AMD · 2020 · 报告 链接核查于 2026年10月20日

    简介

    AMD 介绍 SEV-SNP 的白皮书。SEV-SNP 在加密虚拟机的基础上增加内存完整性保护,以防范恶意的虚拟机监控器。它用每颗芯片及其 TCB 版本独有的密钥签署证明报告;TCB 版本指芯片上各个可信组件的版本。

  • Intel TDX Demystified: A Top-Down Approach

    Pau-Chen Cheng et al. · 2023 · 论文 链接核查于 2026年10月20日

    简介

    Intel 以外的研究人员对 Intel Trust Domain Extensions(TDX)的分析。论文解释了 TDX 如何按设计用加密且受完整性保护的内存隔离虚拟机,以及它的远程证明如何运作。

  • Arm Confidential Compute Architecture

    Arm · 2021 · 规范 链接核查于 2026年10月20日

    简介

    Armv9-A 的安全架构,其中的 Realm 管理扩展(RME)可创建称为 Realm 的硬件隔离执行环境。Realm 由开源的 Realm 管理监控器(RMM)管理。宿主机的虚拟机监控器仍决定运行哪些 Realm、为它们分配哪些内存。但按照架构设计,虚拟机监控器无法访问或修改 Realm 中的代码和数据。

GPU 机密计算 2

  • Confidential Computing on NVIDIA H100 GPUs for Secure and Trustworthy AI

    NVIDIA · 2023 · 报告 链接核查于 2026年10月20日

    简介

    NVIDIA 对 H100 GPU 机密计算的技术概述。内容涵盖片上信任根、度量启动、签名的证明报告,以及 CPU 与 GPU 之间的加密传输。文中说明,封装内的高带宽显存(HBM)不加密。

  • NVIDIA Attestation

    NVIDIA · 工具 链接核查于 2026年10月20日

    简介

    NVIDIA 各项远程证明服务及配套 SDK 的文档,这些 SDK 用于验证 GPU 证据。服务包括 NVIDIA 远程证明服务(NRAS)和参考完整性清单(RIM)服务,后者提供参考值。另有一项 OCSP 服务,用于报告证书是否已被吊销。

使用远程证明的 AI 服务 6

  • Private Cloud Compute: A new frontier for AI privacy in the cloud

    Apple · 2024 · 项目 链接核查于 2026年10月20日

    简介

    Apple 在云端处理 Apple Intelligence 请求的设计。设计围绕五项要求展开:无状态计算、可强制执行的保证、无特权运行时访问、不可定向性和可验证透明性。

  • Private Cloud Compute Security Guide

    Apple · 2024 · 报告 链接核查于 2026年10月20日

    简介

    Apple 关于 Private Cloud Compute(PCC)设计的技术文档。配套的虚拟研究环境(VRE)可在 Mac 上运行 PCC 节点软件。Apple 还公开了部分安全关键组件的源代码。

  • Building Private Processing for AI tools on WhatsApp

    Meta · 2025 · 项目 链接核查于 2026年10月20日

    简介

    Meta 的设计:在机密虚拟机中运行 WhatsApp 的 AI 功能,并使用处于机密计算模式的 GPU。客户端通过 RA-TLS 对照第三方日志核查远程证明;RA-TLS 把远程证明与 TLS 连接绑定在一起。客户端经由不经意 HTTP(OHTTP)中继连接,中继使服务器看不到客户端的 IP 地址。

  • Private AI Compute: our next step in building private and helpful AI

    Google · 2025 · 项目 链接核查于 2026年10月20日

    简介

    Google 宣布推出的平台:借助 Titanium Intelligence Enclaves,在自研的张量处理单元(TPU)上运行 Gemini 模型。用户设备通过远程证明和加密与平台连接。

  • Confidential Inference via Trusted Virtual Machines

    Anthropic, with Pattern Labs · 2025 · 报告 链接核查于 2026年10月20日

    简介

    Anthropic 尚处早期阶段的推理服务器设计。能解密提示词和模型权重的只有一个经过远程证明的小型加载器,而不是整个服务器。可信平台模块(TPM)记录的启动度量值决定密钥能否释放。

  • Azure AI Confidential Inferencing: Technical Deep-Dive

    Mark Russinovich (Microsoft) · 2024 · 报告 链接核查于 2026年10月20日

    简介

    Microsoft 为 Azure OpenAI 服务规划的机密推理设计,宣布时称将推出预览版。客户端用不经意 HTTP(OHTTP)加密提示词。密钥管理服务只把解密密钥发放给通过远程证明的机密 GPU 虚拟机,这些虚拟机基于 AMD SEV-SNP 和 NVIDIA H100。部署的代码、容器策略和密钥释放策略都记录在透明账本中。

攻击与局限 4

  • TEE.fail: Breaking Trusted Execution Environments via DDR5 Memory Bus Interposition

    Jalen Chuang et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    一种物理攻击:用接在 DDR5 内存总线上的插入器,从 Intel TDX 和 AMD SEV-SNP 机器中提取密钥。被提取的密钥包括一把 Intel 证明密钥,研究人员用它伪造了 TDX quote,即 Intel 所称的证明报告。研究还表明,NVIDIA GPU 的证明报告没有绑定特定的机密虚拟机,因此可以从其他机器“借用”。

  • Proof of Cloud: Data Center Execution Assurance for Confidential VMs

    Filip Rezabek et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    一项设计:把机密虚拟机的远程证明与宿主机可信平台模块(TPM)的证据绑定。验证方由此能够确认,工作负载运行在可信数据中心的机器上。按设计,这种绑定还能阻止中继攻击,即拿另一台机器的远程证明冒充本机。

  • BadRAM: Practical Memory Aliasing Attacks on Trusted Execution Environments

    Jesse De Meulemeester et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    一种攻击:内存条的串行存在检测(SPD)芯片被篡改后,会谎报内存容量。错误的容量会产生地址别名,即两个地址指向同一个内存位置。攻击者只需不到 10 美元的设备,就能借此绕过 AMD SEV-SNP 的内存保护。攻击者还能为植入后门的虚拟机重放正常虚拟机在远程证明中的度量值。AMD 随后发布固件,在启动时检查内存配置;Intel TDX 和可扩展 SGX 早已具备此类检查。

  • Battering RAM: Low-Cost Interposer Attacks on Confidential Computing via Dynamic Memory Aliasing

    Jesse De Meulemeester et al. · 2026 · 论文 链接核查于 2026年10月20日

    简介

    一种攻击:在处理器与 DDR4 内存之间安装成本不到 50 美元的插入器。插入器在启动检查期间表现正常,之后在运行时制造地址别名。它能以明文读写 Intel 可扩展 SGX 的飞地内存,并在已打全补丁的系统上攻破 AMD SEV-SNP 的远程证明。Intel 和 AMD 表示,针对 DRAM 的物理攻击不在其现有产品的防护范围之内。

性能 1

TEE 在评测、智能体与模型安全中的应用 6

模型与数据供应链 24

需要信任:签名方及其密钥

  • SLSA Specification v1.2

    SLSA project · 2025 · 规范 链接核查于 2026年10月20日

    简介

    逐级提升的供应链安全等级框架,分为构建(Build)和源代码(Source)两条轨道。它推荐了签名声明(attestation)的格式,其中包括构建溯源,即记录制品如何构建的信息。

  • Sigstore

    OpenSSF (Linux Foundation) · 2021 · 项目 链接核查于 2026年10月20日

    简介

    开源项目,使用与身份绑定的短期证书对软件制品签名和验证。签名事件会记录在 Rekor 透明日志中,这是一种任何人都能核查的公开只追加日志。

  • Model Transparency

    Sigstore · 2023 · 工具 链接核查于 2026年10月20日

    简介

    参考实现库和命令行工具(model_signing),可用 Sigstore、公钥或证书对机器学习模型签名。它依据经签名的文件哈希清单验证模型。1.0 版于 2025 年 4 月发布。

  • OpenSSF Model Signing (OMS) Specification

    OpenSSF AI/ML Working Group · 2025 · 规范 链接核查于 2026年10月20日

    简介

    一种分离式模型签名格式,签名与被签名的文件分开存放。该格式不依赖任何特定实现。一份签名可覆盖模型的各类制品,例如权重、配置文件和分词器。它支持裸密钥、证书链或 Sigstore。

  • in-toto Attestation Framework

    in-toto project · 2021 · 规范 链接核查于 2026年10月20日

    简介

    一项规范,用于描述软件如何产生的可验证声明。它定义了标准的声明格式和经审核的谓词类型;谓词类型说明声明属于哪一类。Sigstore 的模型签名即采用 in-toto 声明。

  • Reproducible Builds

    Reproducible Builds project · 项目 链接核查于 2026年10月20日

    简介

    界定并推广可复现构建的项目。在可复现构建中,任何一方都能用相同的源代码、环境和指令,重建逐位相同的制品。因此,任何人都能核对二进制文件与源代码是否一致。

  • RFC 9943: An Architecture for Trustworthy and Transparent Digital Supply Chains

    IETF · 2026 · 标准 链接核查于 2026年10月20日

    简介

    IETF 的供应链完整性、透明与信任(SCITT)架构,以“建议标准”状态发布。发布方把关于制品的签名声明登记到透明服务。透明服务把声明记入只追加账本,并返回收据,表明声明已被记录。

  • Machine Learning Bill of Materials (AI/ML-BOM)

    OWASP CycloneDX · 2023 · 规范 链接核查于 2026年10月20日

    简介

    CycloneDX 的一项功能,用机器可读的物料清单描述模型、数据集及其依赖关系,涵盖数据集溯源和训练方法。CycloneDX 自 1.5 版起支持 AI。1.6 版已作为 Ecma 标准 ECMA-424 发布。

  • SPDX Specification 3.0.1: AI Profile

    SPDX (Linux Foundation) · 2024 · 规范 链接核查于 2026年10月20日

    简介

    SPDX 规范中的 AI Profile,用于记录 AI 软件包,包含自主类型、能耗、安全风险评估、训练信息和局限性等字段。

  • Model Cards for Model Reporting

    Margaret Mitchell et al. · 2018 · 论文 链接核查于 2026年10月20日

    简介

    提出模型卡:随已训练模型一同发布的简短文档,说明模型的预期用途,以及在相关条件和人群上的评测结果。

  • The Data Provenance Initiative: A Large Scale Audit of Dataset Licensing & Attribution in AI

    Shayne Longpre et al. · 2023 · 论文 链接核查于 2026年10月20日

    简介

    一项审计,追溯了 1800 多个文本数据集的来源、创建者和许可。审计发现,在常用托管网站上,超过 70% 的情况缺失许可信息。

  • Croissant: A Metadata Format for ML-Ready Datasets

    Mubashara Akhtar et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    一种元数据格式,为机器学习数据集提供在各类工具、框架和数据仓库之间通用的机器可读描述。MLCommons 托管其规范和代码。

  • Poisoning Web-Scale Training Datasets is Practical

    Nicholas Carlini et al. · 2023 · 论文 链接核查于 2026年10月20日

    简介

    展示针对网络规模数据集的两种可行投毒攻击,即攻击者把恶意数据混入训练集。其中一种只需约 60 美元,本可污染 LAION-400M 中 0.01% 的数据。论文还提出了低开销的防御措施。

  • Atlas: A Framework for ML Lifecycle Provenance & Transparency

    Marcin Spoczynski, Marcela S. Melara, Sebastian Szyller · 2025 · 论文 链接核查于 2026年10月20日

    简介

    一个框架,面向支持远程证明的机器学习流水线。它结合可信硬件、透明日志和开放的溯源规范,记录模型从训练到部署的谱系,即模型背后的数据和步骤。

  • Signing ML Artifacts: Building towards tamper-proof ML metadata records

    Coalition for Secure AI (OASIS) · 2025 · 报告 链接核查于 2026年10月20日

    简介

    安全 AI 联盟(CoSAI)关于模型签名的论文,讨论模型签名中的角色、基础组件和成熟度等级。文中包括 NVIDIA 的经验:自 2025 年 3 月起,NVIDIA 在 NGC 目录中发布的每个模型都附带 OpenSSF 模型签名(OMS)。

  • Independence Tests for Language Models

    Sally Zhu et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    一组统计检验:给定两个语言模型的权重,判断它们是否由相互独立的随机初始化(初始权重)训练而来。其中基于隐藏层激活匹配的检验能抵御对抗性修改,并能定位从其他模型派生出的组件。例如,它揭示了 Llama 3.2-3B 如何由 Llama 3.1-8B 剪枝初始化而来。

    模型与数据供应链可验证推理与计算

  • Model Provenance Testing for Large Language Models

    Ivica Nikolic, Teodora Baluta, Prateek Saxena · 2025 · 论文 链接核查于 2026年10月20日

    简介

    一种黑盒框架,对模型输出做多重假设检验,以判断某个大模型是否派生自另一个模型。在涵盖 600 多个模型的基准上,报告的精确率为 90% 至 95%,召回率为 80% 至 90%。

  • RFC 6962: Certificate Transparency

    IETF · 2013 · 规范 链接核查于 2026年10月20日

    简介

    IETF 的实验性协议,现已被定义 2.0 版的 RFC 9162 取代。以 Merkle 树(哈希树)构建的公开只追加日志记录 TLS 证书,任何人都可以借此审计证书颁发机构。任何人也可以检查日志本身:Merkle 审计路径表明某张证书已被收录,一致性证明表明日志只被追加过。

    模型与数据供应链智能体身份与问责

  • Datasheets for Datasets

    Timnit Gebru et al. · 2018 · 论文 链接核查于 2026年10月20日

    简介

    提出每个数据集都应附带一份数据表,仿照电子元器件的数据手册,记录数据集的创建动机、构成、收集过程和推荐用途。

  • Planting Undetectable Backdoors in Machine Learning Models

    Shafi Goldwasser et al. · 2022 · 论文 链接核查于 2026年10月20日

    简介

    论文表明,受托训练模型的服务方可以植入后门,任何计算能力有限的观察者都无法发现。在其中一种构造下,即使拿到完整的网络和训练数据,也无法检测出后门。

  • Sleeper Agents: Training Deceptive LLMs that Persist Through Safety Training

    Evan Hubinger et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    训练带后门的概念验证大模型,例如在提示中称年份为 2024 年时编写含漏洞的代码。研究发现,监督微调、强化学习和对抗训练都可能无法消除这些后门。对抗训练有时反而让模型学会隐藏这种行为。

  • Poisoning Attacks on LLMs Require a Near-constant Number of Poison Samples

    Alexandra Souly et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    在 6 亿至 130 亿参数的模型上开展的预训练实验:250 篇投毒文档在各种规模下都植入了后门。这说明,攻击所需的投毒样本数量几乎不随模型和数据集规模增长。

  • Explanatory Notice and Template for the Public Summary of Training Content for general-purpose AI models

    European Commission · 2025 · 标准 链接核查于 2026年10月20日

    简介

    依据欧盟《人工智能法》第 53 条第 1 款(d)项制定的强制性模板,用于训练内容的公开摘要。通用 AI 模型提供者必须公开这份摘要。摘要需列明数据来源,例如大型公开数据集、抓取量最大的网站域名和用户数据。

    模型与数据供应链治理与算力核查

  • AI Cyber Security Code of Practice

    UK Department for Science, Innovation and Technology · 2025 · 标准 链接核查于 2026年10月20日

    简介

    英国的自愿性行为守则,按五个生命周期阶段为 AI 系统规定 13 项基线安全原则。这些原则包括保障供应链安全,记录数据、模型和提示词,以及在使用已发布模型前重新运行评测。

内容溯源与水印 22

需要信任:签名方及其密钥

  • Content Credentials: C2PA Technical Specification (version 2.4)

    C2PA · 2026 · 规范 链接核查于 2026年10月20日

    简介

    定义 C2PA 清单:关于媒体资产来源和编辑过程的签名断言。清单通过密码学哈希与内容绑定,也可选择借助指纹或不可见水印与内容关联。

  • Content Authenticity Initiative

    Content Authenticity Initiative · 2019 · 机构 链接核查于 2026年10月20日

    简介

    由 Adobe 于 2019 年发起的社区,推动 C2PA 内容凭证的采用,并为其开发开源工具。

  • Reducing Risks Posed by Synthetic Content: An Overview of Technical Approaches to Digital Content Transparency

    NIST · 2024 · 报告 链接核查于 2026年10月20日

    简介

    NIST 报告(AI 100-4),梳理数字内容透明度的技术路径及其局限。这些路径包括借助水印和元数据追踪内容溯源,以及检测合成内容。

  • A Watermark for Large Language Models

    John Kirchenbauer et al. · 2023 · 论文 链接核查于 2026年10月20日

    简介

    一种文本水印:在每一步生成时轻微偏向一组伪随机的“绿色”词元。无需访问模型,即可用统计检验检测出水印。

  • Scalable watermarking for identifying large language model outputs

    Sumanth Dathathri et al. (Google DeepMind) · 2024 · 论文 链接核查于 2026年10月20日

    简介

    介绍 SynthID-Text:一种基于采样的文本水印,可与推测采样(一种加快生成速度的技术)配合使用。论文还报告了一项线上实验,评估了近 2000 万条 Gemini 回复的质量。

  • Google SynthID

    Google DeepMind · 2023 · 工具 链接核查于 2026年10月20日

    简介

    Google DeepMind 为 AI 生成的图像、音频、文本和视频提供的水印技术。配套的 SynthID Detector 门户可检测 Google 及 OpenAI、NVIDIA、Kakao 等合作伙伴生成的内容。

  • The Stable Signature: Rooting Watermarks in Latent Diffusion Models

    Pierre Fernandez et al. · 2023 · 论文 链接核查于 2026年10月20日

    简介

    通过微调潜在扩散模型的解码器,使生成的每张图像都带有不可见水印,并在裁剪等编辑后仍可检测。

  • Undetectable Watermarks for Language Models

    Miranda Christ, Sam Gunn, Or Zamir · 2023 · 论文 链接核查于 2026年10月20日

    简介

    一种面向语言模型的密码学水印,没有密钥就无法把其输出与原模型的输出区分开来。

  • Watermarks in the Sand: Impossibility of Strong Watermarking for Generative Models

    Hanlin Zhang et al. · 2023 · 论文 链接核查于 2026年10月20日

    简介

    证明在所述假设下,无法给生成模型的输出加上强水印。强水印指不明显降低输出质量就无法去除的水印。论文还给出一种通用的去水印攻击,已成功用于三种文本水印方案。

  • Code of Practice on Transparency of AI-generated Content

    European Commission · 2026 · 标准 链接核查于 2026年10月20日

    简介

    一项自愿性行为守则,帮助生成式 AI 的提供者和部署者履行欧盟《人工智能法》第 50 条规定的标记与标注义务。这些义务自 2026 年 8 月 2 日起适用。守则最终版本于 2026 年 6 月 10 日发布。

  • Apple Reference Image: A New Approach for Verified Photography

    Apple · 2026 · 项目 链接核查于 2026年10月20日

    简介

    iPhone 的一种可选拍摄模式:图像传感器在拍摄时对像素数据签名。安全隔区(Secure Enclave,iPhone 的安全处理器)对其他元数据签名。随后由 Private Cloud Compute 完成图像显影。Apple 将这一模式与基于 C2PA 的方案作了对比。

  • How to Hack Time, With C2PA

    David Buchanan · 2026 · 报告 链接核查于 2026年10月20日

    简介

    一篇安全分析文章,讨论 C2PA 的排除范围,即签名者可以不纳入签名哈希的文件部分。作者指出,签名者可以把整个文件排除在外。这样一来,声明签名和可信时间戳不覆盖任何内容,事后的修改也不会使其失效。

  • 人工智能生成合成内容标识办法 (Measures for Labeling AI-Generated Synthetic Content)

    Cyberspace Administration of China et al. · 2025 · 标准 链接核查于 2026年10月20日

    简介

    国家互联网信息办公室等四部门制定的办法,自 2025 年 9 月 1 日起施行。服务提供者必须为 AI 生成合成内容添加用户能看到或听到的显式标识,并在文件元数据中写入隐式标识。内容传播平台必须核验元数据,并据此添加提示标识。

  • Framework Act on the Development of Artificial Intelligence and the Creation of a Foundation for Trust

    Republic of Korea · 2025 · 标准 链接核查于 2026年10月20日

    简介

    韩国法律,2026 年 1 月 22 日起施行。此处链接为韩国法制研究院提供的非官方英译本。该法要求标注生成式 AI 的输出,并明确告知难以与真实内容区分的 AI 生成声音、图像或视频。它还对训练算力达到阈值的 AI 系统规定了风险管理义务。

    内容溯源与水印治理与算力核查

  • JPEG Trust (ISO/IEC 21617)

    ISO/IEC JPEG Committee · 2025 · 标准 链接核查于 2026年10月20日

    简介

    JPEG 委员会制定的多部分 ISO/IEC 标准,用于为媒体资产附加溯源、真实性、归属、权利和完整性信息。第 1 部分“核心基础”已于 2025 年 1 月以 ISO/IEC 21617-1:2025 发布。信任配置、水印和参考软件等部分仍在制定中。

  • C2PA Conformance Program

    C2PA · 2025 · 项目 链接核查于 2026年10月20日

    简介

    C2PA 于 2025 年年中启动的符合性计划,覆盖生成类产品、验证类产品和证书颁发机构。它依据内容凭证规范、证书策略和安全要求约束这些对象。它公布合规产品列表、C2PA 信任列表和时间戳机构(TSA)信任列表。

  • How Pixel and Android are bringing a new level of trust to your images with C2PA Content Credentials

    Google · 2025 · 项目 链接核查于 2026年10月20日

    简介

    Google 介绍 Pixel 10 相机和 Google Photos 如何添加内容凭证。Google 称,相机应用借助硬件支持的密钥远程证明(key attestation),达到了 C2PA 符合性计划的 2 级保障。Google 还称,应用用一次性证书为每张图像签名,并通过设备端时间戳服务为离线拍摄的照片提供可信时间戳。

  • SoK: Watermarking for AI-Generated Content

    Xuandong Zhao et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    关于 AI 生成内容水印的知识系统化综述(SoK)。它形式化地给出水印方案的定义和期望性质,并分析其目标和威胁模型。它还梳理评估策略和代表性方案,并讨论监管背景和待解决的问题。

  • WAVES: Benchmarking the Robustness of Image Watermarks

    Bang An et al. · 2024 · 基准 链接核查于 2026年10月20日

    简介

    图像水印稳健性基准,把检测和识别两类任务与一套标准化压力测试结合起来。测试范围从常见的图像失真,到基于扩散模型的攻击和对抗攻击。每次攻击后,它同时衡量图像质量的下降和水印的检测效果。

  • MarkLLM: An Open-Source Toolkit for LLM Watermarking

    Tsinghua University (THU-BPM) · 2024 · 工具 链接核查于 2026年10月20日

    简介

    开源工具包,以统一接口实现 KGW、Unigram、SynthID-Text 等多种大模型文本水印算法。它能可视化展示算法如何工作,并提供评估可检测性、稳健性和文本质量的工具。

  • Video Seal: Open and Efficient Video Watermarking

    Pierre Fernandez et al. (Meta) · 2024 · 论文 链接核查于 2026年10月20日

    简介

    Meta 的开源神经网络视频水印方法。它联合训练嵌入器和提取器,并在两者之间施加视频压缩编码等变换。它在帧间传播水印,因此不必为每一帧高分辨率画面都嵌入水印。

  • PAI’s Responsible Practices for Synthetic Media

    Partnership on AI · 2023 · 报告 链接核查于 2026年10月20日

    简介

    Partnership on AI 于 2023 年 2 月发布的框架,围绕同意、披露和透明,为合成媒体的技术构建者、创作者以及分发和发布者提出实践建议。PAI 收集支持机构的案例研究,但不对其审计或认证。

智能体身份与问责 16

需要信任:签名方及其密钥

  • Infrastructure for AI Agents

    Alan Chan et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    将智能体基础设施定义为智能体之外的系统和协议。它承担三项功能:把行动归因于智能体及其用户、塑造智能体的交互、发现并补救有害行动。

  • Visibility into AI Agents

    Alan Chan et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    评估智能体标识、实时监控和活动日志三类措施,用于了解 AI 智能体在何处、为何、如何以及被谁使用。

  • IDs for AI Systems

    Alan Chan et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    提出为 AI 系统的实例分配标识,使用户和调查者能够查到认证情况、责任方等相关信息。

  • Authenticated Delegation and Authorized AI Agents

    Tobin South et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    在 OAuth 2.0 和 OpenID Connect(授权与登录标准)的基础上,加入智能体专用的凭证和元数据。用户由此能够向 AI 智能体委托限定范围且可审计的权限。

  • Identity Management for Agentic AI

    OpenID Foundation · 2025 · 报告 链接核查于 2026年10月20日

    简介

    OpenID 基金会白皮书,讨论如何把 OAuth 2.1、企业单点登录和 SCIM(一种管理用户账户的标准)应用于 AI 智能体。它还讨论了待解问题,例如委托权限、递归委托(智能体再委托给其他智能体)以及用户面对过多授权请求。

  • Accelerating the Adoption of Software and Artificial Intelligence Agent Identity and Authorization

    NIST NCCoE · 2026 · 报告 链接核查于 2026年10月20日

    简介

    NIST 国家网络安全卓越中心(NCCoE)的概念文件,探讨如何把身份与授权标准应用于 AI 智能体。它就标识、授权、审计、不可否认性和提示注入防控征求意见。

  • Verifiable Credentials Data Model v2.0

    W3C · 2025 · 标准 链接核查于 2026年10月20日

    简介

    W3C 推荐标准,定义了一种凭证数据模型:凭证可检测篡改,作者身份可通过密码学方法验证。签发方、持有方和验证方之间交换这些凭证。

  • Agent2Agent (A2A) Protocol Specification

    A2A Project (Linux Foundation) · 2026 · 规范 链接核查于 2026年10月20日

    简介

    AI 智能体之间的通信规范。2026 年 3 月发布的 1.0 版规定了服务商如何为描述其智能体的 Agent Card 签名。签名采用 JSON Web Signature,客户端因此能够核查 Agent Card 的来源和完整性。

  • Agent Payments Protocol (AP2)

    Google; FIDO Alliance · 2025 · 规范 链接核查于 2026年10月20日

    简介

    面向 AI 智能体发起支付的开放协议。签名授权书记录用户授权的内容,并构成审计轨迹。Google 已于 2026 年 4 月将其捐赠给 FIDO 联盟。

  • HTTP Message Signatures for automated traffic

    IETF Web Bot Auth Working Group · 2026 · 规范 链接核查于 2026年10月20日

    简介

    IETF 工作组互联网草案(尚未成为 RFC),允许机器人和智能体对 HTTP 请求签名,以便服务器核实其身份。Signature-Agent 头字段告诉服务器到哪里查找签名密钥。

  • Efficient Data Structures for Tamper-Evident Logging

    Scott A. Crosby, Dan S. Wallach · 2009 · 论文 链接核查于 2026年10月20日

    简介

    一种基于树结构的篡改可检测日志,事后对条目的任何删除或修改都能被发现。不可信的日志方可以证明事件仍在日志中,且日志与早先版本保持一致。这些证明规模很小,只随日志大小呈对数增长。

    智能体身份与问责模型与数据供应链

  • Workload Identity in Multi System Environments (WIMSE)

    IETF · 2024 · 项目 链接核查于 2026年10月20日

    简介

    IETF 工作组,2024 年 3 月获批成立,为跨信任域运行的软件工作负载制定身份与认证标准。它以 OAuth、JWT 和 SPIFFE 为基础。其草案涵盖工作负载令牌、工作负载之间的认证以及 AI 身份管理系统。

  • OpenTelemetry GenAI Semantic Conventions

    OpenTelemetry · 2024 · 规范 链接核查于 2026年10月20日

    简介

    OpenTelemetry 的语义约定,规定如何以 span(计时的操作记录)、指标和事件记录生成式 AI 模型调用、智能体操作和 Model Context Protocol 活动。该约定目前仍处于 Development 状态。它于 2024 年推出,2026 年迁入独立仓库。

  • Agentic AI Foundation (AAIF)

    Linux Foundation · 2025 · 机构 链接核查于 2026年10月20日

    简介

    Linux 基金会于 2025 年 12 月成立的机构,承载开放的智能体 AI 项目。首批项目为 Anthropic 的 Model Context Protocol、Block 的 goose 和 OpenAI 的 AGENTS.md。其工作组包括身份与信任、可观测性与可追溯性等。

  • Announcing Microsoft Entra Agent ID: Secure and manage your AI agents

    Microsoft · 2025 · 项目 链接核查于 2026年10月20日

    简介

    Microsoft 宣布推出 Entra Agent ID 公开预览版。预览版在 Entra 管理中心以统一目录列出在 Copilot Studio 和 Azure AI Foundry 中创建的智能体身份。Microsoft 表示,计划为智能体提供认证、授权和访问治理功能。

  • Model AI Governance Framework for Agentic AI

    IMDA (Singapore) · 2026 · 报告 链接核查于 2026年10月20日

    简介

    IMDA 面向部署 AI 智能体的机构制定的治理框架,2026 年 1 月首次发布,同年 5 月更新至 1.5 版。框架建议为每个智能体分配唯一且可用密码学方法验证的身份,并关联到负责监督的智能体、人类用户或部门。框架还建议在重要节点设置人工审批,并在部署后持续监测和记录智能体的行为。

可验证评测与审计 19

需要信任:检查方及其获得的访问权限

  • Black-Box Access is Insufficient for Rigorous AI Audits

    Stephen Casper et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    论证白盒访问和“盒外”访问能支撑比黑盒查询多得多的审查。白盒访问可以查看模型内部;盒外访问涵盖训练数据、文档等信息。论文还讨论了在更深访问权限下开展审计所需的技术、物理和法律保障措施。

  • Structured access: an emerging paradigm for safe AI deployment

    Toby Shevlane · 2022 · 论文 链接核查于 2026年10月20日

    简介

    阐述结构化访问:开发者让他人以受控方式与 AI 系统交互(通常通过云端接口),而不是公开发布系统。

  • Frontier AI Auditing: Toward Rigorous Third-Party Assessment of Safety and Security Practices at Leading AI Companies

    Miles Brundage et al. · 2026 · 论文 链接核查于 2026年10月20日

    简介

    提出对前沿 AI 开发者的安全与安保声明开展严格的第三方审计。论文还提出四个 AI 保障等级(AAL),等级越高,审计结论越可信。它建议以 AAL-1 为基准,并把 AAL-2 作为最先进开发者的近期目标。

  • Verifiable evaluations of machine learning models using zkSNARKs

    Tobin South et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    把模型在数据集上输出结果的 zk-SNARK 证明打包成评测证明文件。每份文件表明,权重固定且保密的模型达到了所声明的性能或公平性指标。

    可验证评测与审计可验证推理与计算

  • Trustless Audits without Revealing Data or Models

    Suppakit Waiwitlikhit et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    ZkAudit 协议:服务商公布承诺值,即把自己绑定到特定数据集和模型权重的密码学值。服务商还公布训练过程的零知识证明。之后,服务商以新的证明回答版权核查等审计查询。

  • PySyft

    OpenMined · 2017 · 工具 链接核查于 2026年10月20日

    简介

    OpenMined 的开源库:数据科学家提交计算任务,由数据所有者批准后在私有数据上运行,只有获批的结果才会离开所有者的机器。

  • Enabling External Scrutiny of AI Systems with Privacy-Enhancing Technologies

    Kendrea Beers, Helen Toner · 2025 · 论文 链接核查于 2026年10月20日

    简介

    介绍 OpenMined 的基础设施如何组合多种隐私增强技术(PETs),让外部人员审查 AI 系统。这类技术让各方能对数据做计算,同时限制每一方能看到的内容。论文给出了与“基督城呼吁”和英国 AI 安全研究所合作的案例。

  • Secure Enclaves for AI Evaluation

    OpenMined · 2024 · 报告 链接核查于 2026年10月20日

    简介

    一次试点:OpenMined 与英国 AI 安全研究所和 Anthropic 的工作人员合作,在 NVIDIA H100 安全飞地中运行 AI 评测。GPT-2 和一份五行的数据样本代替了机密资产。

  • Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs

    Will Cai et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    研究发现,仅靠软件无法可靠地检测大模型 API 中的暗中模型替换。模型替换指服务商暗中使用与其宣传不同的模型。论文还评估了以可信执行环境(TEE)保证模型完整性的方案。

    可验证评测与审计可验证推理与计算

  • Proving Test Set Contamination in Black Box Language Models

    Yonatan Oren et al. · 2023 · 论文 链接核查于 2026年10月20日

    简介

    一种统计检验,可以证明测试集污染,即基准的测试题目出现在模型的训练数据中。它既不需要训练数据,也不需要模型权重。它检查模型是否认为按原始顺序排列的基准题目比打乱顺序后更可能出现。

  • The Leaderboard Illusion

    Shivalika Singh et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    记录 Chatbot Arena 上未公开的私下测试和选择性公布分数的做法,其中包括 Meta 在 Llama 4 发布前测试的 27 个私有变体。

  • Inspect

    UK AI Security Institute and Meridian Labs · 2024 · 工具 链接核查于 2026年10月20日

    简介

    英国 AI 安全研究所与 Meridian Labs 开发的开源框架,用于构建并运行大模型评测。一项评测由数据集、负责获取模型回答的求解器(solver)和负责给回答打分的评分器(scorer)组成。框架支持智能体、工具调用和在沙箱中执行模型生成的代码,并提供 200 多项预置评测。

  • Holistic Evaluation of Language Models

    Percy Liang et al. (Stanford CRFM) · 2022 · 基准 链接核查于 2026年10月20日

    简介

    斯坦福大学基础模型研究中心(CRFM)的评测基准,在统一条件下用 42 个场景评测了 30 个语言模型。它衡量了准确性、校准、稳健性、公平性和效率等七项指标,还公开了全部原始提示词和模型输出。

  • Language Model Evaluation Harness

    EleutherAI · 2020 · 工具 链接核查于 2026年10月20日

    简介

    EleutherAI 的开源框架,使用公开的提示词在 60 多个标准学术基准上测试生成式语言模型。它旨在让不同论文的结果可以复现、可以相互比较。

  • A Safe Harbor for AI Evaluation and Red Teaming

    Shayne Longpre et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    论证 AI 公司的服务条款及其执行方式会阻碍善意的安全研究。论文提议主要开发者承诺提供法律和技术上的安全港。安全港将保护出于公共利益的评测和红队测试,使其免受封号和法律追责。

  • In-House Evaluation Is Not Enough: Towards Robust Third-Party Flaw Disclosure for General-Purpose AI

    Shayne Longpre et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    提出三项措施。研究者使用标准化的 AI 缺陷报告格式,并遵守参与规则。通用 AI 系统提供者设立缺陷披露计划,并提供法律安全港。另需建设基础设施,协调缺陷报告的分发,使其送达可能受影响的各方。

  • ISO/IEC 42006:2025 Information technology - Artificial intelligence - Requirements for bodies providing audit and certification of artificial intelligence management systems

    ISO/IEC · 2025 · 标准 链接核查于 2026年10月20日

    简介

    2025 年 7 月发布的国际标准,面向依据 ISO/IEC 42001 审核和认证 AI 管理体系的机构。它在 ISO/IEC 17021-1 的基础上提出补充要求。它可作为认可这些机构时的准则文件。

  • AI Verify Foundation

    IMDA (Singapore) · 2023 · 机构 链接核查于 2026年10月20日

    简介

    新加坡资讯通信媒体发展局(IMDA)旗下的非营利附属机构,2023 年 6 月成立。它开发 AI Verify 工具包和 Project Moonshot 等开源 AI 测试工具。它还为第三方 AI 测试机构提供认可计划。

  • CAISI Evaluation of DeepSeek AI Models Finds Shortcomings and Risks

    NIST CAISI · 2025 · 报告 链接核查于 2026年10月20日

    简介

    NIST 下属 AI 标准与创新中心(CAISI)介绍其对 DeepSeek R1、R1-0528 和 V3.1 的评测。CAISI 在 19 项公开和非公开基准上把这些模型与美国参照模型作了比较。报告称,这些模型性能较低、使用成本较高,且更容易受到智能体劫持和越狱攻击。

治理与算力核查 18

需要信任:检查方及其获得的访问权限

可验证推理与计算 21

需要信任:诚实的核查方或证明系统与被证明的命题

  • A Survey of Zero-Knowledge Proof Based Verifiable Machine Learning

    Zhizhi Peng et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    综述 2017 年 6 月至 2025 年 8 月的零知识机器学习(zkML)研究。zkML 借助零知识证明,让他人无需看到模型权重等秘密信息即可核查机器学习计算。综述把这些研究分为可验证训练、测试和推理三类,并分析生成零知识证明的开销等瓶颈。

  • SafetyNets: Verifiable Execution of Deep Neural Networks on an Untrusted Cloud

    Zahra Ghodsi, Tianyu Gu, Siddharth Garg · 2017 · 论文 链接核查于 2026年10月20日

    简介

    一种交互式证明协议,可让客户端核查不可信的云端是否正确执行了神经网络推理。它适用于可表示为算术电路(只由加法和乘法构成)的网络。

  • Scaling up Trustless DNN Inference with Zero-Knowledge Proofs

    Daniel Kang et al. · 2022 · 论文 链接核查于 2026年10月20日

    简介

    为 ImageNet 规模的模型构造 zk-SNARK,用来证明推理正确执行。zk-SNARK 是一种简短、验证迅速的零知识证明。论文还设计了协议,用这类证明核查机器学习服务的预测结果和准确率。

  • zkLLM: Zero Knowledge Proofs for Large Language Models

    Haochen Sun, Jason Li, Hongyang Zhang · 2024 · 论文 链接核查于 2026年10月20日

    简介

    面向大语言模型的零知识证明系统。它用查找论证(对照预先算好的表格检查数值)处理非算术运算,并为注意力机制设计了专门的证明。作者报告,130 亿参数模型的推理证明可在 15 分钟内完成。

  • DeepProve: Verifiable End-to-End Large Language Model Inference

    Nicolas Gailly et al. · 2026 · 论文 链接核查于 2026年10月20日

    简介

    以 sum-check 协议和查找论证为基础的零知识系统,可证明一个提示词生成的全部词元。在 GPT-2 上,它每分钟约能证明 174 个词元;在 Gemma 3 上约为 86 个。

  • EZKL

    Zkonduit · 2022 · 工具 链接核查于 2026年10月20日

    简介

    一个库和命令行工具,可把导出为 ONNX 格式的模型及其他计算图转换成 zk-SNARK 电路。借助这些电路,可以证明并验证模型的推理过程。EZKL 可通过 Python、JavaScript 或命令行使用。

  • TOPLOC: A Locality Sensitive Hashing Scheme for Trustless Verifiable Inference

    Jack Min Ong et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    推理服务方对中间激活值(模型内部计算出的数值)的局部敏感哈希作出承诺。激活值相近时,这类哈希也相近。验证方由此可以发现模型、提示词或数值精度的改动,同时容忍不同 GPU 型号之间的差异。

  • Verde: Verification via Refereed Delegation for Machine Learning Programs

    Arasu Arun et al. · 2025 · 论文 链接核查于 2026年10月20日

    简介

    面向机器学习训练和推理的仲裁式委托协议。当计算服务商的结果不一致时,仲裁方会把争议缩小到单个算子。协议配套提供算子库 RepOps,其算子每次重新运行都得到逐位相同的结果。

  • Model Equality Testing: Which Model Is This API Serving?

    Irena Gao, Percy Liang, Carlos Guestrin · 2024 · 论文 链接核查于 2026年10月20日

    简介

    把识别 API 背后的模型是否经过量化(降低数值精度)、加水印或微调视为双样本检验问题。双样本检验判断两组输出是否来自同一分布。论文报告,在测试的 31 个端点中,有 11 个的输出分布与 Meta 发布的参考权重不同。

    可验证推理与计算可验证评测与审计

  • IMMACULATE: A Practical LLM Auditing Framework via Verifiable Computation

    Yanpei Guo et al. · 2026 · 论文 链接核查于 2026年10月20日

    简介

    一种审计框架,用可验证计算抽查一小部分 API 请求:服务商需同时返回证据,供他人核查结果是否正确。框架不依赖可信硬件,用于发现模型替换、滥用量化和多计词元费用等行为。

    可验证推理与计算可验证评测与审计

  • Proof-of-Learning: Definitions and Practice

    Hengrui Jia et al. · 2021 · 论文 链接核查于 2026年10月20日

    简介

    提出学习证明:由训练检查点(训练中保存的权重)和训练元数据组成的记录。验证方借此可以核查,某一方确实执行了产生某组权重的训练。

  • Optimistic Verifiable Training by Controlling Hardware Nondeterminism

    Megha Srivastava, Simran Arora, Dan Boneh · 2024 · 论文 链接核查于 2026年10月20日

    简介

    通过更高精度的训练和共享舍入决策,控制不同 GPU 型号之间的非确定性,即计算结果上的细微数值差异。审计方因此能够精确复现训练过程,并对训练方的结果提出质疑。

  • Defeating Nondeterminism in LLM Inference

    Horace He, Thinking Machines Lab · 2025 · 报告 链接核查于 2026年10月20日

    简介

    文章指出,大模型推理服务对相同输入返回不同输出,主要原因是算子缺乏批次不变性,而服务器负载又在不断变化。缺乏批次不变性时,一个请求的结果会随同批处理的其他请求数量而变。文章展示了批次不变的算子,它们使温度为 0 时的 1000 次补全完全一致。

  • Pinocchio: Nearly Practical Verifiable Computation

    Bryan Parno et al. · 2013 · 论文 链接核查于 2026年10月20日

    简介

    一种可验证计算系统,可将 C 语言子集编译为一套协议。执行方返回一个 288 字节的正确执行证明。任何持有公开验证密钥的人都能检查这一证明,通常约需 10 毫秒。系统还可选用零知识版本,额外开销很小。

  • zkCNN: Zero Knowledge Proofs for Convolutional Neural Network Predictions and Accuracy

    Tianyi Liu, Xiang Xie, Yupeng Zhang · 2021 · 论文 链接核查于 2026年10月20日

    简介

    一种零知识证明方案,以针对卷积的新 sum-check 协议为基础。模型所有者可以用它证明,卷积神经网络的某个预测结果来自一个保密模型,同时不泄露模型本身。该方案也能证明模型在公开数据集上的准确率。在 VGG16 上,生成证明耗时 88.3 秒,验证耗时 59.3 毫秒。

    可验证推理与计算可验证评测与审计

  • Proofs, Arguments, and Zero-Knowledge

    Justin Thaler · 2022 · 课程 链接核查于 2026年10月20日

    简介

    免费的教材草稿,讲解交互式证明、论证系统和零知识证明。内容包括 sum-check 协议、Fiat-Shamir 变换、多项式承诺,以及基于多项式交互式预言证明(IOP)构造的 SNARK。书中附有配套视频讲座的链接。

  • Proof-of-Learning is Currently More Broken Than You Think

    Congyu Fang et al. · 2022 · 论文 链接核查于 2026年10月20日

    简介

    提出针对学习证明(proof-of-learning)的伪造攻击:攻击者并未训练某组权重,却能为其伪造训练记录。这些攻击可在不同验证配置下复现,成本仅为以往攻击的一小部分。作者认为,要构建可证明稳健的学习证明验证机制,必须更深入地理解深度学习中的优化过程。

  • Experimenting with Zero-Knowledge Proofs of Training

    Sanjam Garg et al. · 2023 · 论文 链接核查于 2026年10月20日

    简介

    提出零知识训练证明(zkPoT)的概念:模型所有者可以证明模型按照约定规范完成训练,同时不泄露数据和模型。作者结合 MPC-in-the-head 与 zk-SNARK,为逻辑回归实现了相应协议,并在 4 GB 的数据集上测试了性能。

  • SVIP: Towards Verifiable Inference of Open-source Large Language Models

    Yifan Sun et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    一种协议,用于核查去中心化算力提供方是否运行了用户指定的开源大模型。提供方在返回生成文本的同时,返回隐藏层表示,即模型内部的数值。用户借助训练好的代理任务和秘密机制核验这些表示。论文报告的假阴性率低于 5%,假阳性率低于 3%。

  • opML: Optimistic Machine Learning on Blockchain

    KD Conway et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    一种在区块链上执行机器学习推理的乐观(optimistic)方案。它不用零知识证明,而是依靠类似 Optimistic Rollup 的交互式欺诈证明协议。结果默认有效,除非有人提出质疑。作者称,可在不配备 GPU 的普通 PC 上运行 70 亿参数的 LLaMA 模型。

  • K2 Vendor Verifier

    Moonshot AI · 2025 · 工具 链接核查于 2026年10月20日

    简介

    Moonshot AI 推出的工具:向提供 Kimi K2 模型服务的第三方厂商发送 4000 个工具调用请求。它衡量这些厂商是否调用工具的决策与 Moonshot 官方 API 的一致程度。它还衡量厂商返回的工具调用 JSON 通过模式校验(即格式检查)的比例。这项测试现已成为范围更广的 Kimi Vendor Verifier 中的一项基准。

形式化验证 23

需要信任:证明系统与被证明的命题

  • Towards Verified Artificial Intelligence

    Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry · 2016 · 论文 链接核查于 2026年10月20日

    简介

    一篇纲领性论文,从形式化方法(用数学手段描述和验证系统的技术)的角度界定“经验证的人工智能”(Verified AI)。论文提出五项挑战和相应的五条原则。

  • Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems

    David Dalrymple et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    将“可保证安全的 AI”定义为一类方法,这类方法结合世界模型、安全规约和验证器。世界模型以数学方式描述 AI 系统如何影响外部世界。验证器提供可审计的数学证明证书,表明相对于该世界模型,AI 系统满足安全规约。

  • Provably safe systems: the only path to controllable AGI

    Max Tegmark, Steve Omohundro · 2023 · 论文 链接核查于 2026年10月20日

    简介

    立场论文,主张在构建通用人工智能时,应确保能用数学证明它满足人类设定的要求。作者提出借助先进 AI 完成形式化验证和机制可解释性分析;后者研究模型的内部机制。

  • Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

    Guy Katz et al. · 2017 · 论文 链接核查于 2026年10月20日

    简介

    基于单纯形法的 SMT 技术,面向采用 ReLU 激活的神经网络。它要么证明网络满足给定性质,要么找出反例。该技术在机载防撞系统原型(ACAS Xu)的网络上做了评估。

  • alpha-beta-CROWN

    Verified-Intelligence · 2021 · 工具 链接核查于 2026年10月20日

    简介

    基于线性界传播和分支定界的 GPU 加速神经网络验证器。其 README 称,它赢得了 2021 年至 2026 年历届 VNN-COMP(年度神经网络验证竞赛)。

  • The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results

    Konstantin Kaulen et al. · 2025 · 报告 链接核查于 2026年10月20日

    简介

    关于 2025 年度神经网络验证竞赛的报告。该竞赛每年举办,在统一的 ONNX 和 VNN-LIB 基准上比较各类验证器。本届有 8 支队伍参赛。

  • Lean

    Lean FRO · 2013 · 工具 链接核查于 2026年10月20日

    简介

    开源编程语言和证明助手;证明助手是逐步检查证明的软件。Lean 用于编写经过形式化验证的代码和机器检查的数学证明,也是 AI 生成证明的常用目标语言。

  • Dafny

    Dafny project · 工具 链接核查于 2026年10月20日

    简介

    支持验证的编程语言,其静态验证器在代码运行前依据规约检查代码。Dafny 程序可编译为 C#、Java、JavaScript、Go 和 Python 等语言。

  • Verus

    verus-lang · 2021 · 工具 链接核查于 2026年10月20日

    简介

    用于验证 Rust 代码的工具:开发者编写规约和证明,由自动求解器检查代码在所有可能的执行中都满足规约。

  • DafnyBench: A Benchmark for Formal Software Verification

    Chloe Loughridge et al. · 2024 · 基准 链接核查于 2026年10月20日

    简介

    包含 750 多个 Dafny 程序的基准,测试语言模型能否生成 Dafny 验证器所需的验证提示(hints)。发布时,最佳模型与提示组合的成功率为 68%。

  • A benchmark for vericoding: formally verified program synthesis

    Sergiu Bursuc et al. · 2025 · 基准 链接核查于 2026年10月20日

    简介

    包含 12504 条 Dafny、Verus/Rust 和 Lean 形式化规约的基准,用于评测生成形式化验证代码的能力。现成模型在三种语言上的成功率分别为 82%、44% 和 27%。

  • Vero: Can AI Agents Build Formally Verified Software Repositories?

    Zhe Ye et al. · 2026 · 基准 链接核查于 2026年10月20日

    简介

    包含 43 个多模块 Lean 4 任务的仓库级基准,要求智能体同时写出实现和证明。智能体也可以证明某条规约无法满足。最强的智能体完整解决了 27 个任务。

  • Safeguarded AI

    ARIA · 项目 链接核查于 2026年10月20日

    简介

    英国高级研究与发明局(ARIA)的项目,投入 5900 万英镑。项目正在构建一套开源工具,供 AI 智能体生成经过形式化验证的成果,目前主要应用于网络安全领域。

  • Olympiad-level formal mathematical reasoning with reinforcement learning

    Thomas Hubert et al. (Google DeepMind) · 2025 · 论文 链接核查于 2026年10月20日

    简介

    介绍 AlphaProof:一个受 AlphaZero 启发的智能体,通过强化学习学会在 Lean 中寻找形式化证明。它在数百万道自动转写为 Lean 的题目上训练。在 2024 年国际数学奥林匹克竞赛中,它解出了 5 道非几何题中的 3 道。它与 AlphaGeometry 2 合计达到相当于银牌的分数。

  • Aristotle: IMO-level Automated Theorem Proving

    Tudor Achim et al. (Harmonic) · 2025 · 论文 链接核查于 2026年10月20日

    简介

    Harmonic 的自动定理证明系统,为 2025 年国际数学奥林匹克竞赛 6 道题中的 5 道给出了形式化解答。它借助蒙特卡洛图搜索选择 Lean 策略(构造证明的命令)。其非形式推理系统负责起草并形式化引理,另有独立的求解器处理几何题。

  • DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

    Z. Z. Ren et al. (DeepSeek-AI) · 2025 · 论文 链接核查于 2026年10月20日

    简介

    开源的 Lean 4 定理证明模型。第一阶段训练所用的冷启动数据来自一条流水线,由 DeepSeek-V3 把问题分解为子目标。随后进入强化学习阶段。6710 亿参数版本在 MiniF2F-test 上的通过率为 88.9%,并解出 PutnamBench 658 道题中的 47 道。

  • Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

    Luoxin Chen et al. (ByteDance Seed) · 2025 · 论文 链接核查于 2026年10月20日

    简介

    Lean 定理证明模型,利用 Lean 反馈、已证明的引理和自我总结迭代完善整个证明。它配合几何推理引擎 Seed-Geometry 使用。作者报告,它完整证明了 2025 年国际数学奥林匹克竞赛 6 道题中的 5 道,其中 1 道在提交截止后完成。作者还报告,它证明了 78.1% 的已形式化历届 IMO 题目。

  • Certified Adversarial Robustness via Randomized Smoothing

    Jeremy M. Cohen, Elan Rosenfeld, J. Zico Kolter · 2019 · 论文 链接核查于 2026年10月20日

    简介

    证明了经高斯噪声平滑的分类器在 ℓ2 范数下的紧致鲁棒性保证;这类分类器对输入加噪后的多份副本做多数投票来预测。例如,在 ImageNet 上,对 ℓ2 范数小于 0.5 的扰动,它认证了 49% 的 top-1 准确率。由于该保证通过蒙特卡洛采样计算,它只以高概率成立。

  • Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

    Haoze Wu et al. · 2024 · 论文 链接核查于 2026年10月20日

    简介

    Marabou 2.0 的系统描述论文。Marabou 是一款开源神经网络验证器,用于检验网络性质。它借助基于 SMT 的过程求解线性和非线性约束。新版本可为无解的查询生成证明证书。它还支持更多激活函数,并可通过更完善的 Python API 提交查询。

  • Automated Reasoning checks is now available in Amazon Bedrock Guardrails

    Amazon Web Services · 2025 · 报告 链接核查于 2026年10月20日

    简介

    AWS 宣布 Amazon Bedrock Guardrails 中的自动推理检查(Automated Reasoning checks)正式可用。这项防护措施用形式化验证技术,对照自动推理策略检查生成式 AI 的输出。策略中的规则从客户自己的文档中提取。

  • The Rocq Prover

    Inria · 1984 · 工具 链接核查于 2026年10月20日

    简介

    交互式定理证明器和依赖类型编程语言,前身为 Coq 证明助手。它用于编写形式化规约,以及程序符合规约的机器检查证明。它还能从规约中提取 OCaml 或 Haskell 可执行代码。

  • Isabelle

    University of Cambridge and Technical University of Munich · 1986 · 工具 链接核查于 2026年10月20日

    简介

    通用证明助手,主要以基于高阶逻辑的 Isabelle/HOL 形式使用。它可检查关于数学以及硬件、软件和协议正确性的形式化证明。借助 Sledgehammer,它能调用外部自动证明器。它还配有形式化证明档案库(Archive of Formal Proofs),收录经 Isabelle 检查的证明。

  • Theorem Proving in Lean 4

    Jeremy Avigad et al. · 2021 · 课程 链接核查于 2026年10月20日

    简介

    一本教材,讲解如何在 Lean 4 中编写定义和机器检查的证明,Lean 社区也为本书作出了贡献。内容涵盖依赖类型论、命题与证明、策略(tactic)、归纳类型、结构体和类型类。