Learning-based methods provide a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. To ensure the satisfaction of a safety property, learning-based methods jointly learn a control policy together with a certificate function for the property. Popular examples include barrier functions for safety and Lyapunov functions for asymptotic stability. While there has been significant progress on learning-based control with certificate functions in the white-box setting, where the correctness of the certificate function can be formally verified, there has been little work on ensuring their reliability in the black-box setting where the system dynamics are unknown. In this work, we consider the problems of certifying and repairing neural network control policies and certificate functions in the black-box setting. We propose a novel framework that utilizes runtime monitoring to detect system behaviors that violate the property of interest under some initially trained neural network policy and certificate. These violating behaviors are used to extract new training data, that is used to re-train the neural network policy and the certificate function and to ultimately repair them. We demonstrate the effectiveness of our approach empirically by using it to repair and to boost the safety rate of neural network policies learned by a state-of-the-art method for learning-based control on two autonomous system control tasks.
翻译:基于学习的方法为解决高度非线性控制任务提供了一种前景广阔的途径,这类任务对经典控制方法而言往往具有挑战性。为确保满足安全性要求,基于学习的方法会联合学习控制策略以及该性质对应的证书函数。常见的例子包括用于安全性的屏障函数和用于渐近稳定性的李雅普诺夫函数。尽管在白盒设置下(即证书函数的正确性可被形式化验证)基于学习的控制与证书函数研究已取得显著进展,但在黑盒设置下(即系统动态未知)确保其可靠性的工作却鲜有开展。在本工作中,我们研究了黑盒设置下神经网络控制策略与证书函数的验证与修复问题。我们提出了一种新颖框架,该框架利用运行时监控来检测在初始训练的神经网络策略及证书下违反目标性质的系统行为。这些违规行为被用于提取新的训练数据,进而重新训练神经网络策略与证书函数,最终实现修复。我们通过将所提方法应用于两个自主系统控制任务,对通过当前最先进的基于学习控制方法所获得的神经网络策略进行修复并提升其安全率,实证验证了本方法的有效性。