# Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 60 references that are in the map.
- First posted on arXiv 21 Nov 2022.

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Continuous control with deep reinforcement learning](https://mlsanity.com/paper/1509.02971/) (2015)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Scalable Quantitative Verification For Deep Neural Networks](https://mlsanity.com/paper/2002.06864/) (2020)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Time Discretization-Invariant Safe Action Repetition for Policy Gradient Methods](https://mlsanity.com/paper/2111.03941/) (2021)
- [Probabilistic Guarantees for Safe Deep Reinforcement Learning](https://mlsanity.com/paper/2005.07073/) (2020)
- [DRYVR:Data-driven verification and compositional reasoning for automotive systems](https://mlsanity.com/paper/1702.06902/) (2017)
- [Interval Universal Approximation for Neural Networks](https://mlsanity.com/paper/2007.06093/) (2020)
- [PAC Model Checking of Black-Box Continuous-Time Dynamical Systems](https://mlsanity.com/paper/2007.10141/) (2020)
- [Fast Parametric Model Checking through Model Fragmentation](https://mlsanity.com/paper/2102.01490/) (2021)
- [Dependability Analysis of Deep Reinforcement Learning based Robotics and Autonomous Systems through Probabilistic Model Checking](https://mlsanity.com/paper/2109.06523/) (2021)

## Abstract (arXiv)

The intrinsic complexity of deep neural networks (DNNs) makes it challenging to verify not only the networks themselves but also the hosting DNN-controlled systems. Reachability analysis of these systems faces the same challenge. Existing approaches rely on over-approximating DNNs using simpler polynomial models. However, they suffer from low efficiency and large overestimation, and are restricted to specific types of DNNs. This paper presents a novel abstraction-based approach to bypass the crux of over-approximating DNNs in reachability analysis. Specifically, we extend conventional DNNs by inserting an additional abstraction layer, which abstracts a real number to an interval for training. The inserted abstraction layer ensures that the values represented by an interval are indistinguishable to the network for both training and decision-making. Leveraging this, we devise the first black-box reachability analysis approach for DNN-controlled systems, where trained DNNs are only queried as black-box oracles for the actions on abstract states. Our approach is sound, tight, efficient, and agnostic to any DNN type and size. The experimental results on a wide range of benchmarks show that the DNNs trained by using our approach exhibit comparable performance, while the reachability analysis of the corresponding systems becomes more amenable with significant tightness and efficiency improvement over the state-of-the-art white-box approaches.