From Global to Local: Hierarchical Probabilistic Verification for Reachability Learning

TL;DR

This paper introduces a hierarchical probabilistic verification framework that combines global certification and local refinement to improve safety guarantees in reachability learning for nonlinear systems, demonstrated through drone racing simulations.

Contribution

It presents a novel hierarchical approach that integrates offline global certification with online local safety set refinement, enhancing safety and efficiency in reachability learning.

Findings

Reduces conservatism in safety sets

Improves success rates in goal-reaching tasks

Provides probabilistic safety guarantees

Abstract

Hamilton-Jacobi (HJ) reachability provides formal safety guarantees for nonlinear systems. However, it becomes computationally intractable in high-dimensional settings, motivating learning-based approximations that may introduce unsafe errors or overly optimistic safe sets. In this work, we propose a hierarchical probabilistic verification framework for reachability learning that bridges offline global certification and online local refinement. We first construct a coarse safe set using scenario optimization, providing an efficient global probabilistic certificate. We then introduce an online local refinement module that expands the certified safe set near its boundary by solving a sequence of convex programs, recovering regions excluded by the global verification. This refinement reduces conservatism while focusing computation on critical regions of the state space. We provide probabilistic safety guarantees for both the global and locally refined sets. Integrated with a switching mechanism between a learned reachability policy and a model-based controller, the proposed framework improves success rates in goal-reaching tasks with safety constraints, as demonstrated in simulation experiments of two drones racing to a goal with complex safety constraints.