Sound and Complete Verification of Polynomial Networks
- URL: http://arxiv.org/abs/2209.07235v1
- Date: Thu, 15 Sep 2022 11:50:43 GMT
- Title: Sound and Complete Verification of Polynomial Networks
- Authors: Elias Abad Rocamora, Mehmet Fatih Sahin, Fanghui Liu, Grigorios G
Chrysos, Volkan Cevher
- Abstract summary: Polynomial Networks (PNs) have demonstrated promising performance on face and image recognition recently.
Existing verification algorithms on ReLU neural networks (NNs) based on branch and bound (BaB) techniques cannot be trivially applied to PN verification.
We devise a new bounding method, equipped with BaB for global convergence guarantees, called VPN.
- Score: 55.9260539566555
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Polynomial Networks (PNs) have demonstrated promising performance on face and
image recognition recently. However, robustness of PNs is unclear and thus
obtaining certificates becomes imperative for enabling their adoption in
real-world applications. Existing verification algorithms on ReLU neural
networks (NNs) based on branch and bound (BaB) techniques cannot be trivially
applied to PN verification. In this work, we devise a new bounding method,
equipped with BaB for global convergence guarantees, called VPN. One key
insight is that we obtain much tighter bounds than the interval bound
propagation baseline. This enables sound and complete PN verification with
empirical validation on MNIST, CIFAR10 and STL10 datasets. We believe our
method has its own interest to NN verification.
Related papers
- DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using
Bernstein Polynomial Activations and Precise Bound Propagation [1.4620086904601473]
We introduce DeepBerns, a class of NNs with activation functions based on Bernsteins instead of ReLU activation.
We design a novel algorithm, called Bern-IBP, to efficiently compute tight bounds on DeepBern-Nets outputs.
This work establishes Bernstein activation as a promising alternative for improving NN certification tasks across various applications.
arXiv Detail & Related papers (2023-05-22T21:52:57Z) - Quantization-aware Interval Bound Propagation for Training Certifiably
Robust Quantized Neural Networks [58.195261590442406]
We study the problem of training and certifying adversarially robust quantized neural networks (QNNs)
Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization.
We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
arXiv Detail & Related papers (2022-11-29T13:32:38Z) - Can pruning improve certified robustness of neural networks? [106.03070538582222]
We show that neural network pruning can improve empirical robustness of deep neural networks (NNs)
Our experiments show that by appropriately pruning an NN, its certified accuracy can be boosted up to 8.2% under standard training.
We additionally observe the existence of certified lottery tickets that can match both standard and certified robust accuracies of the original dense models.
arXiv Detail & Related papers (2022-06-15T05:48:51Z) - A Mixed Integer Programming Approach for Verifying Properties of
Binarized Neural Networks [44.44006029119672]
We propose a mixed integer programming formulation for BNN verification.
We demonstrate our approach by verifying properties of BNNs trained on the MNIST dataset and an aircraft collision avoidance controller.
arXiv Detail & Related papers (2022-03-11T01:11:29Z) - Neural Network Branch-and-Bound for Neural Network Verification [26.609606492971967]
We propose a novel machine learning framework that can be used for designing an effective branching strategy.
We learn two graph neural networks (GNNs) that both directly treat the network we want to verify as a graph input.
We show that our GNN models generalize well to harder properties on larger unseen networks.
arXiv Detail & Related papers (2021-07-27T14:42:57Z) - Certification of Iterative Predictions in Bayesian Neural Networks [79.15007746660211]
We compute lower bounds for the probability that trajectories of the BNN model reach a given set of states while avoiding a set of unsafe states.
We use the lower bounds in the context of control and reinforcement learning to provide safety certification for given control policies.
arXiv Detail & Related papers (2021-05-21T05:23:57Z) - Beta-CROWN: Efficient Bound Propagation with Per-neuron Split
Constraints for Complete and Incomplete Neural Network Verification [151.62491805851107]
We develop $beta$-CROWN, a bound propagation based verifier that can fully encode per-neuron splits.
$beta$-CROWN is close to three orders of magnitude faster than LP-based BaB methods for robustness verification.
By terminating BaB early, our method can also be used for incomplete verification.
arXiv Detail & Related papers (2021-03-11T11:56:54Z) - Enabling certification of verification-agnostic networks via
memory-efficient semidefinite programming [97.40955121478716]
We propose a first-order dual SDP algorithm that requires memory only linear in the total number of network activations.
We significantly improve L-inf verified robust accuracy from 1% to 88% and 6% to 40% respectively.
We also demonstrate tight verification of a quadratic stability specification for the decoder of a variational autoencoder.
arXiv Detail & Related papers (2020-10-22T12:32:29Z) - Scalable Quantitative Verification For Deep Neural Networks [44.570783946111334]
We propose a test-driven verification framework for deep neural networks (DNNs)
Our technique performs enough tests until soundness of a formal probabilistic property can be proven.
Our work paves the way for verifying properties of distributions captured by real-world deep neural networks, with provable guarantees.
arXiv Detail & Related papers (2020-02-17T09:53:50Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.