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.