Scalable Data-Driven Reachability Analysis and Control via Koopman Operators with Conformal Coverage Guarantees

TL;DR

This work tackles safe, scalable verification of unknown nonlinear dynamics by marrying Koopman operator theory with neural-network liftings and conformal prediction. The approach learns a lifted linear representation to enable fast, closed-loop reachability analysis while training a trajectory-tracking controller in the latent space; true dynamics guarantees are achieved by inflating the lifted reachability with CP-derived bounds, yielding probabilistic containment with probability $1- abla$. A key novelty is the reuse of CP bounds across a distribution of reference trajectories, enabling efficient, cross-controller safety verification for high-dimensional systems (up to 28D) such as MuJoCo swimmers and multi-rotor quadrotors. Empirical results show improved reachability coverage, reduced computation time, and controlled conservativeness compared to baselines, demonstrating the method’s practicality for real-time, data-driven safety verification across complex robotic tasks.

Abstract

We propose a scalable reachability-based framework for probabilistic, data-driven safety verification of unknown nonlinear dynamics. We use Koopman theory with a neural network (NN) lifting function to learn an approximate linear representation of the dynamics and design linear controllers in this space to enable closed-loop tracking of a reference trajectory distribution. Closed-loop reachable sets are efficiently computed in the lifted space and mapped back to the original state space via NN verification tools. To capture model mismatch between the Koopman dynamics and the true system, we apply conformal prediction to produce statistically-valid error bounds that inflate the reachable sets to ensure the true trajectories are contained with a user-specified probability. These bounds generalize across references, enabling reuse without recomputation. Results on high-dimensional MuJoCo tasks (11D Hopper, 28D Swimmer) and 12D quadcopters show improved reachable set coverage rate, computational efficiency, and conservativeness over existing methods.

Figures (12)

• Figure 1: Executed trajectories / reachable sets for a 28D MuJoCo swimmer (a); 11D hopper (b).
• Figure 2: A block diagram that describes the flow of our method (ScaRe-Kro). Green and orange arrows represent KRS and CP computations, respectively.
• Figure 3: To visualize empirical reachable set coverage, we compute Beta posteriors for the SNSA baseline and ScaRe-Kro on the 3D quadcopter (left) and Hopper (right). The dotted lines indicate the mode of the Beta posterior. For SNSA, coverage rate slowly converges to the target $1-\delta$ as calibration dataset size increases, whereas ScaRe-Kro maintains $100\%$ coverage even for small $K^\textrm{cal}$.
• Figure 4: CKRS and KRS (pre-CP) computed for 3D quadcopter, plotted for each dimension.
• Figure 5: Closed-loop trajectories obtained from DeepReach-based controller (orange) can fail to enforce the reach-avoid constraint (reach yellow goal region while avoiding red unsafe set), while our controller (green rollouts) guarantees safety and containment within the blue CKRS with probability 0.99.

Theorems & Definitions (7)

• proposition 1: CG Robustness Xu2020AutoLiRPA
• lemma 1: KRS overapproximation
• theorem 1: CKRS Coverage Guarantee
• lemma 1: KRS overapproximation
• proof
• theorem 1: CKRS Coverage Guarantee
• proof