More Web Proxy on the site http://driver.im/

research-article

Open access

Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks

Authors:

Mark Niklas Müller,

Martin VechevAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue PLDI

Article No.: 138, Pages 786 - 810

https://doi.org/10.1145/3591252

Published: 06 June 2023 Publication History

Abstract

We present a new abstract interpretation framework for the precise over-approximation of numerical fixpoint iterators. Our key observation is that unlike in standard abstract interpretation (AI), typically used to over-approximate all reachable program states, in this setting, one only needs to abstract the concrete fixpoints, i.e., the final program states. Our framework targets numerical fixpoint iterators with convergence and uniqueness guarantees in the concrete and is based on two major technical contributions: (i) theoretical insights which allow us to compute sound and precise fixpoint abstractions without using joins, and (ii) a new abstract domain, CH-Zonotope, which admits efficient propagation and inclusion checks while retaining high precision.

We implement our framework in a tool called CRAFT and evaluate it on a novel fixpoint-based neural network architecture (monDEQ) that is particularly challenging to verify. Our extensive evaluation demonstrates that CRAFT exceeds the state-of-the-art performance in terms of speed (two orders of magnitude), scalability (one order of magnitude), and precision (25% higher certified accuracies).

References

[1]

Matthias Althoff, Olaf Stursberg, and Martin Buss. 2008. Verification of uncertain embedded systems by computing reachable sets based on zonotopes. IFAC Proceedings Volumes, 41, 2 (2008), https://doi.org/10.3182/20080706-5-KR-1001.00861

[2]

Gianluca Amato and Francesca Scozzari. 2012. The Abstract Domain of Parallelotopes. Electron. Notes Theor. Comput. Sci., 287 (2012), https://doi.org/10.1016/j.entcs.2012.09.003

Digital Library

[3]

Gianluca Amato, Francesca Scozzari, Helmut Seidl, Kalmer Apinis, and Vesal Vojdani. 2016. Efficiently intertwining widening and narrowing. Sci. Comput. Program., 120 (2016), https://doi.org/10.1016/j.scico.2015.12.005

Digital Library

[4]

Brandon Amos and J. Zico Kolter. 2017. OptNet: Differentiable Optimization as a Layer in Neural Networks. In Proc. of ICML. 70.

[5]

Shaojie Bai, J. Zico Kolter, and Vladlen Koltun. 2019. Deep Equilibrium Models. In Proc. of NeurIPS.

[6]

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2002. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. In The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday]. 2566, https://doi.org/10.1007/3-540-36377-7_5

[7]

François Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. In Formal Methods in Programming and Their Applications, International Conference, Akademgorodok, Novosibirsk, Russia, June 28 - July 2, 1993, Proceedings. 735, https://doi.org/10.1007/BFb0039704

[8]

Tong Chen, Jean B. Lasserre, Victor Magron, and Edouard Pauwels. 2021. Semialgebraic Representation of Monotone Deep Equilibrium Models and Applications to Certification.

[9]

Jeremy M. Cohen, Elan Rosenfeld, and J. Zico Kolter. 2019. Certified Adversarial Robustness via Randomized Smoothing. In Proc. of ICML. 97.

[10]

Christophe Combastel. 2003. A state bounding observer based on zonotopes. In 2003 European Control Conference (ECC). https://doi.org/10.23919/ECC.2003.7085991

[11]

Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of POPL. https://doi.org/10.1145/512950.512973

Digital Library

[12]

Patrick Cousot and Radhia Cousot. 1977. Static Determination of Dynamic Properties of Recursive Procedures. In Formal Description of Programming Concepts: Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts, St. Andrews, NB, Canada, August 1-5, 1977.

[13]

Patrick Cousot and Radhia Cousot. 1979. Constructive versions of Tarski’s fixed point theorems. Pacific journal of Mathematics, 82, 1 (1979), https://doi.org/10.2140/pjm.1979.82.43

[14]

Patrick Cousot and Radhia Cousot. 1992. Abstract Interpretation Frameworks. J. Log. Comput., 2, 4 (1992), https://doi.org/10.1093/logcom/2.4.511

