Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification
Maya Swisa, Guy Katz
TL;DR
The paper tackles the scalability of formal verification for neural networks with ReLU activations by learning adaptive branching decisions within a branch-and-bound framework. It introduces a reinforcement-learning agent trained with Deep Q-learning from Demonstrations (DQfD) that selects which ReLU to split next, conditioned on a rich state representation. The agent is integrated into the Marabou verifier and is trained using expert heuristics as demonstrations, then fine-tuned with self-play, showing substantial reductions in verification time and number of iterations on ACAS Xu safety and local-robustness benchmarks. The work demonstrates potential for cross-query transfer and sets a path toward portable learned branching policies for neural network verification.
Abstract
State-of-the-art neural network verifiers operate by encoding neural network verification as constraint satisfaction problems. When dealing with standard piecewise-linear activation functions, such as ReLUs, verifiers typically employ branching heuristics that break a complex constraint satisfaction problem into multiple, simpler problems. The verifier's performance depends heavily on the order in which this branching is performed: a poor selection may give rise to exponentially many sub-problem, hampering scalability. Here, we focus on the setting where multiple verification queries must be solved for the same neural network. The core idea is to use past experience to make good branching decisions, expediting verification. We present a reinforcement-learning-based branching heuristic that achieves this, by applying a learning from demonstrations (DQfD) techniques. Our experimental evaluation demonstrates a substantial reduction in average verification time and in the average number of iterations required, compared to modern splitting heuristics. These results highlight the great potential of reinforcement learning in the context of neural network verification.