# Provably Correct Training of Neural Network Controllers Using Reachability Analysis

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 35 of its 52 references that are in the map.
- First posted on arXiv 22 Feb 2021.

## Builds on (most cited first, 30 of 35)

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Constrained Policy Optimization](https://mlsanity.com/paper/1705.10528/) (2017)
- [Safe Model-based Reinforcement Learning with Stability Guarantees](https://mlsanity.com/paper/1705.08551/) (2017)
- [A Lyapunov-based Approach to Safe Reinforcement Learning](https://mlsanity.com/paper/1805.07708/) (2018)
- [Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networks](https://mlsanity.com/paper/1906.04893/) (2019)
- [End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Tasks](https://mlsanity.com/paper/1903.08792/) (2019)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [A General Safety Framework for Learning-Based Control in Uncertain Robotic Systems](https://mlsanity.com/paper/1705.01292/) (2017)
- [Lyapunov-based Safe Policy Optimization for Continuous Control](https://mlsanity.com/paper/1901.10031/) (2019)
- [Bayesian Optimization with Safety Constraints: Safe and Automatic Parameter Tuning in Robotics](https://mlsanity.com/paper/1602.04450/) (2016)
- [Learning-based Model Predictive Control for Safe Exploration](https://mlsanity.com/paper/1803.08287/) (2018)
- [A predictive safety filter for learning-based control of constrained nonlinear dynamical systems](https://mlsanity.com/paper/1812.05506/) (2018)
- [Trial without Error: Towards Safe Reinforcement Learning via Human Intervention](https://mlsanity.com/paper/1707.05173/) (2017)
- [Training robust neural networks using Lipschitz bounds](https://mlsanity.com/paper/2005.02929/) (2020)
- [On the number of response regions of deep feed forward networks with piece-wise linear activations](https://mlsanity.com/paper/1312.6098/) (2013)
- [Learning Control Barrier Functions from Expert Demonstrations](https://mlsanity.com/paper/2004.03315/) (2020)
- [Neural Lander: Stable Drone Landing Control using Learned Dynamics](https://mlsanity.com/paper/1811.08027/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Safe Exploration in Finite Markov Decision Processes with Gaussian Processes](https://mlsanity.com/paper/1606.04753/) (2016)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Linear model predictive safety certification for learning-based control](https://mlsanity.com/paper/1803.08552/) (2018)
- [Safe Learning of Quadrotor Dynamics Using Barrier Certificates](https://mlsanity.com/paper/1710.05472/) (2017)
- [Safe Reinforcement Learning for Autonomous Vehicles through Parallel Constrained Policy Optimization](https://mlsanity.com/paper/2003.01303/) (2020)
- [Synthesis of Control Barrier Functions Using a Supervised Machine Learning Approach](https://mlsanity.com/paper/2003.04950/) (2020)
- [Robust Regression for Safe Exploration in Control](https://mlsanity.com/paper/1906.05819/) (2019)
- [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020)
- [Temporal Logic Guided Safe Reinforcement Learning Using Control Barrier Functions](https://mlsanity.com/paper/1903.09885/) (2019)
- [Safe Multi-Agent Interaction through Robust Control Barrier Functions with Learned Uncertainties](https://mlsanity.com/paper/2004.05273/) (2020)
- [ShieldNN: A Provably Safe NN Filter for Unsafe NN Controllers](https://mlsanity.com/paper/2006.09564/) (2020)
- [TIRA: Toolbox for Interval Reachability Analysis](https://mlsanity.com/paper/1902.05204/) (2019)

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

- [NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing](https://mlsanity.com/paper/2203.15841/) (2022)
- [BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic](https://mlsanity.com/paper/2211.14438/) (2022)
- [Provably Safe Model-Based Meta Reinforcement Learning: An Abstraction-Based Approach](https://mlsanity.com/paper/2109.01255/) (2021)
- [Counterexample-Guided Repair of Reinforcement Learning Systems Using Safety Critics](https://mlsanity.com/paper/2405.15430/) (2024)
- [Failing with Grace: Learning Neural Network Controllers that are Boundedly Unsafe](https://mlsanity.com/paper/2106.11881/) (2021)

## Abstract (arXiv)

In this paper, we consider the problem of training neural network (NN) controllers for nonlinear dynamical systems that are guaranteed to satisfy safety and liveness (e.g., reach-avoid) properties. Our approach is to combine model-based design methodologies for dynamical systems with data-driven approaches to achieve this target. We confine our attention to NNs with Rectifier Linear Unit (ReLU) nonlinearity which are known to represent Continuous Piece-Wise Affine (CPWA) functions. Given a mathematical model of the dynamical system, we compute a finite-state abstract model that captures the closed-loop behavior under all possible CPWA controllers. Using this finite-state abstract model, our framework identifies a family of CPWA functions guaranteed to satisfy the safety requirements. We augment the learning algorithm with a NN weight projection operator during training that enforces the resulting NN to represent a CPWA function from the provably safe family of CPWA functions. Moreover, the proposed framework uses the finite-state abstract model to identify candidate CPWA functions that may satisfy the liveness properties. Using such candidate CPWA functions, the proposed framework biases the NN training to achieve the liveness specification. We show the efficacy of the proposed framework both in simulation and on an actual robotic vehicle.