Provably Overwhelming Transformer Models with Designed Inputs

Fuente: arXiv
Enregistré dans:
Détails bibliographiques
Auteurs principaux: Stambler, Lev, Nezhadi, Seyed Sajjad, Coudron, Matthew
Format: Preprint
Publié: 2025
Sujets:
Accès en ligne:
Tags: Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
_version_ 1866915302896304128
author Stambler, Lev
Nezhadi, Seyed Sajjad
Coudron, Matthew
author_facet Stambler, Lev
Nezhadi, Seyed Sajjad
Coudron, Matthew
contents We develop an algorithm which, given a trained transformer model $\mathcal{M}$ as input, as well as a string of tokens $s$ of length $n_{fix}$ and an integer $n_{free}$, can generate a mathematical proof that $\mathcal{M}$ is ``overwhelmed'' by $s$, in time and space $\widetilde{O}(n_{fix}^2 + n_{free}^3)$. We say that $\mathcal{M}$ is ``overwhelmed'' by $s$ when the output of the model evaluated on this string plus any additional string $t$, $\mathcal{M}(s + t)$, is completely insensitive to the value of the string $t$ whenever length($t$) $\leq n_{free}$. 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.
format Preprint
id arxiv_https___arxiv_org_abs_2502_06038
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Provably Overwhelming Transformer Models with Designed Inputs
Stambler, Lev
Nezhadi, Seyed Sajjad
Coudron, Matthew
Machine Learning
Artificial Intelligence
Computational Complexity
We develop an algorithm which, given a trained transformer model $\mathcal{M}$ as input, as well as a string of tokens $s$ of length $n_{fix}$ and an integer $n_{free}$, can generate a mathematical proof that $\mathcal{M}$ is ``overwhelmed'' by $s$, in time and space $\widetilde{O}(n_{fix}^2 + n_{free}^3)$. We say that $\mathcal{M}$ is ``overwhelmed'' by $s$ when the output of the model evaluated on this string plus any additional string $t$, $\mathcal{M}(s + t)$, is completely insensitive to the value of the string $t$ whenever length($t$) $\leq n_{free}$. 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.
title Provably Overwhelming Transformer Models with Designed Inputs
topic Machine Learning
Artificial Intelligence
Computational Complexity
url https://arxiv.org/abs/2502.06038