Abstract
Control Lyapunov functions are a central tool in the design and analysis ofstabilizing controllers for nonlinear systems. Constructing such functions,however, remains a significant challenge. In this paper, we investigatephysics-informed learning and formal verification of neural network controlLyapunov functions. These neural networks solve a transformedHamilton-Jacobi-Bellman equation, augmented by data generated usingPontryagin's maximum principle. Similar to how Zubov's equation characterizesthe domain of attraction for autonomous systems, this equation characterizesthe null-controllability set of a controlled system. This principled learningof neural network control Lyapunov functions outperforms alternativeapproaches, such as sum-of-squares and rational control Lyapunov functions, asdemonstrated by numerical examples. As an intermediate step, we also presentresults on the formal verification of quadratic control Lyapunov functions,which, aided by satisfiability modulo theories solvers, can performsurprisingly well compared to more sophisticated approaches and efficientlyproduce global certificates of null-controllability.