HyParLyVe: Hyperplane Partitioning for Neural Lyapunov Verification

Abstract

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.