Benchmark: Formal Verification of Semantic Segmentation Neural Networks | SpringerLink
Skip to main content
Springer Nature Link
Log in

Benchmark: Formal Verification of Semantic Segmentation Neural Networks

  • Conference paper
  • First Online:
Bridging the Gap Between AI and Reality (AISoLA 2023)

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

Included in the following conference series:

  • 1114 Accesses

Abstract

Formal verification utilizes a rigorous approach to ensure the absence of critical errors and validate models against predefined properties. While significant progress has been made in verification methods for various deep neural networks (DNNs), such as feed-forward neural networks (FFNNs) and convolutional neural networks (CNNs), the application of these techniques to semantic segmentation remains largely unexplored. Semantic segmentation networks are vital in computer vision applications, where they assign semantic labels to individual pixels within an image. Given their deployment in safety-critical domains, ensuring the correctness of these networks becomes paramount. This paper presents a comprehensive benchmark study on applying formal verification techniques to semantic segmentation networks. We explore a diverse set of state-of-the-art semantic segmentation datasets and generate neural network models, including fully-convolutional networks and encoder-decoder architectures. Our investigation encompasses a wide range of verification properties, focusing on the robustness of these models against bounded adversarial vulnerabilities. To evaluate the networks’ performance, we employ set-based reachability algorithms to calculate the output reachable set(s) and some state-of-the-art performance measures for a comparative study among the networks. This benchmark paper aims to provide the formal verification community with several semantic segmentation networks and their robustness specifications for future use cases in different neural network verification competitions.

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 8007
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 10009
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.

    In this context, “Robust pixels” refer to those pixels that maintain their correct classification even in the presence of an adversarial attack..

References

  1. Anderson, G., Pailoor, S., Dillig, I., Chaudhuri, S.: Optimization and abstraction: A synergistic approach for analyzing neural network robustness. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 731–744. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019). https://doi.org/10.1145/3314221.3314614

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

  3. Blum, H., Sarlin, P.E., Nieto, J., Siegwart, R., Cadena, C.: Fishyscapes: A benchmark for safe semantic segmentation in autonomous driving. In: Proceedings of the IEEE/CVF International Conference on Computer Vision Workshops (2019)

    Google Scholar 

  4. Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Efficient verification of relu-based neural networks via dependency analysis. Proc. AAAI Conf. Artif. Intell. 34(04), 3291–3299 (2020). https://doi.org/10.1609/aaai.v34i04.5729

    Article  Google Scholar 

  5. Brazil, G., Yin, X., Liu, X.: Illuminating pedestrians via simultaneous detection & segmentation. In: Proceedings of the IEEE International Conference on Computer Vision, pp. 4950–4959 (2017)

    Google Scholar 

  6. Brix, C., Müller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the international verification of neural networks competition (VNN-Comp). Int. J. Softw. Tools Technol. Transfer 25, 329–339 (2023)

    Google Scholar 

  7. Brostow, G.J., Fauqueur, J., Cipolla, R.: Semantic object classes in video: A high-definition ground truth database. Pattern Recogn. Lett. 30(2), 88–97 (2009)

    Article  Google Scholar 

  8. Dathathri, S., et al.: Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming (2020)

    Google Scholar 

  9. Demarchi, S.: VNN-LIB – vnnlib.org. https://www.vnnlib.org/ Accessed 31 Aug 2023

  10. Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D’Souza, D., Narayan Kumar, K. (eds.) Automated Technology for Verification and Analysis, pp. 269–286. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_19

    Chapter  Google Scholar 

  11. Fazlyab, M., Morari, M., Pappas, G.J.: Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Trans. Auto. Control 67(1), 1–15 (2022). https://doi.org/10.1109/TAC.2020.3046193

    Article  MathSciNet  Google Scholar 

  12. Flohr, F., Gavrila, D., et al.: Pedcut: an iterative framework for pedestrian segmentation combining shape models and multiple data cues. In: BMVC (2013)

    Google Scholar 

  13. Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: 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 

  14. Girard-Satabin, J., Alberti, M., Bobot, F., Chihani, Z., Lemesle, A.: Caisar: A platform for characterizing artificial intelligence safety and robustness. arXiv preprint arXiv:2206.03044 (2022)

  15. Guo, Y., Gao, Y., Shen, D.: Deformable MR prostate segmentation via deep feature learning and sparse patch matching. IEEE Trans. Med. Imaging 35(4), 1077–1089 (2015)

    Article  Google Scholar 

  16. Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: Reachability analysis of neural-network controlled systems. ACM Trans. Embedded Comput. Syst. (TECS) 18(5s), 1–22 (2019)

    Article  Google Scholar 

  17. Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, pp. 3–29. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_1

    Chapter  Google Scholar 

  18. Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 169–178 (2019)

    Google Scholar 

  19. Kamann, C., Rother, C.: Benchmarking the robustness of semantic segmentation models. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pp. 8828–8838 (2020)

    Google Scholar 

  20. 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.) Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, pp. 97–117. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_5

    Chapter  Google Scholar 

  21. Katz, G., et al.: The Marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, pp. 443–452. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_26

    Chapter  Google Scholar 

  22. LeCun, Y.: The mnist database of handwritten digits. http://yann.lecun.com/exdb/mnist/ (1998)

  23. Li, B., Liu, S., Xu, W., Qiu, W.: Real-time object detection and semantic segmentation for autonomous driving. In: MIPPR 2017: Automatic Target Recognition and Navigation. vol. 10608, pp. 167–174. SPIE (2018)

    Google Scholar 

  24. Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J., et al.: Algorithms for verifying deep neural networks. Found. Trends® in Optimization 4(3–4), 244–404 (2021)

    Google Scholar 

  25. Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351 (2017)

  26. Mohapatra, J., Weng, T.W., Chen, P.Y., Liu, S., Daniel, L.: Towards verifying robustness of neural networks against a family of semantic perturbations. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR) (2020)

    Google Scholar 

  27. Moosavi-Dezfooli, S.M., Fawzi, A., Frossard, P.: Deepfool: a simple and accurate method to fool deep neural networks. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 2574–2582 (2016)

    Google Scholar 

  28. Müller, M.N., Brix, C., Bak, S., Liu, C., Johnson, T.T.: The third international verification of neural networks competition (vnn-comp 2022): summary and results. arXiv preprint arXiv:2212.10376 (2022)

  29. Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. arXiv preprint arXiv:1805.02242 (2018)

  30. Ruan, W., Wu, M., Sun, Y., Huang, X., Kroening, D., Kwiatkowska, M.: Global robustness evaluation of deep neural networks with provable guarantees for the \( l_0 \) norm. arXiv preprint arXiv:1804.05805 (2018)

  31. Shriver, D., Elbaum, S., Dwyer, M.B.: DNNV: a framework for deep neural network verification. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I, pp. 137–150. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81685-8_6

    Chapter  Google Scholar 

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

    Google Scholar 

  33. Szegedy, C., et al.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)

  34. Szeliski, R.: Computer vision: algorithms and applications 2nd edition (2021)

    Google Scholar 

  35. Tao, X., Zhang, D., Ma, W., Liu, X., Xu, D.: Automatic metallic surface defect detection and recognition with convolutional neural networks. Appl. Sci. 8(9), 1575 (2018)

    Article  Google Scholar 

  36. Thoma, M.: A survey of semantic segmentation. arXiv preprint arXiv:1602.06541 (2016)

  37. Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: International Conference on Learning Representations (2019)

    Google Scholar 

  38. Tran, H.-D., Bak, S., Xiang, W., Johnson, T.T.: Verification of Deep Convolutional Neural Networks Using ImageStars. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I, pp. 18–42. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_2

    Chapter  Google Scholar 

  39. Tran, H.D., Cei, F., Lopez, D.M., Johnson, T.T., Koutsoukos, X.: Safety verification of cyber-physical systems with reinforcement learning control. In: ACM SIGBED International Conference on Embedded Software (EMSOFT’19). ACM (2019)

    Google Scholar 

  40. Tran, H.D., et al.: Star-based reachability analysis of deep neural networks. In: Formal Methods-The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings 3, pp. 670–686. Springer (2019)

    Google Scholar 

  41. Tran, H.-D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings, pp. 670–686. Springer International Publishing, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_39

    Chapter  Google Scholar 

  42. Tran, H.-D., et al.: Robustness verification of semantic segmentation neural networks using relaxed reachability. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I, pp. 263–286. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81685-8_12

    Chapter  Google Scholar 

  43. Tran, H.D., Xiang, W., Johnson, T.T.: Verification approaches for learning-enabled autonomous cyber-physical systems. IEEE Design & Test (2020)

    Google Scholar 

  44. Tran, H.-D., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I, pp. 3–17. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_1

    Chapter  Google Scholar 

  45. Tseng, Y.H., Jan, S.S.: Combination of computer vision detection and segmentation for autonomous driving. In: 2018 IEEE/ION Position, Location and Navigation Symposium (PLANS), pp. 1047–1052. IEEE (2018)

    Google Scholar 

  46. Wang, Z., Wei, L., Wang, L., Gao, Y., Chen, W., Shen, D.: Hierarchical vertex regression-based segmentation of head and neck CT images for radiotherapy planning. IEEE Trans. Image Process. 27(2), 923–937 (2017)

    Article  MathSciNet  Google Scholar 

  47. Xiang, W., Johnson, T.T.: Reachability analysis and safety verification for neural network control systems. arXiv preprint arXiv:1805.09944 (2018)

  48. Xiang, W., et al.: Verification for machine learning, autonomy, and neural networks survey. arXiv preprint arXiv:1810.01989 (2018)

  49. Xie, X., Kersting, K., Neider, D.: Neuro-symbolic verification of deep neural networks. arXiv preprint arXiv:2203.00938 (2022)

  50. Yuan, X., He, P., Zhu, Q., Li, X.: Adversarial examples: attacks and defenses for deep learning. IEEE Transac. Neural Netw. Learn. Syst. 30(9), 2805–2824 (2019)

    Article  MathSciNet  Google Scholar 

  51. Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems. vol. 31, pp. 4939–4948. Curran Associates, Inc. (2018)

    Google Scholar 

  52. Zhu, X., Suk, H.I., Lee, S.W., Shen, D.: Subspace regularized sparse multitask learning for multiclass neurodegenerative disease identification. IEEE Trans. Biomed. Eng. 63(3), 607–618 (2015)

    Article  Google Scholar 

  53. Zhu, X., Suk, H.I., Shen, D.: A novel matrix-similarity based loss function for joint regression and classification in ad diagnosis. Neuroimage 100, 91–105 (2014)

    Article  Google Scholar 

