Formal Verification and Control with Conformal Prediction

Motivation

The design of learning-enabled cyber-physical systems promises to enable many future technologies such as autonomous driving, intelligent transportation, and robotics. Over the past years, much progress was made in the design of learning-enabled components (LECs), e.g., for perception tasks such as object detection, localization and state estimation, trajectory prediction, for decision-making tasks such as motion and behavior planning, and for low-level nonlinear control. However, the integration of LECs into safety-critical cyber-physical systems is limited by their fragility that can result in unsafe system behavior, e.g., inaccurate and non-robust object detectors in self-driving cars. The fragility of LECs is well documented and a result of highly nonconvex learning problems, distribution shifts from training to deployment domain, and lack of model robustness. For these reasons, we require verifiable frameworks for the use of LECs in cyber-physical systems, ultimately guaranteeing their safety. Towards this goal, the overall theme of this tutorial is on designing formal verification and control algorithms for learning-enabled cyber-physical systems (LE-CPSs) with practical safety guarantees by using conformal prediction. Conformal prediction is a  statistical tool for uncertainty quantification, originally introduced by Shafer and Vovk  (see https://www.jmlr.org/papers/volume9/shafer08a/shafer08a.pdf), which has recently gained much attention within the machine learning community,  e.g., with a keynote talk on conformal prediction at NeurIPS 2022. By practical safety guarantees, we mean that these algorithms:  (1) are applicable and scale to complex LE-CPSs, (2) come with formal correctness guarantees, and (3) are easy to understand and extend, even for a novice in the field. 

Goals and Tentative Schedule

The tutorial will largely be based on our recent survey article "Formal Verification and Control with Conformal Prediction: Practical Saftey Guarantees for Autonomous Systems" (see https://arxiv.org/pdf/2409.00536). In the first part of the tutorial, we provide an introduction to conformal prediction. This will include the mathematical foundations as well as minimal coding examples that attendees can download and replicate. This will allow attendees to directly verify the presented theoretical results, and the code can be used as a building block for the attendees' own future projects. In the second part of the tutorial, we discuss three topics that are of great relevance for designing safe LE-CPS: (1) verification of LECs (again including simple coding examples), (2) control synthesis for LE-CPS, and (3) verification of LE-CPS. We envision a half day workshop with the following tentative schedule.

Expected Outcomes

The expected outcomes of the tutorial are three-fold: (1) familiarizing the CPS/IoT community with the concept of conformal prediction, and more broadly with uncertainty quantification tools, (2) dissemination of theoretical and computational frameworks for formal verification and control of LE-CPS with conformal prediction, (3) engaging the wider CPS/IoT community and foster discussion on open problems, challenges, and research direction. 

As described above, these outcomes will be implemented via lectures by the organizers and coding examples. We will give sufficient time for discussions and engage the audience during the tutorial, during breaks, and before/after the tutorial. Our survey article "Formal Verification and Control with Conformal Prediction: Practical Saftey Guarantees for Autonomous Systems" (see https://arxiv.org/pdf/2409.00536) complements our lectures. All materials (lecture slides and coding examples) will be made publicly available.

Slides and code from the tutorial is available!

Slides from the tutorial are available for download here: https://tinyurl.com/38umrj94  

Code from the tutorial is available on github: https://github.com/zhaoy37/conformal_prediction_survey_codes

Organizers