# Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization

arXiv: https://arxiv.org/abs/2605.10974 · HTML: https://mlsanity.com/paper/2605.10974/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 20 references that are in the map.
- First posted on arXiv 8 May 2026.

## Builds on (most cited first, 13 of 13)

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Certifying LLM Safety against Adversarial Prompting](https://mlsanity.com/paper/2309.02705/) (2023)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents](https://mlsanity.com/paper/2503.18666/) (2025)
- [SafetyBench: Evaluating the Safety of Large Language Models](https://mlsanity.com/paper/2309.07045/) (2023)
- [Large language model validity via enhanced conformal prediction methods](https://mlsanity.com/paper/2406.09714/) (2024)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [Neural Network Verification with Branch-and-Bound for General Nonlinearities](https://mlsanity.com/paper/2405.21063/) (2024)
- [ProbGuard: Proactive Runtime Monitoring for LLM Agent Safety via Probabilistic Prediction](https://mlsanity.com/paper/2508.00500/) (2025)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [RvLLM: LLM Runtime Verification with Domain Knowledge](https://mlsanity.com/paper/2505.18585/) (2025)
- [Certifying Counterfactual Bias in LLMs](https://mlsanity.com/paper/2405.18780/) (2024)
- [Are Transformers More Robust? Towards Exact Robustness Verification for Transformers](https://mlsanity.com/paper/2202.03932/) (2022)

## Built on by (most cited first, 2 of 2)

- [Truthful AI Advisors: A Pre-Specified Benchmark for Large Language Model Honesty Under Preference Misalignment](https://mlsanity.com/paper/2606.01456/) (2026)
- [Same Game, Different Story: A Minimal Conservative Strategic Robustness Benchmark for Large Language Model Agents](https://mlsanity.com/paper/2607.19670/) (2026)

## Abstract (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.