Reinforcement learning improves neural network verification efficiency
Verifying Neural Networks with Reinforcement Learning
Machine LearningSoftware Engineering
Summary
Checking whether deep neural networks behave safely can be very complex and slow. The authors introduce a method that uses reinforcement learning to make smarter decisions when breaking down this problem into smaller parts. Their system learns from experience to choose better ways to explore solutions, solving more problems while searching less. This helps ensure neural networks in critical situations are more reliably checked.
What this means in practice
- •For safety engineers: Verify the safety of neural networks used in critical systems more efficiently by reducing the number of checks needed.
- •For machine learning practitioners: Improve verification step planning when testing neural networks, enabling faster and more thorough correctness checks.
Authors
Hai Duong, Thanh Le, ThanhVu Nguyen
Abstract
Formal verification can play a key role in ensuring the reliability of Deep Neural Networks (DNNs) deployed in safety-critical systems. Modern DNN verifiers employ a branch-and-bound framework, which alternates between branching (splitting into smaller subproblems) and bounding (pruning subproblems) to efficiently explore the verification space. However, existing branching heuristics make greedy decisions based on static scoring functions. They do not anticipate long-term efficiency or leverage the growing availability of verification data to improve performance. This work introduces RSB, a reinforcement learning framework that learns to refine baseline branching heuristics. It trains an actor-critic architecture to maximize cumulative future rewards rather than immediate scores. The actor generates attention weights from observations of raw neuron features and learned graph embeddings, which rescale baseline heuristic scores to guide neuron branching. Evaluation on 600 challenging instances demonstrates that RSB consistently outperforms state-of-the-art branching heuristics, solving 11% more instances while reducing branch exploration by 50%.