面向神经网络验证的自适应分支定界树探索
机器学习
2025-05-05 v1 编程语言
摘要
形式化验证是一种严谨的方法，能够可证明地确保神经网络的质量。目前，分支定界（BaB）是最先进的技术，它通过按需拆分问题并将现成的验证器应用于子问题来提高性能。然而，现有的BaB可能效率不高，因为它以朴素的方式探索子问题空间，忽略了不同子问题的“重要性”。为了弥补这一差距，我们首先引入了一个“重要性”概念，该概念反映了在子问题中找到反例的可能性，然后我们设计了一种名为ABONN的新型验证方法，该方法以蒙特卡洛树搜索（MCTS）的风格自适应地探索BaB的子问题空间。探索由不同子问题的“重要性”引导，因此它倾向于那些更可能找到反例的子问题。一旦找到反例，它可以立即终止；即使找不到，在访问所有子问题后，它仍然可以设法验证该问题。我们使用来自常用数据集和神经网络模型的552个验证问题对ABONN进行了评估，并将其与最先进的验证器作为基线方法进行了比较。实验评估表明，ABONN在MNIST上实现了高达的加速，在CIFAR-10上实现了高达的加速。我们进一步研究了超参数对ABONN性能的影响，以及我们自适应树探索的有效性。
引用
@article{arxiv.2505.00963,
title = {Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification},
author = {Kota Fukuda and Guanqin Zhang and Zhenya Zhang and Yulei Sui and Jianjun Zhao},
journal= {arXiv preprint arXiv:2505.00963},
year = {2025}
}
备注
7 pages, 6 figures