SCORE: Statistical Certification of Regions of Attraction via Extreme Value Theory

TL;DR

SCORE introduces a statistical framework using Extreme Value Theory and stochastic gradient methods to certify regions of attraction in high-dimensional nonlinear systems, overcoming traditional scalability limitations.

Contribution

The paper presents a novel EVT-based probabilistic certification method that scales to 500 dimensions, surpassing existing deterministic approaches in high-dimensional system verification.

Findings

Achieves certification tightness comparable to SOS in 2D benchmarks.

Successfully certifies a 500-dimensional system with 99.99% confidence.

Provides a scalable alternative to traditional formal verification methods.

Abstract

Certifying the Region of Attraction (ROA) for high-dimensional nonlinear dynamical systems remains a severe computational bottleneck. Traditional deterministic verification methods, such as Sum-of-Squares (SOS) programming and Satisfiability Modulo Theories (SMT), provide hard guarantees but suffer from the curse of dimensionality, typically failing to scale beyond 20 dimensions. To overcome these limitations, we propose SCORE, a statistical certification framework that shifts from seeking deterministic guarantees to bounding the worst-case safety violation with high statistical confidence. By integrating Projected Stochastic Gradient Langevin Dynamics (PSGLD) with Extreme Value Theory (EVT), we frame ROA certification as a constrained extreme-value estimation problem on the sublevel set boundary. We theoretically demonstrate that modeling the optimization process as a stochastic diffusion on a compact manifold places the local maxima of the Lyapunov derivative into the Weibull maximum domain of attraction. Since the Weibull domain features a finite right endpoint, we can compute a rigorous statistical upper bound on the global maximum of the Lyapunov derivative. Numerical experiments validate that our EVT-based approach achieves certification tightness competitive to exact SOS programming on a 2D Van der Pol benchmark. Furthermore, we demonstrate unprecedented scalability by successfully certifying a dense, unstructured 500-dimensional ODE system up to a confidence level of 99.99\%, effectively bypassing the severe combinatorial constraints that limit existing formal verification pipelines.