We present a novel approach for the certification of neural networks against adversarial perturbations which combines scalable overapproximation methods with precise (mixed integer) linear programming. This results in significantly better precision than state-of-the-art verifiers on challenging feedforward and convolutional neural networks with piecewise linear activation functions. Neural networks are increasingly applied in critical domains such as autonomous driving BID1 , medical diagnosis BID0 , and speech recognition BID13 . However, it has been shown by BID11 that neural networks can be vulnerable against adversarial attacks, i.e., imperceptible input perturbations cause neural networks to misclassify. To address this challenge and prove that a network is free of adversarial examples (usually, in a region around a given input), recent work has started investigating the use of certification techniques. Current verifiers can be broadly classified as either complete or incomplete.Complete verifiers are exact, i.e., if the verifier fails to certify a network then the network is nonrobust (and vice-versa) . Existing complete verifiers are based on Mixed Integer Linear Programming (MILP) BID19 BID8 BID5 BID3 or SMT solvers BID16 BID7 . Although precise, these can only handle networks with a small number of layers and neurons. To scale, incomplete verifiers usually employ overapproximation methods and hence they are sound but may fail to prove robustness even if it holds. Incomplete verifiers use methods such as duality BID6 , abstract interpretation BID23 , linear approximations BID29 , semidefinite relaxations BID21 , combination of linear and non-linear approximation BID30 , or search space discretization BID14 . Incomplete verifiers are more scalable than complete ones, but can suffer from precision loss for deeper networks. In principle, incomplete verifiers can be made asymptotically complete by iteratively refining the input space BID26 or the neurons BID27 ; however, in the worst case, this may eliminate any scalability gains and thus defeat the purpose of using overapproximation in the first place.This work: boosting complete and incomplete verifiers. A key challenge then is to design a verifier which improves the precision of incomplete methods and the scalability of complete ones. In this work, we make a step towards addressing this challenge based on two key ideas: (i) a combination of state-of-the-art overapproximation techniques used by incomplete methods, including LP relaxations, together with MILP solvers, often employed in complete verifiers; (ii) a novel heuristic, which points to neurons whose approximated bounds should be refined. We implemented these ideas in a system called RefineZono, and showed that is is faster than state-of-the-art complete verifiers on small networks while improving precision of existing incomplete verifiers on larger networks.The recent works of BID27 and BID25 have also explored the combination of linear programming with overapproximation. However, both use simpler and coarser overapproximations than ours. Our evaluation shows that RefineZono is faster than both for complete verification. For example, RefineZono is faster than the work of BID25 for the complete x 7x 8 x 9x 10 x 11x 12x 13 Figure 1 : Robustness analysis of a toy example neural network using our method. Here, approximation results computed with DeepZ (blue box) are refined using MILP whereas those in green are refined using LP. verification of a 3 × 50 network, while for the larger 9 × 200 network their method does not finish within multiple days on images which RefineZono verifies in ≈ 14 minutes. DISPLAYFORM0 We presented a novel refinement-based approach for effectively combining overapproximation techniques used by incomplete verifiers with linear-programming-based methods used in complete verifiers. We implemented our method in a system called RefineZono and showed its effectiveness on verification tasks involving feedforward and convolutional neural networks with ReLU activations.Our evaluation demonstrates that RefineZono can certify robustness properties beyond the reach of existing state-of-the-art complete verifiers (these can fail due to scalability issues) while simultaneously improving on the precision of existing incomplete verifiers (which can fail due to using too coarse of an overapproximation).Overall , we believe combining the strengths of overapproximation methods with those of mixed integer linear programming as done in this work is a promising direction for further advancing the state-of-the-art in neural network verification.
We refine the over-approximation results from incomplete verifiers using MILP solvers to prove more robustness properties than state-of-the-art.  Introduces a verifier that obtains improvement on precision of incomplete verifiers and scalability of the complete verifiers using over-parameterization, mixed integer linear programming and linear programming relaxation. A mixed strategy to obtain better precision on robustness verifications of feed-forward neural networks with piecewise linear activation functions, achieving better precision than incomplete verifiers and more scalability than complete verifiers.