Global Optimization of Objective Functions Represented by ReLU Networks

Neural networks (NN) learn complex non-convex functions, makingthem desirable solutions in many contexts. Applying NNs to safety-critical tasksdemands formal guarantees about their behavior. Recently, a myriad of verifica-tion solutions for NNs emerged using reachability, optimization, and search basedtechniques. Particularly interesting are adversarial examples, which reveal ways thenetwork can fail. They are widely generated using incomplete methods, such aslocal optimization, which cannot guarantee optimality. We propose strategies to ex-tend existing verifiers to provide provably optimal adversarial examples. Naive ap-proaches combine bisection search with an off-the-shelf verifier, resulting in manyexpensive calls to the verifier. Instead, our proposed approach yields tightly in-tegrated optimizers, achieving better runtime performance. We extend Marabou, an SMT-based verifier, and compare it with the bisection based approach and MIPVerify, an optimization based verifier.