# VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 27 of its 45 references that are in the map.
- First posted on arXiv 20 May 2025.

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (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 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)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Compositional Reinforcement Learning from Logical Specifications](https://mlsanity.com/paper/2106.13906/) (2021)
- [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)
- [Learning Dynamics Models with Stable Invariant Sets](https://mlsanity.com/paper/2006.08935/) (2020)
- [Learning Stable Deep Dynamics Models for Partially Observed or Delayed Dynamical Systems](https://mlsanity.com/paper/2110.14296/) (2021)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [Multiple-Environment Markov Decision Processes](https://mlsanity.com/paper/1405.4733/) (2014)
- [Stochastic Omega-Regular Verification and Control with Supermartingales](https://mlsanity.com/paper/2405.17304/) (2024)
- [Scenario-Based Verification of Uncertain Parametric MDPs](https://mlsanity.com/paper/2112.13020/) (2021)
- [When to Trust AI: Advances and Challenges for Certification of Neural Networks](https://mlsanity.com/paper/2309.11196/) (2023)
- [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)
- [Compositional Neural Certificates for Networked Dynamical Systems](https://mlsanity.com/paper/2303.14564/) (2023)
- [Verifiable Reinforcement Learning Systems via Compositionality](https://mlsanity.com/paper/2309.06420/) (2023)
- [Data-driven Interval MDP for Robust Control Synthesis](https://mlsanity.com/paper/2404.08344/) (2024)
- [Safe Learning for Uncertainty-Aware Planning via Interval MDP Abstraction](https://mlsanity.com/paper/2202.01358/) (2022)

## Abstract (arXiv)

Autonomous systems operating in the real world encounter a range of uncertainties. Probabilistic neural Lyapunov certification is a powerful approach to proving safety of nonlinear stochastic dynamical systems. When faced with changes beyond the modeled uncertainties, e.g., unidentified obstacles, probabilistic certificates must be transferred to the new system dynamics. However, even when the changes are localized in a known part of the state space, state-of-the-art requires complete re-certification, which is particularly costly for neural certificates. We introduce VeRecycle, the first framework to formally reclaim guarantees for discrete-time stochastic dynamical systems. VeRecycle efficiently reuses probabilistic certificates when the system dynamics deviate only in a given subset of states. We present a general theoretical justification and algorithmic implementation. Our experimental evaluation shows scenarios where VeRecycle both saves significant computational effort and achieves competitive probabilistic guarantees in compositional neural control.