Combining Reachable Set Computation with Neuron Coverage

Abstract

As the use of Deep Neural Networks (DNN) continues to increase in the field of Cyber Physical Systems (CPS), we need more methods of guaranteeing their safety. Two recent areas of research into safety of DNNs have been in reachability analysis and neuron coverage. Reachability analysis takes a high dimensional input set, such as hyperrectangles or polytopes, and propagates it through the network to create an output set, and certain properties are tested on the output set to verify the safety of the network. Neuron coverage takes an input set in and measures what proportion of the overall network’s logic is tested by the input set, with the goal of finding corner cases in DNN.

In my thesis, I first propose a method for computing the volume of the star input set, which is a representation of polytopes used in reachability analysis. By computing the volume, we can find a general idea of how much of the overall input space is tested for by a given input set. Secondly, I propose a method for computing neuron coverage for reachable sets. Currently, neuron coverage is only used to test individual inputs, as opposed to continuous input sets, but in this paper, we extend the definition so that we can compute neuron coverage on sets such as the star set. We implement these techniques in the Neural Network Verification (NNV) toolbox, and test it on examples, such as the Aircraft Collision Avoidance System for unmanned aircraft (ACAS Xu).