Gagandeep Singh
Markus Püschel
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We present a novel method for scalable and precise certification of deep neural networks. The key technical insight behind our approach is a new abstract domain which combines floating point polyhedra with intervals and is equipped with abstract transformers specifically tailored to the setting of neural networks. Concretely, we introduce new transformers for affine transforms, the rectified linear unit (ReLU), sigmoid, tanh, and maxpool functions.
We implemented our method in a system called DeepPoly and evaluated it extensively on a range of datasets, neural architectures (including defended networks), and specifications. Our experimental results indicate that DeepPoly is more precise than prior work while scaling to large networks.
We also show how to combine DeepPoly with a form of abstraction refinement based on trace partitioning. This enables us to prove, for the first time, the robustness of the network when the input image is subjected to complex perturbations such as rotations that employ linear interpolation.
Supplemental Material
- Filippo Amato, Alberto López, Eladia María Peña-Méndez, Petr Vaňhara, Aleš Hampl, and Josef Havel. 2013. Artificial neural networks in medical diagnosis. Journal of Applied Biomedicine 11, 2 (2013), 47 – 58.Google Scholar
Cross Ref
- Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya V. Nori, and Antonio Criminisi. 2016. Measuring Neural Net Robustness with Constraints. In Proc. Neural Information Processing Systems (NIPS). 2621–2629. Google ScholarDigital Library
- Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D. Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, Xin Zhang, Jake Zhao, and Karol Zieba. 2016. End to End Learning for Self-Driving Cars. CoRR abs/1604.07316 (2016).Google Scholar
- Nicholas Carlini, Guy Katz, Clark Barrett, and David L. Dill. 2017. Ground-Truth Adversarial Examples. CoRR abs/1709.10207 (2017).Google Scholar
- Nicholas Carlini and David A. Wagner. 2017. Towards Evaluating the Robustness of Neural Networks. In Proc. IEEE Symposium on Security and Privacy (SP). 39–57.Google Scholar
- Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints Among Variables of a Program. In Proc. Principles of Programming Languages (POPL). 84–96. Google ScholarDigital Library
- Yinpeng Dong, Fangzhou Liao, Tianyu Pang, Hang Su, Jun Zhu, Xiaolin Hu, and Jianguo Li. 2018. Boosting adversarial attacks with momentum. In Proc. Computer Vision and Pattern Recognition (CVPR).Google ScholarCross Ref
- Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. 2018. A Dual Approach to Scalable Verification of Deep Networks. In Proc. Uncertainty in Artificial Intelligence (UAI). 162–171.Google Scholar
- Rüdiger Ehlers. 2017. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. In Proc. Automated Technology for Verification and Analysis (ATVA). 269–286.Google ScholarCross Ref
- Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In Proc. IEEE Symposium on Security and Privacy (SP), Vol. 00. 948–963.Google ScholarCross Ref
- Khalil Ghorbal, Eric Goubault, and Sylvie Putot. 2009. The Zonotope Abstract Domain Taylor1+. In Proc. Computer Aided Verification (CAV). 627–633. Google ScholarDigital Library
- Ian Goodfellow, Jonathon Shlens, and Christian Szegedy. 2015. Explaining and Harnessing Adversarial Examples. In Proc. International Conference on Learning Representations (ICLR).Google Scholar
- Kathrin Grosse, Nicolas Papernot, Praveen Manoharan, Michael Backes, and Patrick D. McDaniel. 2016. Adversarial Perturbations Against Deep Neural Networks for Malware Classification. CoRR abs/1606.04435 (2016). http://arxiv.org/ abs/1606.04435Google Scholar
- Shixiang Gu and Luca Rigazio. 2014. Towards deep neural network architectures robust to adversarial examples. arXiv preprint arXiv:1412.5068 (2014).Google Scholar
- Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Proc. International Conference on Computer Aided Verification (CAV). 97–117.Google Scholar
- Alex Krizhevsky. 2009. Learning multiple layers of features from tiny images. Technical Report.Google Scholar
- Yann Lecun, Léon Bottou, Yoshua Bengio, and Patrick Haffner. 1998. Gradient-based learning applied to document recognition. In Proc. of the IEEE. 2278–2324.Google ScholarCross Ref
- Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. 2018. Towards deep learning models resistant to adversarial attacks. In Proc. International Conference on Learning Representations (ICLR).Google Scholar
- Antoine Miné. 2004. Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors. In Proc. European Symposium on Programming (ESOP). 3–17.Google ScholarCross Ref
- Matthew Mirman, Timon Gehr, and Martin Vechev. 2018. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In Proc. International Conference on Machine Learning (ICML). 3575–3583.Google Scholar
- Anh Mai Nguyen, Jason Yosinski, and Jeff Clune. 2015. Deep neural networks are easily fooled: High confidence predictions for unrecognizable images. In Proc. IEEE Computer Vision and Pattern Recognition (CVPR). 427–436.Google ScholarCross Ref
- Kexin Pei, Yinzhi Cao, Junfeng Yang, and Suman Jana. 2017a. DeepXplore: Automated Whitebox Testing of Deep Learning Systems. In Proc. Symposium on Operating Systems Principles (SOSP). 1–18. Google ScholarDigital Library
- Kexin Pei, Yinzhi Cao, Junfeng Yang, and Suman Jana. 2017b. Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems. CoRR abs/1712.01785 (2017).Google Scholar
- Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. 2018. Certified Defenses against Adversarial Examples. In Proc. International Conference on Machine Learning (ICML).Google Scholar
- Xavier Rival and Laurent Mauborgne. 2007. The Trace Partitioning Abstract Domain. ACM Trans. Program. Lang. Syst. 29, 5 (2007). Google ScholarDigital Library
- Sara Sabour, Yanshuai Cao, Fartash Faghri, and David J. Fleet. 2015. Adversarial Manipulation of Deep Representations. CoRR abs/1511.05122 (2015).Google Scholar
- Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. 2018a. Fast and Effective Robustness Certification. In Proc. Neural Information Processing Systems (NIPS).Google Scholar
- Gagandeep Singh, Markus Püschel, and Martin Vechev. 2017. Fast Polyhedra Abstract Domain. In Proc. Principles of Programming Languages (POPL). 46–59. Google ScholarDigital Library
- Gagandeep Singh, Markus Püschel, and Martin Vechev. 2018b. A Practical Construction for Decomposing Numerical Abstract Domains. Proc. ACM Program. Lang. 2, POPL (2018), 55:1–55:28. Google ScholarDigital Library
- Pedro Tabacof and Eduardo Valle. 2016. Exploring the space of adversarial images. In Proc. International Joint Conference on Neural Networks (IJCNN). 426–433.Google ScholarCross Ref
- Vincent Tjeng and Russ Tedrake. 2017. Verifying Neural Networks with Mixed Integer Programming. CoRR abs/1711.07356 (2017).Google Scholar
- Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal Security Analysis of Neural Networks using Symbolic Intervals. In Proc. USENIX Security Symposium (USENIX Security 18). 1599–1614. Google ScholarDigital Library
- Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. 2018. Towards Fast Computation of Certified Robustness for ReLU Networks. In Proc. International Conference on Machine Learning (ICML). 5273–5282.Google Scholar
- Eric Wong and Zico Kolter. 2018. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In Proc. International Conference on Machine Learning (ICML). 5283–5292.Google Scholar
Index Terms
- An abstract domain for certifying neural networks
Recommendations
Quantized neural networks: training neural networks with low precision weights and activations
We introduce a method to train Quantized Neural Networks (QNNs) -- neural networks with extremely low precision (e.g., 1-bit) weights and activations, at run-time. At traintime the quantized weights and activations are used for computing the parameter ...
Minimal gated unit for recurrent neural networks
Recurrent neural networks (RNN) have been very successful in handling sequence data. However, understanding RNN and finding the best practices for RNN learning is a difficult task, partly because there are many competing and complex hidden units, such ...
New Results for Prediction of Chaotic Systems Using Deep Recurrent Neural Networks
AbstractPrediction of nonlinear and dynamic systems is a challenging task, however with the aid of machine learning techniques, particularly neural networks, is now possible to accomplish this objective. Most common neural networks used are the multilayer ...
Comments