On the Cost of Certifying Neural Lyapunov Functions

A neural Lyapunov function certifies stability only where it is formally verified, and branch-and-bound verification can dominate the cost of current pipelines, varying by orders of magnitude between certificates of the same system. We show that this cost has two parts, both governed by the certified radius: the size of the largest box around a point that the verifier's bounding method can certify. The frontier part is geometric. Where the maximal level set touches the set on which the specification fails, the radius collapses: any verifier that checks the clauses separately on axis-aligned boxes needs $\Omega ({\delta }^{-(n-1-k)/2})$ boxes at slack $\delta$, whatever its bounding method, with $n$ the dimension and $k$ the number of faces or kinks at the contact (for a nondegenerate contact and $V$ not flat along any coordinate). The bulk part, paid everywhere, scales with the integral of the inverse $n$-th power of the radius, which a few thousand sampled points estimate without running branch-and-bound. On 25 certificates in two to six dimensions, the predicted exponents match at 22 contacts, and the estimate stays within a single-digit factor of the measured per-clause cost across five orders of magnitude. The decomposition turns the choice of the certified level into a computation, enlarging the certified region of a released quadrotor certificate $1.8$-fold, and shows that certified training moves the frontier but not consistently the bulk.