We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 35 Issue 6
November  2020
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Supplements
Wan-Wei Liu, Fu Song, Tang-Hao-Ran Zhang, Ji Wang. Verifying ReLU Neural Networks from a Model Checking Perspective[J]. Journal of Computer Science and Technology, 2020, 35(6): 1365-1381. DOI: 10.1007/s11390-020-0546-7
Citation: Wan-Wei Liu, Fu Song, Tang-Hao-Ran Zhang, Ji Wang. Verifying ReLU Neural Networks from a Model Checking Perspective[J]. Journal of Computer Science and Technology, 2020, 35(6): 1365-1381. DOI: 10.1007/s11390-020-0546-7
shu

Verifying ReLU Neural Networks from a Model Checking Perspective

  • 1 College of Computer Science, National University of Defense Technology, Changsha 410073, China;
    2 School of Information Science and Technology, ShanghaiTech University, Shanghai 201210, China;
    3 Shanghai Engineering Research Center of Intelligent Vision and Imaging, Shanghai 201210, China;
    4 State Key Laboratory for High Performance Computing, Changsha 410073, China

Funds: This work is supported by the National Natural Science Foundation of China under Grant No. 61872371, the Open Fund from the State Key Laboratory of High Performance Computing of China (HPCL) under Grant No. 202001-07, and the Natural Key Research and Development Program of China under Grant No. 2018YFB0204301.
More Information
  • Author Bio:

    Wan-Wei Liu received his Ph.D. degree in computer science from National University of Defense Technology, Changsha, in 2009. He is an associated professor in College of Computer Science, National University of Defense Technology, Changsha. He is a senior member of CCF. His research interests include theoretical computer science (particularly in automata theory and temporal logic), formal methods (particularly in verification), and software engineering.

  • Received Date: April 11, 2020
  • Revised Date: October 05, 2020
  • Published Date: November 19, 2020
    Abstract
  • Neural networks, as an important computing model, have a wide application in artificial intelligence (AI) domain. From the perspective of computer science, such a computing model requires a formal description of its behaviors, particularly the relation between input and output. In addition, such specifications ought to be verified automatically. ReLU (rectified linear unit) neural networks are intensively used in practice. In this paper, we present ReLU Temporal Logic (ReTL), whose semantics is defined with respect to ReLU neural networks, which could specify value-related properties about the network. We show that the model checking algorithm for the Σ2 ∪ Π2 fragment of ReTL, which can express properties such as output reachability, is decidable in EXPSPACE. We have also implemented our algorithm with a prototype tool, and experimental results demonstrate the feasibility of the presented model checking approach.
    • FullText(HTML)
    • References (35)
  • [1]
    Mcculloch W S, Pitts W. A logical calculus of the ideas immanent in nervous activity. Bulletin of Mathematical Biophysics, 1943, 5:115-133.
    [2]
    Salehinejad H, Baarbe J, Sankar S, Barfett J, Colak E, Valaee S. Recent advances in recurrent neural networks. arXiv:1801.01078, 2018. https://arxiv.org/abs/1801.01078, May 2020.
    [3]
    LeCun Y. Generalization and network design strategies. In Connectionism in Perspective, Pfeifer R, Schreter Z, Fogelman-Soulié F, Steels L (eds.), Elsevier, 1989, pp.143-155.
    [4]
    Nair V, Hinton G E. Rectified linear units improve restricted Boltzmann machines. In Proc. the 27th International Conference on Machine Learning, June 2010, pp.807-814.
    [5]
    Lei N, Luo Z, Yau S, Gu X D. Geometric understanding of deep learning. arXiv:1805.10451, 2018. https://arxiv.org/abs/1805.10451, May 2020.
    [6]
    Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. the 3rd Workshop on Logics of Programs, May 1981, pp.52-71.
    [7]
    Queille J, Sifakis J. Specification and verification of concurrent systems in CESAR. In Proc. the 5th Int. Symp. Programming, April 1982, pp.337-351.
    [8]
    Katz G, Barrett C W, Dill D L, Julian K, Kochenderfer M J. Reluplex:An efficient SMT solver for verifying deep neural networks. In Proc. the 29th Int. Conf. Computer Aided Verification, July 2017, pp.97-117.
    [9]
    Pnueli A. The temporal logic of programs. In Proc. the 18th Annual Symp. Foundations of Computer Science, October 1977, pp.46-57.
    [10]
    Pnueli A, Rosner R. On the synthesis of a reactive module. In Proc. the 16th Annual ACM Symp. Principles of Programming Languages, January 1989, pp.179-190.
    [11]
    Manna Z, Zarba C G. Combining decision procedures. In Proc. the 10th Anniversary Colloquium of the Int. Institute for Software Technology of the United Nations University, March 2002, pp.381-422.
    [12]
    Davenport J H, Heintz J. Real quantifier elimination is doubly exponential. J. Symbolic Computation, 1988, 5(1/2):29-35.
    [13]
    Huang X, Kwiatkowska M, Wang S, Wu M. Safety verification of deep neural networks. In Proc. the 29th Int. Conf. Computer Aided Verification, July 2017, pp.3-29.
    [14]
    Ruan W, Huang X, Kwiatkowska M. Reachability analysis of deep neural networks with provable guarantees. In Proc. the 27th Int. Joint Conf. Artificial Intelligence, July 2018, pp.2651-2659.
    [15]
    Pulina L, Tacchella A. An abstraction-refinement approach to verification of artificial neural networks. In Proc. the 22nd Int. Conf. Computer Aided Verification, July 2010, pp.243-257.
    [16]
    Dutta S, Jha S, Sankaranarayanan S, Tiwari A. Output range analysis for deep feedforward neural networks. In Proc. the 10th Int. Symposium NASA Formal Methods, April 2018, pp.121-138.
    [17]
    Weng T, Zhang H, Chen H, Song Z, Hsieh C, Daniel L, Duane S B, Dhillon I S. Towards fast computation of certified robustness for ReLU networks. In Proc. the 35th Int. Conf. Machine Learning, July 2018, pp.5273-5282.
    [18]
    Penrose R. A generalized inverse for matrices. Mathematical Proc. the Cambridge, 1955, 51:406-413.
    [19]
    Penrose R. On the best approximate solution of linear matrix equations. Mathematical Proceedings of the Cambridge Philosophical Society, 1956, 52(1):17-19.
    [20]
    Farkas G. über die theorie der einfachen ungleichungen. J. die Reine und Angewandte Mathematik, 1902, 124:1-24. (in German)
    [21]
    Lomuscio A, Maganti L. An approach to reachability analysis for feed-forward ReLU neural networks. arXiv:1706.07351, 2017. https://arxiv.org/abs/1706.07351, May 2020.
    [22]
    Huang X, Kroening D, Ruan W, Sharp J, Sun Y, Thamo E, Wu M, Yi X. Safety and trustworthiness of deep neural networks:A survey. arXiv:1812.08342v4, 2019. https://arxiv.org/abs/1812.08342, April 2020.
    [23]
    Szegedy C, Zaremba W, Sutskever I, Bruna J, Erhan D, Goodfellow I J, Fergus R. Intriguing properties of neural networks. In Proc. the 2nd Int. Conf. Learning Representations, April 2014.
    [24]
    Lei Y, Chen S, Fan L, Song F, Liu Y. Advanced evasion attacks and mitigations on practical ML-based phishing website classifiers. arXiv:2004.06954, 2020. https://arxiv.org/abs/2004.06954, May 2020.
    [25]
    Chen G, Chen S, Fan L, Du X, Zhao Z, Song F, Liu Y. Who is real Bob? Adversarial attacks on speaker recognition systems. arXiv:1911.01840, 2019. https://arxiv.org/abs/1911.01840, May 2020.
    [26]
    Duan Y, Zhao Z, Bu L, Song F. Things you may not know about adversarial example:A black-box adversarial image attack. arXiv:1905.07672, 2019. https://arxiv.org/abs/1905.07672, May 2020.
    [27]
    Narodytska N, Kasiviswanathan S P, Ryzhyk L, Sagiv M, Walsh T. Verifying properties of binarized deep neural networks. In Proc. the 32nd AAAI Conf. Artificial Intelligence, February 2018, pp.6615-6624.
    [28]
    Cheng C, Nührenberg G, Ruess H. Maximum resilience of artificial neural networks. In Proc. the 15th Int. Symp. Automated Technology for Verification and Analysis, October 2017, pp.251-268.
    [29]
    Bunel R, Turkaslan I, Torr P H S, Kohli P, Mudigonda P K. A unified view of piecewise linear neural network verification. In Proc. the 32nd Annual Conf. Neural Information Processing Systems, December 2018, pp.4795-4804.
    [30]
    Tran H, Lopez D M, Musau P, Yang X, Nguyen L V, Xiang W, Johnson T T. Star-based reachability analysis of deep neural networks. In Proc. the 3rd World Congress on Formal Methods, October 2019, pp.670-686.
    [31]
    Cousot P, Cousot R. Abstract interpretation:A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. the 4th ACM Symp. Principles of Programming Languages, January 1977, pp.238-252.
    [32]
    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 Proc. the 39th IEEE Symp. Security and Privacy, May 2018, pp.3-18.
    [33]
    Wang S, Pei K, Whitehouse J, Yang J, Jana S. Formal security analysis of neural networks using symbolic intervals. In Proc. the 27th USENIX Security Symp., August 2018, pp.1599-1614.
    [34]
    Singh G, Gehr T, Püschel M, Vechev M. T. Boosting robustness certification of neural networks. In Proc.the 7th International Conference on Learning Representations, May 2019.
    [35]
    Wan W, Zhang Z, Zhu Y, Zhang M, Song F. Accelerating robustness verification of deep neural networks guided by target labels. arXiv:2007.08520, 2020. https://arxiv.org/abs/2007.08520, July 2020.
    • Relative Articles

  • Related Articles

    [1]Zhen Liang, Wan-Wei Liu, Fu Song, Bai Xue, Wen-Jing Yang, Ji Wang, Zheng-Bin Pang. Qualitative and Quantitative Model Checking Against Recurrent Neural Networks[J]. Journal of Computer Science and Technology, 2024, 39(6): 1292-1311. DOI: 10.1007/s11390-023-2703-2
    [2]Zhen-Hua Duan, Maciej Koutny. A Framed Temporal Logic Programming Language[J]. Journal of Computer Science and Technology, 2004, 19(3).
    [3]Li Minglu, Sun Yongqiang, Sheng Huany. Nondeterministic Temporal Relations in Multimedia Data[J]. Journal of Computer Science and Technology, 1997, 12(3): 244-251.
    [4]Zhong Shaochun, Liu Dayou. Processing of Uncertainty Temporal Relations[J]. Journal of Computer Science and Technology, 1996, 11(1): 72-82.
    [5]Sun Yuan. The Modelling of Temporal Data in the Relational Database Environment[J]. Journal of Computer Science and Technology, 1995, 10(2): 163-174.
    [6]Shuai Dianxun. High-Order Two-Dimension Cluster Competitive Activation Mechanisms Used for Performing Symbolic Logic Algorithms of Problem Solving[J]. Journal of Computer Science and Technology, 1995, 10(2): 124-133.
    [7]Zhao Zhaokeng, Dai Jun, Chen Wendan. Automated Theorem Proving in Temporal Logic:T-Resolution[J]. Journal of Computer Science and Technology, 1994, 9(1): 53-62.
    [8]Lin Huimin, Gong Chun, Xie Hongliang. Abstract Implementation of Algebraic Specifications in a Temporal Logic Language[J]. Journal of Computer Science and Technology, 1991, 6(1): 11-20.
    [9]Xie Hongliang, Gong Jie, C.S.Tang. A Structured Temporal Logic Language:XYZ/SE[J]. Journal of Computer Science and Technology, 1991, 6(1): 1-10.
    [10]Li Renwei. A Natural Deduction System of Temporal Logic[J]. Journal of Computer Science and Technology, 1988, 3(3): 173-185.
    • Supplements (2)

  • Others

  • Cited by

    Periodical cited type(21)

    1. Zhen Liang, Taoran Wu, Changyuan Zhao, et al. BIRDNN: Behavior-Imitation Based Repair for Deep Neural Networks. Neural Networks, 2025, 183: 106949. DOI:10.1016/j.neunet.2024.106949
    2. Zhen Liang, Wan-Wei Liu, Fu Song, et al. Qualitative and Quantitative Model Checking Against Recurrent Neural Networks. Journal of Computer Science and Technology, 2024, 39(6): 1292. DOI:10.1007/s11390-023-2703-2
    3. Zhe Zhao, Guangke Chen, Tong Liu, et al. Attack as Detection: Using Adversarial Attack Methods to Detect Abnormal Examples. ACM Transactions on Software Engineering and Methodology, 2024, 33(3): 1. DOI:10.1145/3631977
    4. Zhen Liang, Dejin Ren, Bai Xue, et al. Verifying safety of neural networks from topological perspectives. Science of Computer Programming, 2024, 236: 103121. DOI:10.1016/j.scico.2024.103121
    5. Yedi Zhang, Zhe Zhao, Guangke Chen, et al. Precise Quantitative Analysis of Binarized Neural Networks: A BDD-based Approach. ACM Transactions on Software Engineering and Methodology, 2023, 32(3): 1. DOI:10.1145/3563212
    6. Zhen Liang, Taoran Wu, Wanwei Liu, et al. Towards robust neural networks via a global and monotonically decreasing robustness training strategy. Frontiers of Information Technology & Electronic Engineering, 2023, 24(10): 1375. DOI:10.1631/FITEE.2300059
    7. Lei Bu, Zhe Zhao, Yuchao Duan, et al. Taking Care of the Discretization Problem: A Comprehensive Study of the Discretization Problem and a Black-Box Adversarial Attack in Discrete Integer Domain. IEEE Transactions on Dependable and Secure Computing, 2022, 19(5): 3200. DOI:10.1109/TDSC.2021.3088661
    8. Fu Song, Yusi Lei, Sen Chen, et al. Advanced evasion attacks and mitigations on practical ML‐based phishing website classifiers. International Journal of Intelligent Systems, 2021, 36(9): 5210. DOI:10.1002/int.22510
    9. Yedi Zhang, Zhe Zhao, Guangke Chen, et al. QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks. Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, DOI:10.1145/3551349.3556916
    10. Zhen Liang, Dejin Ren, Wanwei Liu, et al. Theoretical Aspects of Software Engineering. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-35257-7_15
    11. Xingwu Guo, Wenjie Wan, Zhaodi Zhang, et al. Eager Falsification for Accelerating Robustness Verification of Deep Neural Networks. 2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE), DOI:10.1109/ISSRE52982.2021.00044
    12. Xiyue Zhang, Xiaohong Chen, Meng Sun. Theoretical Aspects of Computing – ICTAC 2022. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-17715-6_28
    13. Yedi Zhang, Zhe Zhao, Guangke Chen, et al. Computer Aided Verification. Lecture Notes in Computer Science, DOI:10.1007/978-3-030-81685-8_8
    14. Ye Tao, Wanwei Liu, Fu Song, et al. Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-45329-8_18
    15. Emanuele De Angelis, Guglielmo De Angelis, Maurizio Proietti. A Classification Study on Testing and Verification of AI-based Systems. 2023 IEEE International Conference On Artificial Intelligence Testing (AITest), DOI:10.1109/AITest58265.2023.00010
    16. Yantao Bai, Wanwei Liu, Xinjun Mao, et al. Modeling Neural Networks Training Process with Markov Decision Process. 2021 2nd International Conference on Artificial Intelligence and Computer Engineering (ICAICE), DOI:10.1109/ICAICE54393.2021.00102
    17. Zhe Zhao, Guangke Chen, Jingyi Wang, et al. Attack as defense: characterizing adversarial examples using robustness. Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, DOI:10.1145/3460319.3464822
    18. Yedi Zhang, Fu Song, Jun Sun. Computer Aided Verification. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-37703-7_20
    19. XinFeng Shu, YanLin Li, WeiRan Gao. Structured Object-Oriented Formal Language and Method. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-29476-1_3
    20. Zhe Zhao, Yedi Zhang, Guangke Chen, et al. Static Analysis. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-22308-2_20
    21. Zhen Liang, Changyuan Zhao, Wanwei Liu, et al. A Geometrical Characterization on Feature Density of Image Datasets. 2023 IEEE International Conference on Multimedia and Expo (ICME), DOI:10.1109/ICME55011.2023.00313

    Other cited types(0)

Catalog

    Get Citation
    PDF
    XML
    Read Online
    Article views (70) PDF downloads (0) Cited by(21)
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return