Neural Continuous-Time Supermartingale Certificates
This work addresses the need for continuous-time reasoning in autonomous learning systems, bridging a gap between existing discrete-time methods and deterministic continuous-time approaches.
The authors tackled the problem of probabilistic verification for continuous-time stochastic dynamical systems by introducing a neural-certificate framework that combines machine learning and symbolic reasoning to produce formally certified bounds on probabilities for reachability, avoidance, and persistence specifications, demonstrating efficacy on benchmarks.
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.