Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Probably Approximately Correct (PAC) Guarantees for Data-Driven Reachability Analysis: A Theoretical and Empirical Comparison

Elizabeth Dietrich, Hanna Krasowski, Murat Arcak

Abstract

Reachability analysis evaluates system safety, by identifying the set of states a system may evolve within over a finite time horizon. In contrast to model-based reachability analysis, data-driven reachability analysis estimates reachable sets and derives probabilistic guarantees directly from data. Several popular techniques for validating reachable sets -- conformal prediction, scenario optimization, and the holdout method -- admit similar Probably Approximately Correct (PAC) guarantees. We establish a formal connection between these PAC bounds and present an empirical case study on reachable sets to illustrate the computational and sample trade-offs associated with these methods. We argue that despite the formal relationship between these techniques, subtle differences arise in both the interpretation of guarantees and the parameterization. As a result, these methods are not generally interchangeable. We conclude with practical advice on the usage of these methods.

Probably Approximately Correct (PAC) Guarantees for Data-Driven Reachability Analysis: A Theoretical and Empirical Comparison

Abstract

Reachability analysis evaluates system safety, by identifying the set of states a system may evolve within over a finite time horizon. In contrast to model-based reachability analysis, data-driven reachability analysis estimates reachable sets and derives probabilistic guarantees directly from data. Several popular techniques for validating reachable sets -- conformal prediction, scenario optimization, and the holdout method -- admit similar Probably Approximately Correct (PAC) guarantees. We establish a formal connection between these PAC bounds and present an empirical case study on reachable sets to illustrate the computational and sample trade-offs associated with these methods. We argue that despite the formal relationship between these techniques, subtle differences arise in both the interpretation of guarantees and the parameterization. As a result, these methods are not generally interchangeable. We conclude with practical advice on the usage of these methods.

Paper Structure

This paper contains 16 sections, 7 theorems, 31 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Data-Driven Reachability Analysis
  4. Scenario Optimization
  5. Scenario Optimization with Sample Discarding
  6. Split Conformal Prediction
  7. Training-conditional Coverage
  8. The Holdout Method
  9. Summary of Methods
  10. Conformal Prediction versus The Holdout Method
  11. Conformal Prediction versus Scenario Optimization
  12. Empirical Results
  13. Empirical Conformal Prediction and Holdout Method
  14. Split Conformal Prediction with Training-Conditional Coverage and Sample-Discarding Scenario Optimization
  15. Sample and Computational Complexity
  16. ...and 1 more sections

Key Result

Theorem 1

Let $\beta \in (0,1)$ be any confidence parameter value. If $N$ and $k$ are such that where $n_\theta$ is the number of optimization variables, then Eq. eq:genpacbound holds with $\varepsilon = \epsilon$. $\blacktriangleleft$$\blacktriangleleft$

Figures (3)

  • Figure B1: Relationship between the PAC bounds of conformal prediction, the holdout method, and scenario optimization. A specific conformal procedure (Lemma \ref{['lem:empircalcoverage']}) yields PAC bounds equivalent to the holdout method (Thm. \ref{['thm:conformaltoholdout']}). With suitable choices of score function, error rate, and calibration set, conformal prediction can also produce PAC bounds structurally equivalent to scenario optimization with sample discarding (Prop. \ref{['prop:1']} and Thm. \ref{['thm:thm5']}).
  • Figure E1: Distribution of $\varepsilon$'s for the holdout method and empirical conformal prediction over 50 experiments.
  • Figure E2: Comparison of conformal prediction and scenario optimization with sample discarding applied to reachable sets of the Duffing oscillator. Dark ellipsoids denote the initial reachable set, while light ellipsoids show the resulting set of the conformal procedure and scenario program in Def. \ref{['def:removefromset']}.

Theorems & Definitions (15)

  • Definition 1: Scenario Discarding Algorithm
  • Theorem 1: Theorem 2.1, scenario-sample-discard
  • Theorem 2: Theorem 1, angelopoulos2022gentleintroductionconformalprediction
  • Definition 2: Beta Inverse CDF
  • Definition 3: Binomial Tail Inversion
  • Theorem 3: Theorem 1, dietrich2025datadrivenreachabilityscenariooptimization
  • Lemma 1: Empirical Conformal Coverage for Reachable Sets
  • proof
  • Theorem 4
  • proof
  • ...and 5 more