通过分段优化提升循环神经网络的鲁棒性验证精度
Robustness Verification of Recurrent Neural Networks with Abstraction Refinement
- 对易出错的激活区间进行分段细化，使ReLU变精确，tanh/sigmoid线性逼近更紧
- 在CIFAR10和MNIST笔画数据集上，验证成功率与鲁棒边界紧致性均显著优于基线
- 用SHAP值筛选关键时间步，控制长序列下分段带来的计算爆炸风险
循环神经网络（RNN）的可认证局部鲁棒性验证面临挑战，因非线性松弛引入的近似误差会通过循环连接传播并随时间累积。现有可扩展的线性边界传播方法常过于保守，尤其当大量预激活区间跨越零点时，难以认证实际鲁棒的输入。本文提出一种抽象-精化框架：对这些区间进行划分，使每条分支上的ReLU变为精确，tanh、sigmoid等平滑激活函数的线性包络也大幅收紧。为控制长序列中分割带来的组合爆炸，引入基于SHAP值的时间步选择策略，按对验证目标的贡献度排序，按序仅精化最关键时间步。在CIFAR10和MNIST笔画基准上的实验显示，相比仅使用抽象的基线方法，本方法在验证成功率和鲁棒性边界紧致性上均有持续提升，同时揭示了ReLU与tanh模型在运行时间上的明显权衡。
原文摘要 · Abstract (English)
Certified local robustness verification for recurrent neural networks (RNNs) is challenging because approximation errors introduced by nonlinear relaxations can propagate through recurrent connections and accumulate over time. As a result, scalable linear bound propagation methods often become overly conservative and fail to certify inputs that are in fact robust, especially when many pre-activation intervals cross zero. We propose an abstraction-refinement framework for RNN verification that partitions such intervals to remove the dominant relaxation error: on each refined branch, ReLU becomes exact, and smooth activations such as tanh and sigmoid admit substantially tighter linear envelopes. To control the combinatorial cost of splitting in long sequences, we introduce a SHAP-guided timestep selection strategy that ranks hidden states by their contribution to the verification objective and refines only the most critical timesteps in temporal order. Experiments on CIFAR10 and MNIST stroke benchmarks demonstrate consistent improvements in verification success and robustness-margin tightness over abstraction-only baselines, while exposing clear runtime trade-offs between ReLU and tanh models.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。