Formally Verified Autoresearch for Analyzing the Expressivity of Multi-Head Attention

Karthik Viswanathan; Plamen Dimitrov; Stefano Rocca; Sarayu Sirikonda

cs.CCOct 18, 2026

Formally Verified Autoresearch for Analyzing the Expressivity of Multi-Head Attention

Authors: Karthik Viswanathan, Plamen Dimitrov, Stefano Rocca, Sarayu Sirikonda

Organizations: Verified Mechanisms · MATS Research · University of California, Berkeley

Abstract

Multi-head attention is a central component of the transformer architecture, yet how its expressivity depends on the number of heads remains poorly understood. We study a one-layer, attention-only transformer with additive positional embeddings and define the head complexity $H^\ast(f)$ of a Boolean function $f$ as the minimum number of attention heads required to represent it. We derive an exact linear-fractional normal form for head complexity, prove a general threshold-degree lower bound, and give an explicit ten-bit function for which this bound is strict. For symmetric Boolean functions, we independently show that head complexity equals the number of times the function changes value between consecutive Hamming-weight levels, even when positional embeddings are allowed. This agrees with the concurrent characterization of Hsu and Xu (arXiv:2608.04243) in a model without positional embeddings. The symmetric lower bound combines our general threshold-degree bound with the classical result of Aspnes et al. (1994). These results were discovered and formalized by a frontier model through conjecture generation, theorem proving, and machine verification, while human researchers asked the high-level questions and reviewed the generated theorems. We make the Lean formalization and research traces publicly available to support agent-assisted theorem proving and formal verification in mechanistic interpretability. This work provides a proof of concept for using the capabilities of frontier models, grounded by formal verification, to develop an understanding of transformer architectures.

Figures & tables

Panel of Figure 1 — Figure 1: One-layer attention-only model. The input consists of $n$ bit tokens followed by a dedicated query token $q$ , which also serves as the readout position. Each position is represented by the sum of a token embedding and a positional embedding, and the resulting embedded sequence is shared by all $H$ heads. The heads update all positions in parallel, but the linear readout uses only position $q$ . At this position, the head outputs are added to the residual $\mathbf{u}_{q}$ , yielding $\mathbf{h}_{q}(\mathbf{x})$ . Thus, $f$ is represented exactly when the inputs labelled $0$ and $1$ are linearly separable at the readout position $\mathbf{h}_{q}(\mathbf{x})$ , and $H^{\ast}(f)$ is the minimum $H$ for which this occurs.

Command category	Calls
Python invocations	153
sed inspections	70
rg searches	40
Runs of empirical checks	24
Numbered file inspections	17
Git queries	14

Table 1: Recorded shell activity during the theorem-generation run.

Measure	Summary
Messages	intermediate assistant messages and one final answer. The context was compacted four times.
Tool use	The log records 949 tool calls and 960 operations within those calls. The latter comprise 387 shell commands, 307 file edits, 205 continuations of shell sessions, 55 goal checks, and six goal or plan updates.
Token use	The platform reported about 142.4 million cumulative input tokens, of which 140.2 million were cached, and 0.64 million output tokens, including 0.32 million reasoning tokens.
Research process	The agent registered thirteen approach families and used no public web search, external connector, or delegated model call.

Table 2: Summary of the autonomous theorem-generation run. Token counts are taken from the last record before the final answer and therefore exclude that turn.

Goal	Approach	Outcome
Reformulate head complexity	Replace the full matrix parameterization with a scalar description of each head’s contribution.	Derived Theorem 1 .
Prove upper bounds	Construct representations for functions determined by weighted sums and for symmetric functions.	Derived Theorems 4 and 5 , plus bounds not included in the paper.
Prove lower bounds	Compare head complexity with threshold degree and study functions that require more heads.	Derived Theorem 2 and additional lower-bound arguments.
Evaluate candidate approaches	Check proposed identities and constructions on finite instances.	Rejected approaches that failed finite checks and set aside those that still required an unproved lemma.

Table 3: High-level summary of the proof families explored during the run.

Transformer Expressivity

Transformer expressivity studies which functions and computations attention-based models can represent, and how depth, precision, and context shape those limits.

See all 54 papers

The Head Complexity of Boolean Functions in Single-Layer Attention
Sep 3, 2026Rajmohan Rajaraman, Ravi Sundaram, Amanuel TesfayeSelf-Attention Attention Mechanisms
Northeastern University.
On the Computational Hardness of Transformers
Mar 11, 2026Barna Saha, Yinzhan Xu, Christopher Ye +1Transformer Attention Mechanisms
University of California San Diego · Columbia University
Expressivity of Transformers: A Tropical Geometry Perspective
Apr 16, 2026Ye Su, Yong LiuTransformer Expressivity Transformer
Shenzhen Institutes of Advanced Technology, Chinese Academy of Sciences, Shenzhen 518055, China · University of Chinese Academy of Sciences, Beijing 101407, China · Gaoling School of Artificial Intelligence, Renmin University of China, Beijing 100872, China

Sep 3, 2026J/K move · Enter open · S save

The Head Complexity of Boolean Functions in Single-Layer Attention

Rajmohan Rajaraman, Ravi Sundaram, Amanuel Tesfaye

Northeastern University.

Self-Attention Attention Mechanisms Multi-Head Attention

Open paper AskPDF arXiv

What can a single layer of self-attention compute? We study head complexity: the minimum number of attention heads required to compute a function in a one-layer attention-only model. We establish an exact hierarchy under this measure:

k

heads compute

k

-bit parity but cannot compute

(k+1)

-bit parity. The lower bound is unconditional in the two resources a transformer might otherwise exploit; it holds at unbounded embedding dimension and unbounded numerical precision. The proof rests on an alternating-sum obstruction: after clearing the softmax denominators, every monomial in the resulting decision polynomial omits at least one of the

k+1

input bits, forcing its correlation with parity to vanish. The same obstruction yields lower bounds for related tasks, including the well-studied multi-hop induction-head task. We also establish compactness bounds for embedding dimension and numerical precision. Specifically, a compactness theorem shows that any function computable at all can be computed with embedding dimension and precision bounded by the discrete data of the task, namely, head count, alphabet size, and length. Thus, potentially unbounded dimension or precision provably cannot substitute for heads. Finally, we derive nearly matching universal bounds for general binary functions:

2^n

heads suffice to compute every

n

-bit binary function, with one head per monomial in its multilinear expansion, while a counting argument shows almost all such functions require

Ω(2^n/n^2)

heads. This lower bound matches the upper bound to within a

\operatorname{poly}(n)

factor, even when dimension and precision are unbounded. Together, these results characterize head requirements for Boolean computation in this model.

Abstract

Transformer Expressivity

Explore similar work

The Head Complexity of Boolean Functions in Single-Layer Attention

On the Computational Hardness of Transformers

Expressivity of Transformers: A Tropical Geometry Perspective