Branch-and-Bound Methods for Neural Network Relational Verification

The paper proposes a branch-and-bound (BaB) framework named SaBRe for verifying relational specifications of neural networks (such as global robustness), and compares it with baseline methods on 817 verification problems. The authors point out that verifying relational specifications requires reasoning about relationships between multiple network inferences, and that existing methods based on sound convex over-approximation are inherently incomplete and may produce false positives, thus requiring effective abstraction refinement. The framework iteratively splits problems until all subproblems are fully verified; unlike prior approaches that split individual neurons, it splits relational neurons, and based on the dual form of the verification problem, designs a relational neuron selection strategy to pick the relational neuron whose splitting yields the greatest refinement. The authors evaluate on 817 verification problems from ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB, and state that SaBRe outperforms various baseline methods in both the number of solved instances and verification efficiency.