Parallel Verification for  $$\delta $$ -Equivalence of Neural Network Quantization | SpringerLink
Skip to main content
Springer Nature Link
Log in

Parallel Verification for \(\delta \)-Equivalence of Neural Network Quantization

  • Conference paper
  • First Online:
AI Verification (SAIV 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14846))

Included in the following conference series:

  • 257 Accesses

Abstract

Quantization replaces floating point arithmetic with integer arithmetic in deep neural networks, enabling more efficient on-device inference with less power and memory. However, it also brings in loss of generalization and even potential errors to the models. In this work, we propose a parallelization technique for formally verifying the equivalence between quantized models and their original real-valued counterparts. In order to guarantee both soundness and completeness, mixed integer linear programming (MILP) is deployed as the baseline technique. Nevertheless, the incorporation of two networks as well as the mixture of integer and real number arithmetic make the problem much more challenging than verifying a single network, and thus using MILP alone is inadequate for the non-trivial cases. To tackle this, we design a distributed verification technique that can leverage hundreds of CPUs on high-performance computing clusters. We develop a two-tier parallel framework and propose property- and output-based partition strategies. Evaluated on perception networks quantized with PyTorch, our approach outperforms existing methods in successfully verifying many cases that are otherwise considered infeasible.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 13727
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 17159
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://github.com/huangdiudiu/EQEV.

