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

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

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.

Cite

Cite as @mullerPRIMAGeneralPrecise2022 (helia, typst) · \cite{mullerPRIMAGeneralPrecise2022} (LaTeX)

BibTeX

bibtex · 20 lines

@article{mullerPRIMAGeneralPrecise2022,
 title = {{{PRIMA}}: {{General}} and {{Precise Neural Network Certification}} via {{Scalable Convex Hull Approximations}}},
 author = {Müller, Mark Niklas and Makarchuk, Gleb and Singh, Gagandeep and Püschel, Markus and Vechev, Martin},
 date = {2022-01-16},
 doi = {10.1145/3498704},
 url = {http://arxiv.org/abs/2103.03638},
 urldate = {2024-02-09},
 journaltitle = {Proceedings of the ACM on Programming Languages},
 volume = {6},
 pages = {1--33},
 keywords = {Computer Science - Artificial Intelligence,Computer Science - Machine Learning},
 issue = {POPL},
 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.},
 issn = {2475-1421},
 eprintclass = {cs},
 eprinttype = {arXiv},
 eprint = {2103.03638},
 shortjournal = {Proc. ACM Program. Lang.},
 shorttitle = {{{PRIMA}}}
}

hayagriva YAML (typst)

yaml · 26 lines

mullerPRIMAGeneralPrecise2022:
  type: article
  title:
    value: '{PRIMA}: {General} and {Precise Neural Network Certification} via {Scalable Convex Hull Approximations}'
    short: '{PRIMA}'
  author:
  - Müller, Mark Niklas
  - Makarchuk, Gleb
  - Singh, Gagandeep
  - Püschel, Markus
  - Vechev, Martin
  date: 2022-01-16
  page-range: 1-33
  url:
    value: http://arxiv.org/abs/2103.03638
    date: 2024-02-09
  serial-number:
    arxiv: '2103.03638'
    doi: 10.1145/3498704
    issn: 2475-1421
  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.'
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    issue: POPL
    volume: 6

Download: mullerPRIMAGeneralPrecise2022.bib · mullerPRIMAGeneralPrecise2022.yml

Cited by (1)

Architecture-Preserving Provable Repair of Deep Neural Networks taoArchitecturePreservingProvableRepair2023PLDI · 2023

Deep neural networks (DNNs) are becoming increasingly important components of software, and are considered the state-of-the-art solution for a number of problems, such as image recognition. However, DNNs are far from infallible, and incorrect behavior of DNNs can have disastrous real-world consequences. This paper addresses the problem of architecture-preserving V-polytope provable repair of DNNs. A V-polytope defines a convex bounded polytope using its vertex representation. V-polytope provable repair guarantees that the repaired DNN satisfies the given specification on the infinite set of points in the given V-polytope. An architecture-preserving repair only modifies the parameters of the DNN, without modifying its architecture. The repair has the flexibility to modify multiple layers of the DNN, and runs in polynomial time. It supports DNNs with activation functions that have some linear pieces, as well as fully-connected, convolutional, pooling and residual layers. To the best our knowledge, this is the first provable repair approach that has all of these features. We implement our approach in a tool called APRNN. Using MNIST, ImageNet, and ACAS Xu DNNs, we show that it has better efficiency, scalability, and generalization compared to PRDNN and REASSURE, prior provable repair methods that are not architecture preserving. CCS Concepts: • Computing methodologies → Neural networks; • Theory of computation → Linear programming; • Software and its engineering → Software post-development issues.

PDF · DOI · pldb

Cites 70 works (0 here)

External (70)

Scaling Polyhedral Neural Network Verification on GPUs (2021)
Scaling the Convex Barrier with Active Sets (2021)
A Review of Formal Methods applied to Machine Learning (2021)
Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification (2021)
Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers (2021)
Strong mixed-integer programming formulations for trained neural networks (2020)
Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis (2020)
Branch and bound for piecewise linear neural network verification (2020)
Polyhedral Computation (2020)
Neural Network Branching for Neural Network Verification (2020)
Fastened CROWN: Tightened Neural Network Robustness Certificates (2020)
Efficient Certification of Spatial Robustness (2020)
Learning Certified Individually Fair Representations (2020)
Fast and effective robustness certification for recurrent neural networks (2020)
Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond (2020)
The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verification (2020)
Neural Network Robustness Verification on GPUs (2020)
Enabling certification of verification-agnostic networks via\n memory-efficient semidefinite programming (2020)
An efficient nonconvex reformulation of stagewise convex optimization problems (2020)
Optimization and abstraction: a synergistic approach for analyzing neural network robustness (2019)
Certifying Geometric Robustness of Neural Networks (2019)
CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks (2019)
Scalable Verified Training for Provably Robust Image Classification (2019)
The Marabou Framework for Verification and Analysis of Deep Neural Networks (2019)
Certified Robustness to Adversarial Examples with Differential Privacy (2019)
Beyond the Single Neuron Convex Barrier for Neural Network Certification (2019)
An abstract domain for certifying neural networks (2019)
Boosting Robustness Certification of Neural Networks (2019)
Evaluating Robustness of Neural Networks with Mixed Integer Programming (2019)
Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers (2019)
A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (2019)
Certified Adversarial Robustness via Randomized Smoothing (2019)
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018)
Towards Deep Learning Models Resistant to Adversarial Attacks (2018)
Fast and Effective Robustness Certification (2018)
Efficient Formal Safety Analysis of Neural Networks (2018)
Output Reachable Set Estimation and Verification for Multilayer Neural Networks (2018)
Differentiable Abstract Interpretation for Provably Robust Neural Networks (2018)
Efficient Neural Network Robustness Certification with General Activation Functions (2018)
Scaling provable adversarial defenses (2018)
Semidefinite relaxations for certifying robustness to adversarial\n examples (2018)
Gurobi Optimizer Reference Manual (2018)
Towards Fast Computation of Certified Robustness for ReLU Networks (2018)
Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks (2017)
Safety Verification of Deep Neural Networks (2017)
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017)
Efficient Elimination of Redundancies in Polyhedra by Raytracing (2017)
Branch-and-bound algorithms: A survey of recent advances in searching, branching, and pruning (2016)
Computing the approximate convex hull in high dimensions (2016)
Fast polyhedra abstract domain (2016)
End to End Learning for Self-Driving Cars (2016)
Using Deep Learning to Predict Steering Angles (Udacity) (2016)
The convex hull problem in practice: improving the running time of the double description method (PhD thesis, Genov) (2015)
Finding convex hull vertices in metric space (2014)
A simple algorithm for convex hull determination in high dimensions (2013)
Intriguing properties of neural networks (2013)
The Octahedron Abstract Domain (2004)
Beneath-and-Beyond Revisited (2003)
An approximate algorithm for computing multidimensional convex hulls (1998)
Abstract interpretation (1996)
Double description method revisited (1996)
The quickhull algorithm for convex hulls (1996)
The upper bound theorem for polytopes: an easy proof of its asymptotic version (1995)
An optimal convex hull algorithm in any fixed dimension (1993)
A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra (1992)
A basis enumeration algorithm for linear systems with geometric applications (1991)
Algorithms in Combinatorial Geometry (1987)
Approximation algorithms for convex hulls (1982)
Linear Programming and Extensions (1963)
The Double Description Method (1953)