Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance

“Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance” by Ahmed Irfan, Kyle D. Julian, Haoze Wu, Clark Barrett, Mykel J. Kochenderfer, Baoluo Meng, and James Lopez. In Proceedings of the 39^th Digital Avionics Systems Conference (DASC '20), Oct. 2020.

Abstract

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.

BibTeX entry:

@inproceedings{IJW+20,
   author = {Ahmed Irfan and Kyle D. Julian and Haoze Wu and Clark Barrett
	and Mykel J. Kochenderfer and Baoluo Meng and James Lopez},
   title = {Towards Verification of Neural Networks for Small Unmanned
	Aircraft Collision Avoidance},
   booktitle = {Proceedings of the {\it 39^{th}} Digital Avionics Systems
	Conference (DASC '20)},
   month = oct,
   year = {2020},
   doi = {10.1109/DASC50938.2020.9256616},
   url = {http://theory.stanford.edu/~barrett/pubs/IJW+20.pdf}
}

(This webpage was created with bibtex2web.)