Statistical-Symbolic Verification of Perception-Based Autonomous Systems using State-Dependent Conformal Prediction

TL;DR

This paper tackles safety guarantees for perception-based autonomous systems by introducing state-dependent conformal prediction (CP) to bound perception error as a function of the dynamical state, thereby reducing conservatism in reachability analysis. It couples region-wise CP bounds with Taylor-model-based reachability and a genetic-algorithm–driven region partitioning to produce tighter trajectory-wide guarantees. A branch-merging (cluster-and-enclose) strategy improves scalability in highly-branching hybrid systems, enabling verification of higher-dimensional problems. Empirical evaluation on Mountain Car and a LiDAR-based autonomous racing platform shows substantial reductions in reachable-set size and improved test coverage compared to time-based CP baselines. The work advances neuro-symbolic verification by leveraging state-dependent error structure to achieve safe, scalable, and data-driven guarantees in closed-loop perception systems.

Abstract

Reachability analysis has been a prominent way to provide safety guarantees for neurally controlled autonomous systems, but its direct application to neural perception components is infeasible due to imperfect or intractable perception models. Typically, this issue has been bypassed by complementing reachability with statistical analysis of perception error, say with conformal prediction (CP). However, existing CP methods for time-series data often provide conservative bounds. The corresponding error accumulation over time has made it challenging to combine statistical bounds with symbolic reachability in a way that is provable, scalable, and minimally conservative. To reduce conservatism and improve scalability, our key insight is that perception error varies significantly with the system's dynamical state. This article proposes state-dependent conformal prediction, which exploits that dependency in constructing tight high-confidence bounds on perception error. Based on this idea, we provide an approach to partition the state space, using a genetic algorithm, so as to optimize the tightness of conformal bounds. Finally, since using these bounds in reachability analysis leads to additional uncertainty and branching in the resulting hybrid system, we propose a branch-merging reachability algorithm that trades off uncertainty for scalability so as to enable scalable and tight verification. The evaluation of our verification methodology on two complementary case studies demonstrates reduced conservatism compared to the state of the art.

Figures (7)

• Figure 1: High-confidence reachability approach overview. Step 1 (Partition region): Using perception errors along trajectories, we partition the state space to minimize the trajectory-based perception bounds and compute region-specific conformal bounds. Step 2 (Reachability analysis): We inflate the reachability analysis with these bounds to obtain high-confidence reachable sets.
• Figure 2: Illustration of axis-aligned cuts and resulting regions for 2 cuts in the first state dimension and 3 cuts in the second state dimension ($n_1{=}2, n_2{=}3$), producing $M{=}7$ non-empty regions.
• Figure 3: Examples of noise in Mountain Car environment. The noisy images were cropped to emphasize the car for visibility.
• Figure 4: Perception errors and their respective bounds under our method and a time-based baseline.
• Figure 5: Reachable Sets for our state-based conformal perception bounds (Fixed Confidence, $M=7$) vs. the time-based baseline bounds. Our reachable sets are tighter than the time-based method at all timesteps.

Theorems & Definitions (6)

• definition 1: Taylor Model
• proposition 1: Global Partitioning Guarantee
• theorem 1: High-Confidence Reachability Guarantee
• definition 2: Reachability-Informed Region Optimization
• definition 3: Axis-Aligned Reachability-Informed Region Optimization
• definition 4: Taylor Model Union Enclosure