Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization

Authors: Navid Rezazadeh, Arash Gholami Davoodi

arXiv · PDF

Summary

The authors develop Vertex-Softmax, a method to exactly optimize the softmax function over interval constraints when verifying transformer models — critical for proving robustness guarantees. Existing verifiers approximate softmax independently of the downstream objective, leaving slack. Vertex-Softmax proves the exact optimum always occurs at a vertex (corner) of the constraint box and lies among only linearly many candidates, giving log-linear complexity. They further prove this is the tightest possible bound obtainable from score intervals alone, formally characterizing what additional structure (score correlations, score-value coupling) would be needed for further improvement.

Main takeaways:

• Transformer verification requires bounding softmax over intervals on pre-softmax scores; existing verifiers relax softmax independently of the objective, leaving avoidable slack.
• Vertex-Softmax proves the exact optimum lies at a vertex of the constraint box and among linearly many sorted candidates, enabling log-linear-time exact optimization.
• Formally optimal: provably the tightest sound bound obtainable from score intervals alone, with a characterization of what additional structure is needed for further improvement.
• Integrated into a CROWN-style verifier with soundness guarantees, significantly improving certified rates and tightening lower bounds on MNIST, Fashion-MNIST, and CIFAR-10 attention models.
• Matches or outperforms alpha-CROWN and branch-and-bound baselines at a fraction of their cost.

Relevance

Not directly related to my persona/midtraining work — this is about formal verification and robustness certification for transformers, which is orthogonal to behavioral installation, though understanding how attention mechanisms work under constraints could in principle inform how persona-switching or marker-based behaviors propagate through attention layers.

Abstract

arXiv:2605.10974v1 Announce Type: new Abstract: 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.