[15]

Patrick Cousot and Radhia Cousot. 1992. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP’92, Leuven, Belgium, August 26-28, 1992, Proceedings. 631, https://doi.org/10.1007/3-540-55844-6_142

[16]

Claudio Ferrari, Mark Niklas Müller, Nikola Jovanovic, and Martin T. Vechev. 2022. Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound. In Proc. of ICLR.

[17]

Feisi Fu and Wenchao Li. 2022. Sound and Complete Neural Network Repair with Minimality and Locality Guarantees. In Proc. of ICLR.

[18]

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2013. Abstract Interpretation over Non-lattice Abstract Domains. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 7935, https://doi.org/10.1007/978-3-642-38856-9_3

[19]

Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA. https://doi.org/10.1109/SP.2018.00058

[20]

Laurent El Ghaoui, Fangda Gu, Bertrand Travacca, Armin Askari, and Alicia Y. Tsai. 2021. Implicit Deep Learning. SIAM J. Math. Data Sci., 3, 3 (2021), https://doi.org/10.1137/20M1358517

[21]

Khalil Ghorbal, Eric Goubault, and Sylvie Putot. 2009. The Zonotope Abstract Domain Taylor1+. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. 5643, https://doi.org/10.1007/978-3-642-02658-4_47

Digital Library

[22]

Antoine Girard. 2005. Reachability of uncertain linear systems using zonotopes. In International Workshop on Hybrid Systems: Computation and Control. https://doi.org/10.1007/978-3-540-31954-2_19

Digital Library

[23]

Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. 2015. Explaining and Harnessing Adversarial Examples. In Proc. of ICLR.

[24]

Eric Goubault and Sylvie Putot. 2008. Perturbed affine arithmetic for invariant computation in numerical program analysis. CoRR, https://doi.org/10.48550/arXiv.0807.2961

[25]

Eric Goubault, Sylvie Putot, Philippe Baufreton, and Jean Gassino. 2007. Static Analysis of the Accuracy in Control Systems: Principles and Experiments. In Formal Methods for Industrial Critical Systems, 12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers. 4916, https://doi.org/10.1007/978-3-540-79707-4_3

[26]

Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli. 2018. On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. ArXiv preprint, abs/1810.12715 (2018), https://doi.org/10.48550/arXiv.1810.12715

[27]

Sven Gowal, Jonathan Uesato, Chongli Qin, Po-Sen Huang, Timothy A. Mann, and Pushmeet Kohli. 2019. An Alternative Surrogate Loss for PGD-based Adversarial Testing. ArXiv preprint, abs/1910.09338 (2019), https://doi.org/10.48550/arXiv.1910.09338

[28]

Dwight Guth. 2013. A formal semantics of Python 3.3.

[29]

Shunhua Jiang, Zhao Song, Omri Weinstein, and Hengjie Zhang. 2020. Faster Dynamic Matrix Inverse for Faster LPs. ArXiv preprint, abs/2004.07470 (2020), https://doi.org/10.48550/arXiv.2004.07470

[30]

Kyle D. Julian and Mykel J. Kochenderfer. 2019. Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems. In 2019 IEEE/AIAA 38th Digital Avionics Systems Conference (DASC). https://doi.org/10.1109/DASC43569.2019.9081748

[31]

Kai Kellner. 2015. Containment problems for projections of polyhedra and spectrahedra. ArXiv preprint, abs/1509.02735 (2015), https://doi.org/10.48550/arXiv.1509.02735

[32]

Suyong Kim, Weiqi Ji, Sili Deng, Yingbo Ma, and Christopher Rackauckas. 2021. Stiff neural ordinary differential equations. Chaos: An Interdisciplinary Journal of Nonlinear Science, 31, 9 (2021), https://doi.org/10.1063/5.0060697

[33]

Anna-Kathrin Kopetzki, Bastian Schürmann, and Matthias Althoff. 2017. Methods for order reduction of zonotopes. In 56th IEEE Annual Conference on Decision and Control, CDC 2017, Melbourne, Australia, December 12-15, 2017. https://doi.org/10.1109/CDC.2017.8264508

