# Verifying Probabilistic Regions of Attraction with Neural Lyapunov Functions for Stochastic Systems

## TL;DR

This paper introduces a neural network-based method to accurately estimate the largest probabilistic regions of attraction in stochastic systems, combining physics-informed learning with formal verification techniques.

## Contribution

It develops a neural Lyapunov function approach using a stochastic Zubov's equation and SMT verification, improving over traditional methods in estimating probabilistic ROA.

## Key findings

- More accurate probabilistic ROA estimates than SOS methods
- Effective neural Lyapunov functions for stochastic stability
- Validated on nonlinear stochastic systems

## Abstract

Leveraging a stochastic extension of Zubov's equation, we develop a physics-informed neural network (PINN) approach for learning a neural Lyapunov function that captures the largest probabilistic region of attraction (ROA) for stochastic systems. We then provide sufficient conditions for the learned neural Lyapunov functions that can be readily verified by satisfiability modulo theories (SMT) solvers, enabling formal verification of both local stability analysis and probabilistic ROA estimates. By solving Zubov's equation for the maximal Lyapunov function, our method provides more accurate and larger probabilistic ROA estimates than traditional sum-of-squares (SOS) methods. Numerical experiments on nonlinear stochastic systems validate the effectiveness of our approach in training and verifying neural Lyapunov functions for probabilistic stability analysis and ROA estimates.