Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification

2025/12/11 by Maya Swisa, Guy Katz, Swisa, Maya +1
Computer Science · #Adversarial Robustness in Machine Learning #Explainable Artificial Intelligence (XAI) #Machine Learning and Data Classification #cs.LO

paper · pdf · doi:10.48550/arxiv.2512.10747

openalex publication_date 2025/12/11 · openalex created_date 2025/12/13 · openalex updated_date 2026/07/30

Abstract

Modern neural network verifiers often encode 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-problems, hampering scalability. Here, we focus on the setting in which many related 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 Deep Q-learning from Demonstrations (DQfD). 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.

Citations

• Proof Minimization in Neural Network Verification
• Abstraction-Based Proof Production in Formal Verification of Neural Networks
• Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations
• Neural Network Verification for Gliding Drone Control: A Case Study
• The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results
• Safe and Reliable Training of Learning-Based Aerospace Controllers
• Verifying the Generalization of Deep Learning to Out-of-Distribution Domains
• Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
• A Certified Proof Checker for Deep Neural Network Verification in Imandra
• Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing
• DEM: A Method for Certifying Deep Neural Network Classifier Outputs in Aerospace
• Formally Explaining Neural Networks within Reactive Systems
• Verifying Learning-Based Robotic Navigation Systems
• Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound
• Efficient Neural Network Analysis with Sum-of-Infeasibilities
• An Improved Reinforcement Learning Algorithm for Learning to Branch
• Neural Network Branch-and-Bound for Neural Network Verification
• Pruning and Slicing Neural Networks using Formal Verification
• Neural Network Robustness as a Verification Property: A Principled Case Study
• Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification
• Parallelization Techniques for Verifying Neural Networks
• Branch and Bound for Piecewise Linear Neural Network Verification
• Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
• Towards Evaluating the Robustness of Neural Networks
• Deep Residual Learning for Image Recognition
• Deep Reinforcement Learning with Double Q-learning
• Explaining and Harnessing Adversarial Examples
• Intriguing properties of neural networks

Related

• Neural Network Branch-and-Bound for Neural Network Verification
• Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound
• Neural Network Branching for Neural Network Verification
• Lookahead Branching for Neural Network Verification
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees