基于保形预测的形式化验证与控制
Formal Verification and Control with Conformal Prediction
AI总结：
本综述系统介绍了保形预测在自主系统形式化验证与安全控制中的应用，展示其作为轻量级统计工具如何应对学习使能组件的复杂性，并对比其他统计方法、展望未来研究方向。
摘要：
我们介绍了自主系统形式化验证与控制方面的最新进展，这些进展通过保形预测（CP）——一种用于不确定性量化的统计工具——实现了实用的安全保证。本综述尤其受到学习使能自主系统（LEASs）的推动，其中学习使能组件（LECs）的复杂性构成了应用传统基于模型的验证与控制技术的主要瓶颈。为应对这一挑战，我们主张将CP作为一种轻量级替代方案，并展示其在形式化验证、系统与控制以及机器人学中的应用。CP具有吸引力，原因在于其简单性（易于理解、实现和适配）、通用性（无需对学习模型和底层数据分布作任何假设）以及高效性（具备实时能力且准确）。本综述为有兴趣将CP应用于自主性问题的非专业人士提供了易于理解的CP入门介绍。我们特别展示了如何利用CP对LECs进行形式化验证、设计安全控制，以及为LEASs设计离线和在线验证算法。我们在一个统一的框架内介绍这些技术，以应对LEASs的复杂性。我们的阐述涵盖从简单的规范（如机器人导航任务）到以时序逻辑表达的复杂任务需求。在整个综述中，我们将CP与其他统计技术（包括场景优化和PAC-Bayes理论）进行对比，突出其在验证与控制方面的优势与局限。最后，我们概述了未解决的问题以及未来研究的有前景方向。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
