論文の概要: Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation

• arxiv url: http://arxiv.org/abs/2505.05235v1
• Date: Thu, 08 May 2025 13:29:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-09 21:43:49.899669
• Title: Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation
• Title（参考訳）: 階層型安全抽象解釈によるニューラルネットワーク検証の促進
• Authors: Luca Marzari, Isabella Mastroeni, Alessandro Farinelli,
• Abstract要約: 我々は、安全でない出力の階層構造を検証する抽象的DNN検証と呼ばれる新しい問題定式化を導入する。 出力到達可能な集合に関する抽象的解釈と推論を活用することにより,形式的検証プロセスにおいて,複数の安全性レベルを評価することができる。 我々の貢献には、新しい抽象的安全性の定式化と既存のアプローチとの関係を理論的に探求することが含まれる。
• 参考スコア（独自算出の注目度）: 52.626086874715284
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Traditional methods for formal verification (FV) of deep neural networks (DNNs) are constrained by a binary encoding of safety properties, where a model is classified as either safe or unsafe (robust or not robust). This binary encoding fails to capture the nuanced safety levels within a model, often resulting in either overly restrictive or too permissive requirements. In this paper, we introduce a novel problem formulation called Abstract DNN-Verification, which verifies a hierarchical structure of unsafe outputs, providing a more granular analysis of the safety aspect for a given DNN. Crucially, by leveraging abstract interpretation and reasoning about output reachable sets, our approach enables assessing multiple safety levels during the FV process, requiring the same (in the worst case) or even potentially less computational effort than the traditional binary verification approach. Specifically, we demonstrate how this formulation allows rank adversarial inputs according to their abstract safety level violation, offering a more detailed evaluation of the model's safety and robustness. Our contributions include a theoretical exploration of the relationship between our novel abstract safety formulation and existing approaches that employ abstract interpretation for robustness verification, complexity analysis of the novel problem introduced, and an empirical evaluation considering both a complex deep reinforcement learning task (based on Habitat 3.0) and standard DNN-Verification benchmarks.
• Abstract（参考訳）: ディープニューラルネットワーク(DNN)の従来の形式検証(FV)方法は、安全性特性のバイナリ符号化によって制約され、モデルが安全か安全でないか(ロバストかロバストでないか)に分類される。 このバイナリエンコーディングは、モデル内のニュアンスされた安全性レベルをキャプチャするのに失敗し、しばしば過度に制限されるか、寛容すぎる要求をもたらす。 本稿では,安全でない出力の階層構造を検証し,与えられたDNNの安全性面をより詳細に解析する,Abstract DNN-Verificationと呼ばれる新しい問題定式化を提案する。 重要なことは、出力到達可能な集合に関する抽象的な解釈と推論を活用することで、我々のアプローチは、FVプロセス中に複数の安全性レベルを評価できる。 具体的には、この定式化によって、それらの抽象的安全レベル違反にしたがって、ランク逆入力が許されるかを示し、モデルの安全性と堅牢性をより詳細に評価する。 我々の貢献には、ロバスト性検証のための抽象的解釈を用いた新しい抽象的安全定式化と既存のアプローチとの関係の理論的検討、導入した新しい問題の複雑性分析、複雑な深層強化学習タスク(Habitat 3.0に基づく)と標準DNN-Verificationベンチマークの両方を考慮した実証的評価が含まれる。

関連論文リスト

• Verification-Guided Falsification for Safe RL via Explainable Abstraction and Risk-Aware Exploration [8.246285288584625]
  本稿では、説明可能性、モデルチェック、リスク誘導のファルシフィケーションを統合し、厳密性とカバレッジを両立させるハイブリッドフレームワークを提案する。 我々のアプローチは、包括的抽象ポリシー要約(CAPS)を用いたRLポリシーの人間解釈可能な抽象化の構築から始まる。 違反が検出されない場合、オフラインデータセットの抽象化とカバレッジに制限があるため、満足度を結論付けることはできません。
  論文  参考訳（メタデータ） (2025-06-04T00:54:01Z)
• Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing [57.49021927832259]
  ディープニューラルネットワーク(DNN)は多くのシナリオで異常な結果を示した強力なツールです。 しかし、それらの複雑な設計と透明性の欠如は、現実世界のアプリケーションに適用する際の安全性上の懸念を提起する。 DNNの形式的検証(FV)は、安全面の証明可能な保証を提供する貴重なソリューションとして登場した。
  論文  参考訳（メタデータ） (2023-12-10T13:51:25Z)
• Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees [86.1362094580439]
  安全プロパティとDNNが与えられた場合、安全であるプロパティ入力領域のすべての領域の集合を列挙する。 この問題の #P-hardness のため,epsilon-ProVe と呼ばれる効率的な近似法を提案する。 提案手法は, 許容限界の統計的予測により得られた出力可到達集合の制御可能な過小評価を利用する。
  論文  参考訳（メタデータ） (2023-08-18T22:30:35Z)
• Online Safety Property Collection and Refinement for Safe Deep Reinforcement Learning in Mapless Navigation [79.89605349842569]
  オンラインプロパティのコレクション・リファインメント(CROP)フレームワークをトレーニング時にプロパティを設計するために導入する。 CROPは、安全でない相互作用を識別し、安全特性を形成するためにコストシグナルを使用する。 本手法をいくつかのロボットマップレスナビゲーションタスクで評価し,CROPで計算した違反量によって,従来のSafe DRL手法よりも高いリターンと低いリターンが得られることを示す。
  論文  参考訳（メタデータ） (2023-02-13T21:19:36Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• Exploring Robustness of Unsupervised Domain Adaptation in Semantic Segmentation [74.05906222376608]
  クリーンな画像とそれらの逆の例との一致を、出力空間における対照的な損失によって最大化する、逆向きの自己スーパービジョンUDA(ASSUDA)を提案する。 i) セマンティックセグメンテーションにおけるUDA手法のロバスト性は未解明のままであり, (ii) 一般的に自己スーパービジョン(回転やジグソーなど) は分類や認識などのイメージタスクに有効であるが, セグメンテーションタスクの識別的表現を学習する重要な監視信号の提供には失敗している。
  論文  参考訳（メタデータ） (2021-05-23T01:50:44Z)
• An Abstraction-based Method to Verify Multi-Agent Deep Reinforcement-Learning Behaviours [8.95294551927446]
  マルチエージェント強化学習(RL)はしばしば、学習エージェントの安全な行動を保証するために苦労する。 本稿では,形式検証と(深度)RLアルゴリズムを組み合わせることで,形式化された安全制約の満足度を保証する手法を提案する。
  論文  参考訳（メタデータ） (2021-02-02T11:12:30Z)
• PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier [1.1011268090482575]
  我々は、ReLU NNの最も一般的な安全仕様を正式に検証するための新しいアプローチを導入する。 我々は, 線形実現可能性チェッカーとしてだけでなく, 解法で許容される緩和量のペナルティ化の手段として, 凸解法を用いる。
  論文  参考訳（メタデータ） (2020-06-18T21:33:07Z)

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

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