Compositional Lyapunov Certification of Regions of Attraction
for Lossy Power Grids

A non-integrable vector cross term, an independent sum-of-squares cross-check, and a radius/shape decomposition of certified coverage.
Sehaj Randhir Singh
Independent researcher; partial affiliation with NYU Tandon School of Engineering
Nature Machine Intelligence format IEEE Transactions format GitHub (code + data)
Certifying the region of attraction (ROA) of a large, lossy power grid with a monolithic Lyapunov function requires branch-and-bound (BaB) verification whose cost is exponential in state dimension. We present a compositional certificate, evaluated on the IEEE New England 39-bus test system Kron-reduced to its ten generator buses, that collapses an 18-D relative phase space to a 9-D, angle-only verification problem via closed-form elimination of the speed variables, making sound BaB tractable on a ten-generator benchmark at all. We give a mechanistic diagnosis of why a scalar Lyapunov correction cannot compensate for lossy (non-conservative) line coupling — its required correction field is measured to be ≈98% rotational, hence has no scalar potential — and show that moving the correction into a learned, non-integrable vector cross term resolves the obstruction, reaching 24.8% certified coverage of the true ROA at 100% soundness, within 0.5 points of that certificate family's own zero-relaxation ceiling. We cross-validate the entire pipeline with an independently implemented, exact sum-of-squares (Positivstellensatz) certificate, which ties the interval-BaB result on all three evaluation slices individually — to our knowledge the first exact, non-interval-relaxed cross-check in this line of work. Finally, we show certified coverage decomposes into two independent sub-problems — how far stability can be proved (radius) and how well the proved region's geometry matches the true boundary (shape) — and that a single convex quadratic program recovers a sound 86% relative coverage gain on the shape sub-problem alone, invisible to six independent gradient-based searches that optimized both sub-problems jointly. Both mechanisms transfer to a second, independently constructed benchmark topology (the IEEE/WSCC 9-bus system). We report this decomposition, together with eight independently designed negative results, as the paper's central structural contribution.

Why this matters

Neural Lyapunov certification of multi-machine power grids has been stuck near a small handful of generators because sound branch-and-bound verification is exponential in state dimension. This work shows the exponential wall is a composition problem, not a fundamental verification limit: splitting the grid into per-generator subsystems and composing local certificates with a single linear-algebra coupling test turns exponential cost into low-order polynomial cost — while the thing that actually caps how much of the true region gets certified is a specific, diagnosable obstruction (lossy coupling has no scalar potential), not the compositional machinery itself.

Log-scale plot of monolithic versus compositional branch-and-bound leaf-box count from 2-D to 20-D state dimension.
Exponential to polynomial

Monolithic BaB explores 1.15×10¹⁵ leaf boxes at the full 20-D (10-generator) system; the compositional certificate explores 1,640 — a measured 7.0×10¹⁴× reduction, with sound decentralized composition throughout.

Bar chart comparing physics-only and learned-cross-term BaB-proved coverage on the IEEE 39-bus and IEEE/WSCC 9-bus systems.
The mechanism transfers

The same learned vector cross term, trained once and reused unchanged, improves coverage on a second, independently-built topology (IEEE/WSCC 9-bus, 3 machines) by +38% relative — a larger gain than on the original 39-bus system.

Bar chart comparing classical transient-energy-function shape coverage against a convex QP shape fit, at the same proved radius, on three angle slices.
Radius and shape are separate questions

At the exact same already-proven radius, a single convex QP shape fit recovers +86% relative coverage over the classical TEF sublevel-set shape — a gain six independent gradient-based searches never found, because they optimized radius and shape jointly.

Headline result: physics baseline vs. learned cross term

100% soundness on every slice reported (0 certified-unstable points), dense Monte Carlo ground truth.

SystemGeneratorsPhysics-only coverageLearned coverageRelative gain
IEEE New England 39-bus10 (Kron-reduced)23.2%24.8%+7%
IEEE/WSCC 9-bus3 (independent topology)23.4%32.3%+38%

Independent cross-check: interval BaB vs. exact sum-of-squares

SOS certificate implemented independently from the interval-BaB verifier, run on the same polynomial.

VerifierMean coverage (3 slices)Contradictions
Interval branch-and-bound22.0%—
Exact sum-of-squares (Positivstellensatz)22.0%0
The two independently implemented verifiers tie on all three evaluation slices individually (e.g. 93.8° vs. 93.6° proved radius on one slice) — the first exact, non-interval-relaxed cross-check reported in this line of work.

Side exploration: how far does a genuinely different verifier scale?

Independently of the compositional/BaB line above, we tested whether CROWN-based certified training — a linear-relaxation bound-propagation verifier, fundamentally different from interval BaB — could hold a fixed local Lyapunov certificate as the number of generators included in a joint slice grows, reusing an existing, previously-validated CROWN pipeline unchanged. This is a different question from the coverage numbers above (a local certified box radius in normalized coordinates, not a fraction of the true ROA), reported here for completeness and honesty about what did and did not scale.

Slice dimensionGeneratorsCertified ρ (headline)Independent cross-check ρ
4-D22.5—
6-D32.51.0 (partial gap)
8-D42.52.5 (full agreement)
10-D52.0 (dropped)1.5
Single seed at each rung. The full-ceiling certificate holds cleanly through 8-D with the two verifiers in exact agreement, then degrades at 10-D — not from a training failure but from the input-space BaB verifier timing out at the full box, a bottleneck that would need activation-splitting α,β-CROWN to push further, not more training.

What did not work

Six independently designed architecture searches on the radius sub-problem — scalar residuals, alternative parameterizations, global fields, joint shape+radius training among them — all converged on the same 93–106° ceiling for this certificate family, regardless of verifier (interval BaB, SOS, adversarial search, or a zero-relaxation oracle). A margin-floor training run that pushed structural LMI margins toward 100% of the physics baseline did not cost coverage as expected; it mildly improved it. The trained field is robust to a ±15% loading perturbation on two of three evaluation slices and collapses to 0° on the third — reported as a genuine mixed result, not smoothed into a single robustness claim. None of this is hidden in the writeup: eight independently designed negative results are reported in full as part of the paper's central contribution, not filtered out.