Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systems

Haoyu Li, Xiangru Zhong, Bin Hu, Huan Zhang

TL;DR

This work develops a Jacobian-free framework for learning and formally verifying contraction metrics for discrete-time nonlinear systems, accommodating non-smooth dynamics induced by neural controllers. A new sufficient condition for contraction relies on a continuous metric $M(x)$ and a bound on $f$-image distances, enabling verification with the scalable $\alpha,\!\beta$-CROWN tool and avoiding Jacobians or matrix inequalities. The authors propose a learning pipeline where $M(x)=\mu I+R(x)^T R(x)$ and train using a violation-based loss with counterexample guidance, progressively enlarging the admissible domain. Experiments on multiple autonomous and NN-controlled systems demonstrate substantially larger verified contraction regions than constant metrics, including the first formal contraction certificate for a NN-controlled discrete-time inverted pendulum, highlighting the method's scalability and practical impact for safe NN-based control.

Abstract

Contraction metrics are crucial in control theory because they provide a powerful framework for analyzing stability, robustness, and convergence of various dynamical systems. However, identifying these metrics for complex nonlinear systems remains an open challenge due to the lack of scalable and effective tools. This paper explores the approach of learning verifiable contraction metrics parametrized as neural networks (NNs) for discrete-time nonlinear dynamical systems. While prior works on formal verification of contraction metrics for general nonlinear systems have focused on convex optimization methods (e.g. linear matrix inequalities, etc) under the assumption of continuously differentiable dynamics, the growing prevalence of NN-based controllers, often utilizing ReLU activations, introduces challenges due to the non-smooth nature of the resulting closed-loop dynamics. To bridge this gap, we establish a new sufficient condition for establishing formal neural contraction metrics for general discrete-time nonlinear systems assuming only the continuity of the dynamics. We show that from a computational perspective, our sufficient condition can be efficiently verified using the state-of-the-art neural network verifier $α,\!β$-CROWN, which scales up non-convex neural network verification via novel integration of symbolic linear bound propagation and branch-and-bound. Built upon our analysis tool, we further develop a learning method for synthesizing neural contraction metrics from sampled data. Finally, our approach is validated through the successful synthesis and verification of NN contraction metrics for various nonlinear examples.

Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systems

TL;DR

This work develops a Jacobian-free framework for learning and formally verifying contraction metrics for discrete-time nonlinear systems, accommodating non-smooth dynamics induced by neural controllers. A new sufficient condition for contraction relies on a continuous metric and a bound on -image distances, enabling verification with the scalable -CROWN tool and avoiding Jacobians or matrix inequalities. The authors propose a learning pipeline where and train using a violation-based loss with counterexample guidance, progressively enlarging the admissible domain. Experiments on multiple autonomous and NN-controlled systems demonstrate substantially larger verified contraction regions than constant metrics, including the first formal contraction certificate for a NN-controlled discrete-time inverted pendulum, highlighting the method's scalability and practical impact for safe NN-based control.

Abstract

Contraction metrics are crucial in control theory because they provide a powerful framework for analyzing stability, robustness, and convergence of various dynamical systems. However, identifying these metrics for complex nonlinear systems remains an open challenge due to the lack of scalable and effective tools. This paper explores the approach of learning verifiable contraction metrics parametrized as neural networks (NNs) for discrete-time nonlinear dynamical systems. While prior works on formal verification of contraction metrics for general nonlinear systems have focused on convex optimization methods (e.g. linear matrix inequalities, etc) under the assumption of continuously differentiable dynamics, the growing prevalence of NN-based controllers, often utilizing ReLU activations, introduces challenges due to the non-smooth nature of the resulting closed-loop dynamics. To bridge this gap, we establish a new sufficient condition for establishing formal neural contraction metrics for general discrete-time nonlinear systems assuming only the continuity of the dynamics. We show that from a computational perspective, our sufficient condition can be efficiently verified using the state-of-the-art neural network verifier -CROWN, which scales up non-convex neural network verification via novel integration of symbolic linear bound propagation and branch-and-bound. Built upon our analysis tool, we further develop a learning method for synthesizing neural contraction metrics from sampled data. Finally, our approach is validated through the successful synthesis and verification of NN contraction metrics for various nonlinear examples.

Paper Structure

This paper contains 14 sections, 6 theorems, 24 equations, 1 figure, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Notations
  4. Contraction Metrics
  5. The $\alpha,\beta$-CROWN Verifier
  6. Contraction for Non-Smooth Dynamics
  7. Methodology
  8. Invariant Set Finding
  9. Formal Verification of Contraction Metrics
  10. Learning Neural Network based Contraction Metrics
  11. Experiments
  12. Nonlinear Autonomous Dynamical System
  13. Non-Smooth Neural Network Controlled System
  14. Conclusion

Key Result

theorem 1

The system eq:system is contracting in $\mathcal{X}$ if there exists a nonsingular matrix-valued function $\Theta: \mathcal{X} \to \mathbb{R}^{n\times n}$ and positive constants $\mu, \eta, \rho$ such that for all $x \in \mathcal{X}$ we have where $F(x)= \Theta(f(x))\frac{\partial f}{\partial x}(x) \Theta^{-1}(x)$.

Figures (1)

  • Figure 1: The figures visualize the certified region of contraction for our neural contraction metrics and the baseline constant metrics. For each $x \in \mathcal{B}$, we simulate the minimum of $G(x,\delta)$ for a small neighborhood of $\delta$. The grey region indicates $G(x,\delta) < 0$, and the white region indicates the converse. In principle, any forward invariant set inside the white region can be certified as contraction. The top rows visualize the behavior of our learned neural contraction metrics, whereas the bottom row visualizes thebaseline of using a constant contraction metric.

Theorems & Definitions (7)

  • definition 1: Contraction
  • theorem 1
  • theorem 2
  • lemma 1
  • theorem 3
  • theorem 4
  • theorem 5