arXiv:2409.00536eess.SYcs.RO2024-09被引 52

用置信预测实现自主系统安全验证与控制,无需复杂假设。

Formal Verification and Control with Conformal Prediction

  • 用置信预测量化学习组件不确定性,支持形式化验证
  • 实现实时安全控制与离线/在线验证算法,适配复杂任务需求
  • 方法简单通用高效,适合非专家快速应用到机器人系统

本文介绍基于置信预测(Conformal Prediction, CP)在自主系统形式化验证与控制方面的最新进展,为学习型自主系统(LEASs)提供实际的安全保障。由于学习型组件(LECs)的复杂性,传统基于模型的验证与控制方法面临瓶颈。本文提出以CP作为轻量级替代方案,其无需对学习模型或数据分布做假设,具有易理解、易实现、实时性强等优点。文中展示了如何利用CP进行LEC的形式化验证、安全控制设计,以及针对LEASs的离线与在线验证算法,并构建统一框架应对系统复杂性。涵盖从简单导航任务到基于时序逻辑的复杂任务要求。通过与场景优化、PAC-Bayes理论对比,揭示了其在验证与控制中的优势与局限。最后指出未来研究的关键开放问题与前景方向。

原文摘要 · Abstract (English)

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.

形式化验证置信预测自主系统安全控制

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。