# Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning

arXiv: https://arxiv.org/abs/2405.18548 · HTML: https://mlsanity.com/paper/2405.18548/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 34 references that are in the map.
- First posted on arXiv 28 May 2024.

## Builds on (most cited first, 20 of 20)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Explainability for Large Language Models: A Survey](https://mlsanity.com/paper/2309.01029/) (2023)
- [Theoretical Limitations of Self-Attention in Neural Sequence Models](https://mlsanity.com/paper/1906.06755/) (2019)
- [The Parallelism Tradeoff: Limitations of Log-Precision Transformers](https://mlsanity.com/paper/2207.00729/) (2022)
- [Thinking Like Transformers](https://mlsanity.com/paper/2106.06981/) (2021)
- [Understanding and Overcoming the Challenges of Efficient Transformer Quantization](https://mlsanity.com/paper/2109.12948/) (2021)
- [Saturated Transformers are Constant-Depth Threshold Circuits](https://mlsanity.com/paper/2106.16213/) (2021)
- [What Formal Languages Can Transformers Express? A Survey](https://mlsanity.com/paper/2311.00208/) (2023)
- [Position Information in Transformers: An Overview](https://mlsanity.com/paper/2102.11090/) (2021)
- [Formal Language Recognition by Hard Attention Transformers: Perspectives from Circuit Complexity](https://mlsanity.com/paper/2204.06618/) (2022)
- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [On the Computational Power of Transformers and its Implications in Sequence Modeling](https://mlsanity.com/paper/2006.09286/) (2020)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [Towards Robustness Against Natural Language Word Substitutions](https://mlsanity.com/paper/2107.13541/) (2021)
- [A Logic for Expressing Log-Precision Transformers](https://mlsanity.com/paper/2210.02671/) (2022)
- [Tighter Bounds on the Expressivity of Transformer Encoders](https://mlsanity.com/paper/2301.10743/) (2023)
- [Fundamental Limits in Formal Verification of Message-Passing Neural Networks](https://mlsanity.com/paper/2206.05070/) (2022)
- [Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations](https://mlsanity.com/paper/2105.13217/) (2021)

## Built on by (most cited first, 5 of 5)

- [The Counting Power of Transformers](https://mlsanity.com/paper/2505.11199/) (2025)
- [Transformers are Inherently Succinct](https://mlsanity.com/paper/2510.19315/) (2025)
- [Length Generalization Bounds for Transformers](https://mlsanity.com/paper/2603.02238/) (2026)
- [The Computational Complexity of Satisfiability in State Space Models](https://mlsanity.com/paper/2508.18162/) (2025)
- [Synthesis and Verification of Transformer Programs (Technical Report)](https://mlsanity.com/paper/2602.16473/) (2026)

## Abstract (arXiv)

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.