Conic Certification of Transformer Attention

Masoud Ataei

cs.LGOct 31, 2026

Conic Certification of Transformer Attention

Authors: Masoud Ataei

Organizations: Department of Mathematical and Computational Sciences University of Toronto, Canada.

Abstract

Attention is the computational core of large language models, yet the verifiers that bound how far an attention head's output can move under input perturbations give no guarantee on how loose their bounds are. A weak certificate therefore cannot be told apart from a fragile model. We develop a conic programming theory of attention certification that supplies this guarantee. We prove that the difficulty lies not in the softmax but in the bilinear interaction of a varying query with the keys. This interaction makes certification NP-hard over boxes and inapproximable once the attention logits can move by a constant amount. A fixed query or listed token substitutions, by contrast, make the exact worst case efficiently computable. An exponential cone moment relaxation then certifies a head with an error bounded quadratically in the perturbation radius by computable quantities, an order that cannot be improved. We also show that relaxations that treat a network one operation at a time, linear bound propagation among them, pay on second-order terms a sum of per-operation maxima instead of one coupled maximum. Computational results on GPT-2 indicate that the theory carries over to a trained model. Against exact worst cases with the query fixed, the certificate attains the predicted second-order accuracy. It is tighter than linear bound propagation on every head, and the looseness of bound propagation tracks the predicted per-operation excess.

Figures & tables

symbol	meaning	order
$\Delta$	score width, $\max_{j}(s^{\mathrm{hi}}_{j}-s^{\mathrm{lo}}_{j})$	$\rho$
$w_{t}$	secant width, $\max_{j}\log(a^{\mathrm{hi}}_{j}/a^{\mathrm{lo}}_{j})\leq 2\Delta$	$\rho$
$\theta,\ \gamma$	dispersion of the midpoint pattern, margin of the dominant key	$1$
$a^{\mathrm{lo}}_{j},a^{\mathrm{hi}}_{j}$	attention intervals	$a^{\mathrm{hi}}_{j}-a^{\mathrm{lo}}_{j}=O(\rho)$
$S,\ D_{j}$	weighted secant slack, exact secant gap ( 16 )	$\rho^{2}$
$\operatorname{rad}_{c},\ \nu_{c}$	directional value radius and width	$1$ , $\rho$

Table 1: Controlling quantities of a head certification instance, all computed in closed form or by small convex programs before the certificate is solved, with their orders as

\rho\to 0

for balls of radius

\rho

setting	status	result
scores in a box, values fixed	exact, $O(n\log n)$	Remark 1
fixed query, boxes, zonotopes, point hulls	exact, polynomial	Thm. 7 (ii)
fixed query, ellipsoids	exact, polynomial	Thm. 7 (iii)
listed candidates, any query	exact, polynomial	Remark 3
varying query, two tokens in boxes	NP-hard	Thm. 5
same, score range in $[1.12,2]$	inapproximable within $\frac{1}{200}$ of the range	Thm. 6

Table 2: Complexity of certifying one attention head. “Exact” means that the worst case is computed to any prescribed accuracy with certified bounds.

Figure 1: Gap of the interval pattern bounds, the first-order certificate and the level-one relaxation with and without its interval diagonal (R4) against the perturbation radius, on random and ambiguous synthetic heads with ball token sets (

n=2

; medians and interquartile ranges over

10

seeds and all configurations).

method	random	ambiguous	margin	rank-one
interval pattern bounds	$1.02\,[1.00,1.06]$	$1.01\,[0.98,1.02]$	$1.04\,[0.96,1.09]$	$1.01\,[0.98,1.06]$
first order, $r^{\mathrm{pp}}$	$1.00\,[0.94,1.01]$	$0.99\,[0.98,0.99]$	$1.02\,[0.86,1.12]$	$1.00\,[0.96,1.03]$
level one, unit diagonal	$1.10\,[1.03,1.33]$	$1.35\,[1.24,1.54]$	$1.28\,[1.18,1.44]$	$1.14\,[1.03,1.41]$
level one, $\mathcal{R}^{\exp}_{1}$	$2.01\,[1.93,2.01]$	$2.00\,[1.99,2.01]$	$2.02\,[1.80,2.05]$	$2.00\,[2.00,2.02]$

Table 3: Slope of the certified gap in the perturbation radius on synthetic heads with ball token sets,

\rho\leq 0.1

(medians of per-series least-squares fits, with interquartile ranges).

$\rho_{\mathrm{rel}}$	units	median $w_{t}$	median relative gap		range-norm. gap	share of units
			certificate	first order	certificate	$\leq 1\%$	$\leq 10\%$
$0.001$	$720$	$0.24$	$0.0093$	$0.205$	$1.8\times 10^{-4}$	$54\%$	$100\%$
$0.002$	$720$	$0.48$	$0.019$	$0.213$	$7.3\times 10^{-4}$	$32\%$	$100\%$
$0.005$	$720$	$1.21$	$0.048$	$0.233$	$4.8\times 10^{-3}$	$16\%$	$88\%$
$0.01$	$2{,}160$	$2.65$	$0.135$	$0.322$	$0.030$	$7\%$	$37\%$
$0.02$	$2{,}160$	$5.24$	$0.212$	$0.349$	$0.097$	$7\%$	$24\%$

