Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From Global to Local: Hierarchical Probabilistic Verification for Reachability Learning

Ebonye Smith, Sampada Deglurkar, Jingqi Li, Gechen Qu, Claire J. Tomlin

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.

From Global to Local: Hierarchical Probabilistic Verification for Reachability Learning

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.

Paper Structure

This paper contains 20 sections, 3 theorems, 24 equations, 3 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Reachability Learning
  4. Scenario Optimization Theory
  5. Hybrid Reachability Verification Method
  6. Probabilistic Dynamics Bounding
  7. Coarse Global Verification
  8. Local Growth Iterative Refinement
  9. Hierarchical Verification and Control Framework
  10. Theoretical Reach-avoid Guarantees
  11. Tier 1 & Tier 2: Probabilistic RA Set Verification
  12. Tier 3: Finite-time Recovery
  13. Experiments and Results
  14. Drone Racing Case Study
  15. Joint System Dynamics
  16. ...and 5 more sections

Key Result

Theorem 1

Let $\epsilon$ be the risk level and $\beta \in (0,1)$ be the confidence parameter. Denote by $\mathbb{P}_S$ the probability measure associated with the number of scenarios $N \geq \frac{2}{\epsilon} \left( \ln \frac{1}{\beta} + d \right)$, taken from $\Delta$ and by $P_\Delta$ the probability measu

Figures (3)

  • Figure 1: (a) Building on a learned reachability value function and policy from prior work (e.g., li2025certifiable), our hierarchical verification framework provides probabilistic safety guarantees based on whether the state lies in the globally or locally verified set; otherwise, safe set recovery drives it to a verified region. Our key novelty is leveraging scenario optimization for local safe set expansion. (b) Drone racing example in which the ego drone (blue) reaches a refined local safe set that guarantees safe overtaking of an opponent (black).
  • Figure 2: Evolution of a drone racing simulation against an opponent (black), comparing our method (Hybrid, dark blue) with various baselines. Baselines struggle to balance safety and goal-reaching, whereas our method achieves both, safely overtaking and reaching the gate. Moreover, we observe that the ego agent leverages safe recovery MPPI to try to enter the locally refined set.
  • Figure 3: (a) Performance of our framework compared to control barrier function (CBF) and soft-constraint baselines. (b) Ablation study comparing the hybrid method to its learning-only and model-based variants. In both (a) and (b), the results for our method are shown for reference. Our framework achieves higher success probability over 500 sampled initial conditions, effectively balancing collision avoidance and goal-reaching.

Theorems & Definitions (6)

  • Theorem 1: Sample Complexity campi2009scenariodevonport2020estimating
  • Theorem 2: Global Probabilistic Safety
  • proof
  • Proposition 1: Sequential Probabilistic Guarantees
  • proof
  • Remark 1