From Global to Local: Hierarchical Probabilistic Verification for Reachability Learning

1. Problem Statement

The paper addresses the challenge of designing provably safe controllers for high-dimensional nonlinear systems (e.g., autonomous drones) operating in safety-critical environments.

• The Core Conflict: Traditional Hamilton–Jacobi (HJ) reachability analysis provides formal safety guarantees but suffers from the "curse of dimensionality," making it computationally intractable for complex systems.
• The Limitation of Learning: Learning-based approaches (e.g., Deep Reinforcement Learning) offer scalability but introduce approximation errors. These errors can lead to overly optimistic safe sets, where the controller misclassifies unsafe regions as safe, potentially causing collisions or failures.
• The Gap: Existing verification methods are often either too conservative (deterministic worst-case), too computationally expensive (global probabilistic), or lack adaptability (offline only). There is a need for a framework that balances scalability, accuracy, and computational efficiency while providing rigorous safety guarantees.

2. Methodology

The authors propose a Hierarchical Probabilistic Verification Framework that bridges offline global certification with online local refinement. The system operates on a multi-tier logic, switching between a learned reachability policy and a model-based controller (MPPI) based on the current state's verification status.

A. Core Components

1. Global Probabilistic Certificate (Offline):

   • Goal: Construct a coarse, computationally efficient "safe set" ($V_{global}$) that covers the majority of the state space.
   • Technique: Uses Scenario Optimization. The authors estimate a global sensitivity bound ($\Delta x^*_t$) by sampling trajectory deviations between nominal and perturbed states under the learned policy.
   • Mechanism: They construct a lower-bound value function ($\check{V}_\gamma$) by subtracting Lipschitz-based error margins from the reward and constraint functions. If $\check{V}_\gamma \geq 0$, the state is certified safe with high probability.
   • Trade-off: This tier is fast but conservative; it may exclude safe states near the boundary.

2. Local Refinement (Online):

   • Goal: Recover safe states that were excluded by the conservative global verification, specifically near the boundary of $V_{global}$.
   • Technique: An iterative Local Growth Algorithm.
     • It identifies the closest boundary point of the global set to the current state.
     • It performs targeted sampling in a local neighborhood ($B_r$) around this boundary.
     • It solves a sequence of convex programs (via scenario optimization) to expand the radius $r$ until a violation is detected.
   • Outcome: This creates a "reclaimed" local safe set ($V_{local}$) that is less conservative than the global set but still holds probabilistic guarantees.

3. Hybrid Switching Control Framework:
   The controller switches between modes based on the state's location:

   • Tier 0 (Target Maintenance): If inside the goal set ($T$), use a fast MPPI controller.
   • Tier 1 (Global Verification): If inside $V_{global}$, use the Learned Policy ($\pi_{lp}$).
   • Tier 2 (Local Refinement): If outside $V_{global}$ but inside the locally refined set $V_{local}$, continue using $\pi_{lp}$ (as the local region is now verified).
   • Tier 3 (Safety Recovery): If the state is outside both verified sets, switch to a Model-Based MPPI controller. This controller is "warm-started" with the learned policy to minimize the distance to the nearest verified safe set, steering the system back to safety.

B. Theoretical Guarantees

The framework provides probabilistic safety guarantees for both global and local sets. Using Theorem 1 (Sample Complexity of Scenario Optimization), the authors prove that with a confidence parameter $\beta$ and risk level $\epsilon$, the probability of an unseen state violating safety constraints is bounded.

3. Key Contributions

1. Hierarchical Safe Framework: A novel multi-tier architecture combining offline global probabilistic verification with online local refinement, integrating learned policies with model-based fallbacks.
2. Scenario-Based Local Expansion: An efficient method to expand safe sets near boundaries using convex programs, recovering regions discarded by conservative global approximations without sacrificing safety guarantees.
3. Probabilistic Safety Guarantees: Theoretical proofs ensuring that both the globally verified set and the locally refined set satisfy safety constraints with high confidence.
4. Empirical Validation: Demonstration of improved performance in a high-dimensional drone racing scenario, outperforming standard baselines.

4. Experimental Results

The framework was tested in a 12-dimensional drone racing simulation involving an ego drone and an aggressive opponent. The goal was to overtake the opponent and pass through a narrow gate while avoiding collisions (non-convex constraints).

• Setup: 500 initial conditions were sampled. The framework used $\beta=0.001$ and $\epsilon=0.1$ (requiring 158 samples per verification).
• Comparison: The proposed "Hybrid" method was compared against:
  • MPPI with Control Barrier Functions (CBF).
  • MPPI with soft constraints.
  • PPO with CBF.
  • Ablation studies (Pure MPPI, Pure Learned Policy, etc.).
• Performance:
  • Success Rate: The proposed framework achieved a 90.2% success rate (safely reaching the gate before the opponent).
  • Baselines: MPPI+CBF achieved 62.4%, PPO+CBF achieved 14.2%, and Pure Learned Policy achieved 51.8%.
  • Qualitative: Baseline methods tended to either prioritize safety (failing to reach the goal) or goal-reaching (crashing). The hierarchical framework successfully balanced both, utilizing the "Safe Recovery" mode to steer back into verified regions when necessary.

5. Significance

This work represents a significant step forward in Safe Reinforcement Learning and Autonomous Control:

• Scalability: It overcomes the dimensionality barrier of HJ reachability by using learning for the bulk of the control and verification only for safety certification.
• Reduced Conservatism: By adding an online local refinement layer, it recovers usable state space that traditional conservative methods would discard, enabling more aggressive and efficient maneuvers (e.g., overtaking in racing).
• Robustness: The hybrid switching mechanism ensures that even if the learning model fails or the state enters an unverified region, the system does not crash but actively attempts to recover to a safe state.
• Practical Applicability: The use of scenario optimization allows these guarantees to be computed with a manageable number of samples, making the approach viable for real-world, safety-critical applications like autonomous aviation and robotics.