Neural Network Branch-and-Bound for Neural Network Verification
arXiv:2107.12855
Abstract
Many available formal verification methods have been shown to be instances of a unified Branch-and-Bound (BaB) formulation. We propose a novel machine learning framework that can be used for designing an effective branching strategy as well as for computing better lower bounds. Specifically, we learn two graph neural networks (GNN) that both directly treat the network we want to verify as a graph input and perform forward-backward passes through the GNN layers. We use one GNN to simulate the strong branching heuristic behaviour and another to compute a feasible dual solution of the convex relaxation, thereby providing a valid lower bound. We provide a new verification dataset that is more challenging than those used in the literature, thereby providing an effective alternative for testing algorithmic improvements for verification. Whilst using just one of the GNNs leads to a reduction in verification time, we get optimal performance when combining the two GNN approaches. Our combined framework achieves a 50\% reduction in both the number of branches and the time required for verification on various convolutional networks when compared to several state-of-the-art verification methods. In addition, we show that our GNN models generalize well to harder properties on larger unseen networks.
arXiv commentarXiv admin note: substantial text overlap with arXiv:1912.01329
References in corpus (14)
- End to End Learning for Self-Driving Cars
- Learning Combinatorial Optimization Algorithms over Graphs
- Provable defenses against adversarial examples via the convex outer adversarial polytope
- Evaluating Robustness of Neural Networks with Mixed Integer Programming
- On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models
- Neural Combinatorial Optimization with Reinforcement Learning
- Efficient Formal Safety Analysis of Neural Networks
- A Unified View of Piecewise Linear Neural Network Verification
- Training verified learners with learned verifiers
- Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
- Fast Neural Network Verification via Shadow Prices
- Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition
- Cuts, Primal Heuristics, and Learning to Branch for the Time-Dependent Traveling Salesman Problem
- Lagrangian Decomposition for Neural Network Verification