# Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 28 of its 38 references that are in the map.
- First posted on arXiv 14 May 2026.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Character-level Convolutional Networks for Text Classification](https://mlsanity.com/paper/1509.01626/) (2015)
- [TinyBERT: Distilling BERT for Natural Language Understanding](https://mlsanity.com/paper/1909.10351/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Generating Natural Language Adversarial Examples](https://mlsanity.com/paper/1804.07998/) (2018)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [Generalization in NLI: Ways (Not) To Go Beyond Simple Heuristics](https://mlsanity.com/paper/2110.01518/) (2021)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Towards Crafting Text Adversarial Samples](https://mlsanity.com/paper/1707.02812/) (2017)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results](https://mlsanity.com/paper/2512.19007/) (2025)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [Robustness in deep learning: The good (width), the bad (depth), and the ugly (initialization)](https://mlsanity.com/paper/2209.07263/) (2022)
- [NLP Verification: Towards a General Methodology for Certifying Robustness](https://mlsanity.com/paper/2403.10144/) (2024)
- [Tokenization is Sensitive to Language Variation](https://mlsanity.com/paper/2502.15343/) (2025)
- [Introduction to Transformers: an NLP Perspective](https://mlsanity.com/paper/2311.17633/) (2023)
- [Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks](https://mlsanity.com/paper/2208.09872/) (2022)
- [ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification](https://mlsanity.com/paper/2305.04003/) (2023)
- [Are Transformers More Robust? Towards Exact Robustness Verification for Transformers](https://mlsanity.com/paper/2202.03932/) (2022)
- [Are Synonym Substitution Attacks Really Synonym Substitution Attacks?](https://mlsanity.com/paper/2210.02844/) (2022)

## Abstract (arXiv)

Formal verification of transformers has become increasingly important due to their widespread deployment in safety-critical applications. Compared to classic neural networks, the inferences of transformers involve highly complex computations, such as dot products in self-attention layers, rendering their verification extremely difficult. Existing approaches explored over-approximation methods by constructing convex constraints to bound the output ranges of transformers, which can achieve high efficiency. However, they may sacrifice verification precision, and consequently introduce significant approximation error that leads to frequent occurrences of false alarms. In this paper, we propose a transformer verification approach that can achieve improved precision. At the core of our approach is a novel usage of ReLU, by which we represent a precise but non-linear bound for dot products such that we can further exploit the rich body of literature for convex relaxation of ReLU to derive precise bounds. We extend two classic approaches to the context of transformers, a rule-based one and an optimization-based one, resulting in two new frameworks for efficient and precise verification. We evaluate our approaches on different model architectures and robustness properties derived from two datasets about sentiment analysis, and compare with the state-of-the-art baseline approach. Compared to the baseline, our approach can achieve significant precision improvement for most of the verification tasks with acceptable compromise of efficiency, which demonstrates the effectiveness of our approach.