Learning Certified Neural Network Controllers Using Contraction and Interval Analysis

TL;DR

This paper introduces a framework for training neural network controllers with formal guarantees of contraction and stability, leveraging interval analysis and parallelized corner checks to improve efficiency and robustness.

Contribution

It proposes a novel method that jointly trains controllers and Riemannian metrics with formal contraction guarantees, reducing conservativeness and sample complexity.

Findings

Successfully applied to a 10-state quadrotor model

Learns control policy, contraction metric, and region in under 10 minutes

Provides exponential stabilization guarantees for trajectories

Abstract

We present a novel framework that jointly trains a neural network controller and a neural Riemannian metric with rigorous closed-loop contraction guarantees using formal bound propagation. Directly bounding the symmetric Riemannian contraction linear matrix inequality causes unnecessary overconservativeness due to poor dependency management. Instead, we analyze an asymmetric matrix function $G$, where $2^n$ GPU-parallelized corner checks of its interval hull verify that an entire interval subset $X$ is a contraction region in a single shot. This eliminates the sample complexity problems encountered with previous Lipschitz-based guarantees. Additionally, for control-affine systems under a Killing field assumption, our method produces an explicit tracking controller capable of exponentially stabilizing any dynamically feasible trajectory using just two forward inferences of the learned policy. Using JAX and $\texttt{immrax}$ for linear bound propagation, we apply this approach to a full 10-state quadrotor model. In under 10 minutes of post-JIT training, we simultaneously learn a control policy $\pi$, a neural contraction metric $\Theta$, and a verified 10-dimensional contraction region $X$.