General Cutting Planes for Bound-Propagation-Based Neural Network Verification. (arXiv:2208.05740v2 [cs.LG] UPDATED)

Bound propagation methods, when combined with branch and bound, are among the
most effective methods to formally verify properties of deep neural networks
such as correctness, robustness, and safety. However, existing works cannot
handle the general form of cutting plane constraints widely accepted in
traditional solvers, which are crucial for strengthening verifiers with
tightened convex relaxations. In this paper, we generalize the bound
propagation procedure to allow the addition of arbitrary cutting plane
constraints, including those involving relaxed integer variables that do not
appear in existing bound propagation formulations. Our generalized bound
propagation method, GCP-CROWN, opens up the opportunity to apply general
cutting plane methods for neural network verification while benefiting from the
efficiency and GPU acceleration of bound propagation methods. As a case study,
we investigate the use of cutting planes generated by off-the-shelf mixed
integer programming (MIP) solver. We find that MIP solvers can generate
high-quality cutting planes for strengthening bound-propagation-based verifiers
using our new formulation. Since the branching-focused bound propagation
procedure and the cutting-plane-focused MIP solver can run in parallel
utilizing different types of hardware (GPUs and CPUs), their combination can
quickly explore a large number of branches with strong cutting planes, leading
to strong verification performance. Experiments demonstrate that our method is
the first verifier that can completely solve the oval20 benchmark and verify
twice as many instances on the oval21 benchmark compared to the best tool in
VNN-COMP 2021, and also noticeably outperforms state-of-the-art verifiers on a
wide range of benchmarks. GCP-CROWN is part of the $alpha,!beta$-CROWN
verifier, the VNN-COMP 2022 winner. Code is available at
this http URL