Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Transformers are Inherently Succinct

Pascal Bergsträßer, Ryan Cotterell, Anthony W. Lin

TL;DR

The paper reframes transformer expressiveness through succinctness, showing that fixed-precision UHATs can describe languages far more compactly than classical formalisms. It proves that verifying properties of UHATs is EXPSPACE-complete, and establishes tight gaps in succinctness: transformers are exponentially more succinct than LTL and RNNs and doubly exponentially more succinct than finite automata, with a constructive translation from UHATs to exponential-size LTL formulas. Central to the results is the ability to encode extremely large counters up to $2^{2^n}$ using attention, enabling non-emptiness proofs and tiling-based reductions that underpin the complexity bounds. The work connects Boolean RASP and UHATs, leverages fixed-precision modeling, and situates the findings relative to existing verification and logic translations, highlighting substantial implications for theoretical understanding and practical verification of transformer-based systems.

Abstract

We propose succinctness as a measure of the expressive power of a transformer in describing a concept. To this end, we prove that transformers are highly expressive in that they can represent formal languages substantially more succinctly than standard representations of formal languages like finite automata and Linear Temporal Logic (LTL) formulas. As a by-product of this expressivity, we show that verifying properties of transformers is provably intractable (i.e. EXPSPACE-complete).

Transformers are Inherently Succinct

TL;DR

The paper reframes transformer expressiveness through succinctness, showing that fixed-precision UHATs can describe languages far more compactly than classical formalisms. It proves that verifying properties of UHATs is EXPSPACE-complete, and establishes tight gaps in succinctness: transformers are exponentially more succinct than LTL and RNNs and doubly exponentially more succinct than finite automata, with a constructive translation from UHATs to exponential-size LTL formulas. Central to the results is the ability to encode extremely large counters up to using attention, enabling non-emptiness proofs and tiling-based reductions that underpin the complexity bounds. The work connects Boolean RASP and UHATs, leverages fixed-precision modeling, and situates the findings relative to existing verification and logic translations, highlighting substantial implications for theoretical understanding and practical verification of transformer-based systems.

Abstract

We propose succinctness as a measure of the expressive power of a transformer in describing a concept. To this end, we prove that transformers are highly expressive in that they can represent formal languages substantially more succinctly than standard representations of formal languages like finite automata and Linear Temporal Logic (LTL) formulas. As a by-product of this expressivity, we show that verifying properties of transformers is provably intractable (i.e. EXPSPACE-complete).
Paper Structure (25 sections, 15 theorems, 28 equations)

This paper contains 25 sections, 15 theorems, 28 equations.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Organization.
  4. Preliminaries
  5. Linear Temporal Logic
  6. Masked unique hard-attention transformers
  7. Attention layer.
  8. ReLU layer.
  9. Transformer.
  10. Languages accepted by UHATs.
  11. Boolean RASP
  12. Position-wise operation.
  13. Attention operation.
  14. Recurrent Neural Networks (RNN)
  15. Size measures and succinctness
  16. ...and 10 more sections

Key Result

Proposition 3

An RNN $g: (\mathbb{R}^d \times \Sigma) \to \mathbb{R}^d$ with fixed precision $k$ can be represented by a finite automaton with $2^{kd}$ many states.

Theorems & Definitions (23)

  • Example 1
  • Remark 2
  • Proposition 3
  • Example 4
  • Theorem 5
  • Proposition 6
  • Proposition 7
  • Proposition 8
  • proof : Proof sketch
  • Lemma 9
  • ...and 13 more