PaperlayerView exact revision on arXiv

Source-linked AI summary

Robustness Verification for Transformers

Zhouxing Shi, Huan Zhang, Kai-Wei Chang, Minlie Huang, Cho-Jui Hsieh

arXiv:2002.06622v2cs.LGstat.ML

TL;DR

Existing verification methods generally handle simpler network architectures, while Transformers’ self-attention introduces challenges including cross-nonlinearity and dependencies across positions. This paper develops a robustness verifier for Transformers using linear bounds and specialized attention propagation. Its bounds are reported as significantly tighter than Interval Bound Propagation and as reflecting word importance in sentiment analysis.

  • Problem

    Existing neural-network verification methods generally focus on simpler architectures, leaving robustness verification for Transformers with self-attention unaddressed.

    Source: §1 · p. 1, §2 · p. 3

  • Method

    The paper develops a Transformer robustness verifier that propagates linear bounds and addresses cross-nonlinearity and cross-position dependency in self-attention.

    Source: §1 · p. 2

  • Results

    The certified bounds are significantly tighter than Interval Bound Propagation bounds and consistently reflect word importance in sentiment analysis.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The bounds are presented as meaningful in practice and as a way to shed light on interpreting Transformers through word importance in sentiment analysis.

    Source: §1 · p. 2

    The formulation considers perturbations at selected positions in a sequence around a correctly classified input.

    Source: §3 · p. 3

Abstract

from arXiv · show

Robustness verification that aims to formally certify the prediction behavior of neural networks has become an important tool for understanding model behavior and obtaining safety guarantees. However, previous methods can usually only handle neural networks with relatively simple architectures. In this paper, we consider the robustness verification problem for Transformers. Transformers have complex self-attention layers that pose many challenges for verification, including cross-nonlinearity and cross-position dependency, which have not been discussed in previous works. We resolve these challenges and 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.

1 INTRODUCTION

Neural-network verification helps analyze model behavior and obtain safety guarantees, but existing methods largely target simpler architectures. This paper introduces a Transformer robustness verifier that addresses self-attention challenges and yields tighter bounds than Interval Bound Propagation.

1 INTRODUCTION

  • Adversarial perturbations can make neural-network predictions unreliable and unstable, motivating verification for understanding behavior and supporting safety guarantees.The introduction also identifies model explanation and robustness analysis as applications.Source: §1 · p. 1
  • The paper presents the first robustness verification algorithm for Transformers, whose self-attention architecture existing methods could not handle.Transformers are used across natural-language processing and other domains.Source: §1 · pp. 1–2
  • The method adapts linear relaxation to certify unchanged Transformer predictions when perturbed input frames remain within ℓp-balls around their originals.It recursively propagates linear lower and upper bounds over the perturbation space.Source: §1 · p. 2
  • Self-attention creates cross-nonlinearity and cross-position dependency, which complicate bound propagation and increase computational cost.The method derives closed-form linear bounds for cross-nonlinear operations and combines forward and backward propagation to avoid cross-position dependency in backward bounding, reducing its complexity by O(n) while retaining comparably tight bounds.Source: §1 · p. 2
  • The certified bounds are significantly tighter than Interval Bound Propagation and consistently reflect word importance in sentiment analysis.The paper presents these bounds as meaningful in practice and potentially useful for interpreting Transformers.Source: §1 · p. 2

2 RELATED WORK

Earlier robustness-verification methods largely focused on simpler network architectures, leaving Transformers unhandled. NLP robustness work included adversarial-example generation and certification for other model types, but verification for NLP models remained limited.

2 RELATED WORK

  • Exact verification approaches include mixed-integer linear programming, branch and bound, and satisfiability modulo theory; relaxations offer a route to efficient lower bounds.The paper notes that exact verification is NP-hard even for a simple ReLU network (Katz et al., 2017).Source: §2 · p. 2
  • Most existing verification methods target feed-forward or recurrent networks, and none of the cited methods handle Transformers.The related work also notes approaches based on local Lipschitz constants (Hein & Andriushchenko, 2017; Zhang et al., 2019).Source: §2 · p. 3
  • Prior NLP robustness research generated adversarial examples, while Hsieh et al. (2019) compared Transformer and LSTM robustness.Ko et al. (2019) verified RNN/LSTM models; Jia et al. (2019) and Huang et al. (2019) used Interval Bound Propagation for certified robustness training of CNNs and LSTMs.Source: §2 · p. 3

3 METHODOLOGY

The method certifies prediction robustness by bounding Transformer outputs over perturbations to selected input positions. It combines linear bounds with specialized self-attention propagation to address operations involving multiple perturbed variables and dependencies across sequence positions.

3 METHODOLOGY

  • The method formulates Transformer robustness over a sequence of frames, with a selected set of positions perturbed around a correctly classified input.Binary text classification is used as a running example, with word embeddings as frames and class scores as outputs.Source: §3 · p. 3

3.1 BASE FRAMEWORK

  • The base framework computes global lower and upper bounds for neuron values at each sub-layer and position, representing bounds as linear functions of earlier neurons.It propagates bounds backward recursively toward the perturbed input embeddings.Source: §3.1 · pp. 3–4

3.2 LINEAR TRANSFORMATIONS AND UNARY NONLINEAR FUNCTIONS

  • Linear transformations are handled by substitution, while unary nonlinear functions use linear relaxations over their previously computed bounds.The method supports relaxations for different functions involved in Transformers.Source: §3.2 · p. 4

3.3 SELF-ATTENTION MECHANISM

  • For self-attention, the method bounds multiplication and division with linear functions, including products of two variables whose ranges are already bounded.It handles division indirectly by first bounding a reciprocal as a unary function and then bounding the multiplication.Source: §3.3 · p. 5

A Forward Process

  • A forward process propagates bounds through attention scores, softmax probabilities, and weighted value sums; combining it with backward propagation reduces matrix count from O(m^2n^2) to O(m^2n).The backward process skips earlier self-attention layers; the paper states that backward bounds are tighter than forward-only bounds.Source: A Forward Process · pp. 5–6

4 EXPERIMENTS

Experiments evaluate certified bounds on sentiment-classification Transformers and test whether they support efficient verification and identification of important words. Across the reported settings, the bounds are tighter than IBP, and word-importance analyses show meaningful results on SST and Yelp.

4.1 DATASETS AND MODELS

  • Experiments use Yelp and SST, with Transformers of up to three layers and four attention heads; large-scale pretrained models are excluded as too challenging to verify tightly.Layer-normalization variance terms are removed to tighten bounds while keeping clean accuracies comparable.Source: §4.1 · p. 7

4.2 CERTIFIED BOUNDS

  • Bounds are evaluated on 10 correctly classified test examples, with one-position ℓ1/ℓ2/ℓ∞ and two-position ℓ2 perturbations; enumeration-based upper bounds are limited to one position.The two-position upper bounds are omitted because enumeration grows exponentially with vocabulary size and is difficult to extend to multiple positions.Source: §4.2 · p. 8
  • Our certified lower bounds are significantly tighter than IBP for both 1-position and 2-position perturbations.Tables 1 and 2 report the respective perturbation settings.Source: Table 1 · p. 7, Table 2 · p. 7, §4.2 · p. 8

4.3 EFFECTIVENESS OF COMBINING THE BACKWARD PROCESS WITH A FORWARD PROCESS

  • Backward & Forward produces bounds comparable to Fully-Backward and tighter than Fully-Forward, while taking significantly less computation time than Fully-Backward.This comparison uses smaller models and one-position perturbations to accommodate Fully-Backward's computational cost.Source: §4.3 · p. 8, Table 3 · p. 8

4.4 IDENTIFYING WORDS IMPORTANT TO PREDICTION

  • On SST, lower bounds identify most-important words with higher average importance scores and least-important words with lower scores than the Upper and Grad baselines.Importance is scored by distance from the neutral sentiment label.Source: §4.4 · p. 9, Table 4 · p. 9
  • On Yelp, the method's most-important words typically express sentiment and its least-important words are mostly stopwords, unlike more baseline misidentifications.Yelp examples are assessed qualitatively because the dataset lacks per-word sentiment labels.Source: §4.4 · p. 9

5 CONCLUSION

The paper presents the first robustness verification method for Transformers, addressing cross-nonlinearity and cross-position dependency. Its certified lower bounds are tighter than IBP and reflect word importance in sentiment analysis.

  • The method addresses cross-nonlinearity and cross-position dependency in Transformer verification.The paper presents it as the first robustness verification method for Transformers.Source: §5 · p. 9
  • Its certified lower bounds are significantly tighter than those from IBP.Source: §5 · p. 9
  • Quantitative and qualitative analyses show that the bounds reflect the importance of different words in sentiment analysis.Source: §5 · p. 9

A ILLUSTRATION OF DIFFERENT BOUNDING PROCESSES

The illustration contrasts three bound-propagation processes over a two-layer Transformer. The proposed hybrid uses backward propagation for feed-forward blocks and forward propagation for self-attention blocks.

B LINEAR BOUNDS OF UNARY NONLINEAR FUNCTIONS

The appendix derives neuron-wise linear lower and upper bounds for Transformer unary nonlinearities from each neuron's input range. The relaxation choices depend on the function and its curvature or domain constraints.

  • For each neuron, linear bounds on a unary nonlinearity are determined from the input interval and function-specific parameters.The appendix describes choices intended to keep the bounds valid and as tight as possible.Source: B LINEAR BOUNDS OF UNARY NONLINEAR… · p. 15
  • For ReLU, bounds are exact when the interval stays on one side of zero; for intervals crossing zero, the upper bound joins endpoints and the lower bound is selected by interval width.Source: B LINEAR BOUNDS OF UNARY NONLINEAR… · p. 15
  • For tanh, convex or concave intervals use endpoint and midpoint-tangent bounds; intervals crossing zero use tangents found by binary search.Source: B LINEAR BOUNDS OF UNARY NONLINEAR… · p. 15
  • For exp, the upper bound joins endpoints and the lower tangent is constrained to stay positive for the softmax reciprocal; square and square-root bounds likewise follow their convexity or concavity.The square lower bound is constrained to remain nonnegative before the square-root operation in layer normalization.Source: B LINEAR BOUNDS OF UNARY NONLINEAR… · pp. 15–16

