HyParLyVe: Hyperplane Partitioning for Neural Lyapunov Verification

TL;DR

HyParLyVe is a novel verification algorithm for neural Lyapunov functions that uses hyperplane partitioning to achieve sound, complete, and faster verification compared to existing methods.

Contribution

It introduces a hyperplane partitioning approach for neural Lyapunov verification, providing formal correctness and improved efficiency.

Findings

Achieves significant speedups over state-of-the-art methods.

Provides sound and complete verification of neural Lyapunov candidates.

Reduces positive definiteness verification to finite vertex evaluations.

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.