Digital Library

[34]

Alex Krizhevsky and Geoffrey Hinton. 2009. Learning multiple layers of features from tiny images.

[35]

Wolfgang Kühn. 1998. Rigorously computed orbits of dynamical systems without the wrapping effect. Computing, 61, 1 (1998), https://doi.org/10.1007/BF02684450

Digital Library

[36]

Adrian Kulmburg and Matthias Althoff. 2021. On the co-NP-completeness of the zonotope containment problem. Eur. J. Control, https://doi.org/10.1016/j.ejcon.2021.06.028

[37]

Yann LeCun, Léon Bottou, Yoshua Bengio, and Patrick Haffner. 1998. Gradient-based learning applied to document recognition. Proc. IEEE, 86, 11 (1998), https://doi.org/10.1109/5.726791

[38]

Mathias Lecuyer, Vaggelis Atlidakis, Roxana Geambasu, Daniel Hsu, and Suman Jana. 2018. Certified Robustness to Adversarial Examples with Differential Privacy. Proc. of S&P, https://doi.org/10.1109/SP.2019.00044

[39]

Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. 2018. Towards Deep Learning Models Resistant to Adversarial Attacks. In Proc. of ICLR.

[40]

Matthew Mirman, Timon Gehr, and Martin T. Vechev. 2018. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In Proc. of ICML. 80.

[41]

Mark Niklas Müller, Marc Fischer, Robin Staab, and Martin Vechev. 2023. Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks - Artifact. https://doi.org/10.5281/zenodo.7794269

[42]

Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. 2022. PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations. Proc. ACM Program. Lang., 6, POPL (2022), Article 43, 33 pages. https://doi.org/10.1145/3498704

Digital Library

[43]

Chirag Pabbaraju, Ezra Winston, and J. Zico Kolter. 2021. Estimating Lipschitz constants of monotone deep equilibrium models. In Proc. of ICLR.

[44]

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. 2019. PyTorch: An Imperative Style, High-Performance Deep Learning Library. In Proc. of NeurIPS.

[45]

Sylvie Putot. 2012. Static analysis of numerical programs and systems. Habilitation à diriger des recherches, Université de Paris-Sud, https://doi.org/10.1007/978-3-642-38856-9_1

[46]

Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. 2018. Semidefinite relaxations for certifying robustness to adversarial examples. In Proc. of NeurIPS.

[47]

Max Revay, Ruigang Wang, and Ian R. Manchester. 2020. Lipschitz Bounded Equilibrium Networks. ArXiv preprint, abs/2010.01732 (2020), https://doi.org/10.48550/arXiv.2010.01732

[48]

Ernest K Ryu and Stephen Boyd. 2016. Primer on monotone operator methods. Appl. Comput. Math, 15, 1 (2016).

[49]

Sadra Sadraddini and Russ Tedrake. 2019. Linear Encodings for Polytope Containment Problems. In 58th IEEE Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019. https://doi.org/10.1109/CDC40024.2019.9029363

Digital Library

[50]

François Serre, Christoph Müller, Gagandeep Singh, Markus Püschel, and Martin Vechev. 2021. Scaling Polyhedral Neural Network Verification on GPUs. In Proc. Machine Learning and Systems (MLSys).

[51]

Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin T. Vechev. 2019. Beyond the Single Neuron Convex Barrier for Neural Network Certification. In Proc. of NeurIPS.

[52]

Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. 2018. Fast and Effective Robustness Certification. In Proc. of NeurIPS.

Digital Library

[53]

Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. 2019. An abstract domain for certifying neural networks. PACMPL, 3, POPL (2019), https://doi.org/10.1145/3290354

Digital Library

[54]

Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. 2014. Intriguing properties of neural networks. In Proc. of ICLR.

[55]

Yusuke Tashiro, Yang Song, and Stefano Ermon. 2020. Diversity can be Transferred: Output Diversification for White- and Black-box Attacks. In Proc. of NeurIPS.

[56]

Po-Wei Wang, Priya L. Donti, Bryan Wilder, and J. Zico Kolter. 2019. SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver. In Proc. of ICML. 97.

