基于场景优化与保形预测的神经可达管验证

基于学习的安全关键系统控制方法正迅速普及，因此确保其性能与安全性至关重要。Hamilton-Jacobi (HJ) 可达性分析是一种流行的形式化验证工具，可提供此类保证，因为它能够处理一般的非线性系统动力学、有界对抗性系统扰动以及状态和输入约束。然而，其计算和内存复杂度随状态维度呈指数级增长，使其在大规模系统中难以处理。为克服这一挑战，DeepReach等神经方法已被用于为高维系统合成可达管和安全控制器。然而，验证这些神经可达管仍具挑战性。在本工作中，我们提出了两种基于鲁棒场景优化和保形预测的验证方法，为神经可达管提供概率安全保证。我们的方法允许在神经管中异常值误差（这在基于学习的方法中不可避免）的鲁棒性与概率安全保证的强度之间进行直接权衡。此外，我们证明了split conformal prediction（机器学习社区中广泛使用的不确定性量化方法）可归约为基于场景的方法，使得这两种方法不仅在神经可达管验证中是等价的，而且在更一般的情况下也是等价的。据我们所知，我们的证明是文献中首个展示保形预测与场景优化之间存在强联系的工作。最后，我们提出了一种异常值调整的验证方法，该方法利用神经可达管中的误差分布来恢复更大的安全体积。我们通过多车避碰和带禁飞区的火箭着陆等高维问题，展示了所提方法的有效性。