# Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming

NIPS 2020, 2020.

EI

Weibo:

Abstract:

Convex relaxations have emerged as a promising approach for verifying desirable properties of neural networks like robustness to adversarial perturbations. Widely used Linear Programming (LP) relaxations only work well when networks are trained to facilitate verification. This precludes applications that involve verification-agnostic ne...More

Introduction

- Applications of neural networks to safety-critical domains requires ensuring that they behave as expected under all circumstances [31].
- Several techniques that claimed to enhance neural network robustness were later shown to break under stronger attacks [60, 5].
- This has motivated the search for verification algorithms that can provide provable guarantees on neural networks satisfying input-output specifications

Highlights

- Applications of neural networks to safety-critical domains requires ensuring that they behave as expected under all circumstances [31]
- One way to achieve this is to ensure that neural networks conform with a list of specifications, i.e., relationships between the inputs and outputs of a neural network that ought to be satisfied
- We demonstrate the applicability of first-order semidefinite programming (SDP) techniques to neural network verification
- We focus on SDP relaxations but develop customized solvers that can run on accelerators for deep learning (GPUs/TPUs) enabling their application to large convolutional neural network (CNN)
- To visualize the improvements resulting from our solver, we include a comparison with guarantees based on interval arithmetic bound propagation (IBP) [22, 38], which we use to generate the bounds used in Algorithm 1
- On all networks we study, we significantly improve on the baseline verified accuracies
- Compared to IBP, SDP-FO can successfully verify at perturbation radii roughly 50x as large

Methods

- The authors evaluate the SDP-FO verification algorithm on two specifications: robustness to adversarial perturbations for image classifiers (Sec. 6.1), and robustness to latent space perturbations for a generative model (Sec. 6.2).
- In both cases, the authors focus on verification-agnostic networks.
- The authors further compare to the SDP relaxation from [50] solved using MOSEK [3], a commercial interior point SDP (SDP-IP) solver, and the MIP approach from [58]

Results

- The authors verify a VAE on MNIST with a convolutional decoder containing « 10K total activations.
- While small-scale problems can be solved exactly with second-order interior point methods, these approaches have poor asymptotic scaling factors
- Both the SDP primal and dual problems involve matrix variables with number of elements quadratic in the number of network activations N.
- Using CROWN bounds in place of interval arithmetic bounds improves the overall verified accuracy from 83.0% to 91.2%
- This closes most of the gap to the PGD upper bound of 93.4%.

Conclusion

- The authors have developed a promising approach to scalable tight verification and demonstrated good performance on larger scale than was possible previously.
- This solver is applicable to arbitrarily large networks, further innovations are necessary to get meaningful verified guarantees on larger networks

Summary

## Introduction:

Applications of neural networks to safety-critical domains requires ensuring that they behave as expected under all circumstances [31].- Several techniques that claimed to enhance neural network robustness were later shown to break under stronger attacks [60, 5].
- This has motivated the search for verification algorithms that can provide provable guarantees on neural networks satisfying input-output specifications
## Objectives:

The authors' goal is to develop a custom solver for large-scale neural network verification with the following desiderata: (1) compute anytime upper bounds valid after each iteration, (2) rely on elementary computations with efficient implementations that can exploit hardware like GPUs and TPUs, and (3) have per-iteration memory and computational cost that scales linearly in the number of neurons.- The authors' aim is to certify robustness of the decoder to perturbations in the VAE latent space
## Methods:

The authors evaluate the SDP-FO verification algorithm on two specifications: robustness to adversarial perturbations for image classifiers (Sec. 6.1), and robustness to latent space perturbations for a generative model (Sec. 6.2).- In both cases, the authors focus on verification-agnostic networks.
- The authors further compare to the SDP relaxation from [50] solved using MOSEK [3], a commercial interior point SDP (SDP-IP) solver, and the MIP approach from [58]
## Results:

The authors verify a VAE on MNIST with a convolutional decoder containing « 10K total activations.- While small-scale problems can be solved exactly with second-order interior point methods, these approaches have poor asymptotic scaling factors
- Both the SDP primal and dual problems involve matrix variables with number of elements quadratic in the number of network activations N.
- Using CROWN bounds in place of interval arithmetic bounds improves the overall verified accuracy from 83.0% to 91.2%
- This closes most of the gap to the PGD upper bound of 93.4%.
## Conclusion:

The authors have developed a promising approach to scalable tight verification and demonstrated good performance on larger scale than was possible previously.- This solver is applicable to arbitrarily large networks, further innovations are necessary to get meaningful verified guarantees on larger networks

