技術的サマリー：検証済み SHAP（VERISHAP）

問題定義

シャプレイ付加説明（SHAP）は、機械学習モデルの予測を入力特徴量に帰属させるための標準的な事後説明手法である。しかし、特徴量部分集合の指数関数的な探索空間（$2^n$）に起因し、ニューラルネットワークに対する正確な SHAP 値の計算は、計算量的に非現実的であると考えられている。木ベースモデルや加法的モデルでは正確な計算が可能であるが、一般的なニューラルネットワークに対しては #P 困難である。その結果、既存の文献では統計的推定量（例：KERNELSHAP、FASTSHAP、LEVERAGESHAP）に依存している。これらの推定量は、2 つの根本的な限界に直面している：

1. 不正確性: これらは近似値を提供するが、高度に非線形なモデルや強い特徴量相互作用を有するシナリオでは信頼性が低下する可能性がある。
2. 真実値の欠如: ニューラルネットワークに対する正確な SHAP 値の計算が prohibitively 高価であるため、推定量は通常、正確な計算が可能な玩具規模のモデル上で評価される。これらの設定は、現実世界の多次元ニューラルネットワークへの一般化に失敗することが多い。

手法：検証済み SHAP（VERISHAP）

本論文は、ニューラルネットワークに対する正確な SHAP 値と証明可能な境界を計算するために、最新のニューラルネットワーク検証の進歩を活用する最初のアルゴリズムであるVERISHAPを導入する。このアプローチは、離散的、確率的、かつ総和を多用する SHAP の性質に合わせて、分枝限定検証技術を適応させる。

コアアルゴリズム

VERISHAP は、特徴量空間（特徴量 $i$ に対するすべての連合 $S_i$ の集合）を再帰的に分割する増分的な分枝限定戦略を採用する。

1. 分割: アルゴリズムは、含まれる特徴量（$I$）と除外される特徴量（$E$）の集合に基づいて分枝 $B$ を定義する。ある分枝は、$I$ 内の特徴量が存在し $E$ 内の特徴量が存在しない連合のサブセットを表す。
2. 伝播による境界設定: 各分枝に対して、アルゴリズムは限界貢献 $\Delta_i(S) = v(S \cup \{i\}) - v(S)$ の下限と上限を計算する。
   • 離散集合に連続境界伝播（例：CROWN、IBP）を適用するために、アルゴリズムはブーリアン特徴量マスク $m \in \{0, 1\}^n$ を連続領域 $[0, 1]^n$ に緩和する。
   • 緩和された領域における値関数 $v(S)$ に対する tight な境界を導出するために、線形境界伝播（LBP）（具体的には CROWN-IBP）を使用する。
3. 集約: 全体の 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$ 内の連合に対するシャプレイ重みの閉形式和である。
4. 精緻化: アルゴリズムは、分枝を分割するもの（MAXDIAM などの戦略を使用）と分割対象となる特徴量（SMEARS などの戦略を使用）を反復的に選択し、境界が正確な値または所望の精度に収束するまで精緻化する。

主要な理論的特性

• 終了保証: 分割が最終的に単一の連合を分離するため、アルゴリズムは有限回の反復（最大 $2^{n-1}$ 回）後に正確な SHAP 値で終了することが保証される。
• 線形モデルにおける早期終了: 線形モデルの場合、限界貢献が一定であり、LBP が線形合成に対して近似誤差を導入しないため、アルゴリズムは最初の反復で終了する。
• 区分的線形性: ReLU 活性化ネットワークの場合、分割がネットワークが線形に振る舞う領域に探索を制限する場合、アルゴリズムは早期に終了できる。

主要な貢献

1. ニューラルネットワークに対する最初の正確な SHAP: VERISHAP は、一般的なニューラルネットワークに対する正確な SHAP 値を計算する最初のアルゴリズムであり、以前の正確な手法よりも桁違いに大きな探索空間にスケーリングする。
2. 証明可能な境界: この手法は、SHAP 値に対する任意に tight な下限と上限を提供し、完全な収束前でも信頼性の高い説明的洞察を可能にする。
3. 真実値の基準: 以前は到達不可能だった真実値を伴う、より大規模で現実的な探索空間における統計的 SHAP 推定量の評価のための原理的な枠組みを確立する。
4. 検証による効率性: ニューラルネットワークを準線形領域に分解することを活用することで、多くの実用的なケースにおいてすべての $2^n$ 個の連合を列挙することを回避する。

実験結果

著者らは、表形式データ（UCI データセット）およびビジョン（MNIST、FashionMNIST、CIFAR10、GTSRB）のベンチマークにおいて VERISHAP を評価した。

• ExactSHAP に対するスケーラビリティ: VERISHAP は、最先端の正確な手法（EXACTSHAP）を大幅に上回る。EXACTSHAP は $2^{20}$ を超える探索空間では GPU メモリを枯渇させるが、VERISHAP は $2^{25}$（約 $3 \times 10^7$ 連合）までのインスタンスに対して正確な値を計算し、$2^{60}$（約 $10^{18}$ 連合）までの空間に対して tight な境界を提供する。
• 推定量との比較: 統計的推定量（KERNELSHAP、TREEMSR、LEVERAGESHAP）と比較すると、VERISHAP は、推定量がメモリ制約内で同程度の精度を達成できないことを示している。さらに、VERISHAP は、推定量のパフォーマンスがデータセット間で大きく変動することを明らかにしている（例：TREEMSR は、木ベースモデルと比較してニューラルネットワーク上で不安定なパフォーマンスを示す）。
• アーキテクチャの多様性: このアルゴリズムは、ReLU、tanh、Swish 活性化を備えた全結合ネットワークおよび ResNet など、さまざまなアーキテクチャに対して正確な SHAP 値の計算に成功している。
• 収束: 実験（例：MNIST）において、正確な値が計算される遥か以前から（多くの場合数秒以内）、境界は有益なもの（帰属パターンを明らかにする）となり、正確な計算には数十秒を要する場合がある。

意義と主張

本論文は、ニューラルネットワークに対する正確な SHAP 計算のスケーリングに向けた第一歩として VERISHAP を位置づけている。その意義は以下の 3 つの分野にある：

1. スケーラビリティ: ニューラルネットワーク検証を活用することで、正確な SHAP の理論的非現実性と実用的応用の間のギャップを埋める。
2. 信頼性: 統計的近似に内在する不確実性に対処し、証明可能な保証を伴う「真実値」の説明を得る手法を提供する。
3. 評価枠組み: 玩具モデルを超えて、より大規模な探索空間における SHAP 推定量の評価と改善のための厳密なベンチマークを提供する。

著者らは、正確な SHAP の計算が依然として #P 困難であり、VERISHAP は特定の複雑なネットワークに対しては依然として遅い可能性があることを認めている。しかし、証明可能な境界を計算する能力と、ニューラルネットワーク検証における継続的な改善の可能性が、信頼性の高い AI 説明性のための基礎的な進展であると主張している。