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

TL;DR

This paper proposes a scalable method to verify the contractivity of neural network-based controllers in nonlinear systems by combining interval analysis, eigenvalue checks, and domain partitioning, validated on an inverted pendulum.

Contribution

It introduces a novel approach that integrates a tractable sufficient condition for contraction into training neural controllers using domain partitioning.

Findings

Successfully verified neural controllers for an inverted pendulum.

Demonstrated the method's scalability and effectiveness.

Provided a provable guarantee of closed-loop contraction.

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.