research-article

Open access

An abstract domain for certifying neural networks

Authors:

Gagandeep Singh,

Markus Püschel,

Martin VechevAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL

Article No.: 41, Pages 1 - 30

https://doi.org/10.1145/3290354

Published: 02 January 2019 Publication History

Abstract

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.

Supplementary Material

WEBM File (a41-singh.webm)

Download
80.41 MB

References

[1]

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.

[2]

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.

Digital Library

[3]

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).

[4]

Nicholas Carlini, Guy Katz, Clark Barrett, and David L. Dill. 2017. Ground-Truth Adversarial Examples. CoRR abs/1709.10207 (2017).

[5]

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.

[6]

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.

Digital Library

[7]

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).

[8]

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.

[9]

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.

[10]

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.

[11]

Khalil Ghorbal, Eric Goubault, and Sylvie Putot. 2009. The Zonotope Abstract Domain Taylor1+. In Proc. Computer Aided Verification (CAV). 627–633.

Digital Library

[12]

Ian Goodfellow, Jonathon Shlens, and Christian Szegedy. 2015. Explaining and Harnessing Adversarial Examples. In Proc. International Conference on Learning Representations (ICLR).

[13]

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.04435

[14]

Shixiang Gu and Luca Rigazio. 2014. Towards deep neural network architectures robust to adversarial examples. arXiv preprint arXiv:1412.5068 (2014).

[15]

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.

[16]

Alex Krizhevsky. 2009. Learning multiple layers of features from tiny images. Technical Report.

[17]

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.

[18]

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).

[19]

Antoine Miné. 2004. Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors. In Proc. European Symposium on Programming (ESOP). 3–17.

[20]

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.

[21]

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.

[22]

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.

Digital Library

[23]

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).

[24]

Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. 2018. Certified Defenses against Adversarial Examples. In Proc. International Conference on Machine Learning (ICML).

[25]

Xavier Rival and Laurent Mauborgne. 2007. The Trace Partitioning Abstract Domain. ACM Trans. Program. Lang. Syst. 29, 5 (2007).

Digital Library

[26]

Sara Sabour, Yanshuai Cao, Fartash Faghri, and David J. Fleet. 2015. Adversarial Manipulation of Deep Representations. CoRR abs/1511.05122 (2015).

[27]

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).

[28]

Gagandeep Singh, Markus Püschel, and Martin Vechev. 2017. Fast Polyhedra Abstract Domain. In Proc. Principles of Programming Languages (POPL). 46–59.

Digital Library

[29]

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.

Digital Library

[30]

Pedro Tabacof and Eduardo Valle. 2016. Exploring the space of adversarial images. In Proc. International Joint Conference on Neural Networks (IJCNN). 426–433.

[31]

Vincent Tjeng and Russ Tedrake. 2017. Verifying Neural Networks with Mixed Integer Programming. CoRR abs/1711.07356 (2017).

[32]

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.

Digital Library

[33]

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.

[34]

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.

Cited By

Lin RZhou QNan XHu T(2024)A Parallel Optimization Method for Robustness Verification of Deep Neural NetworksMathematics10.3390/math1212188412:12(1884)Online publication date: 17-Jun-2024
https://doi.org/10.3390/math12121884
Lian ZTian F(2024)DeepSI: A Sensitive-Driven Testing Samples Generation Method of Whitebox CNN Model for Edge ComputingTsinghua Science and Technology10.26599/TST.2023.901005729:3(784-794)Online publication date: Jun-2024
https://doi.org/10.26599/TST.2023.9010057
Mo ZYang YLu SXiang W(2024)Compression Repair for Feedforward Neural Networks Based on Model Equivalence Evaluation2024 American Control Conference (ACC)10.23919/ACC60939.2024.10644492(3604-3609)Online publication date: 10-Jul-2024
https://doi.org/10.23919/ACC60939.2024.10644492
Show More Cited By

Index Terms

An abstract domain for certifying neural networks
1. Computing methodologies
  1. Machine learning
    1. Machine learning approaches
      1. Neural networks
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Abstraction
      2. Program verification

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 ...
Abstract Echo State Networks
Artificial Neural Networks in Pattern Recognition
Abstract
Noisy or adverse input is a threat to the safe deployment of neural networks in production. To ensure the safe operations of such networks they need to be hardened to work under such conditions. Abstract interpretation, as a tool to formally ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue POPL

January 2019

2275 pages

EISSN:2475-1421

DOI:10.1145/3302515

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution-ShareAlike International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019

Published in PACMPL Volume 3, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

348
Total Citations
View Citations
5,499
Total Downloads

Downloads (Last 12 months)1,234
Downloads (Last 6 weeks)169

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lin RZhou QNan XHu T(2024)A Parallel Optimization Method for Robustness Verification of Deep Neural NetworksMathematics10.3390/math1212188412:12(1884)Online publication date: 17-Jun-2024
https://doi.org/10.3390/math12121884
Lian ZTian F(2024)DeepSI: A Sensitive-Driven Testing Samples Generation Method of Whitebox CNN Model for Edge ComputingTsinghua Science and Technology10.26599/TST.2023.901005729:3(784-794)Online publication date: Jun-2024
https://doi.org/10.26599/TST.2023.9010057
Mo ZYang YLu SXiang W(2024)Compression Repair for Feedforward Neural Networks Based on Model Equivalence Evaluation2024 American Control Conference (ACC)10.23919/ACC60939.2024.10644492(3604-3609)Online publication date: 10-Jul-2024
https://doi.org/10.23919/ACC60939.2024.10644492
Mukhopadhyay DSiddiqui SKarmarkar HMadhukar KKatz GFilkov VRay BZhou M(2024)Learning DNN Abstractions using Gradient DescentProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695303(2299-2303)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695303
Rivera JFranchetti FPüschel M(2024)Floating-Point TVPI Abstract DomainProceedings of the ACM on Programming Languages10.1145/36563958:PLDI(442-466)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656395
Banerjee DXu CSingh G(2024)Input-Relational Verification of Deep Neural NetworksProceedings of the ACM on Programming Languages10.1145/36563778:PLDI(1-27)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656377
Pham LSun JChristakis MPradel M(2024)Certified Continual Learning for Neural Network RegressionProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3680322(806-818)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3680322
Kabaha ACohen D(2024)Verification of Neural Networks’ Global RobustnessProceedings of the ACM on Programming Languages10.1145/36498478:OOPSLA1(1010-1039)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649847
Giacobazzi RMastroeni IPerantoni E(2024)Adversities in Abstract Interpretation - Accommodating Robustness by Abstract InterpretationACM Transactions on Programming Languages and Systems10.1145/364930946:2(1-31)Online publication date: 24-Feb-2024
https://dl.acm.org/doi/10.1145/3649309
Liu JXing YShi XSong FXu ZMing Z(2024)Abstraction and Refinement: Towards Scalable and Exact Verification of Neural NetworksACM Transactions on Software Engineering and Methodology10.1145/364438733:5(1-35)Online publication date: 3-Jun-2024
https://dl.acm.org/doi/10.1145/3644387
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents