Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers

Abstract

Formal verification of neural networks (NNs) is a challenging and important problem. Existing efficient complete solvers typically require the branch-and-bound (BaB) process, which splits the problem domain into sub-domains and solves each sub-domain using faster but weaker incomplete verifiers, such as Linear Programming (LP) on linearly relaxed sub-domains. In this paper, we propose to use the backward mode linear relaxation based perturbation analysis (LiRPA) to replace LP during the BaB process, which can be efficiently implemented on the typical machine learning accelerators such as GPUs and TPUs. However, unlike LP, LiRPA when applied naively can produce much weaker bounds and even cannot check certain conflicts of sub-domains during splitting, making the entire procedure incomplete after BaB. To address these challenges, we apply a fast gradient based bound tightening procedure combined with batch splits and the design of minimal usage of LP bound procedure, enabling us to effectively use LiRPA on the accelerator hardware for the challenging complete NN verification problem and significantly outperform LP-based approaches. On a single GPU, we demonstrate an order of magnitude speedup compared to existing LP-based approaches.

arXiv commentAccepted by ICLR 2021

References in corpus (10)

• Provable defenses against adversarial examples via the convex outer adversarial polytope
• Evaluating Robustness of Neural Networks with Mixed Integer Programming
• Semidefinite relaxations for certifying robustness to adversarial examples
• Efficient Formal Safety Analysis of Neural Networks
• A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks
• A Unified View of Piecewise Linear Neural Network Verification
• Training verified learners with learned verifiers
• Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
• The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification
• Fast Neural Network Verification via Shadow Prices

Cited by in corpus (7)

• PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
• Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes
• Learning Security Classifiers with Verified Global Robustness Properties
• Architecture-Preserving Provable Repair of Deep Neural Networks
• Scalable Verification of GNN-based Job Schedulers
• Seven challenges for harmonizing explainability requirements
• Reachability Analysis of Neural Networks with Uncertain Parameters