  In this paper, we study certifying the robustness of ReLU neural networks
against adversarial input perturbations. To diminish the relaxation error
suffered by the popular linear programming (LP) and semidefinite programming
(SDP) certification methods, we propose partitioning the input uncertainty set
and solving the relaxations on each part separately. We show that this approach
reduces relaxation error, and that the error is eliminated entirely upon
performing an LP relaxation with an intelligently designed partition. To scale
this approach to large networks, we consider courser partitions that take the
same form as this motivating partition. We prove that computing such a
partition that directly minimizes the LP relaxation error is NP-hard. By
instead minimizing the worst-case LP relaxation error, we develop a
computationally tractable scheme with a closed-form optimal two-part partition.
We extend the analysis to the SDP, where the feasible set geometry is exploited
to design a two-part partition that minimizes the worst-case SDP relaxation
error. Experiments on IRIS classifiers demonstrate significant reduction in
relaxation error, offering certificates that are otherwise void without
partitioning. By independently increasing the input size and the number of
layers, we empirically illustrate under which regimes the partitioned LP and
SDP are best applied.
