Formally Verified Physics-Informed Neural Control Lyapunov Functions

TL;DR

This paper introduces a method for learning and formally verifying neural network control Lyapunov functions using physics-informed data and satisfiability solvers, improving stability analysis of nonlinear systems.

Contribution

It presents a novel approach combining physics-informed learning with formal verification for neural control Lyapunov functions, outperforming existing methods.

Findings

Neural network control Lyapunov functions solve a transformed Hamilton-Jacobi-Bellman equation.

Formal verification of quadratic Lyapunov functions is efficient and effective.

The approach outperforms sum-of-squares and rational Lyapunov functions in numerical tests.

Abstract

Control Lyapunov functions are a central tool in the design and analysis of stabilizing controllers for nonlinear systems. Constructing such functions, however, remains a significant challenge. In this paper, we investigate physics-informed learning and formal verification of neural network control Lyapunov functions. These neural networks solve a transformed Hamilton-Jacobi-Bellman equation, augmented by data generated using Pontryagin's maximum principle. Similar to how Zubov's equation characterizes the domain of attraction for autonomous systems, this equation characterizes the null-controllability set of a controlled system. This principled learning of neural network control Lyapunov functions outperforms alternative approaches, such as sum-of-squares and rational control Lyapunov functions, as demonstrated by numerical examples. As an intermediate step, we also present results on the formal verification of quadratic control Lyapunov functions, which, aided by satisfiability modulo theories solvers, can perform surprisingly well compared to more sophisticated approaches and efficiently produce global certificates of null-controllability.