Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers

Our work aims to make certified reachability practical for modern robot learning and online planning with neural dynamics and controllers. Existing reachability tools are primarily designed for offline verification and are often non-differentiable, computationally inefficient, or overly conservative for direct integration into modern learning and online planning pipelines. Our main contributions are:

• Parallel Differentiable Reachability Framework: We develop a GPU-parallel and differentiable reachability framework in JAX for continuous- and discrete-time systems with analytical and neural-network dynamics and controllers. Our method combines Taylor-model flowpipe propagation with CROWN-style neural certification through a unified TM-CROWN representation.
• Unified TM-CROWN Reachability Interface: We introduce a unified affine/Taylor-model interface that propagates certified bounds across both analytical dynamics and neural components without intermediate interval relaxation. This preserves cross-state dependencies while remaining compatible with efficient batched tensor computation.
• Certified Training and Reachability-Aware MPC: We demonstrate how differentiable reachable-set objectives can be integrated directly into neural dynamics and controller training, as well as sampling-based MPC with gradient-based refinement, enabling uncertainty-aware learning and online planning with certified reachable-set guarantees.
• Scalable Robotic Evaluations: We validate the framework on manipulation and quadrotor tasks, including real-world T-pushing experiments and higher-dimensional systems up to 72D, demonstrating practical runtime and robust online planning under bounded uncertainty.

Our framework turns reachability analysis into a differentiable, GPU-parallel primitive that can be used directly inside robot learning and online planning.

The core engine combines Taylor-model flowpipes for system dynamics with CROWN-based verification for neural components through a unified TM-CROWN interface. This allows certified reachable sets to be propagated through analytical dynamics, neural dynamics, and neural controllers while preserving useful dependency information.

The same engine is used in two downstream pipelines. During certified training, reachable-set penalties regularize neural dynamics and controllers so that uncertainty remains compact over long horizons. During reachability-aware MPC, candidate action sequences are evaluated by both task cost and reachable-set penalties, enabling robust online planning under bounded uncertainty.