|基金项目:本课题得到国家自然科学基金(No. 61972301, No. 61672403, No. 62192730, No. 62192734); 西安市科技计划项目(No. 22GXFW0025); 陕西省重点研发计划(No. 2020GY-043); 陕西省重点科技创新团队(No. 2019TD-001)资助。
|A Formal Verification Method for Recurrent Neural Network Based on Robustness Radius Solving
|ZHAO Liang,QI Runchuan,DUAN Xinmin,LI Chunyi,WANG Xiaobing
|School of Computer Science and Technology, Xidian University, Xi'an 710071, China
|With the development of software and hardware technology, neural networks have been widely applied to the various walks of life, but they are also exposed with insufficient robustness during their applications. Therefore, it is vital to use formal methods to check and ensure the security of neural networks. However, due to the facts such as complex structure and nonlinear activation function of recurrent neural networks, the work on formal verification of this kind of neural networks is very limited at present. Aiming at the problem that recurrent neural networks are difficult to verify, this paper proposes VR-RRS, a formal Verification method for Recurrent neural networks based on Robustness Radius Solution. First, based on the classical approximate solution framework of neural network verification, the linear expressions of the upper and lower bounds of the approximate interval of neurons at each layer about the input of the recurrent neural network are obtained through layer-by-layer backtracking iteration. On this basis, the analytic solutions of the upper and lower bounds of the approximate interval of neurons at each layer about the disturbance radius are derived using Holder inequality. Then, aiming at the problem that the accuracy of the classical approximate solving method is not high, by analyzing and optimizing approximation modes of the activation function, a solving strategy based on multi-path backtracking is proposed. This strategy constructs different backtracking paths with the fine-grained approximation method. On this basis, the approximate intervals solved by these backtracking paths are intersected to obtain a more accurate approximate interval. Finally, an improved dichotomy is used to solve the robust radius, which mainly aims at the problem of insufficient precision in the classical dichotomy and optimizes the standard to judge the robustness of neural networks. Through comparative experiments with existing methods on recurrent neural networks with different structures, this method shows obvious advantages in the robustness radius obtained and the success rate of verification.
|Key words: formal verification|recurrent neural network|robustness radius|approximate solving