Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation

TL;DR

The paper targets the limitations of traditional neural network formal verification, which yields binary safe/unsafe outcomes, by introducing Abstract DNN-Verification (ADV) that reasons over a hierarchy of unsafe outputs using abstract interpretation. By propagating abstract input domains through the network and using a widening perturbation, ADV produces multiple levels of safety judgments (Abstract Safe, Safe, Unsafe) and can rank adversarial inputs by their impact on the safety hierarchy, potentially with comparable or lower computational cost than standard methods. Theoretical contributions include the Abstract Coherence framework, NP-hardness/NP-completeness results, and a formal relationship to existing weakened robustness concepts. Empirically, ADV is demonstrated on Habitat-Lab DRL tasks and CIFAR-10 benchmarks, showing that output abstractions reduce timeouts and enable nuanced insights into robustness and safety, including ranking of attacks and identification of tolerable misclassifications. Overall, the approach offers a more informative, interpretable, and scalable safety analysis for DNNs in safety-critical settings, with practical applicability to real-world robotics and vision benchmarks.

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.

Figures (11)

• Figure 1: Overview of the proposed Abstract DNN-Verification in this paper. On the left, given the intersection of the reachable sets, the concrete classes are not able to provide an answer. Conversely if we use the first level of abstraction (right part of the image) even if the reachable sets are overlapped, i.e., the intersection is nonempty, it is fully contained in the set of "safety-critical signs" output abstraction, allowing to provide the abstract safe answer.
• Figure 2: Example of Branch-and-Bound verification process with iterative input refinement approach. In the example we consider the safe set $\mathcal{S} = [0, \infty)$ and, for simplicity, a DNN with a single output node.
• Figure 3: Toy DNN employed in the Abstract DNN-Verification example. $\mathbb{C}\hbox{$\stackrel{\hbox{\tt\tiny def}}{\; =\;}$}\{c_i\hbox{$\stackrel{\hbox{\tt\tiny def}}{\; =\;}$}\langle i,Y_i \rangle~|~i\in[1,5]\}$.
• Figure 4: Enumeration result of the verification process for $\mathcal{X}$. The green area represents the portion of the input space mapped in the output abstraction $\{c_2,c_3,c_5\}$, while in orange, the one in $\{c_1\}$.
• Figure 5: Unsafe scenarios from the Habitat Lab experiments: On the left, the humanoid approaches the robot, which should move backward to avoid collision. In the center, the humanoid moves away, and the robot should follow while avoiding obstacles. On the right, the humanoid approaches from behind, and the robot should turn to avoid an unexpected collision while searching for the humanoid.

Theorems & Definitions (12)

• Definition 1: DNN-Verification Problem
• Definition 2: Coherence giacobazzi2024adversities.
• Definition 3: Widening Input Perturbation function
• Proposition 1
• Definition 4: Abstract Coherence
• Theorem 1
• proof
• Definition 5: Abstract DNN-Verification
• Proposition 2
• Example 1