Download references

Acknowledgements

The material presented in this paper is based upon work supported by the National Science Foundation (NSF) through grant numbers 1910017, 2028001, 2220426, and 2220401, and the Defense Advanced Research Projects Agency (DARPA) under contract number FA8750-23-C-0518, and the Air Force Office of Scientific Research (AFOSR) under contract number FA9550-22-1-0019 and FA9550-23-1-0135. Any opinions, findings, conclusions, or recommendations expressed in this paper are those of the authors and do not necessarily reflect the views of AFOSR, DARPA, or NSF. We also want to thank our colleagues, Tianshu and Serena for their valuable feedback.

Author information

Authors and Affiliations

  1. Institute for Software Integration and Systems, Vanderbilt University, Nashville, TN, USA

    Neelanjana Pal, Seojin Lee & Taylor T. Johnson

Authors
  1. Neelanjana Pal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Seojin Lee
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Taylor T. Johnson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Neelanjana Pal .

Editor information

Editors and Affiliations

  1. TU Dortmund University, Dortmund, Germany

    Bernhard Steffen

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

Pal, N., Lee, S., Johnson, T.T. (2024). Benchmark: Formal Verification of Semantic Segmentation Neural Networks. In: Steffen, B. (eds) Bridging the Gap Between AI and Reality. AISoLA 2023. Lecture Notes in Computer Science, vol 14380. Springer, Cham. https://doi.org/10.1007/978-3-031-46002-9_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-46002-9_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-46001-2

  • Online ISBN: 978-3-031-46002-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation