Transformers are Inherently Succinct
This work addresses the theoretical understanding of transformer models for researchers in machine learning and formal verification, providing foundational insights into their computational complexity.
The paper tackles the problem of measuring transformer expressiveness by introducing succinctness as a metric, proving that transformers can represent formal languages more compactly than finite automata or LTL formulas, and showing that verifying transformer properties is EXPSPACE-complete.
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).