  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.
