Towards Learning and Verifying Maximal Neural Lyapunov Functions

TL;DR

This paper introduces a physics-informed neural network method to learn nearly maximal Lyapunov functions for nonlinear system stability analysis, with verifiable conditions and theoretical guarantees.

Contribution

It proposes a novel PINN-based approach to approximate maximal Lyapunov functions and verifies stability conditions using SMT solvers, advancing nonlinear system analysis.

Findings

Successfully learned nearly maximal Lyapunov functions in numerical examples.

Provided theoretical guarantees for the existence of maximal Lyapunov functions.

Verified stability conditions with SMT solvers for both local and global stability.

Abstract

The search for Lyapunov functions is a crucial task in the analysis of nonlinear systems. In this paper, we present a physics-informed neural network (PINN) approach to learning a Lyapunov function that is nearly maximal for a given stable set. A Lyapunov function is considered nearly maximal if its sub-level sets can be made arbitrarily close to the boundary of the domain of attraction. We use Zubov's equation to train a maximal Lyapunov function defined on the domain of attraction. Additionally, we propose conditions that can be readily verified by satisfiability modulo theories (SMT) solvers for both local and global stability. We provide theoretical guarantees on the existence of maximal Lyapunov functions and demonstrate the effectiveness of our computational approach through numerical examples.