Formal verification of neural network controlled autonomous systems
Formal verification of neural network controlled autonomous systems
复制标题
DOI：
10.1145/3302504.3311802
复制
发表时间：
2018-10
期刊：
影响因子：
--
通讯作者：
Xiaowu Sun;Haitham Khedr;Yasser Shoukry
中科院分区：
文献类型：
--
作者：
Xiaowu Sun;Haitham Khedr;Yasser Shoukry
在本文中，我们考虑的问题，正式验证的安全性的自主机器人配备了神经网络（NN）控制器，处理激光雷达图像产生的控制行动。给定一个工作空间，其特征在于由一组多面体障碍物，我们的目标是计算一组安全的初始状态，这样的机器人轨迹从这些初始状态开始，保证避开障碍物。我们的方法是构造一个有限状态抽象的系统，并使用标准的可达性分析的有限状态抽象计算的安全初始状态。为了对将机器人位置映射到激光雷达图像的成像函数进行数学建模，我们引入了工作空间的成像适应分区的概念，其中保证成像函数是仿射的。考虑到这种工作空间划分，机器人的离散时间线性动力学以及具有整流线性单元（ReLU）非线性的预训练NN控制器，我们利用可满足性模凸（SMC）编码来枚举不同ReLU的所有可能分配。为了加速这一过程，我们开发了一种预处理算法，可以快速修剪可行的ReLU分配空间。最后，我们证明了所提出的算法的效率，使用数值模拟的神经网络控制器的复杂性不断增加。
In this paper, we consider the problem of formally verifying the safety of an autonomous robot equipped with a Neural Network (NN) controller that processes LiDAR images to produce control actions. Given a workspace that is characterized by a set of polytopic obstacles, our objective is to compute the set of safe initial states such that a robot trajectory starting from these initial states is guaranteed to avoid the obstacles. Our approach is to construct a finite state abstraction of the system and use standard reachability analysis over the finite state abstraction to compute the set of safe initial states. To mathematically model the imaging function, that maps the robot position to the LiDAR image, we introduce the notion of imaging-adapted partitions of the workspace in which the imaging function is guaranteed to be affine. Given this workspace partitioning, a discrete-time linear dynamics of the robot, and a pre-trained NN controller with Rectified Linear Unit (ReLU) non-linearity, we utilize a Satisfiability Modulo Convex (SMC) encoding to enumerate all the possible assignments of different ReLUs. To accelerate this process, we develop a pre-processing algorithm that could rapidly prune the space of feasible ReLU assignments. Finally, we demonstrate the efficiency of the proposed algorithms using numerical simulations with the increasing complexity of the neural network controller.