pith. sign in

arxiv: 2512.02893 · v2 · submitted 2025-12-02 · 📡 eess.SY · cs.SY

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

Yuang Geng , Thomas Waite , Trevor Turnquist , Radoslav Ivanov , Ivan Ruchkin This is my paper

Pith reviewed 2026-05-17 02:06 UTC · model grok-4.3

classification 📡 eess.SY cs.SY
keywords state-dependent conformal predictionperception errorreachability analysisautonomous systemsneural perceptionsafety verificationgenetic algorithmbranch merging
0
0 comments X

The pith

Perception error bounds tighten when conformal prediction accounts for variation with the system's dynamical state.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper seeks to make safety verification practical for autonomous systems whose controllers rely on neural perception. Standard reachability analysis cannot handle imperfect perception models directly, so statistical bounds from conformal prediction are added, yet existing time-series versions of conformal prediction remain conservative and accumulate error. The authors' central move is to treat perception error as state-dependent rather than uniform, then partition the state space so that each region receives its own calibrated bound. A genetic algorithm searches for partitions that minimize bound width, and a branch-merging reachability procedure limits the resulting explosion in uncertainty. The resulting hybrid verification is shown to be both provable and less conservative than prior statistical-symbolic combinations.

Core claim

Perception error varies significantly with dynamical state, so state-dependent conformal prediction—implemented by genetically partitioning the state space—yields tighter high-confidence intervals than state-independent conformal prediction. These intervals are integrated into symbolic reachability via a branch-merging algorithm that deliberately trades some uncertainty for computational scalability, thereby enabling verification of neurally controlled autonomous systems with reduced conservatism.

What carries the argument

state-dependent conformal prediction, which constructs region-specific prediction intervals by partitioning the state space so that each conformal bound reflects the local statistics of perception error

If this is right

  • Tighter per-state bounds limit error accumulation across time steps in reachability analysis.
  • The branch-merging procedure keeps the hybrid system reachable set computationally tractable while preserving soundness.
  • Verification becomes feasible for perception-based controllers that previously produced intractable uncertainty growth.
  • The overall pipeline supplies both statistical coverage and symbolic safety certificates with less added conservatism than existing methods.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the state-error correlation holds across many sensor modalities, the same partitioning idea could reduce conservatism in verification of other hybrid systems that contain learned components.
  • Replacing the offline genetic algorithm with an online learner might allow the partitions to adapt as the vehicle encounters new environments.
  • The same state-dependency insight could be applied to uncertainties other than perception error, such as actuator noise or environmental disturbances.

Load-bearing premise

Perception error must vary significantly and usefully with dynamical state so that a genetic algorithm can discover partitions that tighten bounds without introducing new conservatism or breaking coverage guarantees.

What would settle it

An experiment on one of the case-study systems in which the state-dependent conformal intervals are not statistically narrower than a single global interval, or in which the final reachability set loses its safety guarantee.

Figures

Figures reproduced from arXiv: 2512.02893 by Ivan Ruchkin, Radoslav Ivanov, Thomas Waite, Trevor Turnquist, Yuang Geng.

