🤖 machine learning

Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networks

本文提出了一种新颖的算法，该算法利用神经网络验证技术来计算精确沙普利值的可证明且任意紧致的界限，从而实现了可扩展且精确的 SHAP 计算，能够处理比现有精确方法大得多的搜索空间。

原作者： David Boetius, Shahaf Bassan, Guy Katz, Stefan Leue, Tobias Sutter

发布于 2026-05-26

📖 1 分钟阅读☕ 轻松阅读

原作者： David Boetius, Shahaf Bassan, Guy Katz, Stefan Leue, Tobias Sutter

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象你拥有一台非常复杂、如同黑盒般的机器（即神经网络），它负责做出决策，例如诊断疾病或批准贷款。你想知道究竟哪些输入特征（如年龄、收入或血压）导致了该机器做出这一特定决策。

回答这一问题的标准方法称为SHAP。可以将 SHAP 想象成一场比赛，你需要弄清楚每位玩家（特征）对团队最终得分的贡献有多大。为了获得完全准确的答案，理论上你需要测试所有可能的玩家组合。

问题所在：
对于简单的机器，测试所有组合轻而易举。但对于拥有数百个特征的复杂神经网络，组合数量之大，简直如同试图数清地球上每一片海滩上的每一粒沙子。这需要耗费如此漫长的时间，以至于实际上变得不可能。正因如此，当今大多数工具只是通过捷径来猜测答案。这些猜测通常速度很快，但可能会出错，而且由于我们无法计算出“真实”答案来进行对比，我们无从知晓它们错得有多离谱。

解决方案：验证性 SHAP（VERISHAP）
本文的作者构建了一个名为VERISHAP的新工具。他们并没有试图去数清每一粒沙子。相反，他们借用了一个名为“神经网络验证”（通常用于证明 AI 系统的安全性和可靠性）领域的巧妙技巧。

以下是 VERISHAP 的工作原理，通过一个简单的类比来说明：

“房间搜索”类比

想象你正在一个巨大的、黑暗的仓库中寻找一件特定的宝藏，仓库里堆满了数百万个盒子（即搜索空间）。

旧方法（猜测）： 你向地图扔出一支飞镖，然后说：“宝藏大概在这个区域。”这很快，但你可能会偏离一英里。
旧精确方法（计数）： 你尝试一个接一个地打开每一个盒子。这能保证你找到宝藏，但你会在完工前老死。
VERISHAP（智能搜索）：
1. 分而治之： 你不是逐个打开盒子，而是将整个仓库划分为大房间。
2. “围栏”技巧： 你使用一种特殊的数学围栏（称为边界传播）一次性检查整个房间。这个围栏会告诉你：“这个房间里的宝藏价值肯定在 10 美元到 20 美元之间。”
3. 逐步逼近： 如果这个范围（10 美元到 20 美元）太宽，你就将该房间分割成更小的房间并再次检查。围栏会变得更紧：“现在我们知道它在 14 美元到 16 美元之间。”
4. 结果： 你不断分割房间，直到围栏收紧到范围实际上为零。你找到了确切的宝藏位置。

为何这是一项重大突破

该论文宣称取得了三大主要胜利：

可扩展性： 以往试图寻找精确答案的方法，一旦问题规模过大就会崩溃或耗尽内存。VERISHAP 能够处理比之前可能范围大几个数量级（即数十亿甚至数万亿倍）的搜索空间。
快速提供“足够好”的答案： 你不必一直等到搜索 100% 完成。如果“围栏”收紧到足够程度（例如，“答案在 14.9 到 15.1 之间”），你可以提前停止并说：“我们有 99.9% 的把握答案是 15。”这让你能比等待完美答案快得多地获得可信的洞察。
建立测试的“黄金标准”： 由于 VERISHAP 能够计算更大规模问题的真实答案，它充当了一台“真理机器”。研究人员现在可以使用它来测试那些猜测工具（如 KERNELSHAP），以观察它们在复杂、现实世界的神经网络上的实际准确度。在此之前，我们只能在那些不能反映现实的小型、玩具示例上测试猜测工具。

论文实际说了什么（以及没说什么）

它确实表示： 他们成功计算了表格数据（如电子表格）和图像数据（如 MNIST 数字）上神经网络的精确 SHAP 值及紧密边界。他们证明了该方法适用于不同类型的网络架构（如 ResNet）和不同的激活函数（如 ReLU、Tanh）。
它确实表示： 目前它比“猜测”方法慢，但它是为大型网络获取数学证明的精确答案的唯一途径。
它并未表示： 论文并未声称该工具已准备好立即在医院等临床环境中使用，或声称它解决了所有 AI 偏见问题。它严格专注于计算这些数值并验证它们的数学能力。它承认，尽管这是一个巨大的进步，但底层数学仍然非常困难，对于某些非常具体、复杂的网络，计算可能仍然需要很长时间。

总结：
VERISHAP 就像是将一个只能指示“大致北方”的指南针，升级为一台即使在大片未测绘森林中也能告诉你确切位置的 GPS。它证明了我们可以为复杂的 AI 决策获取确切的真相，并为我们提供了一把尺子，用来衡量其他更快的工具究竟有多好。

技术摘要：验证性 SHAP（VERISHAP）

问题陈述

Shapley 加性解释（SHAP）是一种标准的后验可解释性方法，用于将机器学习模型的预测归因于输入特征。然而，由于特征子集搜索空间呈指数级增长（ $2^n$ ），计算神经网络的精确 SHAP 值被广泛认为在计算上是不可行的。虽然基于树和加性模型可以 feasibly 进行精确计算，但对于通用神经网络而言，该问题是 #P-难的。因此，现有文献依赖于统计估计器（例如 KERNELSHAP、FASTSHAP、LEVERAGESHAP）。这些估计器面临两个根本性局限：

