Qualitative and Quantitative Model Checking Against Recurrent Neural Networks

作     者：Zhen Liang Wan-Wei Liu Fu Song Bai Xue Wen-Jing Yang Ji Wang Zheng-Bin Pang 梁震;刘万伟;宋富;薛白;杨文婧;王戟;庞征斌

作者机构：Institute for Quantum Information&State Key Laboratory of High Performance ComputingCollege of Computer Science and TechnologyNational University of Defense TechnologyChangsha 410073China College of Computer Science and TechnologyNational University of Defense TechnologyChangsha 410073China School of Information Science and TechnologyShanghaiTech UniversityShanghai 201210China Institute of SoftwareChinese Academy of SciencesBeijing 100190China 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报(英文版))

年 卷 期：2024年第39卷第6期

页      面：1292-1311页

核心收录：

学科分类：07[理学] 0701[理学-数学] 070101[理学-基础数学] 

基　　金：supported by the National Natural Science Foundation of China under Grant Nos.61872371,62032024,and U19A2062 the Open Fund from the State Key Laboratory of High Performance Computing of China(HPCL)under Grant No.202001-07 

主　　题：recurrent neural network model checking temporal logic qualitative/quantitative verification 

摘      要：Recurrent neural networks (RNNs) have been heavily used in applications relying on sequence data such as time series and natural languages. As a matter of fact, their behaviors lack rigorous quality assurance due to the black-box nature of deep learning. It is an urgent and challenging task to formally reason about the behaviors of RNNs. To this end, we first present an extension of linear-time temporal logic to reason about properties with respect to RNNs, such as local robustness, reachability, and some temporal properties. Based on the proposed logic, we formalize the verification obligation as a Hoare-like triple, from both qualitative and quantitative perspectives. The former concerns whether all the outputs resulting from the inputs fulfilling the pre-condition satisfy the post-condition, whereas the latter is to compute the probability that the post-condition is satisfied on the premise that the inputs fulfill the pre-condition. To tackle these problems, we develop a systematic verification framework, mainly based on polyhedron propagation, dimension-preserving abstraction, and the Monte Carlo sampling. We also implement our algorithm with a prototype tool and conduct experiments to demonstrate its feasibility and efficiency.