标题： 通过分支定界树的顺序优先探索进行高效的神经网络验证 显示英文标题

标题： Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees

摘要： 神经网络对对抗扰动的脆弱性促使了形式验证技术的发展，这些技术可以严格认证神经网络的质量。 作为最先进的方法，分支定界（BaB）是一种“分而治之”的策略，它将现成的验证器应用于其表现更好的子问题。 虽然BaB可以识别出需要拆分的子问题，但它以一种简单的“先到先得”的方式探索这些子问题的空间，从而导致在达到验证结论时效率低下。 为了弥补这一差距，我们引入了一种对BaB产生的不同子问题的顺序，该顺序涉及它们包含反例的不同可能性。 基于这个顺序，我们提出了一种新的验证框架Oliva，通过优先考虑更有可能找到反例的子问题来探索子问题空间，以高效地达到验证结论。 即使在任何子问题中都无法找到反例，它也只是改变了访问不同子问题的顺序，因此不会导致性能下降。 具体来说，Oliva有两个变体，包括$Oliva^{GR}$，一种总是优先考虑更可能找到反例的子问题的贪心策略，以及$Oliva^{SA}$，一种受模拟退火启发的平衡策略，它逐渐从探索转向利用，以定位全局最优的子问题。 我们在覆盖5个模型的MNIST和CIFAR10数据集上的690个验证问题上对Oliva的性能进行了实验评估。 与最先进的方法相比，我们在MNIST上展示了Oliva高达25倍的加速，在CIFAR10上展示了高达80倍的加速。 显示英文摘要

摘要： 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.