# Stability Verification in Stochastic Control Systems via Neural Network Supermartingales

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

## Key facts

- Cited by 26 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 58 references that are in the map.
- First posted on arXiv 17 Dec 2021.

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

- [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)
- [Domain Randomization for Transferring Deep Neural Networks from Simulation to the Real World](https://mlsanity.com/paper/1703.06907/) (2017)
- [Safe Model-based Reinforcement Learning with Stability Guarantees](https://mlsanity.com/paper/1705.08551/) (2017)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Safe Exploration in Continuous Action Spaces](https://mlsanity.com/paper/1801.08757/) (2018)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Learning-based Model Predictive Control for Safe Exploration](https://mlsanity.com/paper/1803.08287/) (2018)
- [Learning Stable Deep Dynamics Models](https://mlsanity.com/paper/2001.06116/) (2020)
- [The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems](https://mlsanity.com/paper/1808.00924/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Transferring End-to-End Visuomotor Control from Simulation to Real World for a Multi-Stage Task](https://mlsanity.com/paper/1707.02267/) (2017)
- [Safe Exploration for Interactive Machine Learning](https://mlsanity.com/paper/1910.13726/) (2019)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [Robust Regression for Safe Exploration in Control](https://mlsanity.com/paper/1906.05819/) (2019)
- [Learning Control Lyapunov Functions from Counterexamples and Demonstrations](https://mlsanity.com/paper/1804.05285/) (2018)
- [Almost Surely Stable Deep Dynamics](https://mlsanity.com/paper/2103.14722/) (2021)
- [StocHy: automated verification and synthesis of stochastic processes](https://mlsanity.com/paper/1901.10287/) (2019)
- [Infinite Time Horizon Safety of Bayesian Neural Networks](https://mlsanity.com/paper/2111.03165/) (2021)
- [FAUST2: Formal Abstractions of Uncountable-STate STochastic processes](https://mlsanity.com/paper/1403.3286/) (2014)
- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [Lagrangian Reachtubes: The Next Generation](https://mlsanity.com/paper/2012.07458/) (2020)
- [Termination Analysis of Probabilistic Programs through Positivstellensatz's](https://mlsanity.com/paper/1604.07169/) (2016)
- [AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems](https://mlsanity.com/paper/2005.06191/) (2020)
- [Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs](https://mlsanity.com/paper/1510.08517/) (2015)
- [Stochastic Stability Analysis of Discrete Time System Using Lyapunov Measure](https://mlsanity.com/paper/1503.04438/) (2015)

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

- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [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)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Towards Efficient Verification of Quantized Neural Networks](https://mlsanity.com/paper/2312.12679/) (2023)
- [Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning](https://mlsanity.com/paper/2204.07373/) (2022)
- [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)
- [Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems](https://mlsanity.com/paper/2210.05304/) (2022)
- [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)
- [Neural Control and Certificate Repair via Runtime Monitoring](https://mlsanity.com/paper/2412.12996/) (2024)
- [Deep SPI: Safe Policy Improvement via World Models](https://mlsanity.com/paper/2510.12312/) (2025)
- [Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties](https://mlsanity.com/paper/2405.04015/) (2024)
- [Learning Stabilizing Policies in Stochastic Control Systems](https://mlsanity.com/paper/2205.11991/) (2022)
- [A Policy Optimization Method Towards Optimal-time Stability](https://mlsanity.com/paper/2301.00521/) (2023)
- [Robustness Verification of Deep Reinforcement Learning Based Control Systems using Reward Martingales](https://mlsanity.com/paper/2312.09695/) (2023)
- [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)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)
- [Certifying Almost-Sure Reachability in Unknown MDPs](https://mlsanity.com/paper/2610.18119/) (2026)
- [Runtime Monitoring of Supermartingale Certificates](https://mlsanity.com/paper/2610.19701/) (2026)

## Abstract (arXiv)

We consider the problem of formally verifying almost-sure (a.s.) asymptotic stability in discrete-time nonlinear stochastic control systems. While verifying stability in deterministic control systems is extensively studied in the literature, verifying stability in stochastic control systems is an open problem. The few existing works on this topic either consider only specialized forms of stochasticity or make restrictive assumptions on the system, rendering them inapplicable to learning algorithms with neural network policies. In this work, we present an approach for general nonlinear stochastic control problems with two novel aspects: (a) instead of classical stochastic extensions of Lyapunov functions, we use ranking supermartingales (RSMs) to certify a.s.~asymptotic stability, and (b) we present a method for learning neural network RSMs. We prove that our approach guarantees a.s.~asymptotic stability of the system and provides the first method to obtain bounds on the stabilization time, which stochastic Lyapunov functions do not. Finally, we validate our approach experimentally on a set of nonlinear stochastic reinforcement learning environments with neural network policies.