SpringerLink
Log in

QNNRepair: Quantized Neural Network Repair

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2023)

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

Included in the following conference series:

  • 271 Accesses

Abstract

We present QNNRepair, the first method in the literature for repairing quantized neural networks (QNNs). QNNRepair aims to improve the accuracy of a neural network model after quantization. It accepts the full-precision and weight-quantized neural networks, together with a repair dataset of passing and failing tests. At first, QNNRepair applies a software fault localization method to identify the neurons that cause performance degradation during neural network quantization. Then, it formulates the repair problem into a MILP, solving neuron weight parameters, which corrects the QNN’s performance on failing tests while not compromising its performance on passing tests. We evaluate QNNRepair with widely used neural network architectures such as MobileNetV2, ResNet, and VGGNet on popular datasets, including high-resolution images. We also compare QNNRepair with the state-of-the-art data-free quantization method SQuant [22]. According to the experiment results, we conclude that QNNRepair is effective in improving the quantized model’s performance in most cases. Its repaired models have 24% higher accuracy than SQuant’s in the independent validation set, especially for the ImageNet dataset.

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
EUR 32.99 /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
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 53.49
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 69.54
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. TensorFlow Lite. https://www.tensorflow.org/lite

  2. Abreu, R., Zoeteweij, P., Van Gemund, A.J.: On the accuracy of spectrum-based fault localization. In: Testing: Academic and industrial conference practice and research techniques-MUTATION (TAICPART-MUTATION 2007). IEEE (2007)

    Google Scholar 

  3. Agarwal, P., Agrawal, A.P.: Fault-localization techniques for software systems: a literature review. ACM SIGSOFT Softw. Eng. Notes 39(5), 1–8 (2014)

    Article  Google Scholar 

  4. Amir, G., Wu, H., Barrett, C., Katz, G.: An SMT-based approach for verifying binarized neural networks. In: TACAS 2021. LNCS, vol. 12652, pp. 203–222. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72013-1_11

    Chapter  MATH  Google Scholar 

  5. Bak, S., Liu, C., Johnson, T.: The second international verification of neural networks competition (vnn-comp 2021): Summary and results. ar**v preprint ar**v:2109.00498 (2021)

  6. Borkar, T.S., Karam, L.J.: Deepcorrect: correcting dnn models against image distortions. IEEE Trans. Image Process. 28(12), 6022–6034 (2019)

    Article  MathSciNet  MATH  Google Scholar 

  7. Bressert, E.: Scipy and numpy: an overview for developers (2012)

    Google Scholar 

  8. Choi, J., Wang, Z., Venkataramani, S., Chuang, P.I.J., Srinivasan, V., Gopalakrishnan, K.: Pact: parameterized clip** activation for quantized neural networks. ar**v preprint ar**v:1805.06085 (2018)

  9. Dallmeier, V., Lindig, C., Zeller, A.: Lightweight bug localization with ample. In: Proceedings of the Sixth International Symposium on Automated Analysis-Driven Debugging, pp. 99–104 (2005)

    Google Scholar 

  10. David, R., Duke, et al.: Tensorflow lite micro: Embedded machine learning for tinyml systems. Proc. Mach. Learn. Syst. (2021)

    Google Scholar 

  11. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  12. Deng, J., Dong, W., Socher, R., Li, L.J., Li, K., Fei-Fei, L.: Imagenet: a large-scale hierarchical image database. In: 2009 IEEE Conference on computer vision and Pattern Recognition, pp. 248–255. IEEE (2009)

    Google Scholar 

  13. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37

    Chapter  Google Scholar 

  14. 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  MATH  Google Scholar 

  15. Elboher, Y.Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 43–65. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_3

    Chapter  MATH  Google Scholar 

  16. Eniser, H.F., Gerasimou, S., Sen, A.: DeepFault: fault localization for deep neural networks. In: Hähnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 171–191. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_10

    Chapter  Google Scholar 

  17. Galijasevic, Z., Abur, A.: Fault location using voltage measurements. IEEE Trans. Power Delivery 17(2), 441–445 (2002)

    Article  Google Scholar 

  18. Gehr, T., Mirman, M., Drachsler-Cohen, D., Others: Ai2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy (SP), pp. 3–18. IEEE (2018)

    Google Scholar 

  19. Giacobbe, M., Henzinger, T.A., Lechner, M.: How many bits does it take to quantize your neural network? In: TACAS 2020. LNCS, vol. 12079, pp. 79–97. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_5

    Chapter  Google Scholar 

  20. Goldberger, B., et al.: Minimal modifications of deep neural networks using verification. In: LPAR, p. 23rd (2020)

    Google Scholar 

  21. Gong, R., et al.: Differentiable soft quantization: bridging full-precision and low-bit neural networks. In: Proceedings of the IEEE/CVF International Conference on Computer Vision. pp. 4852–4861 (2019)

    Google Scholar 

  22. Guo, C., et al.: Squant: on-the-fly data-free quantization via diagonal hessian approximation. ar**v preprint ar**v:2202.07471 (2022)

  23. Guo, Y.: A survey on methods and theories of quantized neural networks. ar**v preprint ar**v:1808.04752 (2018)

  24. He, K., et al.: Deep residual learning for image recognition. Proceedings of the IEEE conference on computer vision and pattern recognition pp. 770–778 (2016)

    Google Scholar 

  25. Henzinger, T.A., Lechner, M., et al.: Scalable verification of quantized neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence (2021)

    Google Scholar 

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

  27. ifigotin: Imagenetmini-1000. https://www.kaggle.com/datasets/ifigotin/imagenetmini-1000 (2021), (Accessed 4 April 2023)

  28. Jacob, B., et al.: Quantization and training of neural networks for efficient integer-arithmetic-only inference. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 2704–2713 (2018)

    Google Scholar 

  29. Jones, J.A., Harrold, M.J.: Empirical evaluation of the tarantula automatic fault-localization technique. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, pp. 273–282 (2005)

    Google Scholar 

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

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

  32. Krizhevsky, A., Hinton, G.: CIFAR-10 (canadian institute for advanced research). Tech. rep., University of Toronto (2009). https://www.cs.toronto.edu/kriz/cifar.html

  33. Land, A.H., Doig, A.G.: An automatic method for solving discrete programming problems. In: Jünger, M., et al. (eds.) 50 Years of Integer Programming 1958-2008, pp. 105–132. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-540-68279-0_5

    Chapter  MATH  Google Scholar 

  34. Li, Y., et al.: Brecq: pushing the limit of post-training quantization by block reconstruction. ar**v preprint ar**v:2102.05426 (2021)

  35. Makhorin, A.: Glpk (gnu linear programming kit). http://www.gnu.org/s/glpk/glpk.html (2008)

  36. Meindl, B., Templ, M.: Analysis of commercial and free and open source solvers for linear optimization problems. Eurostat and Statistics Netherlands within the project ESSnet on common tools and harmonised methodology for SDC in the ESS 20 (2012)

    Google Scholar 

  37. Naish, L., Lee, H.J., Ramamohanarao, K.: A model for spectra-based software diagnosis. ACM Trans. Softw. Eng. Methodol. (TOSEM) 20(3), 1–32 (2011)

    Article  Google Scholar 

  38. Nemhauser, G.L., Wolsey, L.A.: Integer and combinatorial optimization john, vol. 118. Wiley & Sons, New York (1988)

    Google Scholar 

  39. Nickel, S., Steinhardt, C., Schlenker, H., Burkart, W.: Ibm ilog cplex optimization studio-a primer. In: Decision Optimization with IBM ILOG CPLEX Optimization Studio: A Hands-On Introduction to Modeling with the Optimization Programming Language (OPL), pp. 9–21. Springer (2022). https://doi.org/10.1007/978-3-662-65481-1_2

  40. Odena, A., Olsson, C., Andersen, D., Goodfellow, I.: Tensorfuzz: Debugging neural networks with coverage-guided fuzzing. In: ICML, pp. 4901–4911. PMLR (2019)

    Google Scholar 

  41. Optimization, G.: Inc. gurobi optimizer reference manual, version 5.0 (2012)

    Google Scholar 

  42. Pei, K., Cao, Y., Yang, J., Jana, S.: Deepxplore: automated whitebox testing of deep learning systems. In: Proceedings of the 26th Symposium on Operating Systems Principles, pp. 1–18 (2017)

    Google Scholar 

  43. Sandler, M., et al.: Mobilenetv 2: inverted residuals and linear bottlenecks. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition (2018)

    Google Scholar 

  44. Sena, L.H., Song, X., da S. Alves, E.H., Bessa, I., Manino, E., Cordeiro, L.C.: Verifying quantized neural networks using smt-based model checking. CoRR abs/ ar**v: 2106.05997 (2021)

  45. Shorten, C., Khoshgoftaar, T.M.: A survey on image data augmentation for deep learning. J. Big Data 6(1), 1–48 (2019)

    Article  Google Scholar 

  46. Simonyan, K., Zisserman, A.: Very deep convolutional networks for large-scale image recognition. ar**v preprint ar**v:1409.1556 (2014)

  47. Song, C., Fallon, E., Li, H.: Improving adversarial robustness in weight-quantized neural networks. ar**v preprint ar**v:2012.14965 (2020)

  48. Song, X., et al.: Qnnverifier: a tool for verifying neural networks using smt-based model checking. CoRR abs/ ar**v: 2111.13110 (2021)

  49. Song, X., Sun, Y., Mustafa, M.A., Cordeiro, L.: Airepair: a repair platform for neural networks. In: ICSE-Companion. IEEE/ACM (2022)

    Google Scholar 

  50. Sotoudeh, M., Thakur, A.V.: Provable repair of deep neural networks. In: PLDI (2021)

    Google Scholar 

  51. Sun, Y., Chockler, H., Huang, X., Kroening, D.: Explaining image classifiers using statistical fault localization. In: Vedaldi, A., Bischof, H., Brox, T., Frahm, J.-M. (eds.) ECCV 2020. LNCS, vol. 12373, pp. 391–406. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58604-1_24

    Chapter  Google Scholar 

  52. Sun, Y., Huang, X., Kroening, D., Sharp, J., Hill, M., Ashmore, R.: Structural test coverage criteria for deep neural networks. ACM Trans. Embedded Comput. Syst. (TECS) 18(5s), 1–23 (2019)

    Article  Google Scholar 

  53. Sun, Y., Wu, M., Ruan, W., Huang, X., Kwiatkowska, M., Kroening, D.: Concolic testing for deep neural networks. In: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, pp. 109–119 (2018)

    Google Scholar 

  54. Usman, M., Gopinath, D., Sun, Y., Noller, Y., Păsăreanu, C.S.: NNrepair: constraint-based repair of neural network classifiers. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 3–25. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81685-8_1

    Chapter  Google Scholar 

  55. Vanholder, H.: Efficient inference with tensorrt. In: GPU Technology Conference, vol. 1, p. 2 (2016)

    Google Scholar 

  56. Wang, S., Zhang, H., Xu, K., Others: Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Advances in Neural Information Processing Systems 34 (2021)

    Google Scholar 

  57. Wong, W.E., Debroy, V., Gao, R., Li, Y.: The dstar method for effective software fault localization. IEEE Trans. Reliab. 63(1), 290–308 (2013)

    Article  Google Scholar 

  58. Wong, W.E., Qi, Y., Zhao, L., Cai, K.Y.: Effective fault localization using code coverage. In: COMPSAC, vol. 1, pp. 449–456. IEEE (2007)

    Google Scholar 

  59. Yu, B., et al.: Deeprepair: style-guided repairing for deep neural networks in the real-world operational environment. IEEE Trans. Reliability (2021)

    Google Scholar 

  60. Zhang, Y., et al.: Qvip: an ilp-based formal verification approach for quantized neural networks. In: ASE. IEEE/ACM (2022)

    Google Scholar 

  61. Zhang, J., Li, J.: Testing and verification of neural-network-based safety-critical control software: a systematic literature review. Inf. Softw. Technol. 123, 106296 (2020)

    Article  Google Scholar 

