Abstract
Formal verification of deep neural networks (DNNs) is essential for safety-critical applications but computationally expensive due to the NP-complete nature of ReLU activations. This paper introduces a reinforcement learning (RL) approach to optimize the "splitting heuristic" within Branch-and-Bound (BaB) verifiers. By employing Double DQN from Demonstrations (DQfD), the proposed agent learns adaptive splitting policies that outperform static, hand-crafted heuristics. Evaluation on the ACAS Xu benchmark demonstrates up to a 56% reduction in verification time and improved success rates in solving complex queries.
Introduction
Ensuring the safety of deep neural networks (DNNs) is a critical challenge, particularly in autonomous systems like flight controllers where a single error can be catastrophic. Formally verifying that a network satisfies specific safety properties—such as avoiding certain steering angles—is notoriously difficult. For networks utilizing Rectified Linear Unit (ReLU) activation functions, this verification task is known to be NP-complete.
The Splitting Heuristic in Verification
Most modern neural network verifiers employ a Branch-and-Bound (BaB) framework. This method decomposes a complex verification query into smaller, more manageable sub-problems by "splitting" on specific neurons. For a ReLU neuron, this typically involves fixing its state to be either "active" or "inactive."
The efficiency of the BaB process is heavily dependent on the splitting heuristic: the rule used to select which neuron to split next. Traditionally, these heuristics (e.g., BaBSR or Polarity) have been static, applying the same logic regardless of the search's progress or the specific network state. This paper proposes replacing these static rules with an adaptive RL-guided policy.
Methodology: Learning to Split
The researchers framed the splitting process as a Markov Decision Process (MDP) and trained an RL agent to serve as the heuristic.
DQfD Algorithm
To overcome the sample inefficiency of training RL from scratch in large search spaces, the authors utilized Double DQN from Demonstrations (DQfD). The agent's memory was initially seeded with demonstrations from expert heuristics like Polarity and BaBSR, allowing it to start with a strong baseline before exploring novel strategies.
State and Reward Design
The agent's state representation includes:
- Local Features: Neuron bounds and scores from traditional heuristics.
- Global Features: Search depth and the total number of splits performed.
The reward function is task-aligned, penalizing the agent based on the size of the resulting search subtree. A split that leads to a rapid proof incurs a minimal penalty, while one that results in a large, complex search tree is heavily penalized. This encourages the agent to prioritize decisions that prune the search space effectively.
Experimental Evaluation
The approach was integrated into the Marabou verifier and evaluated using the ACAS Xu benchmark, a standard suite for airborne collision avoidance.
- Safety Specifications: 180 queries based on original safety properties ($\phi_1$ through $\phi_4$).
- Local Robustness: 3,000 queries testing network stability under input noise ($\ell_\infty$ balls).
Key Results
The RL-guided heuristic, the DQfD Agent, consistently outperformed traditional methods:
- Verification Speed: On safety properties, the agent achieved a reduction in average verification time ranging from 5.88% to 56.20%.
- Success Rate: The agent solved 147 safety instances within a one-hour timeout, surpassing the next best baseline (BaBSR at 145).
- Robustness Performance: In local robustness tests, the agent maintained the lowest average verification time (~328 seconds) and solved the most instances (2,848/3,000).
Discussion and Future Work
The results indicate that RL agents can effectively learn to "transfer knowledge" between related queries, a significant advantage over static heuristics that treat every query in isolation. While the current study focused on ACAS Xu, future work aims to scale this approach to larger architectures like Vision Transformers and improve "Policy Portability"—the ability for a trained agent to generalize to different network architectures without retraining.