Affine Vertex: Directional Softmax Bounds for Transformer Verification

Transformer robustness verification requires bounds on attention that remain useful as they propagate through the network. We introduce Affine Vertex, a method that tightens affine softmax bounds while preserving the slopes supplied by an existing verifier. We use exact ranges of weighted softmax outputs to construct a convex lower bound on the residual, the difference between the weighted softmax output and the fixed linear term. Each tangent gives a valid bound, even if the search for a stronger tangent is stopped early. We evaluate these bounds without forming matrices of pairwise interactions between attention scores. For an attention row with $K$ scores and a fixed number of optimization steps, this reduces the work from $O(K^2)$ to $O(K\log K)$ and the working storage from $O(K^2)$ to $O(K)$. On the official vision-transformer benchmark, Affine Vertex certifies 134 of 200 properties, compared with 127 for a matched control under the same computational budget. Experiments on independently trained models also show certification gains. Controlled comparisons demonstrate gains from convexification and further tangent optimization on selected properties. Independent interval checks validate sampled local bounds. These results show that refining softmax bounds can improve transformer verification, although tighter local bounds do not always yield additional certificates.