神经网络关系验证的分支定界方法

论文提出名为 SaBRe 的分支定界（BaB）框架，用于验证神经网络的关系型规约（如全局鲁棒性），并在 817 个验证问题上与基线方法比较。作者指出，验证关系型规约需要推理多次网络推理之间的关系，现有基于可靠凸过近似的方法本身不完整、可能误报，因此需要有效的抽象精化。该框架迭代分裂问题直至子问题全部验证完成，与以往分裂单个神经元的做法不同，它对关系神经元进行分裂，并基于验证问题的对偶形式设计关系神经元选择策略，以挑选能使分裂带来最大精化的关系神经元。作者在 ACAS Xu、MNIST-F、MNIST-C、CIFAR 和 GTSRB 的 817 个验证问题上评测，称 SaBRe 在求解实例数量和验证效率上均优于不同基线方法。