发表机构
University of New South Wales; Kyushu University; National Institute of Informatics（新南威尔士大学; 九州大学; 信息学研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究针对分支定界（BaB）神经网络验证效率低的问题，提出利用路径单调性、同时拆分多个激活函数并结合指数搜索的判定边界挖掘方法，经基准实验验证可有效提升效率。
AI 中文摘要
分支定界（BaB）旨在通过自适应划分问题并将现成验证器应用于子问题，实现神经网络的完整验证。其问题拆分历史可表示为一棵树，每个子问题对应一个子节点。BaB的关键问题在于搜索所有路径上的判定边界，该边界将已验证与未验证的子问题分开。我们观察到，现有BaB方法通过沿树路径随深度增加依次求解每个昂贵的子问题来解决此问题，要求在每个访问的BaB树节点（即子问题）处进行代价高昂的边界传播，效率低下。为解决此问题，我们提出了有效的搜索方法，利用每条路径的单调性，通过同时拆分多个激活函数（如ReLU）来高效且精确地定位判定边界，而非像经典方法那样逐个处理。我们的方法沿每条路径执行有效的指数搜索，使我们在识别判定边界时能够跳过许多与边界无关的子问题。增强版本通过使用子问题求解获得的定量信息估计边界位置，进一步改进了这一过程。我们在常用基准上进行实验评估以评估我们提出的技术，并将其与最近基于BaB的方法进行比较。
英文摘要
Branch and Bound (BaB) aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems. Its problem-splitting history can be represented as a tree, where each subproblem corresponds to a child node. A key problem of BaB lies in searching for the verdict boundaries across all the paths that divide the verified and unverified subproblems. We observe that the existing BaB approach tackles this problem by solving each expensive subproblem sequentially along the tree path as its depth increases, requiring costly bounds propagation at every visited BaB tree node (i.e., subproblem), which is inefficient. To address this issue, we propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary by simultaneously splitting multiple activation functions (e.g., ReLU), rather than processing them one at a time as in the classical approach. Our approach performs an effective exponential search along each path, allowing us to skip many boundary-unrelated subproblems when identifying the verdict boundary. The enhanced version further improves this process by estimating the boundary's position using quantitative information obtained from subproblem solving. We perform experimental evaluation on commonly-used benchmarks to assess our proposed techniques, and compare them with recent BaB-based approaches.
Comments21 pages, 6 figures, 5 tables. Published in the proceedings of the 27th International Symposium on Formal Methods (FM 2026)
Journal refIn: Sampaio, A., Stoelinga, M. (eds.), Formal Methods, FM 2026, Lecture Notes in Computer Science, vol. 16556, pp. 67-88, Springer Nature Switzerland, Cham, 2026
DOI：10.1007/978-3-032-26204-2_4
