PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations

Abstract

Formal verification of neural networks is critical for their safe adoption in real-world applications. However, designing a precise and scalable verifier which can handle different activation functions, realistic network architectures and relevant specifications remains an open and difficult challenge. In this paper, we take a major step forward in addressing this challenge and present a new verification framework, called PRIMA. PRIMA is both (i) general: it handles any non-linear activation function, and (ii) precise: it computes precise convex abstractions involving multiple neurons via novel convex hull approximation algorithms that leverage concepts from computational geometry. The algorithms have polynomial complexity, yield fewer constraints, and minimize precision loss. We evaluate the effectiveness of PRIMA on a variety of challenging tasks from prior work. Our results show that PRIMA is significantly more precise than the state-of-the-art, verifying robustness to input perturbations for up to 20%, 30%, and 34% more images than existing work on ReLU-, Sigmoid-, and Tanh-based networks, respectively. Further, PRIMA enables, for the first time, the precise verification of a realistic neural network for autonomous driving within a few minutes.

29 pages, 18 figures, 6 tables

References in corpus (5)

• Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
• PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
• An efficient nonconvex reformulation of stagewise convex optimization problems

Cited by in corpus (8)

• PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations
• First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)
• Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes
• Architecture-Preserving Provable Repair of Deep Neural Networks
• A Tale of Two Approximations: Tightening Over-Approximation for DNN Robustness Verification via Under-Approximation
• Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks
• NLP Verification: Towards a General Methodology for Certifying Robustness
• Automated Verification of Soundness of DNN Certifiers