Automated Verification For Neural Networks

This project falls within the EPSRC Verification and Correctness and Artificial Intelligence Technologies research areas.

The use of neural networks is becoming increasingly common, most significantly within safety-critical systems, such as object recognition in autonomous vehicles. These applications demand strict guarantees of safety and security that traditional testing methods cannot provide. Traditional testing does not span the set of all legal inputs and possible behaviours, whereas verification does and is able to provide these guarantees. Within current literature, concerns have been raised about image classification decisions being susceptible to adversarial perturbations of input images. These adversarial examples are often imperceptible to the human eye, but cause misclassification of the image. If the adversarial example is presented to an end-to-end-controller of an autonomous vehicle instead of a clean image, this could lead to the network making the wrong decision. The existing studies within this area have (i) focused on search for adversarial examples to estimate network's robustness, (ii) generated these examples for use in adversarial training, and (iii) argued that the examples are transferable to other networks. Only recently a new trend has emerged (http://qav.comlab.ox.ac.uk/bibitem.php?key=HKW+17, https://arxiv.org/abs/1702.01135), where verification methods were proposed that have the capability to provide guarantees that all adversarial examples will be found for a given input region. However, these methods are prohibitively expensive for larger images and networks, rely on heuristics, and are constrained to certain activation functions (e.g. ReLU) and network architectures (e.g. feed forward networks).

The aim of this project is to develop robust automated verification of neural networks. Within current methods, naïve exhaustive search for adversarial examples is unreasonable as it is too computationally expensive, and is not guaranteed to provide the necessary information to rectify the network if an example is found. One possible approach is to use abstraction-refinement techniques, where counterexamples can be used to refine the abstraction, and, when combined with symbolic methods, can improve scalability. Unfortunately, no suitable abstraction frameworks have been proposed to date for neural networks. This project will aim to formulate such a framework and an abstraction-refinement technique where adversarial examples are used as counterexamples. It is anticipated that suitable abstraction-refinement techniques could be achieved using a combination of probabilistic reasoning and symbolic methods. Neural networks are inherently probabilistic, in view of training, and so probabilistic reasoning is appropriate to analyse their behaviour. Another goal is to widen the applicability of these methods both regarding the types of network architecture (for example to cater for recurrent networks, which are employed as end-to-end-controllers), and the types of activation functions that can be verified (e.g. not restricted to ReLU). From this, several objectives can be formed: (i) to apply the use of probabilistic reasoning and symbolic methods within abstraction and refinement of neural networks, (ii) to improve the scalability and relevance of current verification techniques using (i), (iii) to automate this process, and (iv) to apply the techniques to verify end-to-end controllers for autonomous vehicles.