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

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.

Figures (2)

• Figure 3: Graphical overview of the SCORE certification pipeline. The optimization process begins with the PSGLD sampling of $\dot{V}(x)$ maxima across the constraint manifold. Driven by the projected quadratic geometry near these peaks, the local optimality gap is distributed as a reverse $\chi^2$. From the resulting list of sampled $\dot{V}(x)$, the algorithm divides the samples into $N$ blocks to extract the block maxima. Because the underlying manifold is compact and enforces a finite upper bound, these extreme values are distributed as a Weibull distribution. Finally, the maximum $\dot{V}(x)$ is estimated via a bootstrapping procedure that fits multiple Weibull distributions to resampled subsets of the block maxima, computing a strict upper confidence interval to bound the worst-case violation and certify the ROA.
• Figure 4: Certified Regions of Attraction for the 2D Van der Pol oscillator. Because our primary contribution is the scalable certification engine rather than Lyapunov synthesis, we evaluate EVT on two distinct candidates. While our proposed pipeline (EVT + Dict-Gram) yields a conservative ROA due to the simple dictionary-based synthesis, applying our EVT certification to an SOS-synthesized candidate (solid dark blue) achieves an ROA comparable to exact SOS formal verification (dotted blue). This isolates the conservatism strictly to the synthesis step and demonstrates the tightness of our statistical bound. The parameter $\kappa$ denotes the percentage of the true ROA successfully certified.

Theorems & Definitions (10)

• Remark 1: Local Morse-Type Quadratic Geometry
• Lemma 1: Local Gibbs Law
• proof
• Proposition 1: Local Optimality-Gap Law
• proof
• Theorem 1: Weibull Maximum Domain of Attraction
• proof
• Corollary 1: Finite Endpoint and Statistical Certification
• proof
• Remark 2: Finite Support and Verifiability