論文の概要: Towards Verified and Targeted Explanations through Formal Methods

• arxiv url: http://arxiv.org/abs/2604.14209v1
• Date: Sun, 05 Apr 2026 01:59:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-19 19:09:11.721061
• Title: Towards Verified and Targeted Explanations through Formal Methods
• Title（参考訳）: 形式的手法による検証・目標記述に向けて
• Abstract要約: 数学的保証を伴う半現実的説明を生成する形式的XAIフレームワークであるViTaXを紹介する。 ViTaXは、ユーザーが特定した摂動に対するモデルのレジリエンスを正式に保証する最初の方法である。
• 参考スコア（独自算出の注目度）: 6.649484765004503
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: As deep neural networks are deployed in safety-critical domains such as autonomous driving and medical diagnosis, stakeholders need explanations that are interpretable but also trustworthy with formal guarantees. Existing XAI methods fall short: heuristic attribution techniques (e.g., LIME, Integrated Gradients) highlight influential features but offer no mathematical guarantees about decision boundaries, while formal methods verify robustness yet remain untargeted, analyzing the nearest boundary regardless of whether it represents a critical risk. In safety-critical systems, not all misclassifications carry equal consequences; confusing a "Stop" sign for a "60 kph" sign is far more dangerous than confusing it with a "No Passing" sign. We introduce ViTaX (Verified and Targeted Explanations), a formal XAI framework that generates targeted semifactual explanations with mathematical guarantees. For a given input (class y) and a user-specified critical alternative (class t), ViTaX: (1) identifies the minimal feature subset most sensitive to the y->t transition, and (2) applies formal reachability analysis to guarantee that perturbing these features by epsilon cannot flip the classification to t. We formalize this through Targeted epsilon-Robustness, certifying whether a feature subset remains robust under perturbation toward a specific target class. ViTaX is the first method to provide formally guaranteed explanations of a model's resilience against user-identified alternatives. Evaluations on MNIST, GTSRB, EMNIST, and TaxiNet demonstrate over 30% fidelity improvement with minimal explanation cardinality.
• Abstract（参考訳）: ディープニューラルネットワークは、自律運転や医療診断などの安全クリティカルな領域にデプロイされるため、ステークホルダーは解釈可能であるだけでなく、正式な保証で信頼できる説明を必要とする。 既存のXAIメソッドは不足している: ヒューリスティック属性技術(例えば、LIME、統合グラディエント)は、影響力のある特徴を強調するが、決定境界に関する数学的保証は提供しない。 安全クリティカルなシステムでは、すべての誤分類が同等の結果をもたらすわけではない。"60 kph"記号の"Stop"記号を混乱させるのは、"No Passing"符号と混同するよりもはるかに危険である。 数学的保証を伴う半現実的説明を生成する形式的XAIフレームワークであるViTaX(Verified and Targeted Explanations)を紹介する。 与えられた入力 (class y) とユーザ指定のクリティカルな代替 (class t) に対して、ViTaX: (1) は y->t 遷移に最も敏感な最小の機能部分集合を識別し、(2) エプシロンによるこれらの特徴の摂動を t に反転できないことを保証するために、形式的到達可能性解析を適用する。 我々は、このことをターゲティング・エプシロン・ロバストネス(Targeted epsilon-Robustness)を通して形式化し、ある特徴部分集合が特定の対象クラスに対する摂動下で頑健であるかどうかを証明した。 ViTaXは、ユーザーが特定した代替品に対するモデルのレジリエンスを正式に保証する最初の方法である。 MNIST、GTSRB、EMNIST、TaxiNetの評価は、最小説明基準で30%以上の忠実度の改善を示した。

関連論文リスト

