Verification of deep convolutional neural networks using ImageStars
From MaRDI portal
Abstract: Convolutional Neural Networks (CNN) have redefined the state-of-the-art in many real-world applications, such as facial recognition, image classification, human pose estimation, and semantic segmentation. Despite their success, CNNs are vulnerable to adversarial attacks, where slight changes to their inputs may lead to sharp changes in their output in even well-trained networks. Set-based analysis methods can detect or prove the absence of bounded adversarial attacks, which can then be used to evaluate the effectiveness of neural network training methodology. Unfortunately, existing verification approaches have limited scalability in terms of the size of networks that can be analyzed. In this paper, we describe a set-based framework that successfully deals with real-world CNNs, such as VGG16 and VGG19, that have high accuracy on ImageNet. Our approach is based on a new set representation called the ImageStar, which enables efficient exact and over-approximative analysis of CNNs. ImageStars perform efficient set-based analysis by combining operations on concrete images with linear programming (LP). Our approach is implemented in a tool called NNV, and can verify the robustness of VGG networks with respect to a small set of input states, derived from adversarial attacks, such as the DeepFool attack. The experimental results show that our approach is less conservative and faster than existing zonotope methods, such as those used in DeepZ, and the polytope method used in DeepPoly.
Recommendations
- Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter
- Safety verification of deep neural networks
- Robustness verification of semantic segmentation neural networks using relaxed reachability
- Reluplex: a calculus for reasoning about deep neural networks
- An abstraction-based framework for neural network verification
Cited in
(26)- Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter
- Improving neural network verification through spurious region guided refinement
- Enhancing robustness verification for deep neural networks via symbolic propagation
- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
- Reachability analysis of a general class of neural ordinary differential equations
- An SMT-based approach for verifying binarized neural networks
- Global optimization of objective functions represented by ReLU networks
- Boosting robustness verification of semantic feature neighborhoods
- The octatope abstract domain for verification of neural networks
- Quantitative Verification for Neural Networks using ProbStars
- Verification of Recurrent Neural Networks with Star Reachability
- Maximum output discrepancy computation for convolutional neural network compression
- \textsf{QEBVerif}: quantization error bound verification of neural networks
- Efficient neural network analysis with sum-of-infeasibilities
- LinSyn: synthesizing tight linear bounds for arbitrary neural network activation functions
- Verifying the generalization of deep learning to out-of-distribution domains
- The hexatope and octatope abstract domains for neural network verification
- Quantitative verification of learning-enabled systems using ProbStar reachability
- DNN verification, reachability, and the exponential function problem
- Reachability analysis of recurrent neural networks
- ModelStar: reachability analysis-based safety verification of neural networks against model perturbations
- Towards verified and targeted explanations through formal methods
- Robustness verification of quantum classifiers
- \textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks
- Verisig 2.0: verification of neural network controllers using Taylor model preconditioning
- Robustness verification of semantic segmentation neural networks using relaxed reachability
This page was built for publication: Verification of deep convolutional neural networks using ImageStars
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225072)
