Warmstarting cuts verification time for neural networks
Exploring Solver-Level Warmstarting for Neural Network Verification
Machine Learning
Summary
Checking that neural networks behave correctly can be very slow or even impossible when done from scratch. The authors studied a way to speed up these checks by starting the verification process using hints from previous runs. They tested this idea with different changes to the network and inputs. Their experiments showed that warmstarting often makes the verification faster and sometimes even solves problems that were too hard before.
What this means in practice
- •For ai safety engineers: Verify neural network models more quickly and reliably under varying conditions by reusing previous solver states.
- •For automotive control developers: Guarantee safety properties of neural nets used in vehicle systems within feasible time by leveraging solver warmstarts.
Authors
Annelot Bosman, Minghao Liu, Marta Kwiatkowska, Holger Hoos, Jan van Rijn
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.