[57]

Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal Security Analysis of Neural Networks using Symbolic Intervals. In 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018.

[58]

Colin Wei and J Zico Kolter. 2022. Certified Robustness for Deep Equilibrium Models via Interval Bound Propagation. In Proc. of ICLR.

[59]

Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane S. Boning, and Inderjit S. Dhillon. 2018. Towards Fast Computation of Certified Robustness for ReLU Networks. In Proc. of ICML. 80.

[60]

Ezra Winston and J. Zico Kolter. 2020. Monotone operator equilibrium networks. In Proc. of NeurIPS.

[61]

Eric Wong and J. Zico Kolter. 2018. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In Proc. of ICML. 80.

[62]

Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. 2020. Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond. In Proc. of NeurIPS.

[63]

Xuejiao Yang and Joseph K Scott. 2018. A comparison of zonotope order reduction techniques. Automatica, 95 (2018), https://doi.org/10.1016/j.automatica.2018.06.006

Digital Library

[64]

Hakan Yazarel and George J Pappas. 2004. Geometric programming relaxations for linear system reachability. In Proceedings of the 2004 American Control Conference. 1, https://doi.org/10.23919/ACC.2004.1383661

[65]

Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient Neural Network Robustness Certification with General Activation Functions. In Proc. of NeurIPS.

Cited By

Mastroeni I(2025)Abstract domain adequacyInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00774-xOnline publication date: 2-Jan-2025
https://doi.org/10.1007/s10009-024-00774-x
Eiras FBibi ABunel RDvijotham KTorr PKumar MSalakhutdinov RKolter ZHeller KWeller AOliver NScarlett JBerkenkamp F(2024)Efficient error certification for physics-informed neural networksProceedings of the 41st International Conference on Machine Learning10.5555/3692070.3692560(12318-12347)Online publication date: 21-Jul-2024
https://dl.acm.org/doi/10.5555/3692070.3692560
Kanav SKřetínský JRieder S(2024)A Literature Review on Verification and Abstraction of Neural Networks Within the Formal Methods CommunityPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75778-5_3(39-65)Online publication date: 18-Nov-2024
https://doi.org/10.1007/978-3-031-75778-5_3

Index Terms

Abstract Interpretation of Fixpoint Iterators with Applications to 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

Control-flow analysis of function calls and returns by abstract interpretation

Abstract interpretation techniques are used to derive a control-flow analysis for a simple higher-order functional language. The analysis approximates the interprocedural control-flow of both function calls and returns in the presence of first-class ...
Deriving escape analysis by abstract interpretation

Escape analysis of object-oriented languages approximates the set of objects which do not escape from a given context. If we take a method as context, the non-escaping objects can be allocated on its activation stack; if we take a thread, Java ...
A²I: abstract² interpretation

The fundamental idea of Abstract² Interpretation (A²I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A²I is generally meant to use abstract interpretation to ...

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 7, Issue PLDI

June 2023

2020 pages

EISSN:2475-1421

DOI:10.1145/3554310

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 June 2023

Published in PACMPL Volume 7, Issue PLDI

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
742
Total Downloads

Downloads (Last 12 months)328
Downloads (Last 6 weeks)23

Reflects downloads up to 05 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Mastroeni I(2025)Abstract domain adequacyInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00774-xOnline publication date: 2-Jan-2025
https://doi.org/10.1007/s10009-024-00774-x
Eiras FBibi ABunel RDvijotham KTorr PKumar MSalakhutdinov RKolter ZHeller KWeller AOliver NScarlett JBerkenkamp F(2024)Efficient error certification for physics-informed neural networksProceedings of the 41st International Conference on Machine Learning10.5555/3692070.3692560(12318-12347)Online publication date: 21-Jul-2024
https://dl.acm.org/doi/10.5555/3692070.3692560
Kanav SKřetínský JRieder S(2024)A Literature Review on Verification and Abstraction of Neural Networks Within the Formal Methods CommunityPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75778-5_3(39-65)Online publication date: 18-Nov-2024
https://doi.org/10.1007/978-3-031-75778-5_3

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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