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

TL;DR

This paper introduces a state-dependent conformal prediction method to provide scalable, tight safety bounds for perception-based autonomous systems, improving over existing conservative approaches.

Contribution

It proposes a novel state-dependent conformal prediction technique and a branch-merging reachability algorithm to enhance scalability and reduce conservatism in safety verification.

Findings

Reduced conservatism compared to existing methods

Scalable verification with tight high-confidence bounds

Effective partitioning of state space using genetic algorithms

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.