Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement

• URL: http://arxiv.org/abs/2605.14294v1
• Date: Thu, 14 May 2026 02:55:53 GMT
• Title: Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement
• Abstract summary: We propose a transformer verification approach that can achieve improved precision.<n>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.<n>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.
• Score: 2.7819473614843546
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Dual Path Attribution: Efficient Attribution for SwiGLU-Transformers through Layer-Wise Target Propagation [5.186807923082922]
  We introduce Dual Path Attribution (DPA), a novel framework that faithfully traces information flow on the frozen transformer in one forward and one backward pass.<n>DPA achieves state-of-the-art faithfulness and unprecedented efficiency compared to existing baselines.
  arXiv  Detail & Related papers  (2026-03-20T08:28:24Z)
• Variational Rectification Inference for Learning with Noisy Labels [74.85528327499662]
  We propose variational rectification inference (VRI) to formulate the adaptive rectification for loss functions.<n>VRI is constructed as a hierarchical Bayes by treating the rectifying vector as a latent variable.<n>By introducing the variational term in VRI, the conditional posterior is estimated accurately and avoids collapsing to a Dirac delta function.
  arXiv  Detail & Related papers  (2026-03-18T01:25:08Z)
• Verifiable Reasoning for LLM-based Generative Recommendation [106.7765000777685]
  Reasoning in Large Language Models (LLMs) has recently shown strong potential in enhancing generative recommendation.<n>We propose a novel textbftextitreason-verify-recommend paradigm, which interleaves reasoning with verification to provide reliable feedback.<n>Experiments on four real-world datasets demonstrate that VRec substantially enhances recommendation effectiveness and scalability without compromising efficiency.
  arXiv  Detail & Related papers  (2026-03-08T16:55:45Z)
• Transformer Meets Twicing: Harnessing Unattended Residual Information [2.1605931466490795]
  Transformer-based deep learning models have achieved state-of-the-art performance across numerous language and vision tasks.<n>While the self-attention mechanism has proven capable of handling complex data patterns, it has been observed that the representational capacity of the attention matrix degrades significantly across transformer layers.<n>We propose the Twicing Attention, a novel attention mechanism that uses kernel twicing procedure in nonparametric regression to alleviate the low-pass behavior of associated NLM smoothing.
  arXiv  Detail & Related papers  (2025-03-02T01:56:35Z)
• Transformers Handle Endogeneity in In-Context Linear Regression [34.458004744956334]
  We show that transformers inherently possess a mechanism to handle endogeneity effectively using instrumental variables (IV)<n>We propose an in-context pretraining scheme and provide theoretical guarantees showing that the global minimizer of the pre-training loss achieves a small excess loss.
  arXiv  Detail & Related papers  (2024-10-02T06:21:04Z)
• Learning on Transformers is Provable Low-Rank and Sparse: A One-layer Analysis [63.66763657191476]
  We show that efficient numerical training and inference algorithms as low-rank computation have impressive performance for learning Transformer-based adaption. We analyze how magnitude-based models affect generalization while improving adaption. We conclude that proper magnitude-based has a slight on the testing performance.
  arXiv  Detail & Related papers  (2024-06-24T23:00:58Z)
• End-to-End Meta-Bayesian Optimisation with Transformer Neural Processes [52.818579746354665]
  This paper proposes the first end-to-end differentiable meta-BO framework that generalises neural processes to learn acquisition functions via transformer architectures. We enable this end-to-end framework with reinforcement learning (RL) to tackle the lack of labelled acquisition data.
  arXiv  Detail & Related papers  (2023-05-25T10:58:46Z)
• Full Stack Optimization of Transformer Inference: a Survey [58.55475772110702]
  Transformer models achieve superior accuracy across a wide range of applications. The amount of compute and bandwidth required for inference of recent Transformer models is growing at a significant rate. There has been an increased focus on making Transformer models more efficient.
  arXiv  Detail & Related papers  (2023-02-27T18:18:13Z)
• BiT: Robustly Binarized Multi-distilled Transformer [36.06192421902272]
  We develop binarized transformer models that are at a practical level of accuracy, approaching a full-precision BERT baseline within as little as 5.9%. These approaches allow for the first time, fully binarized transformer models that are at a practical level of accuracy, approaching a full-precision BERT baseline within as little as 5.9%.
  arXiv  Detail & Related papers  (2022-05-25T19:01:54Z)
• Transformer Uncertainty Estimation with Hierarchical Stochastic Attention [8.95459272947319]
  We propose a novel way to enable transformers to have the capability of uncertainty estimation. This is achieved by learning a hierarchical self-attention that attends to values and a set of learnable centroids. We empirically evaluate our model on two text classification tasks with both in-domain (ID) and out-of-domain (OOD) datasets.
  arXiv  Detail & Related papers  (2021-12-27T16:43:31Z)
• Robustness Verification for Transformers [165.25112192811764]
  We develop the first robustness verification algorithm for Transformers. The certified robustness bounds computed by our method are significantly tighter than those by naive Interval Bound propagation. These bounds also shed light on interpreting Transformers as they consistently reflect the importance of different words in sentiment analysis.
  arXiv  Detail & Related papers  (2020-02-16T17:16:31Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.