Verifying Neural Networks with Reinforcement Learning

Hai Duong; Thanh Le; ThanhVu Nguyen

cs.LGSep 28, 2026

Verifying Neural Networks with Reinforcement Learning

Authors: Hai Duong, Thanh Le, ThanhVu Nguyen

Organizations: Department of Computer Science George Mason University Fairfax, VA, USA · Unaffiliated Yokosuka, Japan

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

Figures & tables

Panel of Figure 1 — Fig. 1: Comparison of different search trees performed by Fsb and Rsb for verifying the property in Eq. 1 .

Figure 2

Panel of Figure 3 — Fig. 2: The actor and critic architectures in Rsb .

Benchmark	Layers	Types	Neurons	Parameters	Instances
FNN	4-6	FC, ReLU	0.5K-1.5K	269K-532K	200
CNN	4-6	Conv, FC, ReLU	3.2K-6.8K	55K-215K	200
Sigmoid	5	FC, ReLU, Sigmoid	0.3K	343K	200
Total					600

Tab. 1: Verification instances.

	FNN			CNN			Sigmoid
Method	Time (s)	Branch ( $\times 10^{6}$ )	Solved (#)	Time (s)	Branch ( $\times 10^{6}$ )	Solved (#)	Time (s)	Branch ( $\times 10^{6}$ )	Solved (#)
Polarity	6064.32	170.81	1	8662.55	583.01	0	6027.70	62.98	10
Upb	4359.36	27.17	23	2387.48	1.73	71	3963.69	8.59	39
Fsb	2679.00	6.65	43	2295.89	1.81	71	4336.73	8.99	34
Rsb	2051.94	1.86	50	2419.58	1.69	72	3450.80	5.14	43

Tab. 2: Results across benchmarks (instances solved by at least one method).

Panel of Figure 7 — Fig. 5: Statistical distributions of computational metrics.

Appendix figures & tables2 assets

Supplementary material from the paper’s appendix.

Appendix

Hyperparameter	Value
RL training (Actor and Critic)
Optimizer	AdamW
Actor learning rate	$4\times 10^{-4}$
Critic learning rate	$4\times 10^{-4}$
Discount factor $\gamma$	$0.99$
Replay buffer capacity	$10^{5}$ transitions

Appendix

Tab. 3: Hyperparameters for RL training and for GCN embedding pretraining used in our experiments. The episode count equals the main paper’s (

10^{5}

unless stated otherwise).

Fig. 6: Training loss over time.

Explore similar work

Branch and Bound for Relational Verification of Neural Networks
Aug 13, 2026Kota Fukuda, Zhenya Zhang, Guanqin Zhang +1Neural Network Verification Neural Network
Graduate School and Faculty of Information Science and Electrical Engineering, Kyushu University, Fukuoka, Japan · National Institute of Informatics, Tokyo, Japan · UNSW Sydney, Australia
Neural Network Verification using Partial Multi-Neuron Relaxation
May 28, 2026Ido Shmuel, Guy KatzNeural Network Verification Convex Relaxation
The Hebrew University of Jerusalem, Jerusalem, Israel
Lookahead Branching for Neural Network Verification
Jul 19, 2026Liam Davis, Duo Zhou, Huan Zhang +3Neural Network Verification Formal Verification
Amherst College · University of Illinois Urbana-Champaign · Hebrew University of Jerusalem +1

Aug 13, 2026, cs.LGJ/K move · Enter open · S save

Branch and Bound for Relational Verification of Neural Networks

Kota Fukuda, Zhenya Zhang, Guanqin Zhang, Jianjun Zhao

Graduate School and Faculty of Information Science and Electrical Engineering, Kyushu University, Fukuoka, Japan · National Institute of Informatics, Tokyo, Japan · UNSW Sydney, Australia

Neural Network Verification Neural Network Cyber-Physical System Relational

Open paper AskPDF arXiv

Verification of neural networks against relational specifications, such as global robustness, is crucial for safety-critical applications of cyber-physical systems (CPS), given their increasing adoption of AI components. Compared to simple trace properties (e.g., local robustness), verifying relational specifications requires reasoning about the relationship between multiple network inferences, which brings significant technical challenges. Existing research has explored abstraction techniques based on sound and convex over-approximation of neural network outputs; however, since these approaches are inherently incomplete and may raise false alarms, they further underscore the need of effective abstraction refinement. In this paper, we propose a branch-and-bound (BaB) framework to mitigate the issue, which iteratively splits the problem until all sub-problems are verified. Specifically, our BaB framework features splitting of relational neurons rather than individual neurons as prior works do, and as the core of our technique, we devise a relational neuron selection strategy based on the dual formulation of the verification problem, which allows us to efficiently select the (most likely) optimal relational neuron that maximizes the refinement brought by problem splitting. We evaluate SaBRe on 817 verification problems across ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB. The results show that SaBRe outperforms different baseline approaches, in terms of the number of solved instances and verification efficiency, which demonstrates the effectiveness of our proposed techniques.

Abstract

Explore similar work

Branch and Bound for Relational Verification of Neural Networks

Neural Network Verification using Partial Multi-Neuron Relaxation

Lookahead Branching for Neural Network Verification