CoChat
Sign Up
PreprintCited by 33Adversarial Robustness in Machine LearningFormal Methods in VerificationSoftware Testing and Debugging Techniques

Efficient Exact Verification of Binarized Neural Networks

Open access
Jia, Kai, Rinard, Martin·2020·arXiv
DOI 10.48550/arxiv.2005.03597arXiv 2005.03597
Open this paper in CoChat — free accountOpen PDF

Abstract

Concerned with the reliability of neural networks, researchers have developed verification techniques to prove their robustness. Most verifiers work with real-valued networks. Unfortunately, the exact (complete and sound) verifiers face scalability challenges and provide no correctness guarantees due to floating point errors. We argue that Binarized Neural Networks (BNNs) provide comparable robustness and allow exact and significantly more efficient verification. We present a new system, EEV, for efficient and exact verification of BNNs. EEV consists of two parts: (i) a novel SAT solver that speeds up BNN verification by natively handling the reified cardinality constraints arising in BNN encodings; and (ii) strategies to train solver-friendly robust BNNs by inducing balanced layer-wise sparsity and low cardinality bounds, and adaptively cancelling the gradients. We demonstrate the effectiveness of EEV by presenting the first exact verification results for L-inf-bounded adversarial robustness of nontrivial convolutional BNNs on the MNIST and CIFAR10 datasets. Compared to exact verification of real-valued networks of the same architectures on the same tasks, EEV verifies BNNs hundreds to thousands of times faster, while delivering comparable verifiable accuracy in most cases.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.2005.03597

Cites

3 of 3 references verified0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Extreme quantization is being extended to natural language processing tasks.

    “Recently, there have been attempts to extend this idea to Natural Language Processing (NLP) tasks [7,119,121,278].”

    From A Survey of Quantization Methods for Efficient Neural Network Inference (2022) · cites this paper as [121]

    The Experiments section (p. 8) evaluates binarized networks on MNIST and CIFAR10, but does not discuss NLP tasks. Searches for natural language processing, language tasks, and NLP found no passage in our copy addressing whether extreme quantization is being extended to NLP. (LLM, conf=0.75)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

Flagged first, then by citations

