Verification of Neural Reachable Tubes via Scenario Optimization and Conformal Prediction

TL;DR

This work tackles the verification of learning-based neural reachable tubes for safety-critical systems by introducing two probabilistic guarantees: robust scenario-based verification and split conformal prediction. It formalizes the link between these approaches, showing that conformal prediction reduces to a robust scenario-optimization problem, and adds an outlier-adjusted method to recover larger safe volumes without sacrificing guarantees. The methods are demonstrated on high-dimensional problems, including multi-vehicle collision avoidance and rocket landing with no-go zones, where they yield meaningful increases in safe volume and robust safety assurances. Together, the contributions advance scalable, probabilistic safety guarantees for neural reachability tools in complex dynamical systems, enabling safer deployment of learning-based controllers.

Abstract

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.

Figures (3)

• Figure 1: (Top) For a fixed simulation budget $N$, the cyan curve shows the number of empirical safety violations $k$ for different learned volumes (different super-levels of $\Tilde{V}(x,0)$). The red curve shows the trade-off in safety strength $\epsilon$ (in log scale) for each $k$ using the robust method. The grey point indicates the iterative method baseline. The robust method is able to provide safety assurances even for the volumes that have non-zero outliers. (Dashed black line) By a small decrease in safety level (from $99.999\%$ to $99.974\%$) caused by outliers, we are able to significantly increase the assured safe volume from $0.56$ to $0.81$. (Bottom) Correspondingly, the safe set $\mathcal{S}$ increases greatly from the complement of the grey region to the complement of the blue region.
• Figure 2: (Left) Computing the safety strength $\epsilon$ across different volumes (different super-levels of $\Tilde{V}(x,0)$) for different simulation budgets $N$ using the robust method. The grey points indicate the iterative method baselines. (Right) As we increase $N$, the largest volume achieving the desired $99.968\%$ safety using the robust method increases up to a limit.
• Figure 3: The Beta distribution of $\underset{x \in \mathcal{S}}{\mathbb{P}} \left( J_{\Tilde{\pi}}(x,0) > 0 \right)$ when $k=731$ outliers are found from $N=3684118$ samples. (Dashed black line) For an example choice of confidence $1-\beta=0.9$ (shaded blue), we can lower-bound the fraction of $\mathcal{S}$ which is safe with at least $1-\epsilon=0.99979$ ($99.979\%$) confidence.

Theorems & Definitions (12)

• remark 1
• theorem 1: Robust Scenario-Based Probabilistic Safety Verification
• theorem 2: Conformal Probabilistic Safety Verification
• remark 2
• lemma 1: Conformal Probabilistic Safety Verification
• remark 3
• lemma 2: Solution Feasibility for a 1-D CCP
• proof
• proof
• proof