Computer Science

Computer Science ›› 2023, Vol. 50 ›› Issue (11A): 221000045-5.doi: 10.11896/jsjkx.221000045

• Artificial Intelligence • Previous Articles     Next Articles

Constraint-based Verification Method for Neural Networks

GAO Yuzhao, XING Yunhan, LIU Jiaxiang   

  1. College of Computer Science and Software Engineering,Shenzhen University,Shenzhen,Guangdong 518060,China
  • Published:2023-11-09
  • About author:GAO Yuzhao,born in 1996,postgra-duate.His main research interests include formal verification and neural network.
    LIU Jiaxiang,born in 1987,Ph.D,assistant professor,is a member of China Computer Federation.His main research interests include formal verification and rewriting theory.
  • Supported by:
    Natural Science Foundation of Guangdong Province,China(2022A1515011458,2022A1515010880),National Natural Science Foundation of China(61836005) and Shenzhen Science and Technology Innovation Commission(JCYJ20210324094202008).

PDF (PC)

186

Abstract: The verification of neural networks has always been one of the major challenges in the field of artificial intelligence.Based on the DeepZ method,this paper proposes a method to improve the accuracy of verifying local robustness of deep neural networks by constraints.During the propagation process,constraints are added to reduce the abstract domain,then a tighter neural network output range is solved by linear programming,hence deducing new bounds of neural network output node.With the new bounds,more accurate verification results can be obtained.Based on this method,the DeepZero tool is implemented in this paper,and comprehensive evaluation is carried out on the MNIST dataset.Experimental results show that our method effectively improves the verification success rate of DeepZ.Specifically,the verification success rate of DeepZ increases by 49% in average,indicating the effectiveness of the proposed method.

Key words: Neural network, Software verification, Artificial intelligence, Machine learning, Software security

CLC Number: 

  • TP311