Research works printed but not linked: 60

  1. [1][1] Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks and their applications. In International Conference on Theory and Applications of Satisfiability Testing , pages 167-180. Springer, 2009. -
  2. [2][2] Anish Athalye, Nicholas Carlini, and David Wagner. Obfuscated gradients give a false sense of security: Circumventing defenses to adversarial examples. In Jennifer Dy and Andreas Krause, editors, Proceedings of the 35th International Conference on Machine Learning , volume 80 of Proceedings of Machine Learning Research , pages 274-283, Stockholmsmässan, Stockholm Sweden, 10-15 Jul 2018. PMLR. -
  3. [3][3] Gilles Audemard and Laurent Simon. On the Glucose SAT solver. International Journal on Artificial Intelligence Tools , 27(01):1840001, 2018. -
  4. [4][4] Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S Meel, and Prateek Saxena. Quantitative verification of neural networks and its security applications. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security , pages 1249-1264, 2019. -
  5. [5][5] Tomás Balyo, Marijn JH Heule, and Matti Jarvisalo. SAT competition 2016: Recent developments. In Thirty-First AAAI Conference on Artificial Intelligence , 2017. -
  6. [6][6] Yoshua Bengio, Nicholas Léonard, and Aaron Courville. Estimating or propagating gradients through stochastic neurons for conditional computation. arXiv preprint arXiv:1308.3432 , 2013. - · arXiv
  7. [7][7] Joseph Bethge, Haojin Yang, Marvin Bornstein, and Christoph Meinel. Back to simplicity: How to train accurate bnns from scratch? arXiv preprint arXiv:1906.08637 , 2019. - · arXiv
  8. [8][8] Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability , volume 185. IOS press, 2009. -
  9. [9][9] Jacob Buckman, Aurko Roy, Colin Raffel, and Ian Goodfellow. Thermometer encoding: One hot way to resist adversarial examples. In International Conference on Learning Representations , 2018. -
  10. [10][10] 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. -
  11. [11][11] Nicholas Carlini and David Wagner. Towards evaluating the robustness of neural networks. In 2017 ieee symposium on security and privacy (sp) , pages 39-57. IEEE, 2017. -
  12. [12][12] Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In International Symposium on Automated Technology for Verification and Analysis , pages 251-268. Springer, 2017. -
  13. [13][13] Chih-Hong Cheng, Georg Nührenberg, Chung-Hao Huang, and Harald Ruess. Verification of binarized neural networks via inter-neuron factoring. In Working Conference on Verified Software: Theories, Tools, and Experiments , pages 279-290. Springer, 2018. -
  14. [14][14] Stephen A Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing , pages 151-158, 1971. -
  15. [15][15] Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages 337-340. Springer, 2008. -
  16. [17][17] Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium , pages 121-138. Springer, 2018. -
  17. [18][18] Krishnamurthy Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovic, Brendan O'Donoghue, Jonathan Uesato, and Pushmeet Kohli. Training verified learners with learned verifiers. arXiv preprint arXiv:1805.10265 , 2018. - · arXiv
  18. [19][19] Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In International conference on theory and applications of satisfiability testing , pages 502-518. Springer, 2003. -
  19. [20][20] Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In International Symposium on Automated Technology for Verification and Analysis , pages 269286. Springer, 2017. -
  20. [21][21] Matteo Fischetti and Jason Jo. Deep neural networks and mixed integer linear optimization. Constraints , 23(3):296-309, 2018. -
  21. [22][22] Jonathan Frankle and Michael Carbin. The lottery ticket hypothesis: Finding sparse, trainable neural networks. In International Conference on Learning Representations , 2019. -
  22. [23][23] Angus Galloway, Graham W. Taylor, and Medhat Moussa. Attacking binarized neural networks. In International Conference on Learning Representations , 2018. URL https://openreview. net/forum?id=HkTEFfZRb . -
  23. [24][24] Vijay Ganesh, Charles W O'donnell, Mate Soos, Srinivas Devadas, Martin C Rinard, and Armando Solar-Lezama. Lynx: A programmatic SAT solver for the RNA-folding problem. In International Conference on Theory and Applications of Satisfiability Testing , pages 143-156. Springer, 2012. -
  24. [25][25] Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP) , pages 3-18. IEEE, 2018. -
  25. [26][26] Ian Goodfellow, Yoshua Bengio, and Aaron Courville. Deep Learning . MIT Press, 2016. http://www.deeplearningbook.org . -
  26. [27][27] Song Han, Jeff Pool, John Tran, and William Dally. Learning both weights and connections for efficient neural network. In Advances in neural information processing systems , pages 1135-1143, 2015. -
  27. [28][28] Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In International Conference on Computer Aided Verification , pages 3-29. Springer, 2017. -
  28. [29][29] Itay Hubara, Matthieu Courbariaux, Daniel Soudry, Ran El-Yaniv, and Yoshua Bengio. Binarized neural networks. In D. D. Lee, M. Sugiyama, U. V. Luxburg, I. Guyon, and R. Garnett, editors, Advances in Neural Information Processing Systems 29 , pages 4107-4115. Curran Associates, Inc., 2016. -
  29. [30][30] Sergey Ioffe and Christian Szegedy. Batch normalization: Accelerating deep network training by reducing internal covariate shift. arXiv preprint arXiv:1502.03167 , 2015. - · arXiv
  30. [31][31] Benoit Jacob, Skirmantas Kligys, Bo Chen, Menglong Zhu, Matthew Tang, Andrew Howard, Hartwig Adam, and Dmitry Kalenichenko. Quantization and training of neural networks for efficient integer-arithmetic-only inference. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition , pages 2704-2713, 2018. -
  31. [32][32] Kai Jia and Martin Rinard. Exploiting verified neural networks via floating point numerical error. arXiv preprint arXiv:2003.03021 , 2020. - · arXiv
  32. [33][33] Mainuddin Ahmad Jonas and David Evans. Certifying joint adversarial robustness for model ensembles. arXiv preprint arXiv:2004.10250 , 2020. - · arXiv
  33. [35][35] Elias B Khalil, Amrita Gupta, and Bistra Dilkina. Combinatorial attacks on binarized neural networks. In International Conference on Learning Representations , 2019. -
  34. [37][37] Mark H Liffiton and Jordyn C Maglalang. A cardinality solver: more expressive constraints for free. In International Conference on Theory and Applications of Satisfiability Testing , pages 485-486. Springer, 2012. -
  35. [38][38] Alessio Lomuscio and Lalit Maganti. An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351 , 2017. - · arXiv
  36. [39][39] Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In International Conference on Learning Representations , 2018. -
  37. [40][40] Joao Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of satisfiability , pages 131-153. ios Press, 2009. -
  38. [41][41] Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In Jennifer Dy and Andreas Krause, editors, Proceedings of the 35th International Conference on Machine Learning , volume 80 of Proceedings of Machine Learning Research , pages 3578-3586, Stockholmsmässan, Stockholm Sweden, 10-15 Jul 2018. PMLR. -
  39. [42][42] Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th annual Design Automation Conference , pages 530-535, 2001. -
  40. [43][43] Duncan JM Moss, Eriko Nurvitadhi, Jaewoong Sim, Asit Mishra, Debbie Marr, Suchit Subhaschandra, and Philip HW Leong. High performance binary neural networks on the Xeon+FPGA™platform. In 2017 27th International Conference on Field Programmable Logic and Applications (FPL) , pages 1-4. IEEE, 2017. -
  41. [44][44] Nina Narodytska, Shiva Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. Verifying properties of binarized deep neural networks. In Thirty-Second AAAI Conference on Artificial Intelligence , 2018. -
  42. [45][45] Nina Narodytska, Hongce Zhang, Aarti Gupta, and Toby Walsh. In search for a SAT-friendly binarized neural network architecture. In International Conference on Learning Representations , 2020. -
  43. [46][46] Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. PyTorch: An imperative style, highperformance deep learning library. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'AlchéBuc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems 32 , pages 8024-8035. Curran Associates, Inc., 2019. -
  44. [47][47] Knot Pipatsrisawat and Adnan Darwiche. A lightweight component caching scheme for satisfiability solvers. In International conference on theory and applications of satisfiability testing , pages 294-299. Springer, 2007. -
  45. [48][48] Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems 31 , pages 10877-10887. Curran Associates, Inc., 2018. -
  46. [49][49] Mohammad Rastegari, Vicente Ordonez, Joseph Redmon, and Ali Farhadi. Xnor-net: Imagenet classification using binary convolutional neural networks. In European conference on computer vision , pages 525-542. Springer, 2016. -
  47. [50][50] Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. In Advances in Neural Information Processing Systems , pages 9832-9842, 2019. -
  48. [52][52] Karsten Scheibler, Leonore Winterer, Ralf Wimmer, and Bernd Becker. Towards verification of artificial neural networks. In MBMV , pages 30-40, 2015. -
  49. [53][53] Andy Shih, Adnan Darwiche, and Arthur Choi. Verifying binarized neural networks by angluinstyle learning. In International Conference on Theory and Applications of Satisfiability Testing , pages 354-370. Springer, 2019. -
  50. [54][54] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proc. ACM Program. Lang. , 3(POPL), January 2019. doi: 10.1145/3290354. - · DOI
  51. [55][55] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification of neural networks. In International Conference on Learning Representations , 2019. -
  52. [56][56] Carsten Sinz. Towards an optimal cnf encoding of boolean cardinality constraints. In International conference on principles and practice of constraint programming , pages 827-831. Springer, 2005. -
  53. [57][57] Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings , pages 244-257, 2009. doi: 10.1007/978-3-642-02777-2\_24. - · DOI
  54. [58][58] Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna Estrach, Dumitru Erhan, Ian Goodfellow, and Robert Fergus. Intriguing properties of neural networks. In 2nd International Conference on Learning Representations, ICLR 2014 , 2014. -
  55. [59][59] Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations , 2019. -
  56. [61][61] Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for ReLU networks. In International Conference on Machine Learning , pages 5276-5285, 2018. -
  57. [62][62] Eric Wong and J Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. arXiv preprint arXiv:1711.00851 , 2017. - · arXiv
  58. [63][63] Kai Y. Xiao, Vincent Tjeng, Nur Muhammad (Mahi) Shafiullah, and Aleksander Madry. Training for faster adversarial robustness verification via inducing reLU stability. In International Conference on Learning Representations , 2019. -
  59. [64][64] Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems 31 , pages 4939-4948. Curran Associates, Inc., 2018. -
  60. [65][65] Shuchang Zhou, Yuxin Wu, Zekun Ni, Xinyu Zhou, He Wen, and Yuheng Zou. Dorefa-net: Training low bitwidth convolutional neural networks with low bitwidth gradients. arXiv preprint arXiv:1606.06160 , 2016. · arXiv

Cited by

Sorted by citations

Authors
Jia, K., & Rinard, M.
Affiliations
Massachusetts Institute of Technology (US)
ORCID
Venue
arXiv
Publisher
arXiv
Published
2020
Volume
33
Pages
1782-1795
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.2005.03597
arXiv
2005.03597
OpenAlex
W3021481267
Cited by
33
References
3
Citations by year
2025: 1 · 2024: 3 · 2023: 15 · 2022: 3 · 2021: 11
Type
posted content
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Adversarial Robustness in Machine Learning
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
Keywords
binary neural networks, neural network verification, adversarial robustness, SAT solvers, convolutional neural networks, MNIST, CIFAR-10

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review