Beyond But-for Test: Counterfactual Explanation in Abstract Argumentation via Actual Causality (Extended Version)

技術要約：But-forテストを超えて：実在的因果性（Actual Causality）による抽象論証における反事実的説明

問題提起
説明可能なAI（XAI）の分野において、抽象論証（Abstract Argumentation, AA）は、特定の意味論の下でなぜある議論が受理されるのかという構造的な説明を提供します。既存の手法は、関連性（Relevance）、単調性（Monotonicity）、あるいは必要性（Necessity）といった特性を満たす議論の集合を特定することで、事後的な問いに答えますが、これらは静的な理由のリストに依存しています。しかし、人間の推論は、しばしば因果依存性を探るために「もし〜であったなら（what-if）」というシナリオを用いる、反事実的思考を採用します。

AAにおける反事実的説明への現在のアプローチは、but-forテスト（BFT）に限定されています。この原始的なテストは、疑わしい原因（単一の要素）が変更された場合に、トピックとなる議論の受理状態が変化するかどうかを問うものです（例：攻撃の削除や新たな攻撃者の追加）。本論文は、このアプローチに決定的な欠陥があることを指摘しています。それは、他の議論を「証人（witnesses）」として固定していない点です。その結果、BFTは複雑な論証構造、具体的には先取り（Preemption）（一つの原因が別の原因を阻止するケース）や過決定（Overdetermination）（複数の原因が共同で十分条件となるケース）において、直感に反する結果を生じさせます。これらのケースでは、単一の原因を変更しても、代替経路が活性化するために結果が変わらないことがあり、BFTは真の原因を正しく特定できなかったり、見逃したりすることになります。

手法
but-forテストの限界を克服するため、著者らは構造方程式モデル（SEM）およびハルパーン＝パール（Halpern–Pearl）の実在的因果性の定義に基づいた、介入に基づく反事実的推論フレームワークを導入します。

1. 受理モデル（Acceptability Model）: 本フレームワークは、議論の受理条件を一連の方程式としてエンコードします。議論 $\alpha$ のラベル（$in$, $out$, $und$）は、その攻撃者のラベルによって決定されます。これにより、論証フレームワーク（AF）を関数 $M_F$ のモデルへと変換します。
2. 介入演算子（Intervention Operator）: 著者らは、仮説 $\psi$（原子命題の連言）に従ってモデル $M_F$ を修正する介入演算子 $[\psi]$ を定義します。これは単純なグラフの修正とは異なり、以下の特徴を持ちます。
   • 介入された議論の受理方程式を、規定されたラベルを返す定数関数に置き換える。
   • **複合的な仮説（compound hypotheses）**を可能にし、複数の議論の同時修正をサポートする。
   • 決定的な点として、証人となる議論を実際（actual）のラベルに固定することをサポートし、代替経路が反事実的評価を歪めるのを防ぐ。
3. 洗練された反事実的条件（AC2m）: BFTを超えて、本論文は修正された反事実的条件である AC2m を採用しています。仮説 $\psi$ が*実在的原因（actual cause）*であるとは、以下を満たす場合を指します。
   • 実在性（AC1）: 元のラベリングにおいて、$\psi$ と結果の両方が成立している。
   • 修正された反事実（AC2m）: $\psi$ の修正版 $\psi'$ と、一連の固定された証人 $\chi$（実際ラベルに保持された議論）が存在し、$\psi' \land \chi$ による介入によってトピックとなる議論の状態が変化する。
   • 最小性（AC3）: 原因には冗長な部分が含まれない。

主な貢献

• AAにおける実在的因果性の形式的フレームワーク: 本論文は、primitiveなbut-forテストを超え、HPの実在的因果性と抽象論証を結びつける最初の形式的枠組みを確立しました。
• 先取りと過決定の処理: 証人を固定することにより、本手法はbut-forテストが失敗するシナリオにおいても原因を正しく特定します。
  • 先取り（Preemption）: $\alpha$ が $\beta$ による $\eta$ の防御を阻止するシナリオにおいて、but-forテストは $\alpha$ を原因として特定できません（$\alpha$ を取り除くと $\beta$ が再活性化するため）。提案手法は $\beta$（またはそれが用いる経路）を実際の状態に固定することで、$\alpha$ が真の原因であることを明らかにします。
  • 過決定（Overdetermination）: $\alpha$ と $\beta$ の両方が $\eta$ を防御するのに十分な場合、but-forテストはいずれも原因として特定できません（一方を除去しても他方が残るため）。提案手法は、結合された原因 $in(\alpha) \land in(\beta)$ を実在的原因として特定します。
• グラフ切断（Graph Mutilation）の可視化: 著者らは、論理的介入をAFに対するグラフ操作（攻撃者の追加、攻撃の削除、または自己ループの追加）へとマッピングし、代数的な介入に対する視覚的な対応を提供します。
• 比較分析: 本論文は、新しい手法を既存の議論ベースの説明（Root Reasons、十分/必要集合）および最近傍世界（closest-world）の反事実と比較しています。提案手法は、特に一意のラベリングが存在する場合に、最近傍世界アプローチで見られる「空の説明」問題を回避しており、より選択的かつ信頼性が高いことを示しています。

結果と特性

• 表現力: 本手法は複合的な仮説をサポートしており、atomicな変化に限定されるbut-forテストでは不可能な、共同原因の説明を可能にします。
• 関連性: 本手法は関連性（Relevance）の特性を満たします。つまり、説明に含まれるすべての議論はトピックに関連しています。
• 非単調性: 伝統的な説明手法とは異なり、この反事実的説明は単調ではありません。有効な説明に議論を追加すると、最小性（Minimality）の条件に抵触することがあります。
• 特定の構造における優位性:
  • **先取り（Preemption）**において、本手法は先取りを行う議論を原因として特定しますが、Root Reasonsは無関係な防御者を包含したり、最近傍世界アプローチは説明を返さなかったりすることがあります。
  • **過決定（Overdetermination）**において、本手法は複数の議論の共同の必要性を特定しますが、Root Reasonsや十分性（Sufficient）の説明は、対称的な防御者を区別できなかったり、自明な集合を返したりすることがよくあります。
  • 本手法は、受理されたシンクノードに対して説明の**存在（Existence）**を保証します。これは、AFが唯一のラベリングしか持たない場合に最近傍世界アプローチが失敗する性質です。

意義と主張
本論文は、ハルパーン＝パールの実在的因果性の定義を抽象論証に統合することで、提案されたフレームワークが、より洗練され、人間に即した反事実的説明を提供するものであると主張しています。証人を固定する能力は、複雑な依存構造において原因を正しく特定するために不可欠であり、それによってbut-forの限界を克服できるとしています。著者らは、本研究を、循環依存性や先取り・過決定といった複雑な因果パターンを扱うのに十分な表現力を持ちつつ、論証の構造的特性に根ざした、より堅牢なXAIへの一歩として位置付けています。計算量への対処、他の意味論（grounded, preferred, stable）への拡張、および拡張された論証形式（PAF, ADF, ASPIC+）への適用といった今後の課題についても言及されています。