# Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees

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

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- Builds on 43 of its 69 references that are in the map.
- First posted on arXiv 3 Dec 2023.

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

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [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)
- [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)
- [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)
- [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)
- [Learning-based Model Predictive Control for Safe Exploration](https://mlsanity.com/paper/1803.08287/) (2018)
- [Reinforcement Learning With Temporal Logic Rewards](https://mlsanity.com/paper/1612.03471/) (2016)
- [The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems](https://mlsanity.com/paper/1808.00924/) (2018)
- [Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees](https://mlsanity.com/paper/1909.05304/) (2019)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning](https://mlsanity.com/paper/1909.07299/) (2019)
- [LTL2Action: Generalizing LTL Instructions for Multi-Task RL](https://mlsanity.com/paper/2102.06858/) (2021)
- [A Composable Specification Language for Reinforcement Learning Tasks](https://mlsanity.com/paper/2008.09293/) (2020)
- [Saute RL: Almost Surely Safe Reinforcement Learning Using State Augmentation](https://mlsanity.com/paper/2202.06558/) (2022)
- [Compositional Reinforcement Learning from Logical Specifications](https://mlsanity.com/paper/2106.13906/) (2021)
- [Safe Multi-Agent Reinforcement Learning via Shielding](https://mlsanity.com/paper/2101.11196/) (2021)
- [Enforcing Hard Constraints with Soft Barriers: Safe Reinforcement Learning in Unknown Stochastic Environments](https://mlsanity.com/paper/2209.15090/) (2022)
- [Safe Exploration for Interactive Machine Learning](https://mlsanity.com/paper/1910.13726/) (2019)
- [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)
- [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)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)

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

- [From Frege to chatGPT: Compositionality in language, cognition, and deep neural networks](https://mlsanity.com/paper/2405.15164/) (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)
- [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)
- [Stochastic Minimum-Cost Reach-Avoid Reinforcement Learning](https://mlsanity.com/paper/2605.11975/) (2026)
- [Value Functions as Supermartingale Certificates](https://mlsanity.com/paper/2605.31524/) (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)

Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph's sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.