Certified Robust Invariant Polytope Training in Neural Controlled ODEs

TL;DR

This work addresses safety guarantees for neural network controllers in disturbed dynamical systems by certifying forward invariant polytopes in closed-loop control. It introduces a lifted embedding framework that combines interval analysis and a parametric left-inverse lifting to certify polytopes and enable end-to-end training with invariance guarantees. A novel training objective incorporates the lifted positivity condition, scalable verification via embedding systems, and an adaptive left-inverse parameterization, achieving faster training and better scalability than sampling-based Lyapunov methods. The approach demonstrates robust invariance certification on nonlinear systems like Segways and vehicle platoons, with potential impact on safely deploying learning-based controllers in safety-critical applications.

Abstract

We consider a nonlinear control system modeled as an ordinary differential equation subject to disturbance, with a state feedback controller parameterized as a feedforward neural network. We propose a framework for training controllers with certified robust forward invariant polytopes, where any trajectory initialized inside the polytope remains within the polytope, regardless of the disturbance. First, we parameterize a family of lifted control systems in a higher dimensional space, where the original neural controlled system evolves on an invariant subspace of each lifted system. We use interval analysis and neural network verifiers to further construct a family of lifted embedding systems, carefully capturing the knowledge of this invariant subspace. If the vector field of any lifted embedding system satisfies a sign constraint at a single point, then a certain convex polytope of the original system is robustly forward invariant. Treating the neural network controller and the lifted system parameters as variables, we propose an algorithm to train controllers with certified forward invariant polytopes in the closed-loop control system. Through two examples, we demonstrate how the simplicity of the sign constraint allows our approach to scale with system dimension to over $50$ states, and outperform state-of-the-art Lyapunov-based sampling approaches in runtime.

Figures (4)

• Figure 1: (Left) The mechanical system from Examples \ref{['ex:mechsys']} and \ref{['ex:mechsyscont']} is visualized with several polytopes in solid lines and solution trajectories in dotted lines. The blue set $\mathcal{S}_1$ is a hyperrectangle that cannot be forward invariant, the green invariant set $\mathcal{S}_2$ is obtained from the transformation associated with the eigenvalue decomposition, and the red invariant set $\mathcal{S}_3$ is obtained by lifting the system into $3$-dimensions. (Middle/Right) $\mathcal{I}_\mathcal{H}$ is applied to every face of the box $[\ul{y},\overline{y}] = [-1,1]^3$ (blue) for the subspace $\mathcal{H}$ from Example \ref{['ex:mechsyscont']} (red). The outputs (purple) are refined interval sets which still contain $\mathcal{H}$. The red outlined set ($\mathcal{H}\cap[\ul{y},\overline{y}]$) corresponds to the polytope $\langle H,\ul{y},\overline{y}\rangle$ from Example \ref{['ex:mechsyscont']} and the red polytope from the left figure. The original system evolves on the subspace $\mathcal{H}$ by Proposition \ref{['prop:invsubspace']}, and the positivity condition $\mathsf{E}_{H,H^+}(\ul{y},\overline{y},\ul{w},\overline{w})\geq_{\mathrm{SE}}0$ from Theorem \ref{['thm:polyreach']} implies the vector component points in the direction indicated by the black arrows (middle) along each refined face. The corresponding trajectories from the left figure are shown in dotted lines (right).
• Figure 2: The certified robust invariant polytope in $\mathbb{R}^3$ for the segway is visualized in blue. Simulations of trajectories starting from its vertices are in red.
• Figure 3: The invariant polytope and a sample system trajectory for the platoon with $4$ vehicles is pictured. Vehicles $1$ and $4$ share the same invariant set in orange.
• Figure 4: The connection topology of the platoon. Leaders are filled and arrows represent relative measurements.

Theorems & Definitions (13)

• proposition 1: Invariant hyperrectangles
• definition 1: Lifted system
• proposition 2: Parameterization of left inverses
• proposition 3: Invariant subspace
• definition 2: Interval refinement operator
• definition 3: Lifted embedding system
• theorem 1: Polytope invariant sets
• remark 1: Comparison to the literature
• remark 2: Choice of $\eta$
• proof