# Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning

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

## Key facts

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

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

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Soft Actor-Critic: Off-Policy Maximum Entropy Deep Reinforcement Learning with a Stochastic Actor](https://mlsanity.com/paper/1801.01290/) (2018)
- [Continuous control with deep reinforcement learning](https://mlsanity.com/paper/1509.02971/) (2015)
- [Constrained Policy Optimization](https://mlsanity.com/paper/1705.10528/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Safe Model-based Reinforcement Learning with Stability Guarantees](https://mlsanity.com/paper/1705.08551/) (2017)
- [DeepXplore: Automated Whitebox Testing of Deep Learning Systems](https://mlsanity.com/paper/1705.06640/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Verifiable Reinforcement Learning via Policy Extraction](https://mlsanity.com/paper/1805.08328/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Neurosymbolic Reinforcement Learning with Formally Verified Exploration](https://mlsanity.com/paper/2009.12612/) (2020)
- [Learning Certified Control using Contraction Metric](https://mlsanity.com/paper/2011.12569/) (2020)
- [Robust Model Predictive Shielding for Safe Reinforcement Learning with Stochastic Dynamics](https://mlsanity.com/paper/1910.10885/) (2019)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [An Inductive Synthesis Framework for Verifiable Reinforcement Learning](https://mlsanity.com/paper/1907.07273/) (2019)
- [Compositional Falsification of Cyber-Physical Systems with Machine Learning Components](https://mlsanity.com/paper/1703.00978/) (2017)
- [ReluDiff: Differential Verification of Deep Neural Networks](https://mlsanity.com/paper/2001.03662/) (2020)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks](https://mlsanity.com/paper/1907.10662/) (2019)
- [FAUST2: Formal Abstractions of Uncountable-STate STochastic processes](https://mlsanity.com/paper/1403.3286/) (2014)

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

- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [Ablation Study of How Run Time Assurance Impacts the Training and Performance of Reinforcement Learning Agents](https://mlsanity.com/paper/2207.04117/) (2022)
- [Learning on Abstract Domains: A New Approach for Verifiable Guarantee in Reinforcement Learning](https://mlsanity.com/paper/2106.06931/) (2021)
- [Dependability Analysis of Deep Reinforcement Learning based Robotics and Autonomous Systems through Probabilistic Model Checking](https://mlsanity.com/paper/2109.06523/) (2021)
- [Verification of Neural Network Control Systems in Continuous Time](https://mlsanity.com/paper/2406.00157/) (2024)

## Abstract (arXiv)

There has been significant recent interest in devising verification techniques for learning-enabled controllers (LECs) that manage safety-critical systems. Given the opacity and lack of interpretability of the neural policies that govern the behavior of such controllers, many existing approaches enforce safety properties through shield, a dynamic monitoring-and-repairing mechanism that ensures a LEC does not emit actions that would violate desired safety conditions. These methods, however, have been shown to have significant scalability limitations because verification costs grow as problem dimensionality and objective complexity increase. In this paper, we propose a new automated verification pipeline capable of synthesizing high-quality safe controllers even when the problem domain involves hundreds of dimensions, or when the desired objective involves stochastic perturbations, liveness considerations, and other complex non-functional properties. Our key insight involves separating safety verification from neural controller training, and using pre-computed verified safety shields to constrain the training process. Experimental results over a range of high-dimensional benchmarks demonstrate the effectiveness of our approach in a range of stochastic linear time-invariant and time-variant systems.