通过分支定界树的有序探索实现高效神经网络验证

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