Neural Network Branch-and-Bound for Neural Network Verification

Understand

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.