# Generating Probabilistic Safety Guarantees for Neural Network Controllers

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 37 references that are in the map.
- First posted on arXiv 1 Mar 2021.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Verifiable Reinforcement Learning via Policy Extraction](https://mlsanity.com/paper/1805.08328/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Deep Neural Network Compression for Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1810.04240/) (2018)
- [Learning Finite State Representations of Recurrent Policy Networks](https://mlsanity.com/paper/1811.12530/) (2018)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1912.07084/) (2019)
- [Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers](https://mlsanity.com/paper/1802.06981/) (2018)
- [Reachability Analysis and Safety Verification for Neural Network Control Systems](https://mlsanity.com/paper/1805.09944/) (2018)
- [A Reachability Method for Verifying Dynamical Systems with Deep Neural Network Controllers](https://mlsanity.com/paper/1903.00520/) (2019)
- [Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions](https://mlsanity.com/paper/1903.00762/) (2019)
- [Safety Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2011.05174/) (2020)
- [Point-Based Methods for Model Checking in Partially Observable Markov Decision Processes](https://mlsanity.com/paper/2001.03809/) (2020)
- [Reachable Set Estimation and Verification for Neural Network Models of Nonlinear Dynamic Systems](https://mlsanity.com/paper/1802.03557/) (2018)

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

- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs](https://mlsanity.com/paper/2106.05325/) (2021)
- [YANNs: Y-wise Affine Neural Networks for Exact and Efficient Representations of Piecewise Linear Functions](https://mlsanity.com/paper/2505.07054/) (2025)
- [Defining Operational Conditions for Safety-Critical AI-Based Systems from Data](https://mlsanity.com/paper/2601.22118/) (2026)

## Abstract (arXiv)

Neural networks serve as effective controllers in a variety of complex settings due to their ability to represent expressive policies. The complex nature of neural networks, however, makes their output difficult to verify and predict, which limits their use in safety-critical applications. While simulations provide insight into the performance of neural network controllers, they are not enough to guarantee that the controller will perform safely in all scenarios. To address this problem, recent work has focused on formal methods to verify properties of neural network outputs. For neural network controllers, we can use a dynamics model to determine the output properties that must hold for the controller to operate safely. In this work, we develop a method to use the results from neural network verification tools to provide probabilistic safety guarantees on a neural network controller. We develop an adaptive verification approach to efficiently generate an overapproximation of the neural network policy. Next, we modify the traditional formulation of Markov decision process (MDP) model checking to provide guarantees on the overapproximated policy given a stochastic dynamics model. Finally, we incorporate techniques in state abstraction to reduce overapproximation error during the model checking process. We show that our method is able to generate meaningful probabilistic safety guarantees for aircraft collision avoidance neural networks that are loosely inspired by Airborne Collision Avoidance System X (ACAS X), a family of collision avoidance systems that formulates the problem as a partially observable Markov decision process (POMDP).