基于健壮半径求解的循环神经网络形式化验证方法

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