# Safety Verification of Neural Network Control Systems Using Guaranteed Neural Network Model Reduction

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 20 references that are in the map.
- First posted on arXiv 17 Jan 2023.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [A Survey on Deep Learning in Medical Image Analysis](https://mlsanity.com/paper/1702.05747/) (2017)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Deep Learning in Neural Networks: An Overview](https://mlsanity.com/paper/1404.7828/) (2014)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach](https://mlsanity.com/paper/2004.12273/) (2020)
- [DeepCABAC: A Universal Compression Algorithm for Deep Neural Networks](https://mlsanity.com/paper/1907.11900/) (2019)
- [Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations](https://mlsanity.com/paper/1712.08163/) (2017)

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

- [Bridging Dimensions: Confident Reachability for High-Dimensional Controllers](https://mlsanity.com/paper/2311.04843/) (2023)
- [Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2511.14755/) (2025)

## Abstract (arXiv)

This paper aims to enhance the computational efficiency of safety verification of neural network control systems by developing a guaranteed neural network model reduction method. First, a concept of model reduction precision is proposed to describe the guaranteed distance between the outputs of a neural network and its reduced-size version. A reachability-based algorithm is proposed to accurately compute the model reduction precision. Then, by substituting a reduced-size neural network controller into the closed-loop system, an algorithm to compute the reachable set of the original system is developed, which is able to support much more computationally efficient safety verification processes. Finally, the developed methods are applied to a case study of the Adaptive Cruise Control system with a neural network controller, which is shown to significantly reduce the computational time of safety verification and thus validate the effectiveness of the method.