Exact Imposition of Safety Boundary Conditions in Neural Reachable Tubes

TL;DR

This work tackles safety verification for high-dimensional autonomous systems by improving Hamilton-Jacobi reachability with ExactBC, a method that exactly enforces boundary conditions in neural approximations of the safety value function. By reparameterizing $V_\theta(x,t)$ as $l(x) + (T-t) O_\theta(x,t)$, ExactBC guarantees $V_\theta(x,T)=l(x)$ and trains using a single PDE loss, removing the need for boundary loss weighting. Across four challenging tasks with varying dynamics and boundary complexity, ExactBC consistently yields more accurate value functions and larger verified safe volumes than prior DeepReach or residual-learning variants, including difficult high-dimensional scenarios like autonomous rocket landing and multi-aircraft avoidance. While offering significant accuracy gains, the method remains limited by non-differentiable boundaries and does not reduce computational time, pointing to directions for handling non-differentiability and improving efficiency in future work.

Abstract

Hamilton-Jacobi (HJ) reachability analysis is a widely adopted verification tool to provide safety and performance guarantees for autonomous systems. However, it involves solving a partial differential equation (PDE) to compute a safety value function, whose computational and memory complexity scales exponentially with the state dimension, making its direct application to large-scale systems intractable. To overcome these challenges, DeepReach, a recently proposed learning-based approach, approximates high-dimensional reachable tubes using neural networks (NNs). While shown to be effective, the accuracy of the learned solution decreases with system complexity. One of the reasons for this degradation is a soft imposition of safety constraints during the learning process, which corresponds to the boundary conditions of the PDE, resulting in inaccurate value functions. In this work, we propose ExactBC, a variant of DeepReach that imposes safety constraints exactly during the learning process by restructuring the overall value function as a weighted sum of the boundary condition and the NN output. Moreover, the proposed variant no longer needs a boundary loss term during the training process, thus eliminating the need to balance different loss terms. We demonstrate the efficacy of the proposed approach in significantly improving the accuracy of the learned value function for four challenging reachability tasks: a rimless wheel system with state resets, collision avoidance in a cluttered environment, autonomous rocket landing, and multi-aircraft collision avoidance.

Figures (3)

• Figure 1: (Left) Rimless wheel system. (Right) Trained and ground truth BRT slices. The brown and yellow areas represent the limit cycle (the target set) and the BRT respectively. ExactBC recovers a higher BRT volume than DeepReach and DiffModel, and its BRT is closely aligned with the ground truth BRT.
• Figure 2: Ground truth, trained, and recovered BRT slices for the bicycle robot. The recovered BRT is computed using the robust verification strategy at a safety level of 99.99%. These slices correspond to $v=3.6 \text{m/s}$, $\theta=0.25 \text{rad}$ and $\psi=0$. Due to the complex boundary conditions in this case, ExactBC learns a more accurate value function and recovers a significantly higher BRT volume than DeepReach.
• Figure 3: Trained and recovered BRT slices for (Left) rocket landing and (Right) multi-aircraft collision avoidance system. For the rocket landing system, DeepReach is not able to recover any volume that is verifiably safe, while DiffModel is only able to recover a small fraction of the volume. On the other hand, ExactBC is consistently able to recover a significant portion of the learned volume, which illustrates the increase in learning accuracy over the other baselines.

Theorems & Definitions (1)

• Remark 1