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.

翻译：本文提出一种可扩展的、基于可达性分析的框架，用于对未知非线性动力学系统进行概率化的数据驱动安全验证。我们采用配备神经网络提升函数的Koopman理论，学习动力学的近似线性表示，并在此空间中设计线性控制器，以实现对参考轨迹分布的闭环跟踪。闭环可达集在提升空间中高效计算，并通过神经网络验证工具映射回原始状态空间。为捕捉Koopman动力学模型与真实系统间的失配，我们应用保形预测方法生成统计有效的误差边界，通过膨胀可达集确保真实轨迹以用户指定概率被包含其中。这些边界具备跨参考轨迹的泛化能力，支持重复使用而无需重新计算。在高维MuJoCo任务（11维Hopper、28维Swimmer）及12维四旋翼飞行器上的实验结果表明，相较于现有方法，本框架在可达集覆盖率、计算效率与保守性方面均获得显著提升。