References

  1. FSD chip-tesla (2022). https://en.wikichip.org/wiki/tesla_(car_company)/fsd_chip

  2. Bunda, S., Spreeuwers, L.J., Zeinstra, C.G.: Sub-byte quantization of mobile face recognition convolutional neural networks. In: Brömme, A., et al. (eds.) Proceedings of the 21st International Conference of the Biometrics Special Interest Group, BIOSIG 2022, Darmstadt, Germany, 14–16 September 2022. LNI, vol. P-329, pp. 229–236. IEEE / Gesellschaft für Informatik e.V. (2022)

    Google Scholar 

  3. Cheng, C.-H., Nührenberg, G., Ruess, H.: Maximum resilience of artificial neural networks. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 251–268. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_18

    Chapter  Google Scholar 

  4. Ciresan, D.C., Giusti, A., Gambardella, L.M., Schmidhuber, J.: Deep neural networks segment neuronal membranes in electron microscopy images. In: Advances in Neural Information Processing Systems 25: 26th Annual Conference on Neural Information Processing Systems 2012. Proceedings of a meeting held 3–6 December 2012, Lake Tahoe, Nevada, United States, pp. 2852–2860 (2012)

    Google Scholar 

  5. Devlin, J., Chang, M., Lee, K., Toutanova, K.: BERT: pre-training of deep bidirectional transformers for language understanding. In: Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT 2019, Minneapolis, MN, USA, 2–7 June 2019, vol. 1. pp. 4171–4186. Association for Computational Linguistics (2019)

    Google Scholar 

  6. Dosovitskiy, A., et al.: An image is worth 16\(\,\times \,\)16 words: transformers for image recognition at scale. In: 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, 3–7 May 2021. OpenReview.net (2021)

    Google Scholar 

  7. Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 121–138. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-77935-5_9

    Chapter  Google Scholar 

  8. Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 269–286. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_19

    Chapter  Google Scholar 

  9. Fischetti, M., Jo, J.: Deep neural networks and mixed integer linear optimization. Constraints Int. J. 23(3), 296–309 (2018)

    Article  MathSciNet  Google Scholar 

  10. Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: 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, pp. 3–18. IEEE Computer Society (2018)

    Google Scholar 

  11. Goodfellow, I.J., Bengio, Y., Courville, A.C.: Deep Learning. MIT Press, Adaptive computation and machine learning (2016)

    Google Scholar 

  12. Gurobi: A most powerful mathematical optimization solver (2018)

    Google Scholar 

  13. Han, S., Mao, H., Dally, W.J.: Deep compression: Compressing deep neural network with pruning, trained quantization and Huffman coding. In: 4th International Conference on Learning Representations, ICLR 2016, San Juan, Puerto Rico, 2–4 May 2016, Conference Track Proceedings (2016)

    Google Scholar 

  14. Henzinger, T.A., Lechner, M., Žikelić, D.: Scalable verification of quantized neural networks. In: Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, pp. 3787–3795. AAAI Press (2021)

    Google Scholar 

  15. Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and Conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50–65. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34188-5_8

    Chapter  Google Scholar 

  16. Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228–245. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_15

    Chapter  Google Scholar 

  17. Huang, P., Liu, M., Ge, C., Ma, F., Zhang, J.: Investigating the existence of orthogonal golf designs via satisfiability testing. In: Davenport, J.H., Wang, D., Kauers, M., Bradford, R.J. (eds.) Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, ISSAC 2019, Beijing, China, July 15-18, 2019, pp. 203–210. ACM (2019)

    Google Scholar 

  18. Huang, P., Ma, F., Ge, C., Zhang, J., Zhang, H.: Investigating the existence of large sets of idempotent quasigroups via satisfiability testing. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 354–369. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_24

    Chapter  Google Scholar 

  19. Huang, P., et al.: Towards efficient verification of quantized neural networks. arXiv preprint arXiv:2312.12679 (2023)

  20. Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3–29. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_1

    Chapter  Google Scholar 

  21. Jacob, B., et al.: Quantization and training of neural networks for efficient integer-arithmetic-only inference. In: 2018 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2018, Salt Lake City, UT, USA, 18–22 June 2018, pp. 2704–2713. Computer Vision Foundation/IEEE Computer Society (2018)

    Google Scholar 

  22. Jia, K., Rinard, M.C.: Efficient exact verification of binarized neural networks. In: Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, 6–12 December 2020, virtual (2020)

    Google Scholar 

  23. Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97–117. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_5

    Chapter  Google Scholar 

  24. Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443–452. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_26

    Chapter  Google Scholar 

  25. Kulkarni, U., M, M.S., Gurlahosur, S.V., Bhogar, G.: Quantization friendly MobileNet (QF-MobileNet) architecture for vision based applications on embedded platforms. Neural Networks 136, 28–39 (2021)

    Google Scholar 

  26. LeCun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proc. IEEE 86(11), 2278–2324 (1998). https://doi.org/10.1109/5.726791

  27. Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, 10–15 July 2018. Proceedings of Machine Learning Research, vol. 80, pp. 3575–3583. PMLR (2018)

    Google Scholar 

  28. Mistry, S., Saha, I., Biswas, S.: An MILP encoding for efficient verification of quantized deep neural networks. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), 4445–4456 (2022)

    Google Scholar 

  29. Paulsen, B., Wang, J., Wang, C.: ReluDiff: differential verification of deep neural networks. In: Rothermel, G., Bae, D. (eds.) ICSE ’20: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June–19 July, 2020, pp. 714–726. ACM (2020)

    Google Scholar 

  30. Paulsen, B., Wang, J., Wang, J., Wang, C.: NEURODIFF: scalable differential verification of neural networks using fine-grained approximation. In: 35th IEEE/ACM International Conference on Automated Software Engineering, ASE 2020, Melbourne, Australia, 21–25 September 2020, pp. 784–796. IEEE (2020)

    Google Scholar 

  31. Raghunathan, A., Steinhardt, J., Liang, P.: Semidefinite relaxations for certifying robustness to adversarial examples. In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3–8 December 2018, Montréal, Canada, pp. 10900–10910 (2018)

    Google Scholar 

  32. Simonyan, K., Zisserman, A.: Very deep convolutional networks for large-scale image recognition. In: 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, 7–9 May 2015, Conference Track Proceedings (2015)

    Google Scholar 

  33. Singh, G., Gehr, T., Püschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL), 41:1–41:30 (2019)

    Google Scholar 

  34. Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3–8 December 2018, Montréal, Canada, pp. 6369–6379 (2018)

    Google Scholar 

  35. Weng, T., et al.: Towards fast computation of certified robustness for ReLU networks. In: Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, 10–15 July 2018. Proceedings of Machine Learning Research, vol. 80, pp. 5273–5282. PMLR (2018)

    Google Scholar 

  36. Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, 10–15 July 2018. Proceedings of Machine Learning Research, vol. 80, pp. 5283–5292. PMLR (2018)

    Google Scholar 

  37. Wu, H., et al.: Parallelization techniques for verifying neural networks. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, 21–24 September 2020, pp. 128–137. IEEE (2020)

    Google Scholar 

  38. Xu, H., Gao, Y., Yu, F., Darrell, T.: End-to-end learning of driving models from large-scale video datasets. In: 2017 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2017, Honolulu, HI, USA, 21–26 July 2017, pp. 3530–3538. IEEE Computer Society (2017)

    Google Scholar 

  39. Yang, Y., Lei, W., Huang, P., Cao, J., Li, J., Chua, T.: A dual prompt learning framework for few-shot dialogue state tracking. In: Ding, Y., Tang, J., Sequeda, J.F., Aroyo, L., Castillo, C., Houben, G. (eds.) Proceedings of the ACM Web Conference 2023, WWW 2023, Austin, TX, USA, 30 April 2023–4 May 2023, pp. 1468–1477. ACM (2023)

    Google Scholar 

  40. Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3–8 December 2018, Montréal, Canada, pp. 4944–4953 (2018)

    Google Scholar 

  41. Zhang, Y., Song, F., Sun, J.: QEBVerif: Quantization error bound verification of neural networks. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17–22 July 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 413–437. Springer (2023)

    Google Scholar 

  42. Zhang, Y., et al.: QVIP: an ILP-based formal verification approach for quantized neural networks. In: 37th IEEE/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, 10–14 October 2022, pp. 82:1–82:13. ACM (2022)

    Google Scholar 

