# Neural Continuous-Time Supermartingale Certificates

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 46 references that are in the map.
- First posted on arXiv 23 Dec 2024.

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

- [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)
- [Scalable Gradients for Stochastic Differential Equations](https://mlsanity.com/paper/2001.01328/) (2020)
- [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)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Learning Stable Deep Dynamics Models](https://mlsanity.com/paper/2001.06116/) (2020)
- [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021)
- [The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systems](https://mlsanity.com/paper/1808.00924/) (2018)
- [Learning Certified Control using Contraction Metric](https://mlsanity.com/paper/2011.12569/) (2020)
- [Second-Order Provable Defenses against Adversarial Attacks](https://mlsanity.com/paper/2006.00731/) (2020)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [Learning Dynamics Models with Stable Invariant Sets](https://mlsanity.com/paper/2006.08935/) (2020)
- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)

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

- [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (2025)
- [PaperFit: Vision-in-the-Loop Typesetting Optimization for Scientific Documents](https://mlsanity.com/paper/2605.10341/) (2026)
- [VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change](https://mlsanity.com/paper/2505.14001/) (2025)
- [BarrierBench: Evaluating Large Language Models for Safety Verification in Dynamical Systems](https://mlsanity.com/paper/2511.09363/) (2025)
- [Runtime Monitoring of Supermartingale Certificates](https://mlsanity.com/paper/2610.19701/) (2026)

## Abstract (arXiv)

We introduce for the first time a neural-certificate framework for continuous-time stochastic dynamical systems. Autonomous learning systems in the physical world demand continuous-time reasoning, yet existing learnable certificates for probabilistic verification assume discretization of the time continuum. Inspired by the success of training neural Lyapunov certificates for deterministic continuous-time systems and neural supermartingale certificates for stochastic discrete-time systems, we propose a framework that bridges the gap between continuous-time and probabilistic neural certification for dynamical systems under complex requirements. Our method combines machine learning and symbolic reasoning to produce formally certified bounds on the probabilities that a nonlinear system satisfies specifications of reachability, avoidance, and persistence. We present both the theoretical justification and the algorithmic implementation of our framework and showcase its efficacy on popular benchmarks.