Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formally Verified Physics-Informed Neural Control Lyapunov Functions

Jun Liu, Maxwell Fitzsimmons, Ruikun Zhou, Yiming Meng

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.

Formally Verified Physics-Informed Neural Control Lyapunov Functions

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.
Paper Structure (17 sections, 2 theorems, 37 equations, 4 figures, 3 algorithms)

This paper contains 17 sections, 2 theorems, 37 equations, 4 figures, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Nonlinear control system
  4. Control Lyapunov function and asymptotic stabilization
  5. Connections with optimal control
  6. Null controllable set and CLF via Zubov's equation
  7. Pontryagin's maximum principle
  8. Physics-informed computation of maximal neural network control Lyapunov functions
  9. Zubov-HJB equation
  10. Physics-informed neural solution to Zubov-HJB equation
  11. Data generation using Pontryagin's maximum principle
  12. Formal verification of control Lyapunov functions
  13. Formal verification of quadratic control Lyapunov functions
  14. Formal verification of neural control Lyapunov functions
  15. Formal verification of near-optimal controller
  16. ...and 2 more sections

Key Result

Proposition 1

Suppose that $f$ is continuously differentiable and $g$ is continuous. Assume that $(A,B)$ is stabilizable and $Q$ is positive definite. There exists some $c>0$ such that $V_P(x)=x^\top Px$, where $P$ is the solution to (eq:are), is a control Lyapunov function for (eq:sys) on an open set containing

Figures (4)

  • Figure 1: (Left) Comparison of the formally verified null-controllable set provided by a quadratic CLF using Algorithm \ref{['alg:qclf']} (dashed red), a rational CLF from doban2015feedback (dashed blue), and a sum-of-squares (SOS) CLF with a sixth-degree polynomial (dashed green). It is observed that the quadratic CLF verified by an SMT solver is already comparable to the rational CLF and outperforms the SOS CLF. (Right) Data obtained by solving the TBPVP (\ref{['eq:tpbvp']}) for (\ref{['eq:reverse_vdp']}) in Example \ref{['ex:vdp']} on the domain $[-4,4]$. Solving is successful for 1,524 out of 3,000 randomly sampled initial conditions.
  • Figure 2: A formally verified neural CLF, obtained by solving the Zubov-HJB (\ref{['eq:zubov_hjb']}) with a neural network of two hidden layers, each with 30 neurons, can significantly outperform alternative approaches. The solid blue line represents the formally verified level set of the neural CLF, while the dashed red line represents that of a quadratic CLF (see left of Figure \ref{['fig:compare_qclf_data']} for comparisons). The phase portrait is for the closed-loop system under Sontag's controller (\ref{['eq:sontag']}) using the learned neural CLF.
  • Figure 3: A comparison of the neural network CLF obtained with PMP data alone and with the physics-informed PDE loss (\ref{['eq:lossV']}). Clearly, the PDE loss significantly enhances extrapolation on larger domains beyond where the data were taken. Top: verified neural CLF trained with PMP data alone. Bottom: verified neural CLF trained with the physics-informed PDE loss (\ref{['eq:lossV']}).
  • Figure 4: A comparison of the accumulated cost of the Sontag controller (\ref{['eq:sontag']}) and the neural HJB controller (\ref{['eq:hjb']}) from the same neural CLF/value function $W_N$. The initial condition is set to be $(-8/3,-8/3)$. It is clear that the HJB controller has a lower accumulated cost, as it is expected to be near optimal by solving the Zubov-HJB equation (\ref{['eq:zubov_hjb']}).

Theorems & Definitions (7)

  • Proposition 1
  • proof
  • Proposition 2
  • proof
  • Example V.1
  • Example V.2
  • Example V.3