Lookahead Branching for Neural Network Verification
For developers of neural network verification tools, this work provides a simple yet effective method to accelerate verification, with demonstrated improvements over state-of-the-art heuristics.
The paper introduces a general lookahead branching strategy for branch-and-bound neural network verifiers, showing that it improves branching decisions and generates additional lemmas. This leads to consistent speedups and up to 57% more solved instances in Marabou and α-β-CROWN.
In this work, we investigate the effect of lookahead branching strategies in neural network verification. We present a general recipe to integrate lookahead into any branch-and-bound verifier and demonstrate how one of the current state-of-the-art branching heuristics, FSB, can be viewed as a special instantiation of the lookahead branching strategy. We also describe how, in addition to improving the quality of branching decisions, lookahead can generate additional lemmas that accelerate verification. We instantiate the method in two representative branch-and-bound-based verifiers (Marabou and $α$-$β$-CROWN), and demonstrate that lookahead leads to consistent speedups in verification time and up to $57\%$ more solved instances. Code is available at https://github.com/ai-ar-research/lookahead-branching.