不准确性：它们提供近似值，在高度非线性模型或特征交互强烈的场景中可能不可靠。
缺乏真实值（Ground Truth）：由于为神经网络计算精确 SHAP 值代价过高，估计器通常仅在可计算精确值的玩具级模型上进行评估。这些设置往往无法泛化到现实世界的高维神经网络。

方法论：验证性 SHAP（VERISHAP）

本文介绍了 VERISHAP，这是首个利用神经网络验证最新进展来计算神经网络精确 SHAP 值及可证明界限的算法。该方法将分支定界验证技术适配于 SHAP 的离散性、概率性及求和密集型特性。

核心算法

VERISHAP 采用增量式分支定界策略，递归地划分特征空间（即特征 $i$ 的所有联盟 $S_i$ 的集合）。

划分：算法基于包含集（ $I$ ）和排除集（ $E$ ）定义分支 $B$ 。一个分支代表一个联盟子集，其中 $I$ 中的特征存在，而 $E$ 中的特征不存在。
通过传播进行界定：对于每个分支，算法计算边际贡献 $\Delta_i(S) = v(S \cup \{i\}) - v(S)$ $Δ_{i} (S) = v (S \cup {i}) - v (S)$ 的下界和上界。
- 为了将连续界限传播（如 CROWN、IBP）应用于离散集合，算法将布尔特征掩码 $m \in \{0, 1\}^n$ 松弛到连续域 $[0, 1]^n$ 。
- 它使用线性界限传播（LBP）（具体为 CROWN-IBP）在松弛域上推导价值函数 $v(S)$ 的紧确界限。
聚合：总 SHAP 值界限通过对所有分支的加权界限求和来计算：
$\phi_i^{(t)} = \sum_{B \in \mathcal{B}^{(t)}} \Lambda_B \Delta_i^B \leq \phi_i \leq \sum_{B \in \mathcal{B}^{(t)}} \Lambda_B \Delta_i^B = \bar{\phi}_i^{(t)}$
其中 $\Lambda_B$ 是分支 $B$ 中联盟的 Shapley 权重的闭式求和，通过组合数学推导得出。
细化：算法迭代地选择要分割的分支（使用如 MAXDIAM 的策略）和要分割的特征（使用如 SMEARS 的策略），细化界限直到其收敛至精确值或达到所需精度。

关键理论属性

终止性：该算法保证在有限次迭代后（最多 $2^{n-1}$ 次）以精确 SHAP 值终止，因为划分最终会隔离单个联盟。
线性模型的早期终止：对于线性模型，算法在第一次迭代即终止，因为边际贡献是恒定的，且 LBP 对线性组合不引入近似误差。
分段线性：对于 ReLU 激活的网络，如果划分将搜索限制在网络表现为线性的区域，算法可以提前终止。

主要贡献

首个神经网络的精确 SHAP：VERISHAP 是首个为通用神经网络计算精确 SHAP 值的算法，其可扩展的搜索空间比之前的精确方法大几个数量级。
可证明的界限：该方法提供任意紧确的 SHAP 值上下界，即使在完全收敛之前也能提供可信的解释性洞察。
真实值基准：它建立了一个原则性框架，用于在更大、更真实的搜索空间上评估统计 SHAP 估计器，而这些空间此前无法获得真实值。
通过验证实现效率：通过利用神经网络分解为近线性区域的特性，该算法在许多实际案例中避免了对所有 $2^n$ 个联盟的枚举。

实验结果

作者在表格数据（UCI 数据集）和视觉（MNIST、FashionMNIST、CIFAR10、GTSRB）基准上评估了 VERISHAP。

与 ExactSHAP 的可扩展性对比：VERISHAP 显著优于最先进的精确方法（EXACTSHAP）。当搜索空间大于 $2^{20}$ 时，EXACTSHAP 会耗尽 GPU 显存，而 VERISHAP 能计算高达 $2^{25}$ （约 $3 \times 10^7$ 个联盟）实例的精确值，并为高达 $2^{60}$ （约 $10^{18}$ 个联盟）的空间提供紧确界限。
与估计器的对比：与统计估计器（KERNELSHAP、TREEMSR、LEVERAGESHAP）相比，VERISHAP 表明估计器往往无法在内存约束内达到相同的精度。此外，VERISHAP 揭示估计器性能在不同数据集间差异显著（例如，TREEMSR 在神经网络上的表现相比基于树的模型波动较大）。
架构通用性：该算法成功计算了各种架构的精确 SHAP 值，包括具有 ReLU、tanh 和 Swish 激活的全连接网络以及 ResNet。
收敛性：在实验（如 MNIST）中，界限在计算出精确值之前很久就变得具有信息量（揭示归因模式），通常在数秒内完成，而精确计算可能需要数十秒。

意义与主张

本文将 VERISHAP 定位为扩展神经网络精确 SHAP 计算的第一步。其意义体现在三个方面：

可扩展性：它通过利用神经网络验证，弥合了精确 SHAP 的理论不可行性与实际应用之间的差距。
可信度：它提供了一种获得具有可证明保证的“真实值”解释的方法，解决了统计近似中固有的不确定性。
评估框架：它为在更大搜索空间上评估和改进 SHAP 估计器提供了严格的基准，超越了玩具模型。

作者承认，计算精确 SHAP 仍然是 #P-难的，且 VERISHAP 对于某些复杂网络可能仍然较慢。然而，他们指出，计算可证明界限的能力以及神经网络验证的持续改进潜力，使其成为可信 AI 可解释性的一项基础性进展。