Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization

Navid Rezazadeh, Arash Gholami Davoodi

Certified verification of transformer attention requires bounding the softmax function over interval constraints on the pre-softmax scores. Existing verifiers relax softmax ndepend…