Exploring Solver-Level Warmstarting for Neural Network Verification

arXiv (Cornell University)

Abstract

Neural network verification has become a key tool for providing formal guarantees on the behaviour of neural networks. However, many verification problems remain computationally intractable in the worst case: even for common adversarial robustness specifications, verification is NP-complete. Here, we explore the application of solver-level warmstarting for neural network verification to exploit information from previous solutions. We study the effect on running time as several properties are modified, including perturbation radii, input data and the networks themselves, using a pipeline that is generalisable and potentially adaptable to state-of-the-art verifiers. Our results show that warmstarting can significantly reduce verification time in most cases. Moreover, warmstarting enables the successful verification of instances that could not be solved from scratch within the given time limit.

Authors 5

1. Annelot W. Bosman Aachen Leiden Institute of Advanced Computer Science

   Leiden University

   Affiliation as printed

   Leiden Institute of Advanced Computer Science , Leiden

2. Minghao Liu

   University of Oxford

   Affiliation as printed

   University of Oxford , United Kingdom

3. Marta Kwiatkowska

   University of Oxford

   Affiliation as printed

   University of Oxford , United Kingdom

4. Holger H. Hoos
5. Jan van Rijn Aachen Leiden Institute of Advanced Computer Science

   Leiden University

   Affiliation as printed

   Leiden Institute of Advanced Computer Science , Leiden