Download references

Acknowledgements

This work is funded by the EPSRC grants EP/T026995/1, EP/V000497/1, EU H2020 ELEGANT 957286, Soteria project awarded by the UK Research and Innovation for the Digital Security by Design (DSbD) Programme, and Cal-Comp Electronic by the R &D project of the Cal-Comp Institute of Technology and Innovation.

Author information

Authors and Affiliations

  1. Department of Computer Science, The University of Manchester, Manchester, UK

    **dan Song, Youcheng Sun, Mustafa A. Mustafa & Lucas C. Cordeiro

  2. COSIC, KU Leuven, Leuven, Belgium

    Mustafa A. Mustafa

  3. Federal University of Amazonas, Manaus, Brazil

    Lucas C. Cordeiro

Authors
  1. **dan Song
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Youcheng Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mustafa A. Mustafa
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lucas C. Cordeiro
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Youcheng Sun , Mustafa A. Mustafa or Lucas C. Cordeiro .

Editor information

Editors and Affiliations

  1. NOVA University Lisbon, Caparica, Portugal

    Carla Ferreira

  2. Eindhoven University of Technology, Eindhoven, The Netherlands

    Tim A. C. Willemse

Rights and permissions

Reprints and permissions

Copyright information

© 2023 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

Song, X., Sun, Y., Mustafa, M.A., Cordeiro, L.C. (2023). QNNRepair: Quantized Neural Network Repair. In: Ferreira, C., Willemse, T.A.C. (eds) Software Engineering and Formal Methods. SEFM 2023. Lecture Notes in Computer Science, vol 14323. Springer, Cham. https://doi.org/10.1007/978-3-031-47115-5_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-47115-5_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-47114-8

  • Online ISBN: 978-3-031-47115-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation