PaperlayerView exact revision on arXiv

Source-linked AI summary

Verifying Neural Networks with Reinforcement Learning

Hai Duong, Thanh Le, ThanhVu Nguyen

arXiv:2609.34553v1cs.LGcs.SE

TL;DR

DNN verification needs scalable ways to check specifications, but established branching heuristics make greedy decisions that do not anticipate long-term efficiency. RSB learns to adjust baseline heuristic scores through reinforcement learning. Across 600 challenging instances, it solves 11% more instances while exploring 50% fewer branches than SOTA branching heuristics.

  • Problem

    Existing branching heuristics rely on hand-crafted, greedy scores and do not anticipate long-term search efficiency or leverage growing verification data.

    Source: §1 · p. 1

  • Method

    RSB uses reinforcement learning to refine baseline branching heuristics by learning weights for their scores from neuron features and graph embeddings.

    Source: §1 · p. 1, §4 · p. 4

  • Results

    11% more instances solved and 50% fewer branches explored than SOTA branching heuristics across 600 challenging instances.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The results show that learned branching policies can outperform mature greedy heuristics in DNN verification.

    Source: §8 · p. 9

Abstract

from arXiv · show

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%.

1 Introduction

DNN verification supports assurance for mission-critical applications, but branching heuristics remain under-explored and rely on greedy, hand-crafted scores. RSB learns to refine baseline heuristics, and evaluation reports improved verification outcomes across 600 challenging instances.

1 Introduction

  • DNN verification provides evidence that network behavior meets specifications, supporting assurance for systems used in domains such as autonomous driving and medicine.The introduction notes the growth of reported verifiers and yearly competitions documenting advances.Source: §1 · p. 1
  • Branching is under-explored despite its effect on verifier efficiency, while existing hand-crafted heuristics require expertise, make greedy decisions, and underuse verification data.Much prior DNN verification work instead develops abstract domains to tighten bounds.Source: §1 · p. 1
  • RSB applies deep reinforcement learning to learn adaptive branching policies from verification data and refine baseline heuristics such as FSB.It formulates branching as sequential decision-making and trains for cumulative future rewards rather than greedy local decisions.Source: §1 · pp. 1–2
  • RSB combines learned graph embeddings and raw neuron features in an architecture-agnostic framework intended to enhance existing heuristics across DNN types and activation functions.The contributions also include handling variable-sized inputs and training adapted to BaB branching dynamics.Source: §1 · p. 2
  • 11% more instances solved and 50% fewer branches explored than SOTA branching heuristics such as FSB across 600 challenging instances.The evaluation includes networks of varying sizes and architectures and reports generalization to unseen architectures and activation functions.Source: §1 · p. 2

2 Preliminaries

DNN verification checks whether a network satisfies a specified input-output property, and modern verifiers commonly use branch-and-bound. This section motivates improving branching decisions, particularly by learning to adjust baseline heuristic scores for long-term efficiency.

2 Preliminaries

  • DNN verification checks satisfiability of a formula combining the network and desired property; an unsatisfiable result indicates the property is valid.A proof may accompany an unsatisfiable result.Source: §2 · p. 2
  • Branch-and-bound alternates branching, which splits a problem by assigning neuron status, and bounding, which computes output bounds and checks subproblem feasibility.This work focuses on DECIDE, the branching component, which is less explored than bounding methods.Source: §2 · p. 2
  • Neuron selection is a combinatorial optimization problem: a good decision heuristic can reduce the search space, while a poor one may cause exponential growth in subproblems.The split choice affects search and pruning speed, including verification steps and time.Source: §2 · p. 2
  • FSB estimates the improvement from branching on each neuron, but its greedy local choices do not optimize long-term search efficiency.RSB learns weights that modify baseline heuristic scores such as FSB's.Source: §2 · p. 2
  • Deep reinforcement learning learns sequential decision policies from interaction with an environment and seeks to maximize expected cumulative reward over time.The actor selects actions and the critic estimates their value.Source: §2 · p. 2

3 Motivating example

The example contrasts FSB's locally highest-scoring neuron choice with RSB's learned reweighting of heuristic scores. In this case, RSB prioritizes an earlier neuron whose split constrains downstream neurons and completes verification with fewer steps and branches.

3 Motivating example

  • The example begins with three unstable ReLU neurons, n11, n21, and n22, each eligible for positive or negative branching.A neuron is unstable when its bounds allow it to be either active or inactive.Source: §3 · p. 3
  • FSB first selects n21 because its score is highest, then selects n11, requiring two branching decisions to complete verification.Its scores are 0.3 for n11, 0.5 for n21, and 0.1 for n22 at the first decision.Source: §3 · p. 3
  • RSB adjusts original FSB scores using neuron features and an observation that combines those features with GNN embeddings.The example lists lower and upper bounds, bias, and a stability mask as raw features; the adjusted scores prioritize n11 over n21.Source: §3 · p. 3
  • RSB verifies the example in one step and two branches, rather than FSB's two steps and four branches.Reweighting makes n11 highest priority instead of n21; both branches on n11 are UNSAT.Source: §3 · p. 3
  • The example identifies n11 as a stronger branching point because its wider earlier-layer interval constrains both n21 and n22, tightening intermediate bounds.By contrast, splitting n21 leaves n22 unstable and requires additional splits.Source: §3 · p. 4

4 Branching as DRL environment

RSB frames neuron branching as a reinforcement-learning problem in which a policy uses observations and actions to guide branch-and-bound search. Its reward favors efficient verification while preserving BABNNV’s soundness and completeness.

State space

  • Each neuron split creates active and inactive successor states, so every branching decision expands the search tree into two subproblems.This dual-branch structure distinguishes DNN verification from single-successor combinatorial optimization.Source: §4 · p. 4

Observation space

  • The observation combines unstable-neuron activation bounds, bias, and branching status with GNN embeddings of global verification structure.The observation is designed to generalize across architectures, capture neuron interdependencies, and scale by attending only to unstable neurons.Source: §4 · p. 4

Action space

  • RSB learns a weight for each unstable neuron and multiplies it by the baseline heuristic score to select the branching neuron.This adjusts heuristic priorities based on the current state rather than replacing the heuristic.Source: §4 · p. 4

Reward function

  • A unit reward for each resolved subproblem makes maximizing cumulative discounted reward equivalent to minimizing the total number of generated subproblems.The policy seeks expected cumulative discounted reward across branching decisions.Source: §4 · p. 4

Verification guarantees

  • RSB changes only neuron-selection order, so BABNNV’s soundness and completeness remain unchanged.BABNNV exhaustively explores the necessary branches regardless of branching order.Source: §4 · p. 4

5 The RSB approach

RSB combines graph-based observations, an actor-critic policy, and training adapted to BABNNV’s two-successor branching. At each step, the actor’s attention weights refine baseline heuristic scores to guide neuron selection.

5 The RSB approach

  • RSB integrates an actor that generates attention weights with baseline branching scores, while leaving the rest of BABNNV’s procedure unchanged.Its approach combines graph embeddings, an actor-critic architecture, and off-policy training adapted to dual-branch search.Source: §5 · p. 5

5.1 Observation construction

  • A GCN embeds the neuron graph using activation bounds, bias, branching status, network connections, and heuristic scores as supervision labels.Raw features are projected to the embedding dimension, concatenated with graph embeddings, and projected again to balance local and global information.Source: §5.1 · p. 5

5.2 Actor-Critic architecture

  • PointerNet actor and critic architectures handle variable-length unstable-neuron inputs; the actor uses attention to generate weights, and twin critics estimate Q-values for all neurons.The critic decoder is initialized with the actor’s decoder state from the current branching step.Source: §5.2 · p. 5

5.3 Training procedure

  • Training stores transitions containing both successor observations and termination masks, then adapts the critic loss to account for the two branches.The reward penalizes unsolved branches, and training alternates critic updates for value estimates with actor updates for higher estimated returns.Source: §5.3 · p. 6

6 Evaluation

Across 600 challenging verification instances, RSB solves more problems than the compared branching heuristics while exploring fewer branches. It also performs well on unseen architectures and shows consistent efficiency across repeated runs.

6.1 Experimental design

  • 14,454 challenging instances from 480,960 generated FNN verification instances were used for training, and evaluation covered 600 problems across FNN, CNN, and Sigmoid benchmarks.The evaluation compared RSB with FSB, UPB, and POLARITY; all methods were integrated into NEURALSAT for a fair comparison.Source: §6.1 · pp. 6–7

6.2 RSB performance compared to baselines

  • 165 total instances solved by RSB versus 148 for FSB, 110 for UPB, and 11 for POLARITY; RSB also explores 50% fewer branches than FSB.The results cover instances solved by at least one method across the three benchmarks.Source: Table 2 · p. 7, §6.2 · p. 7
  • RSB’s gains over FSB are meaningful against established heuristics, and the authors state that RSB can improve with more training data, better DRL algorithms, and new architectures.FSB is used in leading verifiers, including αβ-CROWN, GCP-CROWN, and NEURALSAT.Source: §6.2 · p. 7

6.3 RSB’s generalizability

  • On seen FNNs, RSB reaches 50 instances and stays below FSB in runtime and explored branches; on unseen CNN and Sigmoid architectures, it solves 115 instances, ahead of UPB at 110 and FSB at 105.The evaluation properties differ from training properties even when the FNN architecture is shared.Source: §6.3 · p. 8, Figure 3 · p. 8, Figure 4 · p. 8

6.4 RSB’s efficiency

  • Across five seeded runs, RSB has a median of 150 solved instances, compared with 140 for FSB and 125 for UPB, with a tight interquartile range.The authors report that the narrow spread indicates RSB’s advantage is consistent across runs.Source: §6.4 · p. 8, Figure 5 · p. 8
  • In branch-count distributions, RSB’s box is lower and tighter than FSB’s despite both having medians near 10^4; POLARITY explores about 10^6 branches yet solves the fewest instances.The comparison indicates that exploring more branches does not compensate for poor branching decisions.Source: §6.4 · p. 8, Figure 5 · p. 8
  • RSB’s per-step decision time is about 0.11s versus about 0.13s for FSB and UPB, despite the added DRL inference, as its active-subproblem batches are smaller.The reported example is 32 versus 64 active subproblems per batch.Source: Figure 5 · p. 8, §6.4 · p. 9

7 Related work

Prior verification work improves bounding and uses greedy branching heuristics, while DRL approaches in SAT solving have addressed decision guidance with different inference costs. RSB refines baseline branching scores and adapts its training to BaB’s dual-branch dynamics.

7 Related work

  • Abstraction methods, stronger bound-tightening techniques, and verification-aware training address scalability; RSB focuses on branching and complements these approaches.Examples include intervals, zonotopes, polytopes, star sets, multi-neuron relaxations, cutting planes, and neuron stability.Source: §7 · p. 9
  • FSB estimates per-neuron bound improvements using Lagrangian Decomposition, but these branching heuristics make greedy decisions without considering long-term search-tree impact.The related-work discussion also describes UPB, BABSR, POLARITY, and a GNN heuristic as approaches with greedy decisions.Source: §7 · p. 9
  • Some SAT-solving DRL methods require a GNN pass at each decision, while one-shot guidance uses a single pass; RSB instead refines baseline scores and adapts training to BaB’s dual-branch dynamics.The one-shot approach is reported to achieve a 2× speedup and generalize to larger problems.Source: §7 · p. 9

8 Conclusion

The conclusion presents DRL branching policies as a way to outperform mature heuristics and learn long-term search strategies, with input-space branching and online adaptation proposed as future work. The appendices describe the BaB components and the actor-critic training approach.

8 Conclusion

  • DRL branching policies outperform mature DNN-verification heuristics and capture long-term search strategies, while input-space branching and online adaptation remain future directions.The conclusion also notes that learning-based methods may improve as DRL algorithms advance and training data grows.Source: §8 · p. 9

A The BaB algorithm

  • In BaB, DECIDE assigns active/inactive status to a neuron while DEDUCE bounds neuron outputs and checks subproblem feasibility; this work improves DECIDE.BABNNV takes a DNN and property as input and returns whether the property is valid.Source: A The BaB algorithm · p. 12

B DRL details

  • RSB uses a soft actor-critic variant with two Q-networks and target Q-networks; its actor distributes probability over candidate neurons.The policy updates are close to deterministic policy-gradient methods while retaining SAC’s off-policy sample reuse.Source: B DRL details · p. 12
  • The value objective maximizes expected cumulative discounted return; replay reuses transitions, and γ controls emphasis on immediate versus future rewards.Reusing past experiences through the replay buffer improves sample efficiency and stabilizes training.Source: B DRL details · p. 12
  • The critic uses temporal-difference learning to minimize value-prediction error, while policy-gradient updates use critic estimates to guide the actor’s actions.The critic estimates action values from collected experience, and the actor uses those estimates to select better actions.Source: B DRL details · pp. 12–13

C.1 Training setup

The training setup manages replay and reward scales, combines heuristic warm-up with learned actions, and specifies RL optimization and network architecture.

C.1 Training setup

  • The bounded replay buffer removes oldest transitions first to limit memory while retaining diverse histories; rewards are normalized by the episode’s maximum subproblem count.This normalization keeps return scales comparable across instances with different search-tree sizes.Source: §C.1 · p. 13
  • During warm-up, lightweight heuristics choose actions; afterward, the actor usually selects branches, with occasional heuristic actions retained.Optimization may start once the buffer is at least half full, even if the warm-up step count has not been reached.Source: §C.1 · p. 13
  • Training uses γ = 0.99, learning rates around 10^-4, accumulated minibatches, repeated critic updates, twin-Q pessimistic targets, and Polyak target updates.The Polyak averaging coefficient is τ = 10^-4.Source: §C.1 · p. 13
  • Separate PointerNet actor and critic networks process shared observations using raw and embedded neuron features, LSTM encoding and decoding, and attention; the critic scores branch-child pairs.The actor applies softmax over admissible neurons, while the critic outputs one scalar per branch-child pair.Source: §C.1 · p. 13

C.2 DRL training progress

The recorded training run shows actor and critic losses plateauing without divergence; the appendix also reports training cost and the scope of its hyperparameter table.

C.2 DRL training progress

  • Training on one GPU for approximately 105 verification episodes takes several days; frozen model weights are shared across test instances without per-network fine-tuning.The reported episode used batch size 512 with gradient accumulation 8; wall-clock comparisons under competition time budgets appear in the main text alongside branch counts.Source: §C.2 · p. 13
  • Tab. 3 lists RL-training and GCN-embedding-pretraining hyperparameters, with the episode count matching the main paper’s 105 unless stated otherwise.Source: Table 3 · p. 14
  • Both actor and critic losses plateau without divergence after roughly 106 environment steps in the recorded run.Fig. 6 plots training loss over time.Source: §C.2 · p. 13, Figure 6 · p. 14

Related papers

Loading 2609.34553v1…