Verifying Closed-Loop Contractivity of Learning-Based Controllers via Partitioning
This addresses safety verification for learning-based control systems, but it is incremental as it builds on existing interval analysis and partitioning methods.
The paper tackled verifying closed-loop contraction in nonlinear control systems with neural network-based controllers and metrics, using interval analysis and domain partitioning to derive a scalable sufficient condition, validated on an inverted pendulum system to learn provably contractive controllers.
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.