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).
Safety Filtering While Training: Improving the Performance and Sample Efficiency of Reinforcement Learning Agents
University of Toronto（多伦多大学）；University of Toronto Robotics Institute（多伦多大学机器人研究所）；Vector Institute for Artificial Intelligence（向量人工智能研究所）；Technical University of Munich（慕尼黑工业大学）；Munich Institute for Robotics and Machine Intelligence（慕尼黑机器人与机器智能研究所）
Towards provable probabilistic safety for scalable embodied AI systems
Department of Automation, Tsinghua University（清华大学自动化系）；Beijing Academy of Artificial Intelligence（北京人工智能研究院）；School of Intelligence Science and Technology, Peking University（北京大学智能科学与技术学院）；School of Computer, Liaocheng University（聊城大学计算机学院）；Department of Automation, Southeast University（东南大学自动化学院）；Department of Mechanical and Aerospace Engineering, George Washington University（乔治华盛顿大学机械与航空航天工程系）；University of Michigan Transportation Research Institute（密歇根大学交通研究所）；Department of Civil and Environmental Engineering, University of Michigan（密歇根大学土木与环境工程系）
