Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation

要約

ディープニューラルネットワーク（DNNS）の正式な検証（FV）の従来の方法は、安全性のバイナリエンコードによって制約されます。モデルは安全性または安全でない（堅牢または堅牢）として分類されます。
このバイナリエンコーディングは、モデル内の微妙な安全レベルをキャプチャできず、多くの場合、過度に制限的または寛容すぎる要件をもたらします。
このホワイトペーパーでは、抽象的なDNN検証と呼ばれる新しい問題定式化を紹介します。これは、安全でない出力の階層構造を検証し、特定のDNNの安全性のより詳細な分析を提供します。
重要なことは、出力の到達可能なセットに関する抽象的な解釈と推論を活用することにより、私たちのアプローチにより、FVプロセス中に複数の安全レベルを評価することができます。
具体的には、この定式化により、抽象的な安全レベルの違反に応じて敵対的な入力がどのように可能かを示し、モデルの安全性と堅牢性のより詳細な評価を提供します。
私たちの貢献には、我々の新しい抽象的な安全策定と、堅牢性の検証のために抽象的な解釈を採用する既存のアプローチ、導入された新規問題の複雑さ分析、および複雑なディープ強化学習タスク（生息地3.0に基づく）と標準的なDNN検証ベンチマークの両方を考慮した経験的評価との関係の理論的調査が含まれます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google