Download references

Acknowledgments

This work was funded in part by a Ford Alliance Project (199909), NSF (grant number 2211505), and the Stanford Center for AI Safety.

Author information

Authors and Affiliations

  1. Stanford University, Stanford, CA, USA

    Pei Huang, Haoze Wu, Min Wu, Fuqi Jia & Clark Barrett

  2. UCAS, Beijing, China

    Yuting Yang & Fuqi Jia

  3. Institute of Computing Technology, CAS, Beijing, China

    Yuting Yang

  4. IT University of Copenhagen, Copenhagen, Denmark

    Ieva Daukantas

  5. Institute of Software, CAS, Beijing, China

    Fuqi Jia

Authors
  1. Pei Huang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yuting Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Haoze Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ieva Daukantas
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Min Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Fuqi Jia
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Clark Barrett
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Clark Barrett .

Editor information

Editors and Affiliations

  1. University of Haifa, Haifa, Israel

    Guy Avni

  2. University of Birmingham, Birmingham, UK

    Mirco Giacobbe

  3. Vanderbilt University, Nashville, TN, USA

    Taylor T. Johnson

  4. Hebrew University of Jerusalem, Jerusalem, Israel

    Guy Katz

  5. Delft University of Technology, Delft, The Netherlands

    Anna Lukina

  6. VMware by Broadcom, Palo Alto, CA, USA

    Nina Narodytska

  7. Aalborg University, Aalborg, Denmark

    Christian Schilling

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Huang, P. et al. (2024). Parallel Verification for \(\delta \)-Equivalence of Neural Network Quantization. In: Avni, G., et al. AI Verification. SAIV 2024. Lecture Notes in Computer Science, vol 14846. Springer, Cham. https://doi.org/10.1007/978-3-031-65112-0_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-65112-0_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-65111-3

  • Online ISBN: 978-3-031-65112-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation