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.