神经网络关系验证的分支定界法
Branch and Bound for Relational Verification of Neural Networks
浏览论文内容
中文总结 AI 辅助
本文提出分支定界（BaB）框架，通过关系神经元拆分及对应选择策略，在817个跨多数据集的验证问题上，使SaBRe在已解决实例数和效率上优于基线方法，提升神经网络关系验证效果。
中文摘要 AI 辅助
针对关系规范（如全局鲁棒性）的神经网络验证，对于网络物理系统（CPS）的安全关键应用至关重要，因为这类系统越来越多地采用AI组件。与简单的轨迹属性（如局部鲁棒性）相比，验证关系规范需要对多个网络推理之间的关系进行推理，这带来了重大技术挑战。现有研究探索了基于神经网络输出的可靠凸过近似的抽象技术；然而，由于这些方法本质上是不完整的，可能会引发误报，这进一步凸显了对有效抽象细化的需求。本文提出了一种分支定界（BaB）框架来缓解该问题，该框架会迭代拆分问题，直到所有子问题都得到验证。具体而言，我们的BaB框架采用关系神经元的拆分，而非现有工作中的单个神经元拆分；作为技术核心，我们设计了一种基于验证问题对偶形式的关系神经元选择策略，该策略可高效选择最可能的最优关系神经元，以最大化问题拆分带来的细化效果。我们在ACAS Xu、MNIST-F、MNIST-C、CIFAR和GTSRB的817个验证问题上评估了SaBRe。结果表明，SaBRe在已解决实例数量和验证效率方面均优于不同基线方法，证明了所提技术的有效性。
英文摘要
Verification of neural networks against relational specifications, such as global robustness, is crucial for safety-critical applications of cyber-physical systems (CPS), given their increasing adoption of AI components. Compared to simple trace properties (e.g., local robustness), verifying relational specifications requires reasoning about the relationship between multiple network inferences, which brings significant technical challenges. Existing research has explored abstraction techniques based on sound and convex over-approximation of neural network outputs; however, since these approaches are inherently incomplete and may raise false alarms, they further underscore the need of effective abstraction refinement. In this paper, we propose a branch-and-bound (BaB) framework to mitigate the issue, which iteratively splits the problem until all sub-problems are verified. Specifically, our BaB framework features splitting of relational neurons rather than individual neurons as prior works do, and as the core of our technique, we devise a relational neuron selection strategy based on the dual formulation of the verification problem, which allows us to efficiently select the (most likely) optimal relational neuron that maximizes the refinement brought by problem splitting. We evaluate SaBRe on 817 verification problems across ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB. The results show that SaBRe outperforms different baseline approaches, in terms of the number of solved instances and verification efficiency, which demonstrates the effectiveness of our proposed techniques.
发表机构
- Graduate School and Faculty of Information Science and Electrical Engineering, Kyushu University（九州大学情报科学与电气工程研究院及学部）
- National Institute of Informatics（信息学研究所）
- UNSW Sydney（新南威尔士大学悉尼分校）
机构由 AI 辅助整理，请以论文原文为准。
