# Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation

arXiv: https://arxiv.org/abs/2505.05235 · HTML: https://mlsanity.com/paper/2505.05235/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 28 references that are in the map.
- First posted on arXiv 8 May 2025.

## Builds on (most cited first, 19 of 19)

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Habitat: A Platform for Embodied AI Research](https://mlsanity.com/paper/1904.01201/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [An Introduction to Convolutional Neural Networks](https://mlsanity.com/paper/1511.08458/) (2015)
- [Habitat 2.0: Training Home Assistants to Rearrange their Habitat](https://mlsanity.com/paper/2106.14405/) (2021)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks](https://mlsanity.com/paper/2301.07068/) (2023)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)
- [Curriculum Learning for Safe Mapless Navigation](https://mlsanity.com/paper/2112.12490/) (2021)
- [Constrained Reinforcement Learning and Formal Verification for Safe Colonoscopy Navigation](https://mlsanity.com/paper/2303.03207/) (2023)

## Built on by (most cited first, 4 of 4)

- [Formal Verification of Variational Quantum Circuits](https://mlsanity.com/paper/2507.10635/) (2025)
- [Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verification](https://mlsanity.com/paper/2511.11699/) (2025)
- [Probabilistic Verification of Recurrent Neural Networks for Single and Multi-Agent Reinforcement Learning](https://mlsanity.com/paper/2605.14758/) (2026)
- [Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism](https://mlsanity.com/paper/2606.09377/) (2026)

## Abstract (arXiv)

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.