REVIEW 10 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 10 Pith papers
-
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.
-
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.
-
Conformal Safety Shielding for Imperfect-Perception Agents
The paper introduces a conformal prediction-based shield for imperfect-perception agents and proves a global safety bound only for the simpler perfect-perception case.
-
Statistical Guarantees in Data-Driven Nonlinear Control: Conformal Robustness for Stability and Safety
The paper defines conformally robust CLF/CBF conditions and proves that controllers satisfying them keep the true system exponentially stable or safe for a finite horizon with probability at least 1-delta under an exc...
-
PCA-DDReach: Efficient Statistical Reachability Analysis of Stochastic Dynamical Systems via Principal Component Analysis
PCA-DDReach computes probabilistic reachable sets with conformal guarantees, using PCA to orient and shrink the error inflation region and segmented surrogate models to scale to high-dimensional long-horizon systems.
-
Predictive Red Teaming: Breaking Policies Without Breaking Robots
A generative image editing plus anomaly detection pipeline predicts a visuomotor policy's success-rate degradation across off-nominal environmental factors, with an average prediction error below 0.19 in hardware trials.
-
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.
Discussion (0). Continue with ORCID to comment.