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

Clc Number:

TP18

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:February 07,2025
  • Revised:November 14,2025
  • Adopted:
  • Online: June 10,2026
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063