Learning Certified Neural Network Controllers Using Contraction and Interval Analysis
This work addresses the challenge of ensuring stability and safety in neural network-based control systems, particularly for robotics applications, though it is incremental in improving upon existing Lipschitz-based methods.
The authors tackled the problem of certifying neural network controllers with rigorous closed-loop contraction guarantees by developing a framework that jointly trains a controller and a neural Riemannian metric using formal bound propagation, achieving verified contraction regions for a 10-state quadrotor model in under 10 minutes of training.
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 $Ï$, a neural contraction metric $Î$, and a verified 10-dimensional contraction region $X$.