技術要約：因果モデルとしてのバイナリ・スパイキング・ニューラルネットワーク

問題提起

本論文は、人工ニューラルネットワーク（ANN）における精度と説明可能性のトレードオフに取り組んでいる。バイナリ化ニューラルネットワーク（BNN）およびバイナリ・スパイキング・ニューラルネットワーク（BSNN）は、ハードウェア効率と論理的表現性の面で利点があるものの、その内部の意思決定プロセスは依然として不透明である。SHAPのような既存の説明可能なAI（XAI）手法は、モデルを「ブラックボックス」として扱うことが多く、内部の因果構造を考慮できていない。その結果、これらの手法は、ネットワークの出力と因果関係がない（例：重みがゼロの接続）にもかかわらず、特徴量を関連性があると特定してしまうことがある。著者らは、BSNNのダイナミクスを因果フレームワークに正式にマッピングすることでこのギャップを埋め、含まれる特徴量の因果的な関連性を保証する、厳密な論理ベースの説明を生成することを目指している。

手法

1. BSNNの定式化

著者らは、BSNNアーキテクチャ $S$ を、入力ニューロン（$I$）、非入力ニューロン（$L$）、結合関係（$R$）、重み関数（$W$）、および発火閾値（$\tau$）からなるタプルとして定義する。彼らは、リークのない積分発火（IF）メカニズムを用いてスパイキングのダイナミクスをモデル化しており、時刻 $t$ におけるニューロンの発火状態は、その前の状態と、流入するスパイクの重み付き合計に再帰的に依存する。

• 重みの量子化: 本研究は、重みがバイナリの $\{0, 1\}$ または三値の $\{-1, 0, 1\}$ の集合に量子化されたネットワークに焦点を当てている。
• スパイク符号化: 実験では、ポアソン・レート・コーディングおよび閾値二値化スキームを利用する。著者らは、説明生成の計算複雑性を管理するために、複雑な時間的コーディングを明示的に回避している。

2. バイナリ因果モデル（BCM）へのマッピング

核心となる手法上の貢献は、BSNNのスパイキング・ダイナミクスをバイナリ因果モデル（BCM）へマッピングすることである。

• 変数: 各時刻 $t$ における各ニューロン $X$ に、ブール変数 $p_{X,t}$ が割り当てられる。入力ニューロンは外生的変数に対応し、非入力ニューロンは内生的変数に対応する。
• 因果依存性: 発火ロジックは、一連のブール方程式（構造方程式）へと翻訳される。ニューロンが発火するためには、先行するスパイクの特定の組み合わせが閾値条件を満たす必要がある。
• 等価性: 著者らは、BSNNの発火関数が、そのブール解釈がモデル内のすべての方程式を満たす場合に限り、BCMと互換性があることを証明している（定理 5.2）。

3. 仮説的説明（AXp）の生成

本論文では、特定の出力分類を保証する、入力特徴量（リテラル）の最小十分集合として定義される**仮説的説明（Abductive Explanations: AXp）**を採用している。

• 定義: 出力 $\omega_0$ に対するAXp $\lambda$ は、以下を満たさなければならない：(i) $\lambda$ は入力に対して真である、(ii) $\lambda$ はBCMの制約下で $\omega_0$ を論理的に含意する、(iii) $\lambda$ は最小である（$\omega_0$ を含意する真の部分集合が存在しない）。
• アルゴリズム: AXpを見つけるために、2つのソルバーベースのアプローチが実装されている：
  1. SATベース: BCMと説明条件を命題論理へとエンコードする。
  2. SMTベース: モデルを充足可能性モジュロ理論（具体的には線形整数算術）を用いてエンコードする。これにより、変数集合に対する全称量化を回避し、大幅な速度向上を実現する。
• 探索戦略: アルゴリズムは、完全な入力を表す完全な項から開始し、含意が有効であり続けることを検証しながら、反復的にリテラルを削除していく。

4. 実験設定

本手法は、手書き数字認識のためのMNISTデータセットを用いてテストされた。

• アーキテクチャ: 様々な隠れ層サイズ（$k \in \{8, 16, 32, 64, 128\}$）と重み量子化（バイナリおよび三値）を持つ全結合ネットワーク。
• タスク: 3桁のサブセットおよびフル10桁のセットの分類。
• 検証: バイナリおよび三値量子化ネットワークを用いて、高い精度（3桁のタスクで最大約95%まで）を達成した。

主要な貢献

1. BSNNの初の因果マッピング: 本論文は、バイナリ・スパイキング・ニューラルネットワークを、ニューロン間の時間的因果依存性を捉えるバイナリ因果モデル上に正式にマッピングした初の事例を提示している。
2. 論理ベースの説明フレームワーク: バイナリの性質を持つBSNNを用いることで、因果モデルから直接、SATおよびSMTソルバーを使用して仮説的説明を計算できることを示している。
3. 因果的関連性の保証: 理論的な重要な貢献は、本フレームワークから導出された仮説的説明に含まれるあらゆる特徴量は、ネットワークの隠れ層への非ゼロの重み接続を持っていなければならないことを証明した命題 6.2である。これにより、説明に全く無関係な特徴量が含まれないことが保証される。
4. SHAPとの比較分析: 本論文はSHAP（SHapley Additive exPlanations）との厳密な比較を提供し、SHAPがモデルに依存しない性質ゆえに、重みがゼロの接続を持つ特徴量を関連性があると特定してしまう傾向があることを明らかにしている。

結果

• 計算効率: SMTベースのアプローチは、SATベースのアプローチを大幅に上回った。バイナリ重みネットワーク（$S^{bin}_k$）において、SMTは探索時間を数時間（SAT）から数秒（例：$k=32$ の場合、11時間から約12秒へ）に短縮した。三値重みネットワーク（$S^{tern}_k$）において、SMTの探索時間は0.27から1.0時間の範囲であった。
• 説明の質: 生成された説明は、分類をトリガーするのに十分な、活性または非活性なピクセルの最小集合であった。
• SHAPとの比較:
  • SHAPは、サンプルサイズ全体を通じて、平均して約47%のケースで、重みがゼロの接続を持つ特徴量を誤って関連性があると特定した。
  • SHAPのサンプルサイズを増やしても、このエラー率は減少したが、計算時間は劇的に増加した（例：100万サンプルで173秒）。
  • 対照的に、提案された論理ベースの手法は、ゼロ重みの特徴量が説明に含まれないことを数学的に保証している。

意義と主張

著者らは、本研究をBSNNを形式論理を通じて解釈可能にするための基礎的なステップとして位置づけている。彼らは、BSNNに固有の因果構造を活用することで、効率的であるだけでなく、形式的に保証された、無関係な特徴量を含まない説明を生成することが可能であると主張している。これは、SHAPのような統計的またはモデルに依存しない手法では提供できない特性である。

論文では、現在の研究が仮説的説明（AXp）と全結合アーキテクチャにのみ焦に焦点を当てていることを謙虚に述べている。著者らは、本フレームワークがより複雑な因果概念（実際の原因やNESS原因など）や、畳み込みBSNN（C-BSNN）および言語データセットで訓練されたネットワークなどの他のアーキテクチャにも拡張可能であることを示唆しているが、これらは現在の成果ではなく、将来の研究方向として特定されている。