We provide a novel uniform convergence guarantee for DeepReach, a deep learning-based method for solving Hamilton-Jacobi-Isaacs (HJI) equations associated with reachability analysis. Specifically, we show that the DeepReach algorithm, as introduced by Bansal et al. in their eponymous paper from 2020, is stable in the sense that if the loss functional for the algorithm converges to zero, then the resulting neural network approximation converges uniformly to the classical solution of the HJI equation, assuming that a classical solution exists. We also provide numerical tests of the algorithm, replicating the experiments provided in the original DeepReach paper and empirically examining the impact that training with a supremum norm loss metric has on approximation error.

Fast and Safe Tracking (FaSTrack, Herbert* et al. (2017)) is a modular framework that provides safety guarantees while planning and executing trajectories in real time via value functions of Hamilton-Jacobi (HJ) reachability. These value functions are computed through dynamic programming, which is notorious for being computationally inefficient. Moreover, the resulting trajectory does not adapt online to the environment, such as sudden disturbances or obstacles. DeepReach (Bansal and Tomlin (2021)) is a scalable deep learning method to HJ reachability that allows parameterization of states, which opens up possibilities for online adaptation to various controls and disturbances. In this paper, we propose Parametric FaSTrack, which uses DeepReach to approximate a value function that parameterizes the control bounds of the planning model. The new framework can smoothly trade off between the navigation speed and the tracking error (therefore maneuverability) while guaranteeing obstacle avoidance in a priori unknown environments. We demonstrate our method through two examples and a benchmark comparison with existing methods, showing the safety, efficiency, and faster solution times of the framework.

Hamilton-Jacobi (HJ) reachability analysis is a verification tool that provides safety and performance guarantees for autonomous systems. It is widely adopted because of its ability to handle nonlinear dynamical systems with bounded adversarial disturbances and constraints on states and inputs. However, it involves solving a PDE to compute a safety value function, whose computational and memory complexity scales exponentially with the state dimension, making its direct usage in large-scale systems intractable. Recently, a learning-based approach called DeepReach, has been proposed to approximate high-dimensional reachable tubes using neural networks. While DeepReach has been shown to be effective, the accuracy of the learned solution decreases with the increase in system complexity. One of the reasons for this degradation is the inexact imposition of safety constraints during the learning process, which corresponds to the PDE's boundary conditions. Specifically, DeepReach imposes boundary conditions as soft constraints in the loss function, which leaves room for error during the value function learning. Moreover, one needs to carefully adjust the relative contributions from the imposition of boundary conditions and the imposition of the PDE in the loss function. This, in turn, induces errors in the overall learned solution. In this work, we propose a variant of DeepReach that exactly imposes safety constraints during the learning process by restructuring the overall value function as a weighted sum of the boundary condition and neural network output. This eliminates the need for a boundary loss during training, thus bypassing the need for loss adjustment. We demonstrate the efficacy of the proposed approach in significantly improving the accuracy of learned solutions for challenging high-dimensional reachability tasks, such as rocket-landing and multivehicle collision-avoidance problems.

With the continuous advancement in autonomous systems, it becomes crucial to provide robust safety guarantees for safety-critical systems. Hamilton-Jacobi Reachability Analysis is a formal verification method that guarantees performance and safety for dynamical systems and is widely applicable to various tasks and challenges. Traditionally, reachability problems are solved by using grid-based methods, whose computational and memory cost scales exponentially with the dimensionality of the system. To overcome this challenge, DeepReach, a deep learning-based approach that approximately solves high-dimensional reachability problems, is proposed and has shown lots of promise. In this paper, we aim to improve the performance of DeepReach on high-dimensional systems by exploring different choices of activation functions. We first run experiments on a 3D system as a proof of concept. Then we demonstrate the effectiveness of our approach on a 9D multi-vehicle collision problem.

Learning-based approaches for controlling safety-critical systems are rapidly growing in popularity; thus, it is important to assure their performance and safety. Hamilton-Jacobi (HJ) reachability analysis is a popular formal verification tool for providing such guarantees, since it can handle general nonlinear system dynamics, bounded adversarial system disturbances, and state and input constraints. However, its computational and memory complexity scales exponentially with the state dimension, making it intractable for large-scale systems. To overcome this challenge, neural approaches, such as DeepReach, have been used to synthesize reachable tubes and safety controllers for high-dimensional systems. However, verifying these neural reachable tubes remains challenging. In this work, we propose two verification methods, based on robust scenario optimization and conformal prediction, to provide probabilistic safety guarantees for neural reachable tubes. Our methods allow a direct trade-off between resilience to outlier errors in the neural tube, which are inevitable in a learning-based approach, and the strength of the probabilistic safety guarantee. Furthermore, we show that split conformal prediction, a widely used method in the machine learning community for uncertainty quantification, reduces to a scenario-based approach, making the two methods equivalent not only for verification of neural reachable tubes but also more generally. To our knowledge, our proof is the first in the literature to show a strong relationship between conformal prediction and scenario optimization. Finally, we propose an outlier-adjusted verification approach that uses the error distribution in neural reachable tubes to recover greater safe volumes. We demonstrate the efficacy of the proposed approaches for the high-dimensional problems of multi-vehicle collision avoidance and rocket landing with no-go zones.

Hamilton-Jacobi (HJ) reachability approach to approximately solve high-dimensional analysis is a verification method for autonomous systems that reachability problems. What sets DeepReach apart is its computes both the safe configurations and the corresponding ability to compute BRTs (and BRATs) as well as the corresponding safe controller for the system. In reachability analysis, one safety controller for general nonlinear dynamical computes the Backward Reachable Tube (BRT) of a dynamical systems in the presence of disturbances and state and input system. This is the set of states such that the trajectories constraints. DeepReach is rooted in HJ reachability analysis; that start from this set will eventually reach some given target however, instead of solving the value function PDE over a set despite the worst case disturbance (or an exogenous, grid, DeepReach draws inspiration from the recent progress adversarial input more generally). As an example, for an in solving PDEs using deep learning, and represents the aerial vehicle, the disturbance could be wind or another value function as a deep neural network (DNN) to learn adversarial aircraft flying nearby, and the target set could a parameterized approximation of the value function. Thus, be the destination of the vehicle. The BRT provides both the computation and memory requirements for obtaining the the set of states from which the aerial vehicle can safely value function do not scale with the grid resolution, but reach its destination and a robust controller for the vehicle.