- Table1: Comparison of verified accuracy across verification algorithms. Highlighted rows indicate models trained in a verification-agnostic manner. All numbers computed across the same 500 test set examples, except when using previously reported values. For all networks, SDP-FO outperforms previous approaches. The improvement is largest for verification-agnostic models
- Table2: Architecture of CNN models used on MNIST and CIFAR-10. Each layer (except the last fully connected layer) is followed by ReLU activations. CONV T W×H+S corresponds to a convolutional layer with T filters of size W×H with stride of S in both dimensions. FC T corresponds to a fully connected layer with T output neurons
- Table3: The VAE consists of an encoder and a decoder, and the architecture details for both the encoder and the decoder are provided here. CONV-T T W×H+S corresponds to a transpose convolutional layer with T filters of size W×H with stride of S in both dimensions
- Table4: Comparison of verified accuracy across various networks and perturbation radii. All SDP-FO numbers computed on the first 100 test set examples, and numbers for LP on the first 1000 test set examples. The perturbations and training-modes considered here differ from those in Table 1. For all networks, SDP-FO outperforms the LP-relaxation baseline

Related work

- Neural network verification. There is a large literature on verification methods for neural networks. Broadly, the literature can be grouped into complete verification using mixed-integer programming [25, 17, 58, 10, 2], bound propagation [55, 67, 64, 20], convex relaxation [29, 16, 66, 50], and randomized smoothing [34, 11]. Verified training approaches when combined with convex relaxations have led to promising results [29, 50, 22, 6]. Randomized smoothing and verified training approaches requires special modifications to the predictor (smoothing the predictions by adding noise) and/or the training algorithm (training with additional noise or regularizers) and hence are not applicable to the verification-agnostic setting. Bound propagation approaches have been shown to be special instances of LP relaxations [36]. Hence we focus on describing the convex relaxations and complete solvers, as the areas most closely related to this paper.

Funding

- This work was supported by NSF Award Grant no. 1805310
- AR was supported by a Google PhD Fellowship and Open Philanthropy Project AI Fellowship

Study subjects and analysis

samples: 100

Enabling certification of verification-agnostic networks. For 100 random examples on MNIST and CIFAR-10, we plot the verified upper bound on φx against the adversarial lower bound (taking the worst-case over target labels for each). Recall, an example is verified when the verified upper bound φx ă 0. Our key result is that SDP-FO achieves tight verification across all examples, with all points lying close to the line y “ x. In contrast, LP or CROWN bounds produce much looser gaps between the lower and upper bounds. We note that many CROWN bounds exceed the plotted y-axis limits. Comparison of different approaches for verifying the robustness of the decoder of a VAE on MNIST, measured across 100 samples. The lower-bound on the robust accuracy computed with SDP-FO closely matches the upper bound based on a PGD adversarial attack upto perturbations of 0.1 σz, while the lower bound based on IBP begins to diverge from the PGD upper bound at much smaller perturbations. Two digits from the MNIST data set, and the corresponding images when perturbed with Gaussian noise, whose squared 2-norm is equal to the threshold (τ “ 40.97). τ corresponds to threshold on the reconstruction error used in equation (7)

Reference

