Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning

Marco Sälzer, Eric Alsmann, Martin Lange

TL;DR

The paper investigates the satisfiability problem for transformer encoders ($\textsc{trSat}$), revealing undecidability for natural TE classes and exploring decidable regimes. It shows that $\textsc{trSat}$ is undecidable for encoder-only TE in expressiveness-lean classes and identifies two main decidability avenues: bounding input length and employing fixed-width (quantized) arithmetic. The authors provide precise complexity bounds, including $\textsc{btrSat}$ being $\text{NP}$ (unary) or $\text{NEXPTIME}$ (binary) and $\textsc{trSat}$ under fixed-width periodic embeddings falling in $\text{NEXPTIME}$ with corresponding hardness results for broader fixed-width settings. These findings delineate theoretical limits for automatic, sound, and complete formal reasoning about transformers and point to future work on softmax, embedding interactions, and practical fixed-width refinements.

Abstract

We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or interpretation, collectively referred to as formal reasoning. We find that trSAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where trSAT is decidable and establish corresponding complexity bounds. Beyond trivial cases, we find that quantized TE, those restricted by fixed-width arithmetic, lead to the decidability of trSAT due to their limited attention capabilities. However, the problem remains difficult, as we establish scenarios where trSAT is NEXPTIME-hard and others where it is solvable in NEXPTIME for quantized TE. To complement our complexity results, we place our findings and their implications in the broader context of formal reasoning.

Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning

TL;DR

The paper investigates the satisfiability problem for transformer encoders (), revealing undecidability for natural TE classes and exploring decidable regimes. It shows that is undecidable for encoder-only TE in expressiveness-lean classes and identifies two main decidability avenues: bounding input length and employing fixed-width (quantized) arithmetic. The authors provide precise complexity bounds, including being (unary) or (binary) and under fixed-width periodic embeddings falling in with corresponding hardness results for broader fixed-width settings. These findings delineate theoretical limits for automatic, sound, and complete formal reasoning about transformers and point to future work on softmax, embedding interactions, and practical fixed-width refinements.

Abstract

We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or interpretation, collectively referred to as formal reasoning. We find that trSAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where trSAT is decidable and establish corresponding complexity bounds. Beyond trivial cases, we find that quantized TE, those restricted by fixed-width arithmetic, lead to the decidability of trSAT due to their limited attention capabilities. However, the problem remains difficult, as we establish scenarios where trSAT is NEXPTIME-hard and others where it is solvable in NEXPTIME for quantized TE. To complement our complexity results, we place our findings and their implications in the broader context of formal reasoning.
Paper Structure (14 sections, 13 theorems, 1 equation, 3 figures)

This paper contains 14 sections, 13 theorems, 1 equation, 3 figures.

Table of Contents

  1. Introduction
  2. Related work.
  3. Fundamentals
  4. Mathematical basics.
  5. Transformer encoders (TE).
  6. Fixed-width arithmetics.
  7. Overview of complexity results and connection to formal reasoning
  8. Transformer encoder satisfiability is generally undecidable
  9. How to make transformer encoder satisfiability decidable
  10. Summary, limitations and outlook
  11. Tiling Problems
  12. Proofs of Section \ref{['sec:undec']}
  13. Feed-Forward Neural Network
  14. Proofs of Section \ref{['sec:dec']}

Key Result

Lemma 1

Let $\mathcal{S}$ be a tiling system with tiles $S = \{a_1, \dotsc, a_k\}$. There is an embedding function $\mathit{emb}$ and there are encoder layers $l_1$ and $l_2$ definable in $\mathcal{T}_\mathit{udec}$ such that for each word $w = t_{0,0} t_{1,0} t_{1,1} t_{2,0} \dotsb t_{m,n} \in S^+$ holds t

Figures (3)

  • Figure 1: Schematic depiction of an TE $T$ with embedding $\mathit{emb}$ and $k$ (encoder) layers $l_i$. Each layer $l_i$ consists of some $h_i$ attention heads $\mathit{att}_{i,j}$, whose output is combined by $\mathit{comb}_i$. Additionally, for some layer $l_i$, the computational flow of $T$ regarding input position $m$ is schematically depicted in detail.
  • Figure 2: Schematic overview of the computability and complexity results, established in this work. The classes of TE are described in the pretext of the respective theorem. Note that $\mathcal{T}$ refers to an arbitrary class of (computable) TE. The small subset in the classes NP and NEXPTIME refers to the complete problems. The NEXPTIME-hardness result of $\textsc{trSat}[\mathcal{T}^\textsc{fix}]$ is not visualized
  • Figure 3: Schematic depiction of the expressive capabilities of TE from $\mathcal{T}_\mathit{udec}$ in context of the $\textsc{OTWP}^*$ proven in Lemma \ref{['sec:undec;lem:decode']} and Lemma \ref{['sec:undec;lem:lin']}.

Theorems & Definitions (31)

  • Lemma 1
  • Lemma 2
  • Theorem 1
  • proof : Proof Sketch
  • Theorem 2
  • proof : Proof sketch
  • Theorem 3
  • proof : Proof Sketch
  • Lemma 3
  • proof : Proof Sketch
  • ...and 21 more