[1]HINTON G,DENG L,YU D,et al.Deep neural networks foracoustic modeling in speech recognition:The shared views of four research groups[J].IEEE Signal Processing Magazine,2012,29(6):82-97.
[2]KRIZHEVSKY A,SUTSKEVER I,HINTON G E.Imagenetclassification with deep convolutional neural networks[J].Communications of the ACM,2017,60(6):84-90.
[3]LUBOSCH M,KUNATH M,WINKLER H.Industrial sche-duling with Monte Carlo tree search and machine learning[C]//Procedia CIRP.2018:1283-1287.
[4]HUANG X,KROENING D,RUAN W,et al.A survey of safetyand trustworthiness of deep neural networks:Verification,testing,adversarial attack and defence,and interpretability[J].Computer Science Review,2020,37:100270.
[5]ZHANG M H,DU D H,ZHANG M Z,et al.Spatio-temporaltrajectory data-driven autonomous driving scenario meta-mode-ling approach[J].Ruan Jian Xue Bao/Journal of Software,2021,32(4):973-987.
[6]KALRA N,PADDOCK S M.Driving to safety:How many miles of driving would it take to demonstrate autonomous vehicle reliab-ility?[J].Transportation Research Part A:Policy and Practice,2016,94:182-193.
[7]WANG Z,YAN M,LIU S,et al.Survey on testing of deep neural networks[J].Ruan Jian Xue Bao/Journal of Software,2020,31(5):1255-1275.
[8]WANG J,ZHAN N J,FENG X Y,et al.Overview of formalmethods[J].Ruan Jian Xue Bao/Journal of Software,2019,30(1):33-61.
[9]LIU C,ARNON T,LAZARUS C,et al.Algorithms for verifying deep neural networks[J].Foundations and Trends© in Optimization,2021,4(3/4):244-404.
[10]PULINA L,TACCHELLA A.An abstraction-refinement ap-proach to verification of artificial neural networks[C]//International Conference on Computer Aided Verification.Berlin:Springer,2010:243-257.
[11]XIANG W,TRAN H D,JOHNSON T T.Reachable set computation and safety verification for neural networks with relu activations[J].arXiv:1712.08163,2017.
[12]XIANG W,TRAN H D,JOHNSON T T.Output reachable set estimation and verification for multilayer neural networks[J].IEEE Transactions on Neural Networks and Learning Systems,2018,29(11):5777-5783.
[13]SINGH G,GEHR T,MIRMAN M,et al.Fast and effective robustness certification[C]//Proceedings of the 32nd International Conference on Neural Information Processing Systems(NIPS’18).2018:10825-10836.
[14]SINGH G,GEHR T,PÜSCHEL M,et al.An abstract domain for certifying neural networks [C]//Proceedings of the 32nd International Conference on Neural Information Processing Systems(NIPS ’18).2018:10825-10836.
[15]DVIJOTHAM K,STANFORTH R,GOWAL S,et al.A Dual Approach to Scalable Verification of Deep Networks[C]//UAI.2018:3.
[16]RAGHUNATHAN A,STEINHARDT J,LIANG P.Certified defenses against adversarial examples[J].arXiv:1801.09344,2018.
[17]ASHOK P,HASHEMI V,KŘETÍNSKÝ J,et al.Deepab-stract:Neural network abstraction for accelerating verification[C]//International Symposium on Automated Technology for Verification and Analysis.Cham:Springer,2020:92-107.
[18]GEHR T,MIRMAN M,DRACHSLER-COHEN D,et al.Ai2:Safety and robustness certification of neural networks with abstract interpretation[C]//2018 IEEE Symposium on Security and Privacy(SP).IEEE,2018:3-18.
[19]TRAN H D,MANZANAS LOPEZ D,MUSAU P,et al.Star-based reachability analysis of deep neural networks[C]//International Symposium on Formal Methods.Cham:Springer,2019:670-686.
[20]ZHANG H,WENG T W,CHEN P Y,et al.Efficient neural network robustness certification with general activation functions[J/OL].Advances in Neural Information Processing Systems,2018,31.https://dl.acm.org/doi/abs/10.5555/3327345.3327402.
[21]XU K,ZHANG H,WANG S,et al.Fast and complete:Enabling complete neural network verification with rapid and massively parallel incomplete verifiers[J].arXiv:2011.13824,2020.
[22]WANG S,ZHANG H,XU K,et al.Beta-crown:Efficient bound propagation with per-neuron split constraints for neural network robustness verification[J].Advances in Neural Information Processing Systems,2021,34:29909-29921.
[23]DE PALMA A,BUNEL R,DESMAISON A,et al.Improvedbranch and bound for neural network verification via lagrangian decomposition[J].arXiv:2104.06718,2021.
[24]BUNEL R,MUDIGONDA P,TURKASLAN I,et al.Branchand bound for piecewise linear neural network verification[J/OL].Journal of Machine Learning Research,2020,21(2020).https://dl.acm.org/doi/10.5555/3455716.3455758.
[25]LI J,LIU J,YANG P,et al.Analyzing deep neural networks with symbolic propagation:Towards higher precision and faster verification[C]//International Static Analysis Symposium.Cham:Springer,2019:296-319.
[26]LIN W,YANG Z,CHEN X,et al.Robustness verification ofclassification deep neural networks via linear programming[C]//Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition.2019:11418-11427.
[27]YANG P,LI R,LI J,et al.Improving neural network verification through spurious region guided refinement[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Cham:Springer,2021:389-408.
[1] LU Yuhan, CHEN Liquan, WANG Yu, HU Zhiyuan. Efficient Encrypted Image Content Retrieval System Based on SecureCNN [J]. Computer Science, 2023, 50(9): 26-34.
[2] WANG Zibo, ZHANG Yaofang, CHEN Yilu, LIU Hongri, WANG Bailing, WANG Chonghua. Hierarchical Task Network Planning Based Attack Path Discovery [J]. Computer Science, 2023, 50(9): 35-43.
[3] LI Ke, YANG Ling, ZHAO Yanbo, CHEN Yonglong, LUO Shouxi. EGCN-CeDML:A Distributed Machine Learning Framework for Vehicle Driving Behavior Prediction [J]. Computer Science, 2023, 50(9): 318-330.
[4] HUANG Shuxin, ZHANG Quanxin, WANG Yajie, ZHANG Yaoyuan, LI Yuanzhang. Research Progress of Backdoor Attacks in Deep Neural Networks [J]. Computer Science, 2023, 50(9): 52-61.
[5] WANG Yao, LI Yi. Termination Analysis of Single Path Loop Programs Based on Iterative Trajectory Division [J]. Computer Science, 2023, 50(9): 108-116.
[6] YI Qiuhua, GAO Haoran, CHEN Xinqi, KONG Xiangjie. Human Mobility Pattern Prior Knowledge Based POI Recommendation [J]. Computer Science, 2023, 50(9): 139-144.
[7] LI Haiming, ZHU Zhiheng, LIU Lei, GUO Chenkai. Multi-task Graph-embedding Deep Prediction Model for Mobile App Rating Recommendation [J]. Computer Science, 2023, 50(9): 160-167.
[8] ZHU Ye, HAO Yingguang, WANG Hongyu. Deep Learning Based Salient Object Detection in Infrared Video [J]. Computer Science, 2023, 50(9): 227-234.
[9] YI Liu, GENG Xinyu, BAI Jing. Hierarchical Multi-label Text Classification Algorithm Based on Parallel Convolutional Network Information Fusion [J]. Computer Science, 2023, 50(9): 278-286.
[10] HENG Hongjun, MIAO Jing. Fusion of Semantic and Syntactic Graph Convolutional Networks for Joint Entity and Relation Extraction [J]. Computer Science, 2023, 50(9): 295-302.
[11] LIU Xiang, ZHU Jing, ZHONG Guoqiang, GU Yongjian, CUI Liyuan. Quantum Prototype Clustering [J]. Computer Science, 2023, 50(8): 27-36.
[12] TANG Shaosai, SHEN Derong, KOU Yue, NIE Tiezheng. Link Prediction Model on Temporal Knowledge Graph Based on Bidirectionally Aggregating Neighborhoods and Global Aware [J]. Computer Science, 2023, 50(8): 177-183.
[13] MA Weiwei, ZHENG Qinhong, LIU Shanshan. Study and Evaluation of Spiking Neural Network Model Based on Bee Colony Optimization [J]. Computer Science, 2023, 50(8): 221-225.
[14] LI Qiaojun, ZHANG Wen, YANG Wei. Fusion Neural Network-based Method for Predicting LncRNA-disease Association [J]. Computer Science, 2023, 50(8): 226-232.
[15] XIE Tonglei, DENG Li, YOU Wenlong, LI Ruilong. Analysis and Prediction of Cloud VM CPU Load Based on EMPC-BCGRU [J]. Computer Science, 2023, 50(8): 243-250.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.