Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Are Transformers More Robust? Towards Exact Robustness Verification for Transformers

Brian Hsuan-Cheng Liao, Chih-Hong Cheng, Hasan Esen, Alois Knoll

TL;DR

This work tackles exact robustness verification for Sparsemax-based Transformers, addressing a gap in formal guarantees for transformer models in safety-critical tasks. It develops a MIQCP encoding of Sparsemax and two pre-processing heuristics to accelerate solving, enabling exact robustness measurement within $l_p$-norm perturbations. Using Lane Departure Warning as an industrial benchmark, the study finds that Sparsemax-based Transformers do not consistently outperform similarly sized MLPs in robustness, despite competitive accuracy. The results highlight the need for rigorous robustness guarantees when deploying transformer-based systems and open avenues for scalable, verifiable architectures in safety-critical settings.

Abstract

As an emerging type of Neural Networks (NNs), Transformers are used in many domains ranging from Natural Language Processing to Autonomous Driving. In this paper, we study the robustness problem of Transformers, a key characteristic as low robustness may cause safety concerns. Specifically, we focus on Sparsemax-based Transformers and reduce the finding of their maximum robustness to a Mixed Integer Quadratically Constrained Programming (MIQCP) problem. We also design two pre-processing heuristics that can be embedded in the MIQCP encoding and substantially accelerate its solving. We then conduct experiments using the application of Land Departure Warning to compare the robustness of Sparsemax-based Transformers against that of the more conventional Multi-Layer-Perceptron (MLP) NNs. To our surprise, Transformers are not necessarily more robust, leading to profound considerations in selecting appropriate NN architectures for safety-critical domain applications.

Are Transformers More Robust? Towards Exact Robustness Verification for Transformers

TL;DR

This work tackles exact robustness verification for Sparsemax-based Transformers, addressing a gap in formal guarantees for transformer models in safety-critical tasks. It develops a MIQCP encoding of Sparsemax and two pre-processing heuristics to accelerate solving, enabling exact robustness measurement within -norm perturbations. Using Lane Departure Warning as an industrial benchmark, the study finds that Sparsemax-based Transformers do not consistently outperform similarly sized MLPs in robustness, despite competitive accuracy. The results highlight the need for rigorous robustness guarantees when deploying transformer-based systems and open avenues for scalable, verifiable architectures in safety-critical settings.

Abstract

As an emerging type of Neural Networks (NNs), Transformers are used in many domains ranging from Natural Language Processing to Autonomous Driving. In this paper, we study the robustness problem of Transformers, a key characteristic as low robustness may cause safety concerns. Specifically, we focus on Sparsemax-based Transformers and reduce the finding of their maximum robustness to a Mixed Integer Quadratically Constrained Programming (MIQCP) problem. We also design two pre-processing heuristics that can be embedded in the MIQCP encoding and substantially accelerate its solving. We then conduct experiments using the application of Land Departure Warning to compare the robustness of Sparsemax-based Transformers against that of the more conventional Multi-Layer-Perceptron (MLP) NNs. To our surprise, Transformers are not necessarily more robust, leading to profound considerations in selecting appropriate NN architectures for safety-critical domain applications.
Paper Structure (17 sections, 2 theorems, 8 equations, 3 figures, 2 tables, 2 algorithms)

This paper contains 17 sections, 2 theorems, 8 equations, 3 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related Works
  3. Robustness Verification for Neural Networks
  4. Robustness Verification for Transformers
  5. Preliminaries
  6. Methodology
  7. Problem Formulation
  8. MIQCP Encoding
  9. Acceleration Heuristics
  10. Interval Analysis
  11. Progressive Verification with Norm-Space Region Partitioning
  12. Experimental Results and Discussions
  13. Lane Departure Warning
  14. Accuracy Benchmark
  15. Ablation Study
  16. ...and 2 more sections

Key Result

lemma thmcounterlemma

For all $k=1, \dots, D$, the smallest value for the Big-$M$ encoding in eq:M_pos is $\prescript{opt}{}M_k^{+} = 1$.

Figures (3)

  • Figure 1: The Sparsemax-based Transformer under exact robustness verification dosovitskiy2021imagevaswani2017attention.
  • Figure 2: Softmax vs. Sparsemax, given an input vector $\textbf{u}=[t, 0] \in \mathbb{R}^2$ (adapted from martins2016softmax).
  • Figure 3: Robustness of the Transformer and MLP on 60 random data points (better if larger). The dashed line highlights where they perform equally. There are 2 points on the dashed line, 26 in the lower triangle and 32 in the upper one. Since verifying the Transformer still takes much time, we report the lower bounds of the robustness values for the data points requiring more than one hour to verify. This means the points marked by "lower" can be further pushed to the right if the verifier is given more time. Nonetheless, this does not affect the overall observation as we ensure all such cases are points where the Transformer performs more robustly already.

Theorems & Definitions (4)

  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof