{"ID":2891330,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2507.17453","arxiv_id":"2507.17453","title":"Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees","abstract":"The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch and bound (BaB) is a \"divide-and-conquer\" strategy that applies off-the-shelf verifiers to sub-problems for which they perform better. While BaB can identify the sub-problems that are necessary to be split, it explores the space of these sub-problems in a naive \"first-come-first-serve\" manner, thereby suffering from an issue of inefficiency to reach a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning with their different likelihoods of containing counterexamples. Based on this order, we propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples, in order to efficiently reach the conclusion of the verification. Even if no counterexample can be found in any sub-problem, it only changes the order of visiting different sub-problem and so will not lead to a performance degradation. Specifically, Oliva has two variants, including $Oliva^{GR}$, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples, and $Oliva^{SA}$, a balanced strategy inspired by simulated annealing that gradually shifts from exploration to exploitation to locate the globally optimal sub-problems. We experimentally evaluate the performance of Oliva on 690 verification problems spanning over 5 models with datasets MNIST and CIFAR10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25X in MNIST, and up to 80X in CIFAR10.","short_abstract":"The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch and bound (BaB) is a \"divide-and-conquer\" strategy that applies off-the-shelf verifiers to sub-problems for which...","url_abs":"https://arxiv.org/abs/2507.17453","url_pdf":"https://arxiv.org/pdf/2507.17453v1","authors":"[\"Guanqin Zhang\",\"Kota Fukuda\",\"Zhenya Zhang\",\"H. M. N. Dilum Bandara\",\"Shiping Chen\",\"Jianjun Zhao\",\"Yulei Sui\"]","published":"2025-07-23T12:20:20Z","proceeding":"cs.LG","tasks":"[\"cs.LG\",\"cs.PL\",\"cs.SE\"]","methods":"[\"LoRA\"]","has_code":false}