Learning Lyapunov Functions for Power System Transient Stability: Neural Verification and Retraining

Transient stability is fundamental to maintaining reliable power-system operation following large disturbances, and its importance becomes increasingly pronounced as renewable generation displaces conventional synchronous generation and re duces system inertia. A common approach to certifying transient stability is through Lyapunov functions, but constructing a function that satisfies the required Lyapunov conditions is challenging. Neural networks have recently emerged as a powerful tool for parameterizing and learning Lyapunov functions due to their expressive capability. Nevertheless, verifying that a learned neural Lyapunov function satisfies the required Lyapunov conditions throughout a continuous region remains difficult. In particular, validation on finitely sampled states cannot provide the universal guar antees required for formal certification. This work revisits a Lyapunov-regularized learning framework for the lossy, Kron-reduced swing equations used to study power-system transient stability. We integrate CROWN (a neural network verifier that computes certified output bounds) into Lyapunov learning, both to expose violations missed by sample-based validation and to guide training toward enlarging the certified region. Case studies show that the proposed framework detects genuine violations that remain undetected even with 200,000 uniformly sampled states and substantially enlarges the region over which the Lyapunov conditions can be formally certified.