# Safe and Reliable Training of Learning-Based Aerospace Controllers

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in Safe and constrained RL, one of 15 directions in Deep reinforcement learning methods.
- Builds on 52 of its 75 references that are in the map.
- First posted on arXiv 9 Jul 2024.

## Placed in

- Deep reinforcement learning methods / [Safe and constrained RL](https://mlsanity.com/deeprl/safe-and-constrained-rl/)

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [Safe Learning in Robotics: From Learning-Based Control to Safe Reinforcement Learning](https://mlsanity.com/paper/2108.06266/) (2021)
- [A Lyapunov-based Approach to Safe Reinforcement Learning](https://mlsanity.com/paper/1805.07708/) (2018)
- [Control Barrier Function Based Quadratic Programs for Safety Critical Systems](https://mlsanity.com/paper/1609.06408/) (2016)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances](https://mlsanity.com/paper/1709.07523/) (2017)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificates](https://mlsanity.com/paper/2101.05436/) (2021)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Reachability Constrained Reinforcement Learning](https://mlsanity.com/paper/2205.07536/) (2022)
- [Safety and Liveness Guarantees through Reach-Avoid Reinforcement Learning](https://mlsanity.com/paper/2112.12288/) (2021)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Reach-Avoid Problems with Time-Varying Dynamics, Targets and Constraints](https://mlsanity.com/paper/1410.6445/) (2014)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [Iterative Reachability Estimation for Safe Reinforcement Learning](https://mlsanity.com/paper/2309.13528/) (2023)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [Stabilizing Neural Control Using Self-Learned Almost Lyapunov Critics](https://mlsanity.com/paper/2107.04989/) (2021)
- [Abstraction based Output Range Analysis for Neural Networks](https://mlsanity.com/paper/2007.09527/) (2020)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Robustness of Control Barrier Functions for Safety Critical Control](https://mlsanity.com/paper/1612.01554/) (2016)
- [NNrepair: Constraint-based Repair of Neural Network Classifiers](https://mlsanity.com/paper/2103.12535/) (2021)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)

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

- [Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation](https://mlsanity.com/paper/2408.03915/) (2024)
- [Defining Operational Conditions for Safety-Critical AI-Based Systems from Data](https://mlsanity.com/paper/2601.22118/) (2026)
- [On Improving Deep Active Learning with Formal Verification](https://mlsanity.com/paper/2512.14170/) (2025)
- [Neural Network Verification using Partial Multi-Neuron Relaxation](https://mlsanity.com/paper/2605.30155/) (2026)

## Abstract (arXiv)

In recent years, deep reinforcement learning (DRL) approaches have generated highly successful controllers for a myriad of complex domains. However, the opaque nature of these models limits their applicability in aerospace systems and safety-critical domains, in which a single mistake can have dire consequences. In this paper, we present novel advancements in both the training and verification of DRL controllers, which can help ensure their safe behavior. We showcase a design-for-verification approach utilizing k-induction and demonstrate its use in verifying liveness properties. In addition, we also give a brief overview of neural Lyapunov Barrier certificates and summarize their capabilities on a case study. Finally, we describe several other novel reachability-based approaches which, despite failing to provide guarantees of interest, could be effective for verification of other DRL systems, and could be of further interest to the community.