*** Slides available here

Motivation

The design of learning-enabled cyber-physical systems (LE-CPSs) promises to enable many future technologies such as self-driving cars, autonomous space exploration, wildfire drones, and assistive 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 trajectory prediction, for decision-making tasks such as motion planning and nonlinear control, and for integration with generative AI and LLMs. 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., perception systems that are unreliable in off-nominal conditions. 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. 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.

Content

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 allows attendees to directly verify the 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 two topics that are of great relevance for designing safe LE-CPS: (1) control synthesis for LE-CPS (statistical abstractions of LECs for control synthesis), and (2) verification of LE-CPS (offline and runtime verification, reachable set estimation). 
 

Expected Outcomes

The expected outcomes of the tutorial are three-fold: (1) familiarizing the CPS 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-CPSs with conformal prediction, (3) engaging the wider CPS community and foster discussion on open problems, challenges, and research direction. All materials (lecture slides and coding examples) will be made publicly available on this homepage.

Organizers