Parameterized Abstract Interpretation for Transformer Verification

Background & Motivation

Models based on the self-attention mechanism have exhibited remarkable performance across a wide range of tasks. Notably, their success in large language models (LLMs) has significantly advanced the practical deployment of deep learning in diverse real-world domains. However, they also suffer from various security and safety issues, e.g., instability under input perturbations. This highlights the pressing need for formal verification, a rigorous technique grounded in mathematical reasoning, to systematically analyze, understand, and guarantee the reliable behavior of safety-critical systems.

Our paper studies the verification of Transformers via abstract interpretation, which involves overapproximating the behavior of a neural network with abstract domains (e.g., symbolic lower and upper bounds), with the hope that the property of interest still holds in the abstraction. As is well known, the attention module is one of the most important components of the Transformer architecture. Therefore, our work focuses on developing abstract interpretations for attention modules to improve verification success rates. To better control the overapproximation error, we propose two parameterized symbolic upper and lower bounds for the inner products used in the attention mechanism. With the aid of parameters, task-specific optimization objectives can be introduced to dynamically adjust the abstract domain, thereby making verification more likely to succeed (Fig. 1 provides an intuitive illustration).

More details can be found in the paper that we published at AAAI-26.


Figure 1: Motivation and Methodology

Methods

Computing the attention module involves two inner product operations. The output of one self-attention head is given by:

B = Q^T K / sqrt(d_K), Z = V · σ(B)

The construction of linear bounds for the inner product operation in attention reduces to finding parameterized linear bounds on a product of scalars $xy$. We design two methods:

The first method (PBverifierT) begins by constructing quadratic upper and lower bounds on the product $xy$ of two scalars $x$ and $y$; the upper bound is concave and the lower bound is convex. This ensures that any tangent plane to these quadratic functions serves as a valid affine upper or lower bound for $xy$.
The second method (PBverifierI) interpolates between the two affine bounds proposed in previous work [1]. We observe that, since the mean gap between $xy$ and a bound is a linear function of the bound, any convex combination of bounds that minimize the mean gap is also mean-gap-optimal. Therefore, we parameterize the bounds via interpolation to obtain a family of bounds.

To simplify implementation and make the optimization smoother, we reformulate the optimization procedures for both types of bounds as unconstrained optimization problems. We express each optimization variable $\underline{x_0}$, $\underline{y_0}$, $\overline{x_0}$, $\overline{y_0}$, $\underline{\alpha}$ and $\overline{\alpha}$ as a sigmoid function of an unconstrained variable $\lambda \in (-\infty, +\infty)$, for example:

$x_0 = l_x + (u_x - l_x) / (1 + e^{-λ}), α = 2 / (1 + e^{-λ}) - 1$

We can then tune the bounds with gradient-based methods, using objectives defined by the verification task. We denote by $\Lambda_l$ the set of all optimization variables $\lambda$ up to and including layer $l$.

[1] Zhouxing Shi et al. Robustness Verification for Transformers. ICLR 2020.

Pei Huang is a Postdoctoral Researcher advised by Clark Barrett in the Stanford Center for AI Safety. His work focuses on trustworthy AI.