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.
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.