- Martín Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, et al. Tensorflow: A system for large-scale machine learning. In 12th tUSENIXu Symposium on Operating Systems Design and Implementation (tOSDIu 16), pages 265–283, 2016.
- Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming, pages 1–37, 2020.
- MOSEK ApS. The MOSEK optimization toolbox for MATLAB manual. Version 9.0., 2019. URL http://docs.mosek.com/9.0/toolbox/index.html.
- Sanjeev Arora and Satyen Kale. A combinatorial, primal-dual approach to semidefinite programs. J. ACM, 63(2), May 2016. ISSN 0004-5411. doi: 10.1145/2837020. URL https://doi.org/10.1145/2837020.
- Anish Athalye, Nicholas Carlini, and David Wagner. Obfuscated gradients give a false sense of security: Circumventing defenses to adversarial examples. arXiv preprint arXiv:1802.00420, 2018.
- Mislav Balunovic and Martin Vechev. Adversarial training and provable defenses: Bridging the gap. In International Conference on Learning Representations, 2020. URL https://openreview.net/forum?id=SJxSDxrKDr.
- Battista Biggio, Igino Corona, Davide Maiorca, Blaine Nelson, Nedim Šrndic, Pavel Laskov, Giorgio Giacinto, and Fabio Roli. Evasion attacks against machine learning at test time. In Joint European conference on machine learning and knowledge discovery in databases, pages 387–402.
- James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, and Skye Wanderman-Milne. Jax: composable transformations of python+ numpy programs, 201URL http://github.com/google/jax, page 18.
- James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, and Skye Wanderman-Milne. JAX: composable transformations of Python+NumPy programs, 2018. URL http://github.com/google/jax.
- Rudy R Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan K Mudigonda. A unified view of piecewise linear neural network verification. In Advances in Neural Information Processing Systems, pages 4790–4799, 2018.
- Jeremy M Cohen, Elan Rosenfeld, and J Zico Kolter. Certified adversarial robustness via randomized smoothing. arXiv preprint arXiv:1902.02918, 2019.
- Gal Dalal, Krishnamurthy Dvijotham, Matej Vecerik, Todd Hester, Cosmin Paduraru, and Yuval Tassa. Safe exploration in continuous action spaces. arXiv preprint arXiv:1801.08757, 2018.
- John M Danskin. The theory of max-min with applications. Siam J. Appl. Math, 1966.
- Alexandre d’Aspremont and Noureddine El Karoui. A stochastic smoothing algorithm for semidefinite programming. SIAM Journal on Optimization, 24(3):1138–1177, 2014.
- John Duchi, Elad Hazan, and Yoram Singer. Adaptive subgradient methods for online learning and stochastic optimization. Journal of machine learning research, 12(Jul):2121–2159, 2011.
- Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. A dual approach to scalable verification of deep networks. arXiv preprint arXiv:1803.06567, 104, 2018.
- Rüdiger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In Deepak D’Souza and K. Narayan Kumar, editors, Automated Technology for Verification and Analysis, pages 269–286, Cham, 20Springer International Publishing. ISBN 978-3-319-68167-2.
- Mahyar Fazlyab, Manfred Morari, and George J Pappas. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. arXiv preprint arXiv:1903.01287, 2019.
- Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George Pappas. Efficient and accurate estimation of lipschitz constants for deep neural networks. In Advances in Neural Information Processing Systems, pages 11423–11434, 2019.
- Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai 2: Safety and robustness certification of neural networks with abstract interpretation. In Security and Privacy (SP), 2018 IEEE Symposium on, 2018.
- Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arXiv:1810.12715, 2018.
- Sven Gowal, Krishnamurthy Dj Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In Proceedings of the IEEE International Conference on Computer Vision, pages 4842–4851, 2019.
- Sven Gowal, Chongli Qin, Po-Sen Huang, Taylan Cemgil, Krishnamurthy Dvijotham, Timothy Mann, and Pushmeet Kohli. Achieving robustness in the wild via adversarial mixing with disentangled representations. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pages 1211–1220, 2020.
- Christoph Helmberg and Franz Rendl. A spectral bundle method for semidefinite programming. SIAM Journal on Optimization, 10(3):673–696, 2000.
- Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pages 97–117.
- Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014.
- Diederik P. Kingma and Max Welling. Auto-encoding variational bayes. In Yoshua Bengio and Yann LeCun, editors, 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings, 2014. URL http://arxiv.org/abs/1312.6114.
- Torsten Koller, Felix Berkenkamp, Matteo Turchetta, and Andreas Krause. Learning-based model predictive control for safe exploration. In 2018 IEEE Conference on Decision and Control (CDC), pages 6059–6066. IEEE, 2018.
- J Zico Kolter and Eric Wong. Provable defenses against adversarial examples via the convex outer adversarial polytope. arXiv preprint arXiv:1711.00851, 2017.
- Jacek Kuczynski and Henryk Wozniakowski. Estimating the largest eigenvalue by the power and lanczos algorithms with a random start. SIAM journal on matrix analysis and applications, 13(4):1094–1122, 1992.
- Lindsey Kuper, Guy Katz, Justin Gottschlich, Kyle Julian, Clark Barrett, and Mykel Kochenderfer. Toward scalable verification for safety-critical deep networks. arXiv preprint arXiv:1801.05950, 2018.
- Guanghui Lan, Zhaosong Lu, and Renato DC Monteiro. Primal-dual first-order methods with Op1{ ) iteration-complexity for cone programming. Mathematical Programming, 126(1):1–29, 2011.
- Cornelius Lanczos. An iteration method for the solution of the eigenvalue problem of linear differential and integral operators. United States Governm. Press Office Los Angeles, CA, 1950.
- Mathias Lecuyer, Vaggelis Atlidakis, Roxana Geambasu, Daniel Hsu, and Suman Jana. Certified robustness to adversarial examples with differential privacy. arXiv preprint arXiv:1802.03471, 2018.
- Claude Lemaréchal and François Oustry. Nonsmooth algorithms to solve semidefinite programs. In Advances in linear matrix inequality methods in control, pages 57–77. SIAM, 2000.
- Changliu Liu, Tomer Arnon, Christopher Lazarus, Clark Barrett, and Mykel J Kochenderfer. Algorithms for verifying deep neural networks. arXiv preprint arXiv:1903.06758, 2019.
- Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.06083, 2017.
- Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In International Conference on Machine Learning, pages 3575–3583, 2018.
- Teodor Mihai Moldovan and Pieter Abbeel. Safe exploration in markov decision processes. arXiv preprint arXiv:1205.4810, 2012.
- Renato DC Monteiro. First-and second-order methods for semidefinite programming. Mathematical Programming, 97(1-2):209–244, 2003.
- Yurii Nesterov. Smoothing technique and its applications in semidefinite optimization. Mathematical Programming, 110(2):245–259, 2007.
- Yurii Nesterov. Lectures on convex optimization, volume 137.
- T. E. Oliphant. Python for scientific computing. Computing in Science Engineering, 9(3):10–20, 2007.
- Neal Parikh and Stephen Boyd. Proximal algorithms. Foundations and Trends in optimization, 1(3):127–239, 2014.
- Beresford N Parlett. The symmetric eigenvalue problem, volume 20. siam, 1998.
- Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, et al. Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Systems, pages 8024–8035, 2019.
- Barak A Pearlmutter. Fast exact multiplication by the hessian. Neural computation, 6(1): 147–160, 1994.
- Chongli Qin, Krishnamurthy (Dj) Dvijotham, Brendan O’Donoghue, Rudy Bunel, Robert Stanforth, Sven Gowal, Jonathan Uesato, Grzegorz Swirszcz, and Pushmeet Kohli. Verification of non-linear specifications for neural networks. In International Conference on Learning Representations, 2019. URL https://openreview.net/forum?id=HyeFAsRctQ.
- Haonan Qiu, Chaowei Xiao, Lei Yang, Xinchen Yan, Honglak Lee, and Bo Li. Semanticadv: Generating adversarial examples via attribute-conditional image editing. arXiv preprint arXiv:1906.07927, 2019.
- Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Certified defenses against adversarial examples. In International Conference on Learning Representations, 2018. URL https://openreview.net/forum?id=Bys4ob-Rb.
- Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems, pages 10877–10887, 2018.
- James Renegar. Efficient first-order methods for linear programming and semidefinite programming. arXiv preprint arXiv:1409.5832, 2014.
- Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robust verification of neural networks. arXiv preprint arXiv:1902.08722, 2019.
- Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. CoRR, abs/1902.08722, 2019. URL http://arxiv.org/abs/1902.08722.
- Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems 31, pages 10802–10813. Curran Associates, Inc., 2018. URL http://papers.nips.cc/paper/8278-fast-and-effective-robustness-certification.pdf.
- Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199, 2013.
- Tijmen Tieleman and Geoffery Hinton. Rmsprop gradient optimization. URL http://www.cs.toronto.edu/tijmen/csc321/slides/lecture_slides_lec6.pdf, 2014.
- Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations, 2019. URL https://openreview.net/forum?id=HyGIdiRqtm.
- Stephen Tu and Jingyan Wang. Practical first order methods for large scale semidefinite programming. Technical report, Technical report, University of California, Berkeley, 2014.
- Jonathan Uesato, Brendan O’Donoghue, Aaron van den Oord, and Pushmeet Kohli. Adversarial risk and the dangers of evaluating against weak attacks. arXiv preprint arXiv:1802.05666, 2018.
- Pauli Virtanen, Ralf Gommers, Travis E. Oliphant, Matt Haberland, Tyler Reddy, David Cournapeau, Evgeni Burovski, Pearu Peterson, Warren Weckesser, Jonathan Bright, Stéfan J. van der Walt, Matthew Brett, Joshua Wilson, K. Jarrod Millman, Nikolay Mayorov, Andrew R. J. Nelson, Eric Jones, Robert Kern, Eric Larson, CJ Carey, ̇Ilhan Polat, Yu Feng, Eric W. Moore, Jake Vand erPlas, Denis Laxalde, Josef Perktold, Robert Cimrman, Ian Henriksen, E. A. Quintero, Charles R Harris, Anne M. Archibald, Antônio H. Ribeiro, Fabian Pedregosa, Paul van Mulbregt, and SciPy 1. 0 Contributors. SciPy 1.0: Fundamental Algorithms for Scientific Computing in Python. Nature Methods, 17:261–272, 2020. doi: https://doi.org/10.1038/s41592-019-0686-2.
- Zaiwen Wen. First-order methods for semidefinite programming. Columbia University, 2009.
- Zaiwen Wen, Donald Goldfarb, and Wotao Yin. Alternating direction augmented lagrangian methods for semidefinite programming. Mathematical Programming Computation, 2(3-4): 203–230, 2010.
- Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Duane Boning, Inderjit S Dhillon, and Luca Daniel. Towards fast computation of certified robustness for relu networks. arXiv preprint arXiv:1804.09699, 2018.
- Eric Wong and J Zico Kolter. Learning perturbation sets for robust machine learning. arXiv preprint arXiv:2007.08450, 2020.
- Eric Wong, Frank Schmidt, Jan Hendrik Metzen, and J Zico Kolter. Scaling provable adversarial defenses. In Advances in Neural Information Processing Systems, pages 8400–8409, 2018.
- Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in neural information processing systems, pages 4939–4948, 2018.

Full Text

Tags

Comments