| 摘要: |
| 随着软硬件技术的发展,神经网络在各行各业取得了广泛的应用,然而在应用过程中也暴露出健壮性的不足。因此,采用形式化的手段来检验和保障神经网络的安全性是至关重要的。然而,由于循环神经网络结构复杂、激活函数非线性等因素,目前关于这类神经网络的形式化验证工作非常有限。针对循环神经网络难于验证的问题,本文提出了VR-RRS,一种基于健壮半径求解的循环神经网络形式化验证方法。首先,基于神经网络验证的经典近似求解框架,通过逐层回溯迭代的方式得到循环神经网络各层神经元近似区间上下界关于输入的线性表达式,在此基础上利用赫尔德不等式推导出各层神经元的近似上下界关于扰动半径的解析解。随后,针对经典近似求解方法精度不高的问题,通过对激活函数的近似方式进行分析和优化,提出一种基于多路径回溯的求解策略。该策略以细粒度近似方法构造不同的回溯路径,在此基础上将这些回溯路径求解的近似区间取交集,能够得到更为精确的近似区间。最后,采用改进的二分法对健壮半径进行求解,主要针对经典二分法中精度不足的问题,优化了判断神经网络健壮性的标准。通过在不同结构的循环神经网络上与已有方法开展对比实验,结果表明了该方法在求解出的健壮半径和验证成功率上具有明显优势。 |
| 关键词: 形式化验证|循环神经网络|健壮半径|近似求解 |
| DOI：10.19363/J.cnki.cn10-1380/tn.2023.05.02 |
| 投稿时间：2022-09-10修订日期：2022-12-14 |
| 基金项目:本课题得到国家自然科学基金(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 |
| Abstract: |
| 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 |
