形式手法による検証可能かつターゲット化された説明へ

要旨: 深層ニューラルネットワークが、自動運転や医療診断のような安全性が極めて重要な領域に導入されるにつれ、関係者には、解釈可能であると同時に、形式的な保証に裏打ちされた信頼性の高い説明が求められます。既存のXAI手法はこの点で不十分です。ヒューリスティックな帰属（アトリビューション）技術（例: LIME、Integrated Gradients）は、影響の大きい特徴を強調するものの、意思決定境界に関する数学的保証を提供しません。一方で、形式手法によるアプローチは頑健性を検証することはできますが、対象が定まっていないため、重要なリスクを表しているかどうかにかかわらず、最も近い境界を解析するだけに留まります。安全性が極めて重要なシステムでは、誤分類のすべてが同じ重大性を持つわけではありません。「停止（Stop）」標識を「60 kph」標識だと誤って解釈することは、「追い越し禁止（No Passing）」標識と誤るよりもはるかに危険です。我々は、ViTaX（Verified and Targeted Explanations）という形式的XAIフレームワークを導入します。これは、数学的保証を伴う、的を絞った（ターゲット）反事実的説明を生成します。入力（クラス y）と、ユーザが指定する重要な代替（クラス t）に対して、ViTaXは次を行います:（1）y→t への遷移に対して最も敏感な、最小の特徴部分集合を特定し、（2）これらの特徴を epsilon によって摂動しても分類が t に反転しないことを保証するために、形式的到達可能性解析を適用します。これは、Targeted epsilon-Robustness（ターゲット付き epsilon-頑健性）として形式化し、特定のターゲット・クラスに向けた摂動に対して、特徴部分集合が頑健性を維持するかどうかを証明します。ViTaXは、ユーザが特定した代替に対するモデルの耐性について、形式的に保証された説明を提供する最初の手法です。MNIST、GTSRB、EMNIST、TaxiNetでの評価により、説明の要素数（最小の説明集合）を抑えつつ、忠実度が30%以上改善することが示されます。