# Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees

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

## Key facts

- Cited by 23 papers in the map (data through 14 Oct 2026).
- Builds on 36 of its 75 references that are in the map.
- First posted on arXiv 11 Oct 2022.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [Concrete Problems in AI Safety](https://mlsanity.com/paper/1606.06565/) (2016)
- [Constrained Policy Optimization](https://mlsanity.com/paper/1705.10528/) (2017)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (2019)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [A Lyapunov-based Approach to Safe Reinforcement Learning](https://mlsanity.com/paper/1805.07708/) (2018)
- [Safe Exploration in Continuous Action Spaces](https://mlsanity.com/paper/1801.08757/) (2018)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [Learning-based Model Predictive Control for Safe Exploration](https://mlsanity.com/paper/1803.08287/) (2018)
- [The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems](https://mlsanity.com/paper/1808.00924/) (2018)
- [Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificates](https://mlsanity.com/paper/2101.05436/) (2021)
- [Safe Multi-Agent Reinforcement Learning via Shielding](https://mlsanity.com/paper/2101.11196/) (2021)
- [Safe Exploration for Interactive Machine Learning](https://mlsanity.com/paper/1910.13726/) (2019)
- [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)
- [Cautious Reinforcement Learning with Logical Constraints](https://mlsanity.com/paper/2002.12156/) (2020)
- [Linear model predictive safety certification for learning-based control](https://mlsanity.com/paper/1803.08552/) (2018)
- [Neural Certificates for Safe Control Policies](https://mlsanity.com/paper/2006.08465/) (2020)
- [Stabilizing Neural Control Using Self-Learned Almost Lyapunov Critics](https://mlsanity.com/paper/2107.04989/) (2021)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Robust Regression for Safe Exploration in Control](https://mlsanity.com/paper/1906.05819/) (2019)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [Almost Surely Stable Deep Dynamics](https://mlsanity.com/paper/2103.14722/) (2021)
- [A Barrier Function Approach to Finite-Time Stochastic System Verification and Control](https://mlsanity.com/paper/1909.05109/) (2019)
- [Shielding Atari Games with Bounded Prescience](https://mlsanity.com/paper/2101.08153/) (2021)
- [Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions](https://mlsanity.com/paper/2206.07811/) (2022)

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

- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty](https://mlsanity.com/paper/2210.05989/) (2022)
- [Shielded Reinforcement Learning for Hybrid Systems](https://mlsanity.com/paper/2308.14424/) (2023)
- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [Neural Model Checking](https://mlsanity.com/paper/2410.23790/) (2024)
- [Neural Continuous-Time Supermartingale Certificates](https://mlsanity.com/paper/2412.17432/) (2024)
- [Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates](https://mlsanity.com/paper/2406.00826/) (2024)
- [Composing Reinforcement Learning Policies, with Formal Guarantees](https://mlsanity.com/paper/2402.13785/) (2024)
- [Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties](https://mlsanity.com/paper/2405.04015/) (2024)
- [Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation](https://mlsanity.com/paper/2511.06341/) (2025)
- [Myopically Verifiable Probabilistic Certificates for Safe Control and Learning](https://mlsanity.com/paper/2404.16883/) (2024)
- [Robustness Verification of Deep Reinforcement Learning Based Control Systems using Reward Martingales](https://mlsanity.com/paper/2312.09695/) (2023)
- [VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change](https://mlsanity.com/paper/2505.14001/) (2025)
- [Automating the Refinement of Reinforcement Learning Specifications](https://mlsanity.com/paper/2512.01047/) (2025)
- [Neural Proofs for Sound Verification and Control of Complex Systems](https://mlsanity.com/paper/2512.18389/) (2025)
- [Formal Synthesis of Certifiably Robust Neural Lyapunov-Barrier Certificates](https://mlsanity.com/paper/2602.05311/) (2026)
- [Value Functions as Supermartingale Certificates](https://mlsanity.com/paper/2605.31524/) (2026)
- [Certificate-Guided Evaluation of Reinforcement Learning Generalization](https://mlsanity.com/paper/2606.00840/) (2026)
- [Physics-informed Reinforcement Learning for Stochastic Reach-Avoid Analysis](https://mlsanity.com/paper/2608.17117/) (2026)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)
- [Runtime Monitoring of Supermartingale Certificates](https://mlsanity.com/paper/2610.19701/) (2026)

## Abstract (arXiv)

We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p∈[0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks.
