Abstract
Designing provably safe control is a core problem in trustworthy autonomy. However, most prior work in this regard assumes either that the system dynamics are known or deterministic, or that the state and action space are finite, significantly limiting application scope. We address this limitation by developing a probabilistic verification framework for unknown dynamical systems which combines conformal prediction with reachability analysis. In particular, we use conformal prediction to obtain valid uncertainty intervals for the unknown dynamics at each time step, with reachability then verifying whether safety is maintained within the conformal uncertainty bounds. Next, we develop an algorithmic approach for training control policies that optimize nominal reward while also maximizing the planning horizon with sound probabilistic safety guarantees. We evaluate the proposed approach in seven safe control settings spanning four domains -- cartpole, lane following, drone control, and safe navigation -- for both affine and nonlinear safety specifications. Our experiments show that the policies we learn achieve the strongest provable safety guarantees while still maintaining high average reward.
Abstract (translated)
设计可证明安全的控制是可信自主系统中的核心问题。然而，先前大多数相关工作要么假设系统的动力学特性已知或为确定性的，要么假设状态和动作空间是有限的，这大大限制了应用范围。为了克服这一局限性，我们开发了一个针对未知动态系统的概率验证框架，该框架结合了符合预测（conformal prediction）与可达性分析（reachability analysis）。具体来说，通过使用符合预测来获得每个时间步中未知动力学的有效不确定性区间，并利用可达性分析验证在符合预测的不确定性范围内是否能维持安全性。接下来，我们开发了一种算法方法，用于训练控制策略，在优化名义奖励的同时最大化规划时间范围，并确保具有坚实的概率安全保证。 我们在七种不同的安全控制设置下评估了所提出的方法，这些设置涵盖了四个领域——倒立摆（cartpole）、车道跟随、无人机控制以及安全导航——并且针对仿射和非线性安全规范进行了测试。我们的实验结果表明，我们学习到的策略能够实现最强有力的可证明的安全保证，同时保持较高的平均奖励。 这段描述强调了开发一个适用于未知且具有不确定性的动态系统的概率验证框架的重要性，并展示了如何通过结合预测模型和安全性分析来优化控制策略，在确保安全的同时提高性能。这种方法为构建更加可靠、实用的自主系统提供了一种新途径。
URL
https://arxiv.org/abs/2602.03799
