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

TL;DR

This paper introduces a scalable, data-driven approach for safety verification of unknown nonlinear systems using Koopman operators, neural networks, and conformal prediction to ensure probabilistic reachability guarantees.

Contribution

It combines Koopman theory with neural networks and conformal prediction to efficiently compute and validate probabilistic reachable sets for complex nonlinear systems.

Findings

Improved coverage rate of reachable sets on high-dimensional tasks

Enhanced computational efficiency compared to existing methods

Achieved statistically-valid safety guarantees with conformal bounds

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.