技術要約：説明可能なASPに対するXAIの視点

問題提起

回答集合プログラミング（ASP）は、記号的AIにおける主要な宣言型推論パラダイムであり、そのルールベースの形式体系はニューラルネットワークのようなサブシンボリックな手法よりも本質的に解釈性が高いことで価値を認められている。それにもかかわらず、ソルバーの出力が持つ「ブラックボックス」的な性質は、特に説明可能なAI（XAI）が台頭する中で、産業界や社会への導入における障壁となっている。ユーザーは、特定のソルバーの結果（回答集合）の背後にある推論メカニズムや、プログラム全体の挙動（例：なぜ解が存在しないのか）を理解することに苦慮している。

先行研究（例：Fandinno and Schulz, 2019）では、特定の説明技術（例：「なぜリテラル $a$ は回答集合 $I$ に含まれるのか？」）をカタログ化しているが、これらは狭い設定に焦点を当てていることが多い。多様なユーザーの問いを既存の理論的アプローチやツールへとマッピングし、現在のカバー範囲のギャップを特定し、ASPの説明能力を、ローカルな説明とグローバルな説明という広範なXAIの区別に整合させる、包括的かつユーザー中心の概観は不足している。

メソドロジー

著者らは、XAIの視点に基づいたASP説明手法の調査を実施した。そのメソドロジーは以下の通りである：

1. 分類： 説明のランドスケープを、ローカルな説明（特定の計算された回答集合に関するもの）とグローバルな説明（プログラム全体またはすべての回答集合の集合に関するもの）に構造化する。
2. 問い駆動型の分析： 「なぜリテラル $\ell$ は $I$ に含まれるのか？」から「なぜプログラムには回答集合が存在しないのか？」、「なぜ $I$ は最適なのか？」に至るまで、典型的なユーザーの問い（Q1–Q8）の包括的なリストを特定する。
3. マッピングと還元： 既存の手法（M1–M15とラベル付け）およびシステム（例：xASP2, xclingo, s(CASP), UCOREXPLAIN）が、これらの問いにどのように対処しているかを分析する。また、問いが他の解ける問題（例：「なぜ $a \in I$ か」を「修正されたプログラムがなぜ充足不能か」に還元する）へどのように還元できるかを特定する。
4. ギャップの特定： 言語機能（選言、集約、選択ルール、弱制約）およびユーザーのニーズ（スケーラビリティ、認知負荷、インタラクション）に対する現在のツールのカバー範囲を評価する。

主な貢献

本論文は、ASP説明手法の構造化されたタクソノミーを提供し、以下の具体的な貢献を強調している。

1. 説明タイプのタクソノミー

• ローカルな説明： 特定の回答集合 $I$ における原子の存在または不在の導出に焦点を当てる。
  • 正当化（Justifications）（M1–M4）： オフラインの正当化（導出グラフ）、ABAベースの正当化（議論木）、因果的正当化（代数項）、およびソルバーのトレースからのルールベースの正当化を含む。
  • 拡張された正当化（M5）： UCOREXPLAINで使用される、リテラルを説明するための最小限のルールセットを特定するための単一証明可能充足不能部分集合（1-PUS）。
  • サポートグラフ（M6）： xclingoで使用され、原子をそれをサポートするルールにリンクさせ、自然言語による注釈を可能にする。
  • ウィットネス（Witnesses）（M7）： ソルバーに依存しない段階的な論理的導出。
  • 対照的な説明（Contrastive Explanations）（M8）： なぜ原子の集合 $E$ が $I$ に含まれ、代わりに $F$ が含まれないのかを、反事実を用いて説明する（Eiter et al., 2023）。
• グローバルな説明： 特定の回答集合を持たない、プログラムの挙動に焦点を当てる。
  • Why-not プロバナンス（M9）： 真理値を変化させるために必要なプログラムの修正を特定する。
  • トップダウン計算（M10）： 目標指向の正当化木（例：s(CASP)）。
  • 証明システム（M11）： 懐疑的な含意（なぜある原子がすべての、あるいはどの回答集合にも含まれないのか）のための計算体系。
  • デバッグ（M12–M14）： メタエンコーディング（spock）、最小充足不能集合（MUS）、およびインタラクティブなステップ実行などの、不整合を説明するための技術。
  • 抽象化（M15）： 無関係な詳細を省略することで、充足不能な部分に「ズームイン」するための過剰近似技術。

