# Provably Overwhelming Transformer Models with Designed Inputs

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 16 references that are in the map.
- First posted on arXiv 9 Feb 2025.

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

- [RoFormer: Enhanced Transformer with Rotary Position Embedding](https://mlsanity.com/paper/2104.09864/) (2021)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [On the Bottleneck of Graph Neural Networks and its Practical Implications](https://mlsanity.com/paper/2006.05205/) (2020)
- [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)
- [The Lipschitz Constant of Self-Attention](https://mlsanity.com/paper/2006.04710/) (2020)
- [Representational Strengths and Limitations of Transformers](https://mlsanity.com/paper/2306.02896/) (2023)
- [Transformers need glasses! Information over-squashing in language tasks](https://mlsanity.com/paper/2406.04267/) (2024)
- [Why are Sensitive Functions Hard for Transformers?](https://mlsanity.com/paper/2402.09963/) (2024)
- [On Limitations of the Transformer Architecture](https://mlsanity.com/paper/2402.08164/) (2024)
- [Compact Proofs of Model Performance via Mechanistic Interpretability](https://mlsanity.com/paper/2406.11779/) (2024)

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

- [Continuity and Isolation Lead to Doubts or Dilemmas in Large Language Models](https://mlsanity.com/paper/2505.10606/) (2025)

## Abstract (arXiv)

We develop an algorithm which, given a trained transformer model M as input, as well as a string of tokens s of length nfix and an integer nfree, can generate a mathematical proof that M is ``overwhelmed'' by s, in time and space widetildeO(nfix2 + nfree3). We say that M is ``overwhelmed'' by s when the output of the model evaluated on this string plus any additional string t, M(s + t), is completely insensitive to the value of the string t whenever length(t) ≤ nfree. Along the way, we prove a particularly strong worst-case form of ``over-squashing'', which we use to bound the model's behavior. Our technique uses computer-aided proofs to establish this type of operationally relevant guarantee about transformer models. We empirically test our algorithm on a single layer transformer complete with an attention head, layer-norm, MLP/ReLU layers, and RoPE positional encoding. We believe that this work is a stepping stone towards the difficult task of obtaining useful guarantees for trained transformer models.