# Robustness Verification of Recurrent Neural Networks with Abstraction Refinement

arXiv: https://arxiv.org/abs/2606.12490 · HTML: https://mlsanity.com/paper/2606.12490/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 18 of its 29 references that are in the map.
- First posted on arXiv 10 Jun 2026.

## Builds on (most cited first, 18 of 18)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [A Unified Approach to Interpreting Model Predictions](https://mlsanity.com/paper/1705.07874/) (2017)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Axiomatic Attribution for Deep Networks](https://mlsanity.com/paper/1703.01365/) (2017)
- [Sequence to Sequence Learning with Neural Networks](https://mlsanity.com/paper/1409.3215/) (2014)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Speech Recognition with Deep Recurrent Neural Networks](https://mlsanity.com/paper/1303.5778/) (2013)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [POPQORN: Quantifying Robustness of Recurrent Neural Networks](https://mlsanity.com/paper/1905.07387/) (2019)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Fooling LiDAR Perception via Adversarial Trajectory Perturbation](https://mlsanity.com/paper/2103.15326/) (2021)
- [Scalable Polyhedral Verification of Recurrent Neural Networks](https://mlsanity.com/paper/2005.13300/) (2020)
- [Certified Robustness to Programmable Transformations in LSTMs](https://mlsanity.com/paper/2102.07818/) (2021)
- [DiffRNN: Differential Verification of Recurrent Neural Networks](https://mlsanity.com/paper/2007.10135/) (2020)

## Abstract (arXiv)

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.