CoChat
Sign Up
Cited by 80Formal Methods in VerificationLogic, programming, and type systemsSoftware Testing and Debugging Techniques

Introduction to Neural Network Verification

Open access
Albarghouthi, Aws·2021·Foundations and Trends® in Programming Languages
DOI 10.1561/2500000051
Open this paper in CoChat — free account

Abstract

Deep learning has transformed the way we think of software and what it can do. But deep neural networks are fragile and their behaviors are often surprising. In many settings, we need to provide formal guarantees on the safety, security, correctness, or robustness of neural networks. This monograph covers foundational ideas from formal verification and their adaptation to reasoning about neural networks and deep learning.

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

Crossref · 10.1561/2500000051

Cites

22 of 37 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?

  • This literature has proposed a range of algorithms which can be used to ensure that a given neural network satisfies a given specification, or that a system containing neural components satisfies a safety specification.

    “This literature has proposed a range of algorithms which can be used to ensure that a given neural network (potentially belonging to some restricted class) satisfies a given specification (typically specified over its interfaces), or that a system containing neural components satisfies a safety specification.”

    From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Albarghouthi (2021)

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: 47

  1. Martín Abadi and Gordon D. Plotkin. A simple differentiable programming language. Proc. ACM Program. Lang. , 4(POPL):38:1-38:28, 2020. doi: 10.1145/ 3371106. URL https://doi.org/10.1145/3371106 . · DOI
  2. Martín Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, Manjunath Kudlur, Josh Levenberg, Rajat Monga, Sherry Moore, Derek Gordon Murray, Benoit Steiner, Paul A. Tucker, Vijay Vasudevan, Pete Warden, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. Tensorflow: A system for large-scale machine learning. In Kimberly Keeton and Timothy Roscoe, editors, 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016 , pages 265283. USENIX Association, 2016. URL https://www.usenix.org/conference/ osdi16/technical-sessions/presentation/abadi .
  3. Turing Alan. On checking a large routine. In Report of a Conference on 11i9h Speed Automatic Calculating Machines , pages 67-69, 1949.
  4. Greg Anderson, Abhinav Verma, Isil Dillig, and Swarat Chaudhuri. Neurosymbolic reinforcement learning with formally verified exploration. In Hugo Larochelle, Marc'Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin, editors, Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual , 2020. URL https://proceedings.neurips.cc/ paper/2020/hash/448d5eda79895153938a8431919f4c9f-Abstract.html .
  5. Maximilian Baader, Matthew Mirman, and Martin T. Vechev. Universal approximation with certified networks. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020 . OpenReview.net, 2020. URL https://openreview.net/forum?id=B1gX8kBtPr .
  6. Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya V. Nori, and Antonio Criminisi. Measuring neural net robustness with constraints. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors, Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain , pages 2613-2621, 2016. URL https://proceedings.neurips.cc/paper/2016/hash/ 980ecd059122ce2e50136bda65c25e07-Abstract.html .
  7. Osbert Bastani, Yewen Pu, and Armando Solar-Lezama. Verifiable reinforcement learning via policy extraction. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada , pages 2499-2509, 2018. URL https://proceedings.neurips. cc/paper/2018/hash/e6d8545daa42d5ced125a4bf747b3688-Abstract.html .
  8. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability , volume 185 of Frontiers in Artificial Intelligence and Applications . IOS Press, 2009. ISBN 978-1-58603-929-5.
  9. Robert G. Bland. New finite pivoting rules for the simplex method. Math. Oper. Res. , 2(2):103-107, 1977. doi: 10.1287/moor.2.2.103. URL https://doi.org/10. 1287/moor.2.2.103 . · DOI
  10. Aleksandar Bojchevski, Johannes Klicpera, and Stephan Günnemann. Efficient robustness certificates for discrete data: Sparsity-aware randomized smoothing for graphs, images and more. In Proceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event , volume 119 of Proceedings of Machine Learning Research , pages 1003-1013. PMLR, 2020. URL http://proceedings.mlr.press/v119/bojchevski20a.html .
  11. Bob F Caviness and Jeremy R Johnson. Quantifier elimination and cylindrical algebraic decomposition . Springer Science & Business Media, 2012.
  12. Jeremy M. Cohen, Elan Rosenfeld, and J. Zico Kolter. Certified adversarial robustness via randomized smoothing. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA , volume 97 of Proceedings of Machine Learning Research , pages 1310-1320. PMLR, 2019. URL http://proceedings.mlr.press/v97/cohen19c.html .
  13. George B Dantzig. Origins of the simplex method. In A history of scientific computing , pages 141-151. 1990.
  14. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings , volume 4963 of Lecture Notes in Computer Science , pages 337-340. Springer, 2008. doi: 10.1007/ 978-3-540-78800-3\_24. URL https://doi.org/10.1007/978-3-540-78800-3\_ 24 . · DOI
  15. Marc Peter Deisenroth, A Aldo Faisal, and Cheng Soon Ong. Mathematics for machine learning . Cambridge University Press, 2020.
  16. Niklas Een. Minisat: A sat solver with conflict-clause minimization. In Proc. SAT05: 8th Int. Conf. on Theory and Applications of Satisfiability Testing , pages 502-518, 2005.
  17. Kevin Eykholt, Ivan Evtimov, Earlence Fernandes, Bo Li, Amir Rahmati, Chaowei Xiao, Atul Prakash, Tadayoshi Kohno, and Dawn Song. Robust physical-world attacks on deep learning visual classification. In 2018 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2018, Salt Lake City, UT, USA, June 1822, 2018 , pages 1625-1634. IEEE Computer Society, 2018. doi: 10.1109/CVPR. 2018.00175. URL http://openaccess.thecvf.com/content\_cvpr\_2018/html/ Eykholt\_Robust\_Physical-World\_Attacks\_CVPR\_2018\_paper.html . · DOI
  18. Aymeric Fromherz, Klas Leino, Matt Fredrikson, Bryan Parno, and Corina S. Pasareanu. Fast geometric projections for local robustness certification. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021 . OpenReview.net, 2021. URL https://openreview.net/ forum?id=zWy1uxjDdZJ .
  19. Antoine Girard. Reachability of uncertain linear systems using zonotopes. In Manfred Morari and Lothar Thiele, editors, Hybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11,
  20. 2005, Proceedings , volume 3414 of Lecture Notes in Computer Science , pages 291305. Springer, 2005. doi: 10.1007/978-3-540-31954-2\_19. URL https://doi. org/10.1007/978-3-540-31954-2\_19 . · DOI
  21. Ian J. Goodfellow, Yoshua Bengio, and Aaron C. Courville. Deep Learning . Adaptive computation and machine learning. MIT Press, 2016. ISBN 978-0-262-035613. URL http://www.deeplearningbook.org/ .
  22. Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. CoRR , abs/1810.12715, 2018. URL http://arxiv.org/abs/ 1810.12715 . · arXiv
  23. Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. Verisig: verifying safety properties of hybrid systems with neural network controllers. In Necmiye Ozay and Pavithra Prabhakar, editors, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019 , pages 169-178. ACM, 2019. doi: 10.1145/3302504.3311806. URL https://doi.org/10.1145/3302504. 3311806 . · DOI
  24. Kai Jia and Martin Rinard. Efficient exact verification of binarized neural networks, 2020a. URL https://proceedings.neurips.cc/paper/2020/hash/ 1385974ed5904a438616ff7bdb3f7439-Abstract.html .
  25. Kai Jia and Martin Rinard. Exploiting verified neural networks via floating point numerical error. CoRR , abs/2003.03021, 2020b. URL https://arxiv.org/abs/ 2003.03021 . · arXiv
  26. Mathias Lécuyer, Vaggelis Atlidakis, Roxana Geambasu, Daniel Hsu, and Suman Jana. Certified robustness to adversarial examples with differential privacy. In 2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA,
  27. Qiyang Li, Saminul Haque, Cem Anil, James Lucas, Roger B. Grosse, and JörnHenrik Jacobsen. Preventing gradient attenuation in lipschitz constrained convolutional networks. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d'Alché-Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada , pages 15364-15376, 2019. URL https://proceedings.neurips.cc/ paper/2019/hash/1ce3e6e3f452828e23a0c94572bef9d9-Abstract.html .
  28. Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 - May 3, 2018, Conference Track Proceedings . OpenReview.net, 2018. URL https://openreview.net/forum?id=rJzIBfZAb .
  29. Christoph Müller, Gagandeep Singh, Markus Püschel, and Martin T. Vechev. Neural network robustness verification on gpus. CoRR , abs/2007.10868, 2020. URL https://arxiv.org/abs/2007.10868 . · arXiv
  30. Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. Verifying properties of binarized deep neural networks. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, Proceedings of the ThirtySecond AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018 , pages 6615-6624. AAAI Press, 2018. URL https:// www.aaai.org/ocs/index.php/AAAI/AAAI18/paper/view/16898 .
  31. Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d'Alché-Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada , pages 8024-8035, 2019. URL https://proceedings.neurips.cc/paper/2019/ hash/bdbca288fee7f92f2bfa9f7012727740-Abstract.html .
  32. Luca Pulina and Armando Tacchella. An abstraction-refinement approach to verification of artificial neural networks. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings , volume 6174 of Lecture Notes in Computer Science , pages 243-257. Springer, 2010. doi: 10.1007/ 978-3-642-14295-6\_24. URL https://doi.org/10.1007/978-3-642-14295-6\_ 24 . · DOI
  33. 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 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019 . OpenReview.net, 2019. URL https://openreview.net/ forum?id=HyeFAsRctQ .
  34. Goutham Ramakrishnan and Aws Albarghouthi. Backdoors in neural models of source code. CoRR , abs/2006.06841, 2020. URL https://arxiv.org/abs/2006. 06841 . · arXiv
  35. Elan Rosenfeld, Ezra Winston, Pradeep Ravikumar, and J. Zico Kolter. Certified robustness to label-flipping attacks via randomized smoothing. In Pro- ceedings of the 37th International Conference on Machine Learning, ICML 2020, 1318 July 2020, Virtual Event , volume 119 of Proceedings of Machine Learning Research , pages 8230-8241. PMLR, 2020. URL http://proceedings.mlr.press/ v119/rosenfeld20b.html .
  36. Benjamin Sherman, Jesse Michel, and Michael Carbin. l s : computable semantics for differentiable programming with higher-order functions and datatypes. Proc. ACM Program. Lang. , 5(POPL):1-31, 2021. doi: 10.1145/3434284. URL https://doi.org/10.1145/3434284 . · DOI
  37. Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. Fast and effective robustness certification. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò CesaBianchi, and Roman Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada , pages 10825-10836, 2018. URL https://proceedings.neurips.cc/paper/2018/ hash/f2f446980d8e971ef3da97af089481c3-Abstract.html .
  38. Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin T. Vechev. Beyond the single neuron convex barrier for neural network certification. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d'AlchéBuc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Informa- tion Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada , pages 15072-15083, 2019a. URL https://proceedings.neurips.cc/paper/ 2019/hash/0a9fdbb17feb6ccb7ec405cfb85222c4-Abstract.html .
  39. Aishwarya Sivaraman, Golnoosh Farnadi, Todd D. Millstein, and Guy Van den Broeck. Counterexample-guided learning of monotonic neural networks. In Hugo Larochelle, Marc'Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin, editors, Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual , 2020. URL https://proceedings.neurips. cc/paper/2020/hash/8ab70731b1553f17c11a3bbc87e0b605-Abstract.html .
  40. Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. Intriguing properties of neural networks. 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.6199 . · arXiv
  41. Alfred Tarski. A decision method for elementary algebra and geometry. In Quantifier elimination and cylindrical algebraic decomposition , pages 24-84. Springer, 1998.
  42. Vincent Tjeng, Kai Yuanqing Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-
  43. 9, 2019 . OpenReview.net, 2019b. URL https://openreview.net/forum?id= HyGIdiRqtm .
  44. Hoang-Dung Tran, Stanley Bak, Weiming Xiang, and Taylor T. Johnson. Verification of deep convolutional neural networks using imagestars. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I , volume 12224 of Lecture Notes in Computer Science , pages 18-42. Springer, 2020b. doi: 10.1007/978-3-030-53288-8\_2. URL https://doi.org/10.1007/ 978-3-030-53288-8\_2 . · DOI
  45. Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. In H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems , volume 33, pages 1129-1141. Curran Associates, Inc., 2020. URL https://proceedings.neurips.cc/paper/2020/file/ 0cbc5671ae26f67871cb914d81ef8fc1-Paper.pdf .
  46. Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grau- man, Nicolò Cesa-Bianchi, and Roman Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada , pages 4944-4953, 2018a. URL https://proceedings.neurips.cc/paper/2018/hash/ d04863f100d59b3eb688a11f95b0ae60-Abstract.html .
  47. Xin Zhang, Armando Solar-Lezama, and Rishabh Singh. Interpreting neural network judgments via minimal, stable, and symbolic corrections. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada , pages 4879-4890, 2018b. URL https://proceedings.neurips.cc/paper/2018/hash/ 300891a62162b960cf02ce3827bb363c-Abstract.html .

Cited by

Sorted by citations

Related

Authors
Albarghouthi, A.
Affiliations
University of Wisconsin–Madison (US)
Corresponding author
Albarghouthi, Aws
ORCID
Albarghouthi, Aws
Venue
Foundations and Trends® in Programming Languages
Publisher
Emerald
Published
2021-12-02
Volume
7
Issue
1-2
Pages
1-157
ISSN
  • 2325-1107 (ISSN-L)
  • 2325-1131
DOI
10.1561/2500000051
OpenAlex
W3200928619
Cited by
78
References
25
Citations by year
2026: 7 · 2025: 21 · 2024: 19 · 2023: 18 · 2022: 9 · 2021: 4
FWCI
6.59
Type
journal article
Language
en
Open access
Locations
  • Foundations and Trends® in Programming Languages (publishedVersion)
  • arXiv (Cornell University) (submittedVersion, other-oa)
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Funders
University of Wisconsin-Madison
Topics
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
Keywords
neural network verification, formal verification, deep neural network, deep learning, safety guarantees, robustness, correctness, security (computing), formal methods

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