Learning Robust Control Lyapunov Functions through Lipschitz Neural Networks

Technical Summary: Learning Robust Control Lyapunov Functions through Lipschitz Neural Networks

Problem Statement
The paper addresses the challenge of designing stabilizing controllers for nonlinear dynamical systems subject to additive disturbances. While Lyapunov functions are a foundational tool for stability analysis, their automatic construction for general nonlinear systems remains an open problem. Existing computational methods, such as Sum-of-Squares (SOS) or Linear Matrix Inequalities (LMI), often struggle with scalability or generality. Furthermore, recent deep learning approaches that learn Control Lyapunov Functions (CLFs) using neural networks typically focus on exact dynamics without disturbances or rely on verification methods that are computationally expensive and conservative (e.g., using only zeroth-order information). The specific challenge addressed here is learning a Robust Control Lyapunov Function (RCLF) and a corresponding state-feedback controller that guarantees Uniform Ultimate Boundedness (UUB) in the presence of state-dependent additive disturbances, while ensuring the verification of these conditions is computationally tractable.

Methodology
The proposed framework integrates Lipschitz Neural Networks (LNNs) with a high-order Branch-and-Bound (BnB) verification algorithm.

1. Lipschitz Neural Networks (LNNs):
   The authors employ LNNs to jointly learn the RCLF ($V_{\theta_1}$) and the stabilizing controller ($\pi_{\theta_2}$). Unlike standard networks, LNNs enforce a predefined Lipschitz constant through specific layer parameterizations (e.g., Spectral Normalization, Orthogonal Layers, or Sandwich Layers). This constraint is critical because it allows for the derivation of explicit, tight bounds on higher-order derivatives (Hessian and third-order derivatives) of the network output with respect to its input. The RCLF is defined as a shifted network output to ensure the equilibrium condition $V(0)=0$.

2. Training Algorithm:
   The training process minimizes a composite loss function over a sampled state space and boundary. The loss terms enforce:

   • Positive Definiteness: Ensuring $V(x) > 0$ for $x \neq 0$.
   • Decrease Condition: Ensuring the time derivative $\dot{V}$ is negative outside a small ball around the origin, accounting for the worst-case disturbance. This involves upper-bounding the disturbance term using the known disturbance bound function $\epsilon(x)$ and the Lipschitz constants of the network and system dynamics.
   • Boundary and Coverage: Encouraging the sublevel set of $V$ to cover a maximal portion of the state space and maintain a consistent value on the boundary.
     The algorithm initializes parameters using Linear Quadratic Regulator (LQR) solutions and iteratively refines them, storing the parameters that yield the largest empirically verified forward-invariant region.

3. High-Order Verification (Branch-and-Bound):
   A novel GPU-friendly BnB algorithm is introduced to formally verify the learned RCLF. Unlike traditional solvers (e.g., dReal) that rely on zeroth-order bounds or SMT solvers that face scalability limits, this method leverages the smoothness of the LNNs.

   • Higher-Order Bounds: The authors derive explicit spectral norm bounds for the Hessian and third-order derivatives of LNNs. These bounds are used to construct tight lower and upper bounds on the network output via Taylor expansions (up to second-order).
   • Algorithm Efficiency: By incorporating first- and second-order information, the algorithm creates significantly tighter enclosures of the function values within search rectangles. This allows for more aggressive pruning of the search space compared to zeroth-order methods.
   • Complexity: The paper establishes worst-case time complexity bounds, showing that the number of evaluated rectangles scales polynomially with the system dimension and inversely with the tolerance, but is drastically reduced in practice by the tighter bounds.

Key Contributions

1. Novel Framework: A unified approach to learning robust CLFs and stabilizing controllers for nonlinear systems with additive, state-dependent disturbances using LNNs.
2. Derivative Bounds: The establishment of explicit spectral norm bounds for the Hessian and third-order derivatives of LNNs. These bounds are tighter than those derived from zeroth- or first-order information alone, addressing the non-convexity of Lyapunov verification.
3. GPU-Friendly Verification: The development of a BnB algorithm that utilizes these higher-order bounds and supports batch evaluation on GPUs. This significantly accelerates the verification process compared to CPU-based SMT solvers.
4. Empirical Validation: Extensive simulations on six dynamical systems (inverted pendulum, unicycle, third-order system, cartpole, 2D quadrotor, and SCARA arm) demonstrating the method's ability to verify stability and outperform existing tools (dReal, $\alpha,\beta$-CROWN) in terms of speed and scalability.

Results
The paper presents simulation results comparing the proposed method against dReal (CPU-based SMT) and $\alpha,\beta$-CROWN (GPU-based bound propagation).

• Verification Speed: The proposed GPU-based BnB algorithm consistently outperforms dReal, often reducing verification time from hours (or timeouts) to seconds, even for systems with higher state dimensions (e.g., SCARA arm with $n_x=8$).
• Scalability: While dReal fails to verify systems with more than 2-3 layers within a reasonable time, the proposed method successfully verifies networks with up to 4 layers.
• Forward Invariant Regions: The learned controllers achieve significantly larger forward-invariant regions compared to standard LQR and non-robust neural CLF (NLC) approaches. For the inverted pendulum, the proposed method achieved a forward-invariant region ratio of ~75%, compared to ~23% for LQR.
• Robustness: The verification confirms that the learned controllers satisfy the UUB condition, keeping trajectories within a bounded region despite the presence of disturbances.

Significance and Claims
The paper claims that its primary significance lies in bridging the gap between the expressivity of deep learning and the rigorous requirements of robust control verification. By leveraging the specific structure of Lipschitz networks to derive higher-order derivative bounds, the authors enable a verification process that is both mathematically rigorous and computationally efficient.

The authors explicitly state that their framework does not certify stability for an unknown model without a known error bound; rather, it provides a deterministic guarantee of robustness against a certified model mismatch or bounded disturbance. The work highlights that while LNNs may have reduced expressivity compared to unconstrained networks, the trade-off is justified by the ability to perform efficient, high-order verification, which is essential for safety-critical control applications. The paper concludes that this approach makes the formal verification of robust, learned controllers for complex nonlinear systems practically feasible.