Figure 1
Figure 1. Figure 1: High-confidence reachability approach overview. [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. 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 [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Examples of noise in Mountain Car environment. The noisy images were cropped to emphasize the car for visibility. [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Perception errors and their respective bounds under our method and a time-based baseline. [PITH_FULL_IMAGE:figures/full_fig_p019_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Reachable Sets for our state-based conformal perception bounds (Fixed Confi￾dence, 𝑀 = 7) vs. the time-based baseline bounds. Our reachable sets are tighter than the time-based method at all timesteps. Altogether, we collect 4000 trajectories from MC. The initial states are uniformly sampled from [-0.55, -0.45] and are simulated for 90 steps. We split each trajectory dataset evenly into a 2,000-trajectory … view at source ↗
Figure 6
Figure 6. Figure 6: Illustration of heading and position errors against reference trajectory. 7.2.1 Perception Pipeline. The perception model for the LiDAR-based au￾tonomous racing car consists of a CNN followed by a particle filter [6]. Given a 21-dimensional LiDAR input scan, the CNN is trained to predict the signed error in the relative heading and distance of the car to a reference trajectory. See [PITH_FULL_IMAGE:figure… view at source ↗
Figure 7
Figure 7. Figure 7: Perception errors and their respective bounds under our method and a time-based baseline. [PITH_FULL_IMAGE:figures/full_fig_p022_7.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper claims that perception error in neurally controlled autonomous systems varies significantly with dynamical state; it introduces state-dependent conformal prediction that uses a genetic algorithm to partition the state space and optimize conformal bound tightness, then combines the resulting bounds with a branch-merging reachability algorithm to obtain scalable, less conservative safety verification than standard conformal prediction plus reachability, with supporting results on two case studies.

Significance. If the coverage guarantees survive the data-dependent partitioning step, the method would meaningfully reduce conservatism in statistical-symbolic verification pipelines for perception-based systems while preserving high-confidence bounds, addressing a practical bottleneck in combining reachability analysis with imperfect neural perception.

major comments (2)
  1. [§3.2] §3.2 (Genetic-algorithm partitioning): the partitions are chosen by minimizing bound width directly on the calibration dataset used to compute nonconformity scores and quantiles. Because the partition boundaries are therefore data-dependent, the exchangeability assumption underlying marginal coverage in conformal prediction is no longer guaranteed; the manuscript must either (a) reserve an independent hold-out set for partition optimization or (b) supply a proof that post-selection coverage remains controlled at the nominal level. Without one of these safeguards the reported high-confidence bounds may be optimistically biased.
  2. [Evaluation] Evaluation (case-study results): the abstract asserts reduced conservatism on two complementary case studies, yet the manuscript provides neither quantitative bound-width comparisons, coverage-frequency tables, error-bar statistics, nor explicit verification-time numbers that would allow the reader to verify the claimed improvement over standard CP. These metrics are load-bearing for the central empirical claim.
minor comments (1)
  1. [§3.1] Clarify the precise definition of the state-dependent nonconformity score and how the quantile is computed after partitioning; the current notation leaves open whether the quantile is taken marginally or conditionally on each partition.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback. We address each major comment below, agreeing where the concerns are valid and outlining specific revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: [§3.2] §3.2 (Genetic-algorithm partitioning): the partitions are chosen by minimizing bound width directly on the calibration dataset used to compute nonconformity scores and quantiles. Because the partition boundaries are therefore data-dependent, the exchangeability assumption underlying marginal coverage in conformal prediction is no longer guaranteed; the manuscript must either (a) reserve an independent hold-out set for partition optimization or (b) supply a proof that post-selection coverage remains controlled at the nominal level. Without one of these safeguards the reported high-confidence bounds may be optimistically biased.

    Authors: We agree that performing genetic-algorithm partition optimization directly on the calibration data used for nonconformity scores renders the partitions data-dependent and can invalidate the exchangeability assumption required for marginal coverage guarantees in conformal prediction. To address this rigorously, we will revise the method to reserve an independent hold-out set exclusively for the genetic-algorithm optimization of state-space partitions. Conformal prediction quantiles and bounds will then be computed on the remaining calibration data. We will update §3.2 with the revised procedure and add a brief discussion confirming that this split restores the standard coverage guarantees. revision: yes

  2. Referee: [Evaluation] Evaluation (case-study results): the abstract asserts reduced conservatism on two complementary case studies, yet the manuscript provides neither quantitative bound-width comparisons, coverage-frequency tables, error-bar statistics, nor explicit verification-time numbers that would allow the reader to verify the claimed improvement over standard CP. These metrics are load-bearing for the central empirical claim.

    Authors: We acknowledge that the current presentation of the case-study results does not include the quantitative metrics needed to substantiate the claims of reduced conservatism. In the revised manuscript we will add (i) tables reporting average and worst-case bound widths for state-dependent versus standard conformal prediction, (ii) coverage-frequency tables with error bars obtained from repeated random splits, and (iii) explicit wall-clock verification times for the branch-merging reachability algorithm on both case studies. These additions will be placed in the evaluation section and will directly support the abstract claims. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation adapts standard CP with independent partitioning step

full rationale

The paper extends conformal prediction by using a genetic algorithm to partition the state space and tighten perception-error bounds, then combines the resulting sets with a branch-merging reachability procedure. This construction does not reduce any claimed bound or coverage guarantee to a quantity that is definitionally identical to its own inputs or to a fitted parameter that is merely renamed as a prediction. The optimization of partitions is presented as an empirical means to exploit state dependence rather than a self-referential loop, and the overall verification pipeline retains independent content from the calibration data and the symbolic reachability component. No self-citation load-bearing step, uniqueness theorem imported from the authors, or ansatz smuggled via prior work is required for the central claims. The method therefore remains self-contained against external conformal-prediction benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on the standard validity guarantees of conformal prediction under exchangeability and on the correctness of reachability analysis for the resulting hybrid system; no new physical entities or ad-hoc constants are introduced in the abstract.

axioms (2)
  • domain assumption Conformal prediction yields valid coverage guarantees under the exchangeability assumption for the calibration and test data
    Standard assumption invoked by any conformal prediction method; required for the high-confidence bounds to hold.
  • domain assumption Reachability analysis on the hybrid system obtained after inserting the conformal bounds produces sound over-approximations of reachable sets
    Core assumption of symbolic verification methods used to combine the statistical bounds with formal analysis.

pith-pipeline@v0.9.0 · 5541 in / 1399 out tokens · 64377 ms · 2026-05-17T02:06:58.957970+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

77 extracted references · 77 canonical work pages

  1. [1]

    Abhijeet Agnihotri, Matthew O’Kelly, Rahul Mangharam, and Houssam Abbas. 2020. Teaching Autonomous Systems at 1/10th-scale: Design of the F1/10 Racecar, Simulators and Curriculum. InProceedings of the 51st ACM Technical Symposium on Computer Science Education(Portland, OR, USA) (SIGCSE ’20). Association for Computing Machinery, New York, NY, USA, 657–663....

    work page doi:10.1145/3328778.3366796 2020

  2. [2]

    Matthias Althoff. 2015. An Introduction to CORA 2015.ARCH@ CPSWeek34 (2015), 120–151

    work page 2015

  3. [3]

    R. Alur. 2011. Formal verification of hybrid systems.Communications of the ACM / selected conference paper(2011). Survey; discusses scalability challenges

    work page 2011

  4. [4]

    Anastasios Angelopoulos, Emmanuel Candes, and Ryan J Tibshirani. 2023. Conformal pid control for time series prediction.Advances in neural information processing systems36 (2023), 23047–23074

    work page 2023

  5. [5]

    Anastasios N Angelopoulos, Stephen Bates, et al. 2023. Conformal prediction: A gentle introduction.Foundations and Trends®in Machine Learning 16, 4 (2023), 494–591

    work page 2023

  6. [6]

    M. S. Arulampalam, S. Maskell, N. Gordon, and T. Clapp. 2002. A tutorial on particle filters for online nonlinear/non-Gaussian Bayesian tracking. IEEE Transactions on Signal Processing50, 2 (2002), 174–188

    work page 2002

  7. [7]

    2024.GM Cruise robotaxi made technical errors in pedestrian crash

    Automotive News Europe. 2024.GM Cruise robotaxi made technical errors in pedestrian crash. https://europe.autonews.com/automakers/gm-cruise- robotaxi-made-technical-errors-pedestrian-crash Accessed: 2025-10-13

    work page 2024

  8. [8]

    Christopher M. Bishop. 2006.Pattern Recognition and Machine Learning. Springer

    work page 2006

  9. [9]

    Radu Calinescu, Calum Imrie, Ravi Mangal, Genaína Nunes Rodrigues, Corina Păsăreanu, Misael Alpizar Santana, and Gricel Vázquez. 2024. Controller Synthesis for Autonomous Systems With Deep-Learning Perception Components.IEEE Transactions on Software Engineering(2024). https://www.computer.org/csdl/journal/ts/2024/06/10496502/1W28Vqz3hQc

    work page 2024

  10. [10]

    2025.Waymo recalls 672 autonomous vehicles after crash with utility pole

    Car Industry News. 2025.Waymo recalls 672 autonomous vehicles after crash with utility pole. https://carindust.com/news/362/waymo-recalls-672- autonomous-vehicles-after-crash-with-utility-pole Accessed: 2025-10-13

    work page 2025

  11. [11]

    Kaustav Chakraborty and Somil Bansal. 2023. Discovering closed-loop failures of vision-based controllers via reachability analysis.IEEE Robotics and Automation Letters8, 5 (2023), 2692–2699

    work page 2023

  12. [12]

    Silva, M

    Kong Yao Chee, Thales C. Silva, M. Ani Hsieh, and George J. Pappas. 2024. Uncertainty quantification and robustification of model-based controllers using conformal prediction. InProceedings of the 6th Annual Learning for Dynamics & Control Conference (Proceedings of Machine Learning Research, Vol. 242), Alessandro Abate, Mark Cannon, Kostas Margellos,...

    work page 2024

  13. [13]

    Xin Chen, Erika Abraham, and Sriram Sankaranarayanan. 2012. Taylor model flowpipe construction for non-linear hybrid systems. In2012 IEEE 33rd Real-Time Systems Symposium. IEEE, 183–192

    work page 2012

  14. [14]

    Matthew Cleaveland, Insup Lee, George J Pappas, and Lars Lindemann. 2024. Conformal prediction regions for time series using linear complemen- tarity programming. InProceedings of the AAAI Conference on Artificial Intelligence, Vol. 38. 20984–20992

    work page 2024

  15. [15]

    Matthew Cleaveland, Lars Lindemann, Radoslav Ivanov, and George J. Pappas. 2022. Risk verification of stochastic systems with neural network controllers.Artificial Intelligence313 (2022), 103782. https://doi.org/10.1016/j.artint.2022.103782

    work page doi:10.1016/j.artint.2022.103782 2022

  16. [16]

    Matthew Cleaveland, Pengyuan Lu, Oleg Sokolsky, Insup Lee, and Ivan Ruchkin. 2025. Conservative Perception Models for Probabilistic Verification. InProc. of Allerton 2025. https://doi.org/10.48550/arXiv.2503.18077

    work page doi:10.48550/arxiv.2503.18077 2025

  17. [17]

    Sarah Dean, Nikolai Matni, Benjamin Recht, and Vickie Ye. 2020. Robust guarantees for perception-based control. InLearning for Dynamics and Control. PMLR, 350–360

    work page 2020

  18. [18]

    Souradeep Dutta, Xin Chen, and Sriram Sankaranarayanan. 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference. InProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. 157–168

    work page 2019

  19. [19]

    Dutta, S

    S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari. 2018. Output Range Analysis for Deep Feedforward Neural Networks. InNASA Formal Methods Symposium. Springer, 121–138

    work page 2018

  20. [20]

    Michael Everett. 2021. Neural network verification in control. In2021 60th IEEE Conference on Decision and Control (CDC). IEEE, 6326–6340

    work page 2021

  21. [21]

    Jiameng Fan, Chao Huang, Xin Chen, Wenchao Li, and Qi Zhu. 2020. Reachnn*: A tool for reachability analysis of neural-network controlled systems. InInternational Symposium on Automated Technology for Verification and Analysis. Springer, 537–542

    work page 2020

  22. [22]

    Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable verification of hybrid systems. InInternational Conference on Computer Aided Verification. Springer, 379–395

    work page 2011

  23. [23]

    Y. Gao, Z. Liu, J. Zhou, and M. Cannon. 2024.Robust reachability under uncertainty: propagation, computation, and applications. Survey chapter on reachability with uncertainty

    work page 2024

  24. [24]

    Yuang Geng, Jake Brandon Baldauf, Souradeep Dutta, Chao Huang, and Ivan Ruchkin. 2024. Bridging Dimensions: Confident Reachability for High-Dimensional Controllers. InInternational Symposium on Formal Methods. Springer, 381–402

    work page 2024

  25. [25]

    Bineet Ghosh and Parasara Sridhar Duggirala. 2019. Robust reachable set: Accounting for uncertainties in linear dynamical systems.ACM Transactions on Embedded Computing Systems (TECS)18, 5s (2019), 1–22

    work page 2019

  26. [26]

    Gymnasium. [n. d.]. Mountain Car. https://gymnasium.farama.org/environments/classic_control/mountain_car_continuous/

    work page

  27. [27]

    P Habeeb, Deepak D’Souza, Kamal Lodaya, and Pavithra Prabhakar. 2024. Interval image abstraction for verification of camera-based autonomous systems.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems43, 11 (2024), 4310–4321. Statistical-Symbolic Verification of Perception-Based Autonomous Systems 27

    work page 2024

  28. [28]

    Navid Hashemi, Lars Lindemann, and Jyotirmoy Deshmukh. 2025. PCA-DDReach: Efficient Statistical Reachability Analysis of Stochastic Dynamical Systems via Principal Component Analysis.arXiv preprint arXiv:2505.14935(2025)

    work page arXiv 2025

  29. [29]

    Deshmukh

    Navid Hashemi, Xin Qin, Lars Lindemann, and Jyotirmoy V. Deshmukh. 2023. Data-Driven Reachability Analysis of Stochastic Dynamical Systems with Conformal Inference. arXiv:2309.09187 [eess.SY] https://arxiv.org/abs/2309.09187

    work page arXiv 2023

  30. [30]

    Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li, and Qi Zhu. 2022. POLAR: A polynomial arithmetic framework for verifying neural-network controlled systems. InInternational Symposium on Automated Technology for Verification and Analysis. Springer, 414–430

    work page 2022

  31. [31]

    Chao Huang, Jiameng Fan, Wenchao Li, Xin Chen, and Qi Zhu. 2019. Reachnn: Reachability analysis of neural-network controlled systems.ACM Transactions on Embedded Computing Systems (TECS)18, 5s (2019), 1–22

    work page 2019

  32. [32]

    Radoslav Ivanov, Taylor Carpenter, James Weimer, Rajeev Alur, George Pappas, and Insup Lee. 2021. Verisig 2.0: Verification of neural network controllers using taylor model preconditioning. InComputer Aided Verification: 33rd International Conference, CA V 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I. Springer, 249–262

    work page 2021

  33. [33]

    Ivanov, T

    R. Ivanov, T. Carpenter, J. Weimer, R. Alur, G. J. Pappas, and I. Lee. 2020. Case Study: Verifying the Safety of an Autonomous Racing Car with a Neural Network Controller. InInternational Conference on Hybrid Systems: Computation and Control

    work page 2020

  34. [34]

    Radoslav Ivanov, James Weimer, Rajeev Alur, George J Pappas, and Insup Lee. 2019. Verisig: verifying safety properties of hybrid systems with neural network controllers. InProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. 169–178

    work page 2019

  35. [35]

    Saber Jafarpour, Zishun Liu, and Yongxin Chen. 2024. Probabilistic reachability analysis of stochastic control systems.arXiv preprint arXiv:2407.12225 (2024)

    work page arXiv 2024

  36. [36]

    G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. 2017. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification. Springer, 97–117

    work page 2017

  37. [37]

    Sydney M Katz, Anthony L Corso, Christopher A Strong, and Mykel J Kochenderfer. 2022. Verification of image-based neural network controllers using generative models.Journal of Aerospace Information Systems19, 9 (2022), 574–584

    work page 2022

  38. [38]

    Shayan Kiyani, George Pappas, and Hamed Hassani. 2024. Length optimization in conformal prediction.arXiv preprint arXiv:2406.18814(2024)

    work page arXiv 2024

  39. [39]

    Marta Kwiatkowska, Gethin Norman, and David Parker. 2002. PRISM: Probabilistic Symbolic Model Checker. InComputer Performance Evaluation: Modelling Techniques and Tools, Tony Field, Peter G. Harrison, Jeremy Bradley, and Uli Harder (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 200–204

    work page 2002

  40. [40]

    Jordan Lekeufack, Anastasios N Angelopoulos, Andrea Bajcsy, Michael I Jordan, and Jitendra Malik. 2024. Conformal decision theory: Safe autonomous decisions from imperfect predictions. In2024 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 11668–11675

    work page 2024

  41. [41]

    Thomas Lew, Lucas Janson, Riccardo Bonalli, and Marco Pavone. 2022. A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis. InProceedings of The 4th Annual Learning for Dynamics and Control Conference (Proceedings of Machine Learning Research, Vol. 168), Roya Firoozi, Negar Mehr, Esen Yel, Rika Antonova, Jeannette Bohg, Mac Schw...

    work page 2022

  42. [42]

    Albert Lin and Somil Bansal. 2024. Verification of neural reachable tubes via scenario optimization and conformal prediction. In6th Annual Learning for Dynamics & Control Conference. PMLR, 719–731

    work page 2024

  43. [43]

    Lars Lindemann, Matthew Cleaveland, Gihyun Shim, and George J Pappas. 2023. Safe planning in dynamic environments using conformal prediction. IEEE Robotics and Automation Letters(2023)

    work page 2023

  44. [44]

    Lars Lindemann, Yiqi Zhao, Xinyi Yu, George J Pappas, and Jyotirmoy V Deshmukh. 2024. Formal verification and control with conformal prediction. arXiv preprint arXiv:2409.00536(2024)

    work page arXiv 2024

  45. [45]

    Moussa Maiga, Nacim Ramdani, Louise Travé-Massuyès, and Christophe Combastel. 2015. A comprehensive method for reachability analysis of uncertain nonlinear hybrid systems.IEEE Trans. Automat. Control61, 9 (2015), 2341–2356

    work page 2015

  46. [46]

    Kyoko Makino and Martin Berz. 2003. Taylor models and other validated functional inclusion methods.International Journal of Pure and Applied Mathematics6 (2003), 239–316

    work page 2003

  47. [47]

    2019.Genetic Algorithm

    Seyedali Mirjalili. 2019.Genetic Algorithm. Springer. 43–55 pages. https://doi.org/10.1007/978-3-319-93025-1_4

    work page doi:10.1007/978-3-319-93025-1_4 2019

  48. [48]

    Seshia, Ravi Mangal, Yangge Li, Christopher Watson, Divya Gopinath, and Huafeng Yu

    Sayan Mitra, Corina Păsăreanu, Pavithra Prabhakar, Sanjit A. Seshia, Ravi Mangal, Yangge Li, Christopher Watson, Divya Gopinath, and Huafeng Yu. 2025. Formal Verification Techniques for Vision-Based Autonomous Systems – A Survey. InPrinciples of Verification: Cycling the Probabilistic Landscape : Essays Dedicated to Joost-Pieter Katoen on the Occasion of ...

    work page doi:10.1007/978-3-031-75778-5_5 2025

  49. [49]

    Anish Muthali, Haotian Shen, Sampada Deglurkar, Michael H Lim, Rebecca Roelofs, Aleksandra Faust, and Claire Tomlin. 2023. Multi-agent reachability calibration with conformal prediction. In2023 62nd IEEE Conference on Decision and Control (CDC). IEEE, 6596–6603

    work page 2023

  50. [50]

    Roberto I Oliveira, Paulo Orenstein, Thiago Ramos, and Joao Vitor Romano. 2024. Split conformal prediction and non-exchangeable data.Journal of Machine Learning Research25, 225 (2024), 1–38

    work page 2024

  51. [51]

    2018.Hands-On Intelligent Agents with OpenAI Gym: Your guide to developing AI agents using deep reinforcement learning

    Praveen Palanisamy. 2018.Hands-On Intelligent Agents with OpenAI Gym: Your guide to developing AI agents using deep reinforcement learning. Packt Publishing Ltd

    work page 2018

  52. [52]

    Pasareanu, Ravi Mangal, Divya Gopinath, Sinem Getir Yaman, Calum Imrie, Radu Calinescu, and Huafeng Yu

    Corina S. Pasareanu, Ravi Mangal, Divya Gopinath, Sinem Getir Yaman, Calum Imrie, Radu Calinescu, and Huafeng Yu. 2023. Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study. InComputer Aided Verification (Lecture Notes in Computer Science). Springer Nature Switzerland, Cham, 289–303. https://doi.org/10.1007/978-3-031-37706-8_15 28 Geng et al

    work page doi:10.1007/978-3-031-37706-8_15 2023

  53. [53]

    Jordan Peper, Yan Miao, Sayan Mitra, and Ivan Ruchkin. 2025. Towards Unified Probabilistic Verification and Validation of Vision-Based Autonomy. InAutomated Technology for Verification and Analysis. Springer Nature Switzerland, Cham, 231–259. https://doi.org/10.1007/978-3-032-08707-2_11

    work page doi:10.1007/978-3-032-08707-2_11 2025

  54. [54]

    Nacim Ramdani, Nacim Meslem, and Yves Candau. 2009. A hybrid bounding method for computing an over-approximation for the reachable set of uncertain nonlinear systems.IEEE Transactions on automatic control54, 10 (2009), 2352–2364

    work page 2009

  55. [55]

    RoboRacer. 2025. RoboRacer. https://roboracer.ai/. Accessed: 2025-10-13

    work page 2025

  56. [56]

    Serve Robotics. 2025. Serve Robotics. https://www.serverobotics.com/. Accessed: 2025-10-13

    work page 2025

  57. [57]

    Yaniv Romano, Evan Patterson, and Emmanuel Candes. 2019. Conformalized quantile regression.Advances in neural information processing systems 32 (2019)

    work page 2019

  58. [58]

    Ulices Santa Cruz and Yasser Shoukry. 2023. Certified vision-based state estimation for autonomous landing systems using reachability analysis. In 2023 62nd IEEE Conference on Decision and Control (CDC). IEEE, 6052–6057

    work page 2023

  59. [59]

    Sushmita Sarker, Prithul Sarker, Gunner Stone, Ryan Gorman, Alireza Tavakkoli, George Bebis, and Javad Sattarvand. 2024. A comprehensive overview of deep learning techniques for 3D point cloud classification and semantic segmentation.Machine Vision and Applications35, 4 (2024), 67

    work page 2024

  60. [60]

    Glenn Shafer and Vladimir Vovk. 2008. A tutorial on conformal prediction.Journal of Machine Learning Research9, 3 (2008)

    work page 2008

  61. [61]

    Apoorva Sharma, Sushant Veer, Asher Hancock, Heng Yang, Marco Pavone, and Anirudha Majumdar. 2024. PAC-Bayes generalization certificates for learned inductive conformal prediction.Advances in Neural Information Processing Systems36 (2024)

    work page 2024

  62. [62]

    Taleb et al

    R. Taleb et al . 2023. Uncertainty in runtime verification: A survey.Science of Computer Programming(2023). Survey on monitoring with incomplete/noisy traces

    work page 2023

  63. [63]

    Sebastian Thrun. [n. d.]. Probabilistic robotics. 45, 3 ([n. d.]), 52–57. https://doi.org/10.1145/504729.504754

    work page doi:10.1145/504729.504754

  64. [64]

    H. Tran, S. Bak, W. Xiang, and T. T. Johnson. 2020. Verification of Deep Convolutional Neural Networks Using ImageStars. In32nd International Conference on Computer-Aided Verification (CA V). Springer

    work page 2020

  65. [65]

    Renukanandan Tumu, Matthew Cleaveland, Rahul Mangharam, George Pappas, and Lars Lindemann. 2024. Multi-modal conformal prediction regions by optimizing convex shape templates. In6th Annual Learning for Dynamics & Control Conference. PMLR, 1343–1356

    work page 2024

  66. [66]

    VoloCity. [n. d.]. VoloCity:The air taxi that’s a cut above. https://www.volocopter.com/en/solutions/volocity

    work page

  67. [67]

    2005.Algorithmic learning in a random world

    Vladimir Vovk, Alexander Gammerman, and Glenn Shafer. 2005.Algorithmic learning in a random world. Vol. 29. Springer

    work page 2005

  68. [68]

    Thomas Waite, Yuang Geng, Trevor Turnquist, Ivan Ruchkin, and Radoslav Ivanov. 2025. State-Dependent Conformal Perception Bounds for Neuro-Symbolic Verification of Autonomous Systems. arXiv:2502.21308 [eess.SY] https://arxiv.org/abs/2502.21308

    work page arXiv 2025

  69. [69]

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. 2021. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification.Advances in Neural Information Processing Systems34 (2021)

    work page 2021

  70. [70]

    Yixuan Wang, Weichao Zhou, Jiameng Fan, Zhilu Wang, Jiajun Li, Xin Chen, Chao Huang, Wenchao Li, and Qi Zhu. 2023. Polar-express: Efficient and precise formal reachability analysis of neural-network controlled systems.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems43, 3 (2023), 994–1007

    work page 2023

  71. [71]

    Waymo. [n. d.]. Waymo: The World’s Most Experienced Driver. https://waymo.com/

    work page

  72. [72]

    Chen Xu and Yao Xie. 2023. Conformal Prediction for Time Series.IEEE Transactions on Pattern Analysis and Machine Intelligence45, 10 (2023), 11575–11587. https://doi.org/10.1109/TPAMI.2023.3272339

    work page doi:10.1109/tpami.2023.3272339 2023

  73. [73]

    Shuo Yang, George J Pappas, Rahul Mangharam, and Lars Lindemann. 2023. Safe perception-based control under stochastic sensor uncertainty using conformal prediction. In2023 62nd IEEE Conference on Decision and Control (CDC). IEEE, 6072–6078

    work page 2023

  74. [74]

    Hakan Yildiz and Subhash Suri. 2012. On Klee’s measure problem for grounded boxes. InProceedings of the twenty-eighth annual symposium on computational geometry. 111–120

    work page 2012

  75. [75]

    Yunchuan Zhang, Sangwoo Park, and Osvaldo Simeone. 2024. Bayesian optimization with formal safety guarantees via online conformal prediction. IEEE Journal of Selected Topics in Signal Processing(2024)

    work page 2024

  76. [76]

    Yiqi Zhao, Bardh Hoxha, Georgios Fainekos, Jyotirmoy V Deshmukh, and Lars Lindemann. 2024. Robust conformal prediction for STL runtime verification under distribution shift. In2024 ACM/IEEE 15th International Conference on Cyber-Physical Systems (ICCPS). IEEE, 169–179

    work page 2024

  77. [77]

    Yanfei Zhou, Lars Lindemann, and Matteo Sesia. 2024. Conformalized adaptive forecasting of heterogeneous trajectories.arXiv preprint arXiv:2402.09623(2024)

    work page arXiv 2024