We study succinctness as a measure of the expressive power of transformers. Succinctness -- how compactly a formalism can describe a language relative to other formalisms -- is a classical notion in logic and automata theory. We prove that fixed-precision transformers are remarkably succinct: they can be exponentially more succinct than both linear temporal logic (LTL) and recurrent neural networks, and, by extension, state-space models, and doubly exponentially more succinct than finite automata. In other words, there exist families of languages describable by polynomial-size transformers whose smallest equivalent LTL formula or recurrent neural network is exponentially large, and whose smallest equivalent automaton is doubly exponentially large. We also establish matching upper bounds, showing that any fixed-precision transformer can be converted to an LTL formula with at most an exponential blow-up -- improving a prior doubly exponential translation. As a consequence of this succinctness, we show that basic verification problems for transformers, such as emptiness and equivalence, are provably intractable: specifically, EXPSPACE-complete.

翻译：我们研究了作为Transformer表达能力度量指标的简洁性。简洁性——一种形式化体系相比其他体系描述语言的紧凑程度——是逻辑学与自动机理论中的经典概念。我们证明固定精度Transformer具有显著的简洁性：它们可以比线性时序逻辑（LTL）和循环神经网络（以及扩展的状态空间模型）指数级地更简洁，且比有限自动机双指数级地更简洁。换言之，存在可由多项式规模的Transformer描述的语言族，其等效的最小LTL公式或循环神经网络规模呈指数级增长，而等效的最小自动机规模呈双指数级增长。我们还建立了匹配的上界，表明任意固定精度Transformer均可转换为规模最多指数膨胀的LTL公式——改进了此前双指数级转换的结果。基于这种简洁性，我们证明Transformer的基本验证问题（如空性检验与等价性检验）在本质上是难解的：具体而言，它们属于EXPSPACE完全问题。