基于线性松弛与对偶优化的循环神经网络验证方法
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

TP18

基金项目:

国家自然科学基金(61972301, 62192734); 陕西省重点研发计划(2023-YBGY-229); 西安市科技计划(22GXFW0025)


Verification Method for Recurrent Neural Network Based on Linear Relaxation and Dual Optimization
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    随着当今软硬件和人工智能技术的不断发展, 以神经网络为代表的智能模型在各行各业被广泛应用, 但同时也暴露出不少安全问题, 例如与鲁棒性相关的对抗样本问题. 因此, 通过形式化验证的方式来检测并保障神经网络的鲁棒性和安全性至关重要. 然而, 现有的神经网络验证工作主要面向以ReLU作为激活函数的前馈神经网络, 对于结构复杂、激活函数非线性的循环神经网络(RNN)的验证工作比较有限. 基于此现状, 提出一种基于线性松弛与对偶优化的循环神经网络验证方法, 以计算鲁棒半径的方式为这类网络模型提供严格的鲁棒性保障. 首先, 将RNN验证问题通过线性松弛编码为输出关于输入的优化问题. 考虑到网络的层级结构, 将该优化问题进行拉格朗日分解, 每个子问题中仅包含相邻的两层神经元, 子问题之间采用同一性约束进行关联. 随后, 构建其对偶问题并采用梯度上升算法来优化求解, 得到输出神经元的近似区间上下界, 其中解的有效性由对偶优化的性质所保障. 最后, 对输入扰动采用二分搜索的方式计算网络的鲁棒半径. 通过在不同结构的朴素RNN与较为复杂的长短期记忆网络(LSTM)上与已有的验证方法进行实验对比, 结果表明所提方法在朴素RNN上求解出的鲁棒半径上较已有方法提升了17.7%–30.2%, 在LSTM中亦有5.2%–10.2%的提升.

    Abstract:

    With the rapid advancement of modern hardware, software and artificial intelligence technologies, intelligent models represented by neural networks have been widely applied across various industries. However, these models also reveal significant safety problems, such as the robustness-related problem of adversarial examples. Therefore, ensuring and detecting the robustness and safety of neural networks through formal verification methods is of paramount importance. However, most existing research on neural network verification primarily targets feedforward neural networks with ReLU activation functions. In contrast, verification efforts for recurrent neural networks (RNN), which feature more complex structures and nonlinear activation functions, are relatively limited. To address this issue, this study proposes a verification method for RNNs based on linear relaxation and dual optimization. This method provides rigorous robustness guarantees by computing the robustness radius of these networks. First, the RNN verification problem is formulated as an optimization problem relating the network’s output to its input through linear relaxation. Taking into account the hierarchical structure of the network, the optimization problem is decomposed using Lagrangian decomposition into subproblems, each involving only two adjacent neuron layers, with equality constraints linking these subproblems. Next, the dual problem is formulated and solved using a gradient ascent algorithm to obtain approximate upper and lower bounds for the output neurons, with the validity of the solution ensured by the properties of dual optimization. Finally, binary search is applied to compute the network’s robustness radius with respect to input perturbations. By conducting experimental comparisons with existing verification methods on vanilla RNNs of different structures and more complex long short-term memory (LSTM) networks, results demonstrate that the proposed method achieves a 17.7% to 30.2% improvement in the robustness radius for vanilla RNNs and a 5.2% to 10.2% improvement for LSTM networks.

    参考文献
    相似文献
    引证文献
引用本文

赵亮,杨成龙,闫宗祥,王小兵.基于线性松弛与对偶优化的循环神经网络验证方法.软件学报,,():1-24

复制
相关视频

分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2025-02-07
  • 最后修改日期:2025-11-14
  • 录用日期:
  • 在线发布日期: 2026-06-10
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号