REVIEW 16 cited by
Formal Verification and Control with Conformal Prediction
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
We present recent advances in formal verification and control for autonomous systems with practical safety guarantees enabled by conformal prediction (CP), a statistical tool for uncertainty quantification. This survey is particularly motivated by learning-enabled autonomous systems (LEASs), where the complexity of learning-enabled components (LECs) poses a major bottleneck for applying traditional model-based verification and control techniques. To address this challenge, we advocate for CP as a lightweight alternative and demonstrate its use in formal verification, systems and control, and robotics. CP is appealing due to its simplicity (easy to understand, implement, and adapt), generality (requires no assumptions on learned models and underlying data distributions), and efficiency (real-time capable and accurate). This survey provides an accessible introduction to CP for non-experts interested in applying CP to autonomy problems. We particularly show how CP can be used for formal verification of LECs and the design of safe control as well as offline and online verification algorithms for LEASs. We present these techniques within a unifying framework that addresses the complexity of LEASs. Our exposition spans simple specifications, such as robot navigation tasks, to complex mission requirements expressed in temporal logic. Throughout the survey, we contrast CP with other statistical techniques, including scenario optimization and PAC-Bayes theory, highlighting advantages and limitations for verification and control. Finally, we outline open problems and promising directions for future research.
Forward citations
Cited by 16 Pith papers
-
Conformal Risk-Averse Decision Making with Action Conditional Guarantee
Action-conditional conformal prediction sets provide per-action safety guarantees for risk-averse policies that optimize conditional value-at-risk through pinball-loss minimization.
-
A PAC-Bayes Approach for Controlling Unknown Linear Discrete-time Systems
PAC-Bayes framework derives high-probability performance bounds for learned controllers on unknown stochastic linear discrete-time systems and provides efficient algorithms for finite and infinite controller spaces.
-
Risk-Controlled Post-Processing of Decision Policies
Risk-controlled post-processing yields a threshold-structured policy that follows the baseline except where an oracle fallback sharply reduces conditional violation risk, achieving O(log n/n) expected excess risk in i...
-
Enhancing Conformal Prediction via Class Similarity
Adding a class-similarity penalty to conformal scores can shrink prediction sets and reduce the number of semantic groups they span.
-
Safe Planning in Interactive Environments via Iterative Policy Updates and Adversarially Robust Conformal Prediction
The work develops an iterative safe planner that adjusts conformal prediction bounds across policy updates via sensitivity analysis to maintain distribution-free safety guarantees despite interaction-induced distribut...
-
Uncertainty Quantification via Invariant-Measure Conformal Prediction
Proposes imCP framework that uses independent samples from the invariant measure of a Markov process for conformal calibration in one-step and multi-step predictions of learned dynamical systems.
-
PAC-Bayesian Certificates for Quadratic Closed-Loop Control
PAC-Bayesian bounds are derived for quadratic closed-loop control via SLS parameterization, yielding Chernoff certificates for posteriors over responses, a mean-response deployment result, and a data-driven learning a...
-
A PAC-Bayes Approach for Controlling Unknown Linear Discrete-time Systems
A PAC-Bayes method supplies high-probability bounds on the cost of any learned stochastic controller for unknown linear systems and gives efficient algorithms that work for both finite and infinite controller sets, in...
-
Statistical-Symbolic Verification of Perception-Based Autonomous Systems using State-Dependent Conformal Prediction
State-dependent conformal prediction with genetic-algorithm state partitioning and branch-merging reachability produces tighter high-confidence perception-error bounds for scalable verification of neurally controlled ...
-
Efficient Quantification of Time-Series Prediction Error: Optimal Selection Conformal Prediction
OSCP optimizes conformal prediction score offsets via MILP minimization of an empirical region-size proxy for time-series, with validity guarantees and reduced computation versus prior methods.
-
pacSTL: PAC-Bounded Signal Temporal Logic from Data-Driven Reachability Analysis
pacSTL composes PAC-bounded reachable sets with interval STL to compute spec-level robustness intervals that contain an unseen trajectory's robustness with probability ≥ 1−ε.
-
Conformal Predictive Monitoring for Multi-Modal Scenarios
GenQPM trains a diffusion surrogate of stochastic dynamics, partitions predicted trajectories by mode, and applies class-conditional conformalized quantile regression to issue mode-specific STL robustness intervals.
-
Multi-Agent Path Finding Among Dynamic Uncontrollable Agents with Statistical Safety Guarantees
CP-Solver integrates conformal prediction intervals into Enhanced Conflict-Based Search to give statistical collision-safety guarantees for multi-agent path finding among dynamic uncontrollable agents.
-
Conformal Contraction for Robust Nonlinear Control with Distribution-Free Uncertainty Quantification
A conformal-prediction-based contraction controller guarantees, with probability 1-alpha, that the tracking error stays below an explicit exponential bound despite unknown nonlinear uncertainty.
-
Finite-Sample Conformal Coverage Recovery via Fusion under Degraded Local Guarantees in Occupancy Map Estimation
Averaging per-agent conformal e-values with a per-neighborhood miscoverage budget restores the target coverage α in fused multi-robot occupancy maps under local stationarity and mixing assumptions.
-
Probably Approximately Correct (PAC) Guarantees for Data-Driven Reachability Analysis: A Theoretical and Empirical Comparison
Formal connections between PAC bounds for three data-driven reachability methods are established, with empirical results showing they are not interchangeable despite similarities.
Discussion (0). Sign in to comment.