This work introduces HyParLyVe (Hyperplane Partitioned Lyapunov Verifier), a novel algorithm for sound and complete verification of neural Lyapunov candidates by interpreting shallow ReLU networks as hyperplane arrangements. This perspective reduces positive definiteness verification to a finite set of vertex evaluations, and the decrease condition to a bounded optimization problem over each region. We formally prove correctness of the proposed verification procedures and demonstrate that HyParLyVe achieves significant speedups over state-of-the-art methods.
Cite
@article{arxiv.2605.03992,
title = {HyParLyVe: Hyperplane Partitioning for Neural Lyapunov Verification},
author = {Jesse Wayment and Brian Yarbrough and Jingbo Wang and Shreyas Sundaram and Philip E. Paré},
journal= {arXiv preprint arXiv:2605.03992},
year = {2026}
}