Table 4: Certificate accuracy on GPT-2 small by relative radius, with the relative and range-normalized gaps of Section 2 .

Figure 2: The order of accuracy on GPT-2 small (all heads, five prompts, query position four). Left: gaps of the two certificates and the output’s range of motion against the relative radius (medians and interquartile ranges over

720

units). Right: per-unit slopes on

\rho_{\mathrm{rel}}\leq 0.005

Figure 3: The gap of the certificate on GPT-2 small against the weighted secant slack $S$ (left) and against the value-weighted slack (right), coloured by the dispersion of the nominal pattern; $6{,}442$ units.

$\rho_{\mathrm{rel}}$	certificate		first order	share of units
	median [IQR]	max	median	within $1\%$
$0.002$	$0.0039\ [0.0012,0.0070]$	$0.020$	$0.172$	$89\%$
$0.005$	$0.010\ [0.003,0.018]$	$0.056$	$0.181$	$50\%$
$0.01$	$0.022\ [0.008,0.039]$	$0.13$	$0.193$	$32\%$
$0.02$	$0.048\ [0.018,0.084]$	$0.28$	$0.215$	$15\%$
slope	$2.04\ [2.01,2.07]$		$1.04$

Table 5: Exact relative gaps with a fixed query on GPT-2 small (all

144

heads, five prompts, query position four;

720

units per radius).

query	$\rho_{\mathrm{rel}}$	IBP	CROWN	$\alpha$ -CROWN	first	certifi-	ratio to cert.
					order	cate	CROWN	$\alpha$
fixed	$0.002$	$5.7$	$0.020$	$0.016$	$0.172$	$0.0039$	$4.4$	$3.9$
	$0.005$	$7.4$	$0.053$	$0.042$	$0.181$	$0.010$	$4.5$	$3.9$
	$0.01$	$11.2$	$0.113$	$0.090$	$0.193$	$0.022$	$4.5$	$3.8$
	$0.02$	$16.8$	$0.255$	$0.199$	$0.215$	$0.048$	$4.7$	$4.0$
varying	$0.001$	$7.2$	$0.083$	$0.072$	$0.205$	$0.0093$	$7.8$	$6.7$

Table 6: Relative gaps of linear bound propagation and of our certificates on the same GPT-2 units (all

144

heads, five prompts, query position four;

720

units per row; medians). The last two columns are median per-unit ratios to the gap of the certificate.

Figure 4: Relative gaps of CROWN,

\alpha

-CROWN, the first-order certificate and the certificate on the same GPT-2 units (

720

units per radius; medians and interquartile ranges).

Figure 5: Looseness of CROWN on the remainder of a GPT-2 block, its bound on

\max f

divided by the attained maximum, against the looseness

s_{\mathrm{op}}/s_{\mathrm{spec}}

predicted by Lemma 19 (

132

units).

Transformer Attention

Transformer attention lets models relate tokens by weighting information from other positions, enabling context-dependent sequence and multimodal processing.

See all 331 papers

Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization
May 8, 2026Navid Rezazadeh, Arash Gholami DavoodiSoftmax Attention Neural Network Verification
University of California, Irvine · Carnegie Mellon University
Certified Mechanistic Interpretability: Lifting Single-Input Findings to Bounded Neighbourhoods
Aug 17, 2026Zhen Zhang, Yanliang Huang, Peng Xie +2Mechanistic Interpretability Neural Network Verification
School of Computation, Information and Technology Technical University of Munich, Germany
Exact Attention Sensitivity and the Geometry of Transformer Stability
Feb 21, 2026Seyed Morteza EmadiTransformer Attention Softmax Attention
UNC-Chapel Hill, Kenan-Flagler Business School Chapel Hill, NC, USA

May 8, 2026J/K move · Enter open · S save

Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization

Navid Rezazadeh, Arash Gholami Davoodi

University of California, Irvine · Carnegie Mellon University

Softmax Attention Neural Network Verification Certified Robustness

Open paper AskPDF arXiv

Certified verification of transformer attention requires bounding the softmax function over interval constraints on the pre-softmax scores. Existing verifiers relax softmax ndependently of the downstream objective, leaving avoidable slack. We prove that the exact optimum of this score-box problem is attained at a vertex of the constraint box, and establish a threshold structure theorem showing that, after sorting the objective coefficients, the optimum lies among only linearly many candidates, yielding the Vertex-Softmax primitive with log-linear complexity in the sequence length. We further prove a formal optimality result showing that Vertex-Softmax is the tightest sound bound obtainable from score intervals alone, characterizing precisely what additional structure (score correlations, score-value coupling) is needed for further improvement. Integrated into a CROWN Convex Relaxation based Optimization for Worst-case Neurons)-style verifier with a formal soundness guarantee, Vertex-Softmax significantly improves certified rates and substantially tightens lower bounds across MNIST, Fashion-MNIST, and CIFAR-10 attention models, while consistently matching or outperforming alpha-CROWN and branch-and-bound baselines at a fraction of their cost.

Abstract

Transformer Attention

Explore similar work

Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization

Certified Mechanistic Interpretability: Lifting Single-Input Findings to Bounded Neighbourhoods

Exact Attention Sensitivity and the Geometry of Transformer Stability