Neural networks serve as effective controllers in a variety of complex settings due to their ability to represent expressive policies. The complex nature of neural networks, however, makes their output difficult to verify and predict, which limits their use in safety-critical applications. While simulations provide insight into the performance of neural network controllers, they are not enough to guarantee that the controller will perform safely in all scenarios. To address this problem, recent work has focused on formal methods to verify properties of neural network outputs. For neural network controllers, we can use a dynamics model to determine the output properties that must hold for the controller to operate safely. In this work, we develop a method to use the results from neural network verification tools to provide probabilistic safety guarantees on a neural network controller. We develop an adaptive verification approach to efficiently generate an overapproximation of the neural network policy. Next, we modify the traditional formulation of Markov decision process (MDP) model checking to provide guarantees on the overapproximated policy given a stochastic dynamics model. Finally, we incorporate techniques in state abstraction to reduce overapproximation error during the model checking process. We show that our method is able to generate meaningful probabilistic safety guarantees for aircraft collision avoidance neural networks that are loosely inspired by Airborne Collision Avoidance System X (ACAS X), a family of collision avoidance systems that formulates the problem as a partially observable Markov decision process (POMDP).
翻译:神经网络因其代表表达政策的能力而成为各种复杂环境中的有效控制器。但是,神经网络的复杂性使得其输出难以核查和预测,从而限制其在安全关键应用中的使用。模拟为神经网络控制器的性能提供了洞察力,但不足以保证控制器在所有情况下都能安全地运行。为了解决这一问题,最近的工作侧重于核实神经网络输出输出的特性的正式方法。对于神经网络控制器,我们可以使用动态模型来确定控制器必须安全操作的输出特性。在这项工作中,我们开发了一种方法,用神经网络核查工具的结果为神经网络控制器提供概率性安全保障。我们开发了一种适应性核查方法,以有效地产生对神经网络政策的过度兼容性。接下来,我们修改了Markov决策程序(MDP)模式的传统的配置,以根据一个随机相容动态动态模型,为过近的政策提供保障。最后,我们将一些技术引入国家抽象性,以降低神经网络控制器的稳定性保障。在测试模型期间,我们通过安全性地模拟了一种安全性稳定的系统。