Retrain the network to be verifiable by construction. On the same swing model, the same seeds, and the same verifier, the certified region grows on every seed, and the state dimension becomes a single config knob.
[Code] [Prior CEGIS result] [Shi et al. (CT-BaB)] [Cui & Zhang]
A neural Lyapunov function trained against sampled violations can pass on 99.98% of samples and still fail a verifier, because a certificate quantifies over an entire region while sampling only visits a measure-zero subset. The prior work closed that gap with CEGIS, repairing the trained network against the finite counterexamples the verifier returns. Certified training takes the same starting network and instead makes the CROWN certified margin over a whole region a differentiable term in the loss, following Shi, Li, Hsieh, and Zhang (arXiv:2411.18235), so the network is shaped to be verifiable while it trains rather than patched afterward. Warm-started from the exact same weights CEGIS started from, and measured by the exact same audited branch-and-bound verifier, it certifies the Lie-derivative condition on Cui and Zhang's gen-5 slice out to the ρ = 2.5 measurement ceiling on all five seeds, where CEGIS averaged 1.8, at the same Proposition-2 rate β = 3.97, with an independent JacobianOP verifier agreeing and zero soundness contradictions. The whole pipeline is dimension-agnostic, so the projected slice grows from 2-D toward the full 20-D state by changing one config line, and this run holds at the 2-D gate on purpose.
Certified radius ρ for the Lie-derivative condition (4b) on the gen-5 slice, per seed. Both bars come from the identical certify_box branch-and-bound, at ε = 0, audited by an independent projected-gradient attack. Higher is a larger certified region.
Dashed lines mark the ρ = 2.5 grid ceiling (the trained box side, which certified training reaches on every seed) and the CEGIS five-seed mean of 1.8. Because 2.5 is the ceiling, the true certified radius may be larger; per seed the certified box area (ρ²) is 1.6× to 2.8× that of CEGIS.
| Seed | 0 | 1 | 2 | 3 | 4 | mean |
|---|---|---|---|---|---|---|
| CEGIS ρ | 2.0 | 2.0 | 1.5 | 1.5 | 2.0 | 1.8 ± 0.24 |
| Certified training ρ | 2.5 | 2.5 | 2.5 | 2.5 | 2.5 | 2.5 |
This is a controlled comparison, and the control is enforced in code, not by convention. Certified training warm-starts from the exact lyap_seed{k}.pt checkpoint CEGIS started from and refines those weights, and a missing checkpoint raises rather than quietly initializing a fresh network, so the training method is the only thing that changes between the two columns below. The headline ρ and β are read out of the same audited certify_box the CEGIS result used, never the coarser training-time branch-and-bound, which is logged only as a diagnostic. The soundness cross-check against auto_LiRPA's JacobianOP path, the route the brief named, holds for the certified-trained network exactly as it did for the CEGIS one.
| CEGIS (prior) | Certified training (this work) | |
|---|---|---|
| Certified ρ, gen-5 slice (4b) | 1.8 ± 0.24 | 2.5 on all five seeds |
| Proposition-2 rate β | 3.97 | 3.97 |
| Starting network | as-trained lyap_seed{k}.pt | same weights, warm-started and refined |
| How V is made verifiable | repaired on counterexamples, after the fact | shaped by the CROWN bound, during training |
| Region measured by | certify_box + PGD audit | identical certify_box + PGD audit |
| JacobianOP cross-check | 0 contradictions | 0 contradictions |
The certified margin becomes the loss. For a region B the verifier returns a CROWN lower bound on the Lyapunov condition F, and every relaxation and propagation step that produces that bound is differentiable in the network's weights. So the bound flows gradients back to V, and training descends on the hinge that pushes the certified margin above zero over the whole region, not just at sampled points. A feasibility probe confirmed this end to end on CPU before any training code was written: the CROWN margin was differentiable to the first-layer weights with a gradient norm of 7.09 and every entry nonzero.
Training-time branch-and-bound. A dynamic set of subregions tiles the target box, all bounded in one batched call, and after every few steps only the hard subregions, the ones whose certified bound is still negative, are split along the coordinate that most raises the children's bound. Effort concentrates on the hard pieces, which is what keeps the loop tractable, and it is the same mechanism that is meant to survive into higher dimensions where post-hoc repair does not.
Soundness is unchanged. This procedure only produces V. The certificate still comes from the standalone verifier, audited by an independent attack and cross-checked against the JacobianOP path, so a number printed during training is a diagnostic and never a certificate.
The whole notion of which coordinates vary and which stay pinned at equilibrium lives in one object, a SliceSpec, built programmatically from the slice dimension with no literal 2 anywhere in it. Raising the dimension is a single line in the config, the list of active generator buses, and the box, the initial branch-and-bound grid, the sampler, and the embedding maps all follow. This run holds at the 2-D gate on purpose: nothing above 2-D was executed, and the driver refuses any slice above 2-D so the gate is enforced, not just intended.
| active_buses | slice_dim | status |
|---|---|---|
| [5] | 2-D | certified ρ = 2.5 (this work) |
| [5, 9] | 4-D | one config line away, not run |
| [1, 5, 9] | 6-D | one config line away, not run |
| [1, 2, …, 10] | 20-D | the full state, the horizon |
Verified programmatically: the same code maps [5] to a 2-D slice, [5, 9] to 4-D, and [1, 5, 9] to 6-D, with the correct raw-state coordinates in each case. Branch-and-bound cost grows with dimension, which is the whole reason certified training exists, and the climb past 2-D is the next session's work.
The ρ = 2.5 figure is the grid ceiling, equal to the trained box side, so on every seed certified training certifies the entire measured region and the true radius may be larger; measuring past 2.5 needs a larger trained box and is left for the climb. The β = 3.97 parity is expected, since β is limited by the verifier on this annulus rather than by the training method. The gen-5 slice is a 2-D projection with the other buses fixed at equilibrium, not the full state, and scalability here is architectural, one config knob plus the self-test, not yet a higher-dimensional certificate. The dReal SMT encoding is built and ready for the certified-trained network but its runtime is unavailable on the current host, so the independent JacobianOP verifier carries the soundness cross-check. Everything is simulation on the Kron-reduced lossy swing model, with no hardware.
git clone https://github.com/sehajr-singhs/certified-training-lyapunov
export KMP_DUPLICATE_LIB_OK=TRUE # Anaconda + torch OpenMP workaround
make certtrain # certified training, all 5 seeds, the CEGIS head-to-head
# writes results/e7_seed{k}.json with slice_dim as a field
# raise the dimension in configs/certified_train.yaml:
# active_buses: [5] -> 2-D (this result)
# active_buses: [5, 9] -> 4-D, one line, no code change
Every number here traces to a per-seed JSON a script wrote, on CPU (Python 3.13, torch 2.11, auto_LiRPA 0.7.2). See NOTES.md and SCALING.md in the repo.