2. ユーザーの問い（Q1–Q8）の分析

論文は、特定のユーザーのクエリを利用可能な手法にマッピングしている：

• Q1 (なぜ $\ell \in I$ か？): ほとんどのローカルな手法（M1–M7）によってカバーされている。
• Q2 (なぜ $\ell \in I$ だが $\ell' \notin I$ なのか？): 対照的な説明（M8）または充足不能性への還元によって対処される。
• Q3 (なぜ $I$ は最適なのか？): 現在、ネイティブなサポートは欠如しているが、より良い回答集合が存在しないことの説明へと還元可能である。
• Q4–Q6 (グローバルな存在/非存在): プロバナンス、証明システム、およびデバッグ/抽象化手法によって対処される。
• Q7–Q8 (定量的/集合的な挙動): ギャップとして特定されている。現在のツールは、特性がなぜ集合（複数の回答集合）にわたって成立するのか、あるいはプログラムになぜ特定の数の回答集合が存在するのかをネイティブに説明することはできない。

3. ツールと言語のサポート分析

著者らは、既存のツールをASP言語の拡張機能に対して評価している（表2）：

• 選言（Disjunction）: サポートが乏しい。ほとんどのツール（LABAS, s(CASP), xASP2）は、説明生成の複雑さから、選言ルールをうまく扱えない。
• 選択ルールと集約（Choice Rules & Aggregates）: 部分的にサポートされている（例：xASP2, xclingo, UCOREXPLAIN）が、しばしば制限がある。
• 弱制約（Weak Constraints）: 一般に説明目的としてはサポートされていないが、デバッグにおけるDWASPは例外である。
• ソルバー依存性: ソルバー依存の手法（例：xclingo, s(CASP)）と、ソルバーに依存しない手法（例：LABAS, 因果的正当化）の両方が存在する。

結果と知見

• カバー範囲: ほとんどのユーザーの問いは、ネイティブに、あるいは充足不能性への還元（なぜプログラムに回答集合が存在しないのかの説明）によって回答可能である。
• 限界:
  • 言語のギャップ: 選言と弱制約は、説明ツールにとって依然として大きな障壁である。
  • スケーラビリティ: ほとんどの手法はポストホック（事後的）であり、グラウンドプログラム上で動作するため、大規模な問題に対して高い計算複雑度を持つ。
  • 認知負荷: 不整合（デバッグ）に関する説明は、技術的（ルールセット）であり、非専門家にとって解釈が困難である。
  • 欠落しているシナリオ: 回答集合の数量に関する問いや、複数の回答集合にわたって特性が保持される理由に関する問いを扱う手法は現在存在しない。
• 相互運用性: ユーザーはローカルな説明ツールかグローバルな説明ツールのどちらかを選択しなければならず、「システムの分断」が存在する。統一されたフレームワークは欠如している。

意義と今後の方向性

本論文は、理論的な説明能力と実用的なユーザーニーズの間の溝を埋めることを目的として、研究者と非専門家のASPユーザーの両方にとってのガイドとして位置づけている。

意義:

• ローカルな推論とグローバルな推論を区別することで、ASPのための統一されたXAIフレームワークを確立した。
• 不整合（充足不能性）を説明することが、普遍的な説明アプローチへの重要なステップであることを強調している。なぜなら、多くの問いがこの形式に還元されるからである。
• 簡潔で解釈可能な説明の必要性を特定しており、抽象化と段階的な推論が認知努力を軽減するために不可ントであることを示唆している。

今後の研究方向:

• 認知的側面: 不整合（例：グラフ彩色における隠れた「補題」やクリーク）を、非専門家にも理解できる形で提示する方法の開発。
• インタラクション: 技術的な説明（例：MUS）を自然言語に翻訳し、ユーザーのクエリを解析するために、大規模言語モデル（LLM）を統合すること。
• スケーラビリティ: 非グラウンドプログラムや大規模な問題を扱うために、説明技術をソルバーに直接組み込むこと。
• 新しい問いのタイプ: 回答集合の数量や集合的な挙動に関する専用のソリューションの開発。

著者らは、豊かな手法の風景が存在する一方で、単一のツールですべてのニーズを満たすことはできず、今後の研究は言語サポート、スケーラビリティ、および複雑な論理的推論の認知的解釈に対処する必要があると結論づけている。