软件学报:jos:7657 · 记录 #1

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

来源日期 2026-06-10

来源记录日期 2026-06-10

雷达观测 2026-11-05 00:20

摘要

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