# Safety Verification of Neural Network Controlled Systems

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Nov 2020.

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

- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability](https://mlsanity.com/paper/2201.06626/) (2022)
- [Generating Probabilistic Safety Guarantees for Neural Network Controllers](https://mlsanity.com/paper/2103.01203/) (2021)
- [Verification of Neural Network Control Systems using Symbolic Zonotopes and Polynotopes](https://mlsanity.com/paper/2306.14619/) (2023)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [Dependable Neural Networks Through Redundancy, A Comparison of Redundant Architectures](https://mlsanity.com/paper/2108.02565/) (2021)
- [Physics-model-guided Worst-case Sampling for Safe Reinforcement Learning](https://mlsanity.com/paper/2412.13224/) (2024)
- [Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2511.14755/) (2025)

## Abstract (arXiv)

In this paper, we propose a system-level approach for verifying the safety of neural network controlled systems, combining a continuous-time physical system with a discrete-time neural network based controller. We assume a generic model for the controller that can capture both simple and complex behaviours involving neural networks. Based on this model, we perform a reachability analysis that soundly approximates the reachable states of the overall system, allowing to achieve a formal proof of safety. To this end, we leverage both validated simulation to approximate the behaviour of the physical system and abstract interpretation to approximate the behaviour of the controller. We evaluate the applicability of our approach using a real-world use case. Moreover, we show that our approach can provide valuable information when the system cannot be proved totally safe.