2026-07-20T04:49:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23328 2025-10-02T12:48:49Z ddc:004 open_access

Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees Zhang, Guanqin Fukuda, Kota Zhang, Zhenya Bandara, H.M.N. Dilum Chen, Shiping Zhao, Jianjun Sui, Yulei neural network verification branch and bound counterexample potentiality simulated annealing stochastic optimization 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-served" 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-problems 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 CIFAR-10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25× in MNIST, and up to 80× in CIFAR-10. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Guanqin Zhang and Kota Fukuda and Zhenya Zhang and H.M.N. Dilum Bandara and Shiping Chen and Jianjun Zhao and Yulei Sui 2025 Is Part Of LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2025.36 urn:nbn:de:0030-drops-233281 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.36 eng https://creativecommons.org/licenses/by/4.0/legalcode