Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification

TL;DR

This paper introduces a novel solution-aware ReLU scoring method for DNN verification, significantly reducing binary variables and improving efficiency and accuracy in partial MILP-based verification of large CNNs.

Contribution

It proposes the SAS ReLU scoring method and adapts global scoring functions, enhancing variable selection for partial MILP in DNN verification, outperforming previous methods.

Findings

SAS reduces binary variables by around 6 times.

Achieves up to 40% reduction in undecided instances.

Maintains accuracy with reasonable runtime.

Abstract

To handle complex instances, we revisit a divide-and-conquer approach to break down the complexity: instead of few complex BaB calls, we rely on many small {\em partial} MILP calls. The crucial step is to select very few but very important ReLUs to treat using (costly) binary variables. The previous attempts were suboptimal in that respect. To select these important ReLU variables, we propose a novel {\em solution-aware} ReLU scoring ({\sf SAS}), as well as adapt the BaB-SR and BaB-FSB branching functions as {\em global} ReLU scoring ({\sf GS}) functions. We compare them theoretically as well as experimentally, and {\sf SAS} is more efficient at selecting a set of variables to open using binary variables. Compared with previous attempts, SAS reduces the number of binary variables by around 6 times, while maintaining the same level of accuracy. Implemented in {\em Hybrid MILP}, calling first $\alpha,\beta$-CROWN with a short time-out to solve easier instances, and then partial MILP, produces a very accurate yet efficient verifier, reducing by up to $40\%$ the number of undecided instances to low levels ($8-15\%$), while keeping a reasonable runtime ($46s-417s$ on average per instance), even for fairly large CNNs with 2 million parameters.