Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying Closed-Loop Contractivity of Learning-Based Controllers via Partitioning

Alexander Davydov

TL;DR

The paper addresses the challenge of certifying closed-loop contraction for nonlinear systems with neural network controllers and neural contraction metrics. It introduces a scalable sufficient condition based on a Metzler majorant that reduces the infinite-dimensional contraction inequality to a dominant-eigenvalue check, and combines interval bound propagation with domain partitioning to produce verifiable certificates that can be integrated into training. The main contributions are the Metzler-majorant verification framework, IBP-based bounds for NN Jacobians, and an adaptive domain-partitioned training algorithm demonstrated on an inverted pendulum. This approach enables scalable, certifiable contraction guarantees for learning-based controllers in nonlinear settings, with potential applicability to larger-scale systems and non-Euclidean metrics in future work.

Abstract

We address the problem of verifying closed-loop contraction in nonlinear control systems whose controller and contraction metric are both parameterized by neural networks. By leveraging interval analysis and interval bound propagation, we derive a tractable and scalable sufficient condition for closed-loop contractivity that reduces to checking that the dominant eigenvalue of a symmetric Metzler matrix is nonpositive. We combine this sufficient condition with a domain partitioning strategy to integrate this sufficient condition into training. The proposed approach is validated on an inverted pendulum system, demonstrating the ability to learn neural network controllers and contraction metrics that provably satisfy the contraction condition.

Verifying Closed-Loop Contractivity of Learning-Based Controllers via Partitioning

TL;DR

The paper addresses the challenge of certifying closed-loop contraction for nonlinear systems with neural network controllers and neural contraction metrics. It introduces a scalable sufficient condition based on a Metzler majorant that reduces the infinite-dimensional contraction inequality to a dominant-eigenvalue check, and combines interval bound propagation with domain partitioning to produce verifiable certificates that can be integrated into training. The main contributions are the Metzler-majorant verification framework, IBP-based bounds for NN Jacobians, and an adaptive domain-partitioned training algorithm demonstrated on an inverted pendulum. This approach enables scalable, certifiable contraction guarantees for learning-based controllers in nonlinear settings, with potential applicability to larger-scale systems and non-Euclidean metrics in future work.

Abstract

We address the problem of verifying closed-loop contraction in nonlinear control systems whose controller and contraction metric are both parameterized by neural networks. By leveraging interval analysis and interval bound propagation, we derive a tractable and scalable sufficient condition for closed-loop contractivity that reduces to checking that the dominant eigenvalue of a symmetric Metzler matrix is nonpositive. We combine this sufficient condition with a domain partitioning strategy to integrate this sufficient condition into training. The proposed approach is validated on an inverted pendulum system, demonstrating the ability to learn neural network controllers and contraction metrics that provably satisfy the contraction condition.

Paper Structure

This paper contains 8 sections, 5 theorems, 18 equations, 1 figure, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Technical Results
  4. Contraction Verification
  5. Domain Partitioning and Training Algorithm
  6. Numerical Experiment
  7. Conclusions
  8. Additional Training Details

Key Result

Lemma 1

The dynamical system eq:nonlinear-dynamics is contracting with rate $c > 0$ if there exists a continuously-differentiable matrix-valued map $M: \mathbb{R}^n \rightarrow \mathbb{R}^{n \times n}$ and two constants $a_0, a_1>0$ such that for all $x \in \mathbb{R}^n$, $M(x) = M(x)^\top$ and $a_0 I_n \pr

Figures (1)

  • Figure 1: Closed-loop vector field of the inverted pendulum \ref{['eq:inv-pend']} with a neural network controller trained using the loss function \ref{['eq:training-loss']}.

Theorems & Definitions (9)

  • Lemma 1: Contraction inequality WL-JJES:98
  • Lemma 2
  • Theorem 3
  • proof
  • Lemma 4
  • Remark 5
  • Remark 6
  • Corollary 7
  • proof