C LINEAR BOUNDS OF MULTIPLICATIONS AND DIVISIONS

This section derives linear bounds for multiplication and division operations. It seeks tight multiplication bounds and obtains division bounds indirectly from multiplication and reciprocal bounds.

C LINEAR BOUNDS OF MULTIPLICATIONS AND DIVISIONS

  • Multiplication is bounded by lower and upper linear planes over input intervals, with parameters chosen to make the bounds as tight as possible.Division bounds are obtained indirectly using multiplication bounds and the reciprocal function.Source: C LINEAR BOUNDS OF MULTIPLICATIONS AND… · p. 16

C.1 LOWER BOUND OF MULTIPLICATIONS

  • The lower-plane derivation checks rectangle corners to enforce a nonnegative gap, then minimizes its integral; a minimum can occur on the boundary.At a minimum point with zero gap, at least one input equals an interval endpoint.Source: §C.1 · pp. 16–17

C.2 UPPER BOUND OF MULTIPLICATIONS

  • For the upper plane, the derivation compares endpoint choices for x0 and adopts the first case; the objective is independent of y0.The derivation takes y0 from its interval, such as y0 = ly.Source: §C.2 · pp. 18–19

C.3 LINEAR BOUNDS OF DIVISIONS

Directly deriving linear bounds for division is difficult because the difference function may attain its minimum away from the interval corners. The section instead uses multiplication and reciprocal bounds.

C.3 LINEAR BOUNDS OF DIVISIONS

  • Directly bounding division with a linear plane is difficult because the difference function’s minimum may occur away from the corners.That possibility makes closed-form parameters satisfying the bounding constraints more difficult to derive.Source: §C.3 · p. 19
  • The section identifies an interior minimum at (0.1, 0.1) for intervals [0.05, 0.15] on both inputs and a particular candidate plane.The example uses α = 10, β = −20, and γ = 2.Source: §C.3 · p. 19
  • Instead of deriving division bounds directly, the method uses bounds for reciprocal functions and multiplication.It bounds the reciprocal-related quantity before bounding the multiplication z = xy.Source: §C.3 · p. 19

D TIGHTNESS OF BOUNDS BY THE BACKWARD PROCESS AND FORWARD PROCESS

The section compares forward and backward bound propagation and explains why the method combines them. Forward propagation can reduce computational complexity, but its bounds can be looser.

D TIGHTNESS OF BOUNDS BY THE BACKWARD PROCESS AND FORWARD PROCESS

  • Combining forward and backward propagation can reduce computational complexity, but forward bounds can be looser, so forward propagation is used only for self-attention layers.The method does not apply the forward process to all sub-layers.Source: D TIGHTNESS OF BOUNDS BY THE BACKWARD… · p. 19
  • The section measures bound tightness through the difference between the weight matrices for lower and upper bounds.This measure is motivated by the role of the weight-matrix norm in the certified lower-bound search.Source: D TIGHTNESS OF BOUNDS BY THE BACKWARD… · p. 20

D.1 THE FORWARD PROCESS

  • The forward process starts with identity and zero bounds, propagates neuron bounds through each layer, and applies activation bounds using global pre-activation bounds.The section tracks the difference between upper and lower bounds as propagation proceeds.Source: §D.1 · p. 20

D.2 THE BACKWARD PROCESS AND DISCUSSIONS

The backward process propagates linear bounds to earlier layers and can continue to the input. In the comparison described here, backward bounds tend to be tighter than forward bounds.

D.2 THE BACKWARD PROCESS AND DISCUSSIONS

  • Backward propagation expresses neurons in a layer as linear functions of neurons in an earlier layer and recursively continues toward the input.The section treats a nonsequential input as a sequence of length one for this propagation.Source: §D.2 · pp. 20–21
  • Forward-propagated bound norms can grow large across layers when weight-matrix norms exceed 1.The section contrasts this with the backward process, which uses the weight matrix rather than its absolute value.Source: §D.2 · p. 21
  • Backward-process bounds tend to be tighter than forward-process bounds, consistent with the reported experiment results.The section attributes this tendency to possible cancellations among elements of the weight matrices.Source: §D.2 · p. 21

E IMPACT OF MODIFYING THE LAYER NORMALIZATION

This section examines modifying layer normalization to make Transformer verification tighter. It removes the standard-deviation term and compares certified bounds and clean accuracy across settings.

Loading 2002.06622v2…