Formal Verification and Control With Conformal Prediction: Practical Safety Guarantees For Autonomous Systems

The design of autonomous systems, which are becoming increasingly learning enabled, has attracted much attention within the research community. Research in this area promises to enable many future technologies, such as autonomous driving, intelligent transportation, and robotics. In recent years, great progress has been made in the design of learning-enabled components (LECs), for example, with neural networks for perception tasks, such as object detection [1], [2], localization and state estimation [3], [4], and trajectory prediction [5], [6], [7]; for decision-making tasks, such as motion and behavior planning [8], [9]; and for low-level control [10], [11], [12]. However, the integration of LECs into safety-critical autonomous systems is limited by their fragility and can result in unsafe behavior, for example, inaccurate and nonrobust object detectors in self-driving cars. The fragility of LECs is the result of highly nonconvex learning problems, distribution shifts from training to the deployment domain, and a lack of model robustness [13], [14]. Unfortunately, these safety challenges are further amplified by the complexity of modern autonomous systems that operate in uncertain and dynamic environments, where traditional approaches for localization and mapping may fail to provide guarantees, for example, simultaneous localization and mapping techniques [4], [15] or Kalman/particle filters [16], [17], [18].