Robustness Verification of Recurrent Neural Networks with Abstraction Refinement
It addresses the challenge of overly conservative RNN verification for safety-critical applications, offering a method that improves certification tightness at the cost of increased runtime.
The paper proposes an abstraction-refinement framework for certified local robustness verification of RNNs that partitions problematic pre-activation intervals to reduce relaxation errors, achieving consistent improvements in verification success and robustness-margin tightness on CIFAR10 and MNIST stroke benchmarks.
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.