Formal verification of neural networks

Thesis

Machine learning models and in particular Deep Neural Networks are being deployed in an ever increasing number of applications, making it crucial for methods capable of verifying their behaviour to be developed. In order to go beyond treating them as black boxes, we study the feasibility of verifying that certain properties on the mapping that the models encode should always hold and propose algorithms to perform this verification. We advocate the developments of these methods through the lens of optimisation.

By reformulating the verification of properties as optimisation problems over Neural Networks, we introduce a unified framework to reason about algorithms and identify the necessary components of verification systems. An attempt at verifying a property either results in a formal proof that the property holds or in concrete examples of cases where it is violated.

Current state of the art in verification technology of machine learning artifacts is constrained by both the restricted applicability of existing techniques and by their limited scalability. With the aim of making it more feasible to prove statements over widely used models, we present general methods that increase the diversity of verifiable properties and architectures amenable to verification. In order to get closer to the scale of models that power industrial applications, we refine heuristics used during the proving process and introduce algorithmic improvements to the optimisation algorithms underlying the methods, leading to order of magnitude speedups. Benchmarks empirically validate our runtime improvement claims, showing our contribution to addressing the problem of limited scalability of formal methods in the context of Neural Networks.

Authors: Bunel, R

• DOI: 10.5287/ora-keajwxx82
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: verification; machine learning; optimisation; neural networks; robustness