DeepReach: A Deep Learning Approach to High-Dimensional Reachability
This addresses a critical scalability issue in formal verification for safety-critical systems like autonomous driving, though it is an incremental improvement over existing reachability methods.
The authors tackled the computational bottleneck of Hamilton-Jacobi reachability analysis, which scales exponentially with state dimensions, by proposing DeepReach, a neural PDE solver that achieves comparable results to state-of-the-art methods on high-dimensional problems like a 9D multi-vehicle collision and a 10D narrow passage.
Hamilton-Jacobi (HJ) reachability analysis is an important formal verification method for guaranteeing performance and safety properties of dynamical control systems. Its advantages include compatibility with general nonlinear system dynamics, formal treatment of bounded disturbances, and the ability to deal with state and input constraints. However, it involves solving a PDE, whose computational and memory complexity scales exponentially with respect to the number of state variables, limiting its direct use to small-scale systems. We propose DeepReach, a method that leverages new developments in sinusoidal networks to develop a neural PDE solver for high-dimensional reachability problems. The computational requirements of DeepReach do not scale directly with the state dimension, but rather with the complexity of the underlying reachable tube. DeepReach achieves comparable results to the state-of-the-art reachability methods, does not require any explicit supervision for the PDE solution, can easily handle external disturbances, adversarial inputs, and system constraints, and also provides a safety controller for the system. We demonstrate DeepReach on a 9D multi-vehicle collision problem, and a 10D narrow passage problem, motivated by autonomous driving applications.