• Automatic Red Teaming for Implicit Vulnerabilities of Text-to-Image Models [58.59008920408855]
  本稿では,ターゲットモデルのパラメータへのアクセスを必要とせずに,暗黙の脆弱性を明らかにするためのAdvPIE(Adversarial Probing for Implicit VulnErabilities)を提案する。 AdvPIEは、審査員からのフィードバックに基づいて暗黙の敵のプロンプトを生成し、洗練するためのポリシーエージェントを採用する。 標準および安全性に適合したT2Iモデルの実験では、AdvPIE1が暗黙の脆弱性を効果的に発見している。
  論文  参考訳（メタデータ） (2026-09-05T13:45:09Z)
• Detecting Contaminated Code-Generation Prompt Batches via Influence Functions [4.185678330063222]
  大規模言語モデル(LLM)は、コード生成にますます使われているが、安全でない実装を誘発するプロンプトに弱いままである。 本稿では、影響関数を利用して異常モデル動作を誘発するプロンプトのバッチを識別する脅威モデル非依存検出手法であるCodeSIFTを提案する。
  論文  参考訳（メタデータ） (2026-08-14T13:37:53Z)
• A Self-Explainable Deep Architecture for Security Applications [19.98791465260198]
  セキュリティアプリケーション用に開発された自己説明可能なディープアーキテクチャであるXSecを紹介する。 トレーニング中、XSecは新しいマスクベースのアプローチを使用して、データから情報サブフィーチャを抽出する。 次に、XSecはテスト時に専用の類似度層でプロトタイプを利用し、類似度スコアを計算し、ポストホック解析を必要とせずに解釈可能な説明を生成する。 我々は、XSecを5つの異なるセキュリティシナリオで評価し、パフォーマンスの妥協を最小限にして、平均的な分類精度97.33%を達成する能力を示した。
  論文  参考訳（メタデータ） (2026-08-06T03:08:13Z)
• Evaluating Explainability in Safety-Critical ATR Systems: Limitations of Post-Hoc Methods and Paths Toward Robust XAI [2.3099144596725574]
  本稿では,安全クリティカルなATRシステムにおける説明可能性手法の構造化評価について述べる。 我々は、サリエンシベース、注意ベース、サロゲート・アプ・パッチを含む主要なXAIパラダイムを特定した。 我々は、急激な説明、摂動下での不安定性、視覚的に干渉する出力によって引き起こされる過度な信頼など、致命的な障害モードを導出する。
  論文  参考訳（メタデータ） (2026-05-07T06:42:08Z)
• The Inevitability of Side-Channel Leakage in Encrypted Traffic [18.365496056967917]
  効率優先のシステムでは、少なくとも1つのアプリケーションペアが識別可能である場合、リークは避けられないことを示す。 これにより、暗号化されたトラフィックサイドチャネルのための厳密な情報理論の基礎が確立される。
  論文  参考訳（メタデータ） (2026-02-15T08:55:19Z)
• EXCODER: EXplainable Classification Of DiscretE time series Representations [11.617069798807762]
  ディープラーニングは時系列分類を大幅に改善したが、これらのモデルに説明可能性の欠如は依然として大きな課題である。 本稿では,ベクトル量子化変分オートエンコーダ(VQ-VAE)や離散変分オートエンコーダ(DVAE)など,時系列を離散潜在表現に変換する方法について検討する。 これらの圧縮表現にXAI法を適用すると、分類性能を犠牲にすることなく忠実性を維持するための簡潔で構造化された説明が得られることを示す。
  論文  参考訳（メタデータ） (2026-02-13T16:47:45Z)
• The Compliance Paradox: Semantic-Instruction Decoupling in Automated Academic Code Evaluation [11.984098021215878]
  SPACI(Semantic-Preserving Adrial Code Injection)フレームワークとAST-ASIP(Abstract Syntax Tree-Aware Semantic Injection Protocol)を紹介する。 これらの方法は、抽象構文木(英語版)の構文的に不活性な領域(トリヴィアノード)に逆方向の指示を埋め込むことにより、構文解析ギャップを利用する。 Python、C、C++、Javaの25,000のサブミッションにまたがる9つのSOTAモデルの大規模な評価を通じて、DeepSeek-V3のような高容量オープンウェイトモデルにおいて、破滅的な失敗率(>95%)を明らかにします。
  論文  参考訳（メタデータ） (2026-01-29T07:40:58Z)
