Formal Verification and Control with Conformal Prediction

TL;DR

This paper surveys the use of conformal prediction as a lightweight, general, and efficient method for formal verification and control in autonomous systems, especially those with learning-enabled components, offering safety guarantees.

Contribution

It introduces conformal prediction as a novel, practical approach for verification and control in complex autonomous systems, contrasting it with existing statistical techniques.

Findings

CP is simple, adaptable, and real-time capable.

CP provides formal safety guarantees without assumptions on data.

The survey covers verification, control, and robotics applications.

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.