Neural Continuous-Time Supermartingale Certificates
Grigory Neustroev, Mirco Giacobbe, Anna Lukina
Abstract
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.
BibTeX
@article{Neustroev_Giacobbe_Lukina_2025, title={Neural Continuous-Time Supermartingale Certificates}, volume={39}, url={https://ojs.aaai.org/index.php/AAAI/article/view/34966}, DOI={10.1609/aaai.v39i26.34966}, abstractNote={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.}, number={26}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Neustroev, Grigory and Giacobbe, Mirco and Lukina, Anna}, year={2025}, month={Apr.}, pages={27538-27546} }