• Deciding When Not to Decide: Indeterminacy-Aware Intrusion Detection with NeutroSENSE [0.0]
  NeutroSENSEは、IoT環境における侵入検出を解釈するためのニュートロゾフィックのアンサンブルフレームワークである。 システムは予測信頼を真理(T)、虚偽(F)、不確定性(I)に分解し、不確実な定量化と棄却を可能にする。
  論文  参考訳（メタデータ） (2025-06-05T11:43:31Z)
• Conformal Predictions for Probabilistically Robust Scalable Machine Learning Classification [1.757077789361314]
  コンフォーマルな予測により、信頼性と堅牢な学習アルゴリズムを定義することができる。 基本的には、アルゴリズムが実際に使われるのに十分であるかどうかを評価する方法である。 本稿では,設計当初から信頼性の高い分類学習フレームワークを定義した。
  論文  参考訳（メタデータ） (2024-03-15T14:59:24Z)
• Credible Teacher for Semi-Supervised Object Detection in Open Scene [106.25850299007674]
  Open Scene Semi-Supervised Object Detection (O-SSOD)では、ラベル付きデータはラベル付きデータで観測されていない未知のオブジェクトを含む可能性がある。 より不確実性が、偽ラベルのローカライズと分類精度の低下につながるため、主に自己学習に依存する現在の手法には有害である。 我々は,不確実な擬似ラベルがモデルに誤解をもたらすのを防ぐための,エンドツーエンドのフレームワークであるCredible Teacherを提案する。
  論文  参考訳（メタデータ） (2024-01-01T08:19:21Z)
• ASSERT: Automated Safety Scenario Red Teaming for Evaluating the Robustness of Large Language Models [65.79770974145983]
  ASSERT、Automated Safety Scenario Red Teamingは、セマンティックなアグリゲーション、ターゲットブートストラップ、敵の知識注入という3つの方法で構成されている。 このプロンプトを4つの安全領域に分割し、ドメインがモデルの性能にどのように影響するかを詳細に分析する。 統計的に有意な性能差は, 意味的関連シナリオにおける絶対分類精度が最大11%, ゼロショット逆数設定では最大19%の絶対誤差率であることがわかった。
  論文  参考訳（メタデータ） (2023-10-14T17:10:28Z)
• Certified Interpretability Robustness for Class Activation Mapping [77.58769591550225]
  本稿では,解釈可能性マップのためのCORGI(Certifiable prOvable Robustness Guarantees)を提案する。 CORGIは入力画像を取り込み、そのCAM解釈可能性マップのロバスト性に対する証明可能な下限を与えるアルゴリズムである。 交通標識データを用いたケーススタディによるCORGIの有効性を示す。
  論文  参考訳（メタデータ） (2023-01-26T18:58:11Z)
• Robust-by-Design Classification via Unitary-Gradient Neural Networks [66.17379946402859]
  安全クリティカルシステムにおけるニューラルネットワークの使用には、敵攻撃が存在するため、安全で堅牢なモデルが必要である。 任意の入力 x の最小逆摂動を知るか、または同値に、分類境界から x の距離は、分類ロバスト性を評価し、証明可能な予測を与える。 Unitary-Gradient Neural Networkと呼ばれる新しいネットワークアーキテクチャが紹介される。 実験結果から,提案アーキテクチャは符号付き距離を近似し,単一の推論コストでxのオンライン分類が可能であることがわかった。
  論文  参考訳（メタデータ） (2022-09-09T13:34:51Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。 これは、説明に表される論理述語に基づいて、反実仮説を生成する。 そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
  論文  参考訳（メタデータ） (2022-05-25T03:40:59Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。