論文の概要: 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ベンチマークの両方を考慮した実証的評価が含まれる。

関連論文リスト

• Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing [57.49021927832259]
  ディープニューラルネットワーク(DNN)は多くのシナリオで異常な結果を示した強力なツールです。 しかし、それらの複雑な設計と透明性の欠如は、現実世界のアプリケーションに適用する際の安全性上の懸念を提起する。 DNNの形式的検証(FV)は、安全面の証明可能な保証を提供する貴重なソリューションとして登場した。
  論文  参考訳（メタデータ） (2023-12-10T13:51:25Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)

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

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