Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance
Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance
复制标题
DOI：
10.1109/dasc50938.2020.9256616
复制
发表时间：
2020-10
期刊：
影响因子：
--
通讯作者：
A. Irfan;Kyle D. Julian;Haoze Wu;Clark W. Barrett;Mykel J. Kochenderfer;Baoluo Meng;J. Lopez
中科院分区：
文献类型：
--
作者：
A. Irfan;Kyle D. Julian;Haoze Wu;Clark W. Barrett;Mykel J. Kochenderfer;Baoluo Meng;J. Lopez
ACAS X飞机避免碰撞系统的家族使用大型数字查找表来做出决定。最近的工作使用了深层神经网络来近似和压缩避免碰撞表，模拟表明神经网络性能与原始表相当。因此，正在探索神经网络表示形式，以用于存储容量有限的小型飞机。但是，深神经网络的黑盒性质引起了安全问题，因为仿真结果并不详尽。这项工作通过应用正式方法来分析孤立和闭环系统中的碰撞避免神经网络的行为来解决这些问题。我们在一组特定的碰撞避免网络上评估了我们的方法，并表明，即使网络并不总是在本地稳健，他们的闭环行为也可以确保它们不会达到不安全（碰撞）状态。
The ACAS X family of aircraft collision avoidance systems uses large numeric lookup tables to make decisions. Recent work used a deep neural network to approximate and compress a collision avoidance table, and simulations showed that the neural network performance was comparable to the original table. Consequently, neural network representations are being explored for use on small aircraft with limited storage capacity. However, the black-box nature of deep neural networks raises safety concerns because simulation results are not exhaustive. This work takes steps towards addressing these concerns by applying formal methods to analyze the behavior of collision avoidance neural networks both in isolation and in a closed-loop system. We evaluate our approach on a specific set of collision avoidance networks and show that even though the networks are not always locally robust, their closed-loop behavior ensures that they will not reach an unsafe (collision) state.