Abstract
In this paper, we study certifying the robustness of ReLU neural networksagainst adversarial input perturbations. To diminish the relaxation errorsuffered by the popular linear programming (LP) and semidefinite programming(SDP) certification methods, we take a branch-and-bound approach to proposepartitioning the input uncertainty set and solving the relaxations on each partseparately. We show that this approach reduces relaxation error, and that theerror is eliminated entirely upon performing an LP relaxation with a partitionintelligently designed to exploit the nature of the ReLU activations. To scalethis approach to large networks, we consider using a coarser partition wherebythe number of parts in the partition is reduced. We prove that computing such acoarse partition that directly minimizes the LP relaxation error is NP-hard. Byinstead minimizing the worst-case LP relaxation error, we develop a closed-formbranching scheme in the single-hidden layer case. We extend the analysis to theSDP, where the feasible set geometry is exploited to design a branching schemethat minimizes the worst-case SDP relaxation error. Experiments on MNIST,CIFAR-10, and Wisconsin breast cancer diagnosis classifiers demonstratesignificant increases in the percentages of test samples certified. Byindependently increasing the input size and the number of layers, weempirically illustrate under which regimes the branched LP and branched SDP arebest applied. Finally, we extend our LP branching method into a multi-layerbranching heuristic, which attains comparable performance to priorstate-of-the-art heuristics on large-scale, deep neural network certificationbenchmarks.