Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization

# Tight Transformer Verification via Exact Softmax OptimizationCode: https://github.com/navidrezazad/VertexSoftmax.
Source: [https://arxiv.org/html/2605.10974](https://arxiv.org/html/2605.10974)
Navid Rezazadeh &Arash Gholami Davoodi33footnotemark:3 University of California, Irvine,nrezazad@uci\.edu\.‡Carnegie Mellon University,agholami@andrew\.cmu\.edu\.

###### Abstract

Certified verification of transformer attention requires bounding the softmax function over interval constraints on the pre\-softmax scores\. Existing verifiers relax softmax independently 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\.

## 1Introduction

Certified verifiers for feedforward networks have matured into practical tools\. Transformers remain stubbornly harder—and softmax attention is the reason\. The normalized exponential couples all tokens, and existing verifiers must relax it at a cost in certificate tightness: every input where the relaxation is too loose is an input the verifier cannot certify\. Closing that gap, making attention verification tighter without sacrificing scalability, is the motivation for this work\.

Table 1:Comparison of verification methods at the softmax interface\. The timing column gives representative wall\-clock seconds per trial from selected small\-attention experiments in Section[5](https://arxiv.org/html/2605.10974#S5); it is not the full\-block hybrid runtime, which is broken down separately in Appendix Table[11](https://arxiv.org/html/2605.10974#A5.T11)\.†Before interval abstraction only\.‡Through optimized graph relaxations\.§Not as a local score\-box primitive; gains correlations through domain splitting\.

CROWN/LiRPA\-style verifiers propagate affine bounds through neural networks at scale\(Zhanget al\.,[2018](https://arxiv.org/html/2605.10974#bib.bib1); Xuet al\.,[2020](https://arxiv.org/html/2605.10974#bib.bib2)\), but attention introduces a normalized exponential map

a​\(s\)=softmax⁡\(s\),aj​\(s\)=exp⁡\(sj\)∑r=1Kexp⁡\(sr\)\.a\(s\)=\\operatorname\{softmax\}\(s\),\\qquad a\_\{j\}\(s\)=\\frac\{\\exp\(s\_\{j\}\)\}\{\\sum\_\{r=1\}^\{K\}\\exp\(s\_\{r\}\)\}\.\(1\)After a score\-bounding pass, a verifier often knows only an independent score box

ℬ=∏j=1K\[ℓj,uj\]\\mathcal\{B\}=\\prod\_\{j=1\}^\{K\}\[\\ell\_\{j\},u\_\{j\}\]\(2\)and a directionc∈ℝKc\\in\\mathbb\{R\}^\{K\}induced by value\-side bounds or by a downstream margin\. The verifier’s task at each attention row thus reduces to optimizing a linear objective over softmax outputs, constrained only by these independent score intervals:

mins∈ℬ⁡c⊤​softmax⁡\(s\)\.\\min\_\{s\\in\\mathcal\{B\}\}c^\{\\top\}\\operatorname\{softmax\}\(s\)\.\(3\)Generic softmax relaxations first relax the vector maps↦softmax⁡\(s\)s\\mapsto\\operatorname\{softmax\}\(s\)and only then contract withcc\. We instead solve the direction\-dependent scalar problem directly\.

The result is exact and small\. The minimum over the continuous score box is attained at a vertex of the constraint box\. The intuition is that an optimizer trading off mass against cost can always push each coordinate to an endpoint without increasing the objective\. After sortingcc, the optimal vertex puts upper endpoints on themmsmallest coefficients and lower endpoints on the rest, for some thresholdm∈\{0,…,K\}m\\in\\\{0,\\ldots,K\\\}\. A naïve search examines2K2^\{K\}vertices\. We show that sorting the objective coefficients collapses this to exactlyK\+1K\+1candidates—one sort and one prefix\-sum sweep\. We call this primitive*Vertex\-Softmax*\.

This also identifies the information surface of the score\-box interface\. Any sound lower\-bound procedure whose inputs are only\(c,ℓ,u\)\(c,\\ell,u\)cannot return a value larger than the exact minimum in \([3](https://arxiv.org/html/2605.10974#S1.E3)\)\. Tighter certificates must use information discarded before this interface, such as score correlations, score–value coupling, or a reachable score set smaller than the independent box\.

#### Contributions\.

- •We prove vertex exactness andK\+1K\+1threshold exactness for \([3](https://arxiv.org/html/2605.10974#S1.E3)\), giving anO​\(K​log⁡K\)O\(K\\log K\)exact solver for the weighted\-softmax box problem\.
- •We derive a score\-box information optimality statement: Vertex\-Softmax is the tightest sound bound obtainable from independent score intervals alone\.
- •We integrate the primitive into Vertex\-CROWN, a sound CROWN\-style attention verifier, and show large certified\-rate improvements on MNIST and Fashion\-MNIST patch\-attention models, competitive or improved certificates against alpha\-CROWN and branch\-and\-bound baselines on selected attention blocks, and full\-block gains on attention–residual–MLP models with a CROWN\-suffix hybrid\.

#### Positioning\.

Scalable neural\-network verifiers based on affine bound propagation, including CROWN, auto\_LiRPA, andα,β\\alpha,\\beta\-CROWN\(Zhanget al\.,[2018](https://arxiv.org/html/2605.10974#bib.bib1); Xuet al\.,[2020](https://arxiv.org/html/2605.10974#bib.bib2); Wanget al\.,[2021](https://arxiv.org/html/2605.10974#bib.bib3)\), have been extended to transformer attention layers\(Shiet al\.,[2020](https://arxiv.org/html/2605.10974#bib.bib4); Bonaertet al\.,[2021](https://arxiv.org/html/2605.10974#bib.bib5)\)\. Within this line, recent softmax\-focused relaxations tighten the vector\-valued softmax bounds used inside the verifier\. The convex bounds ofWeiet al\.\([2023](https://arxiv.org/html/2605.10974#bib.bib7)\)and the GaLileo relaxation ofZhanget al\.\([2024](https://arxiv.org/html/2605.10974#bib.bib8)\)are representative; both relax softmax rather than solve the direction\-dependent score\-box objective exactly\.

On the other end of the precision–cost spectrum, exact methods such as MILP, MIQCP, SMT, and nonlinear branch\-and\-bound\(Tjenget al\.,[2019](https://arxiv.org/html/2605.10974#bib.bib9); Katzet al\.,[2019](https://arxiv.org/html/2605.10974#bib.bib10); Shiet al\.,[2025](https://arxiv.org/html/2605.10974#bib.bib12)\)can give complete answers on small instances but do not scale to dense softmax attention\. Our contribution sits between these extremes: Vertex\-Softmax solves the recurring score\-box subproblem exactly inO​\(K​log⁡K\)O\(K\\log K\)time, complementing both relaxation\-based and search\-based approaches\. A broader discussion of related work, including LLM\-scale statistical and runtime\-monitoring approaches, is in Appendix[A](https://arxiv.org/html/2605.10974#A1)\. The exactness claim is local to the score\-box interface; remaining sources of verifier looseness are discussed in Section[6](https://arxiv.org/html/2605.10974#S6)\. Table[1](https://arxiv.org/html/2605.10974#S1.T1)summarizes the landscape\.

## 2Problem Setup

We now formalize the interface between a CROWN\-style score\-bounding pass and the softmax layer, and define the scalar optimization problem that Vertex\-Softmax solves\. Table[2](https://arxiv.org/html/2605.10974#S2.T2)collects the key notation\.

Table 2:Key notation used throughout the paper\.Let𝒳\\mathcal\{X\}be an input box and letm:𝒳→ℝm:\\mathcal\{X\}\\to\\mathbb\{R\}be a scalar margin\. Certification means provingm​\(x\)≥0m\(x\)\\geq 0for allx∈𝒳x\\in\\mathcal\{X\}, usually by computing a sound lower bound onminx∈𝒳⁡m​\(x\)\\min\_\{x\\in\\mathcal\{X\}\}m\(x\)\. For one attention row, write

si​\(x\)∈ℝK,ai​\(x\)=softmax⁡\(si​\(x\)\)\.s\_\{i\}\(x\)\\in\\mathbb\{R\}^\{K\},\\qquad a\_\{i\}\(x\)=\\operatorname\{softmax\}\(s\_\{i\}\(x\)\)\.\(4\)When a backward bound pass reaches this row, the downstream contribution at this interface is summarized by a fixed vectorci∈ℝKc\_\{i\}\\in\\mathbb\{R\}^\{K\}, so the row certificate needs a lower bound onci⊤​softmax⁡\(si​\(x\)\)c\_\{i\}^\{\\top\}\\operatorname\{softmax\}\(s\_\{i\}\(x\)\)\.

The same pass supplies sound elementwise score bounds

ℓi​j≤si​j​\(x\)≤ui​j,j=1,…,K,x∈𝒳,\\ell\_\{ij\}\\leq s\_\{ij\}\(x\)\\leq u\_\{ij\},\\qquad j=1,\\ldots,K,\\quad x\\in\\mathcal\{X\},\(5\)forming a product intervalℬi=∏j=1K\[ℓi​j,ui​j\]\\mathcal\{B\}\_\{i\}=\\prod\_\{j=1\}^\{K\}\[\\ell\_\{ij\},u\_\{ij\}\]\. Dropping the row index, define

Fc​\(s\)=c⊤​softmax⁡\(s\)=∑j=1Kcj​esj∑j=1Kesj,Lbox​\(c,ℓ,u\)=mins∈ℬ⁡Fc​\(s\)\.F\_\{c\}\(s\)=c^\{\\top\}\\operatorname\{softmax\}\(s\)=\\frac\{\\sum\_\{j=1\}^\{K\}c\_\{j\}e^\{s\_\{j\}\}\}\{\\sum\_\{j=1\}^\{K\}e^\{s\_\{j\}\}\},\\qquad L\_\{\\mathrm\{box\}\}\(c,\\ell,u\)=\\min\_\{s\\in\\mathcal\{B\}\}F\_\{c\}\(s\)\.\(6\)The matching upper bound isUbox​\(c,ℓ,u\)=−Lbox​\(−c,ℓ,u\)U\_\{\\mathrm\{box\}\}\(c,\\ell,u\)=\-L\_\{\\mathrm\{box\}\}\(\-c,\\ell,u\), so we state lower bounds only\. Throughout,K≥1K\\geq 1, intervals are finite, degenerate intervals are allowed, andccis fixed with respect toss\. Equation \([6](https://arxiv.org/html/2605.10974#S2.E6)\) is exact for the product box, not necessarily for the reachable set\{s​\(x\):x∈𝒳\}⊆ℬ\\\{s\(x\):x\\in\\mathcal\{X\}\\\}\\subseteq\\mathcal\{B\}\.

## 3Exact Score\-Box Softmax Optimization

Setyj=esjy\_\{j\}=e^\{s\_\{j\}\},Lj=eℓjL\_\{j\}=e^\{\\ell\_\{j\}\}, andUj=eujU\_\{j\}=e^\{u\_\{j\}\}\. The maps↦ys\\mapsto ysendsℬ\\mathcal\{B\}bijectively toℬy=∏j=1K\[Lj,Uj\]\\mathcal\{B\}\_\{y\}=\\prod\_\{j=1\}^\{K\}\[L\_\{j\},U\_\{j\}\], and

Fc​\(s\)=R​\(y\)≔∑j=1Kcj​yj∑j=1Kyj\.F\_\{c\}\(s\)=R\(y\)\\coloneqq\\frac\{\\sum\_\{j=1\}^\{K\}c\_\{j\}y\_\{j\}\}\{\\sum\_\{j=1\}^\{K\}y\_\{j\}\}\.\(7\)Thus the softmax problem is a bounded linear\-fractional optimization problem over a positive box\. The vertex property of linear\-fractional programs over boxes is classical\(Dinkelbach,[1967](https://arxiv.org/html/2605.10974#bib.bib21)\); the contribution here is theK\+1K\+1threshold reduction and its integration into attention verification\. Full proofs are in Appendix[B](https://arxiv.org/html/2605.10974#A2)\.

###### Theorem 3\.1\(Score\-box vertex exactness\)\.

LetK≥1K\\geq 1,c∈ℝKc\\in\\mathbb\{R\}^\{K\}, and finite intervalsℓj≤uj\\ell\_\{j\}\\leq u\_\{j\}\. Then

mins∈ℬ⁡Fc​\(s\)=minv∈Vert⁡\(ℬ\)⁡Fc​\(v\),\\min\_\{s\\in\\mathcal\{B\}\}F\_\{c\}\(s\)=\\min\_\{v\\in\\operatorname\{Vert\}\(\\mathcal\{B\}\)\}F\_\{c\}\(v\),\(8\)and the analogous equality holds for the maximum\.

The one\-coordinate reason is simple: fixing all coordinates exceptyiy\_\{i\}, the ratio has form\(ci​yi\+A\)/\(yi\+D\)\(c\_\{i\}y\_\{i\}\+A\)/\(y\_\{i\}\+D\)and its derivative has constant sign\. Therefore each coordinate can be pushed to an endpoint without increasing the objective\.

Sort the coefficients ascending,c\(1\)≤⋯≤c\(K\)c\_\{\(1\)\}\\leq\\cdots\\leq c\_\{\(K\)\}, and reindexL,UL,Uaccordingly\. Form∈\{0,…,K\}m\\in\\\{0,\\ldots,K\\\}define

y\(j\)\(m\)=\{U\(j\),j≤m,L\(j\),j\>m,y^\{\(m\)\}\_\{\(j\)\}=\\begin\{cases\}U\_\{\(j\)\},&j\\leq m,\\\\ L\_\{\(j\)\},&j\>m,\\end\{cases\}\(9\)and

τm=R​\(y\(m\)\)=∑j≤mc\(j\)​U\(j\)\+∑j\>mc\(j\)​L\(j\)∑j≤mU\(j\)\+∑j\>mL\(j\)\.\\tau\_\{m\}=R\(y^\{\(m\)\}\)=\\frac\{\\sum\_\{j\\leq m\}c\_\{\(j\)\}U\_\{\(j\)\}\+\\sum\_\{j\>m\}c\_\{\(j\)\}L\_\{\(j\)\}\}\{\\sum\_\{j\\leq m\}U\_\{\(j\)\}\+\\sum\_\{j\>m\}L\_\{\(j\)\}\}\.\(10\)
###### Theorem 3\.2\(Threshold exactness\)\.

For everyc∈ℝKc\\in\\mathbb\{R\}^\{K\}and every finite boxℬ\\mathcal\{B\},

Lbox​\(c,ℓ,u\)=mins∈ℬ⁡Fc​\(s\)=minm=0,…,K⁡τm\.L\_\{\\mathrm\{box\}\}\(c,\\ell,u\)=\\min\_\{s\\in\\mathcal\{B\}\}F\_\{c\}\(s\)=\\min\_\{m=0,\\ldots,K\}\\tau\_\{m\}\.\(11\)ConsequentlyLbox​\(c,ℓ,u\)L\_\{\\mathrm\{box\}\}\(c,\\ell,u\)can be evaluated inO​\(K​log⁡K\)O\(K\\log K\)time\.

The intuition is that the optimizer trades off mass against cost: to minimize the weighted softmax, it maximizes the exponentiated scores on the coordinates with the smallestcccoefficients \(making them as heavy as possible\) and minimizes the scores on the most expensive coordinates\. Becauseccis sorted, the optimal split between “heavy\-cheap” and “light\-expensive” coordinates is always a contiguous threshold\.

Algorithm 1Vertex\-Softmax threshold solver1:Input:coefficients

cc, score lower/upper bounds

ℓ,u\\ell,u
2:Sort indices so

c\(1\)≤⋯≤c\(K\)c\_\{\(1\)\}\\leq\\cdots\\leq c\_\{\(K\)\}
3:Set

a=maxj⁡uja=\\max\_\{j\}u\_\{j\}
4:Compute

Lj=exp⁡\(ℓj−a\)L\_\{j\}=\\exp\(\\ell\_\{j\}\-a\)and

Uj=exp⁡\(uj−a\)U\_\{j\}=\\exp\(u\_\{j\}\-a\)
5:Compute prefix sums of

U\(j\)U\_\{\(j\)\}and

c\(j\)​U\(j\)c\_\{\(j\)\}U\_\{\(j\)\}
6:Compute suffix sums of

L\(j\)L\_\{\(j\)\}and

c\(j\)​L\(j\)c\_\{\(j\)\}L\_\{\(j\)\}
7:Evaluate all ratios

τm\\tau\_\{m\}in \([10](https://arxiv.org/html/2605.10974#S3.E10)\)

8:return

minm⁡τm\\min\_\{m\}\\tau\_\{m\}

The stability shift in Algorithm[1](https://arxiv.org/html/2605.10974#alg1)rescales every numerator and denominator by the same positive factor, so it preserves all ratios and avoids overflow\. A proof\-producing interval\-arithmetic evaluation path is described in Appendix[D](https://arxiv.org/html/2605.10974#A4)\.

###### Corollary 3\.3\(Score\-box optimality\)\.

LetG​\(c,ℓ,u\)G\(c,\\ell,u\)be any lower\-bound procedure depending only onccand the independent intervals\. If

G​\(c,ℓ,u\)≤Fc​\(s\)∀s∈ℬ,G\(c,\\ell,u\)\\leq F\_\{c\}\(s\)\\qquad\\forall s\\in\\mathcal\{B\},\(12\)then

G​\(c,ℓ,u\)≤Lbox​\(c,ℓ,u\)\.G\(c,\\ell,u\)\\leq L\_\{\\mathrm\{box\}\}\(c,\\ell,u\)\.\(13\)Vertex\-Softmax therefore exhausts the information available at the score\-box interface: any tighter certificate must exploit score correlations, score–value coupling, or a reachable score set smaller than the independent box\.

## 4Vertex\-CROWN Attention Bound

The previous section provides an exact solver for a single softmax row given fixed coefficients and score intervals\. To turn this into a working verifier, we need to extract those quantities from a CROWN/LiRPA backward pass and compose the row\-level certificates into an end\-to\-end margin bound\. Vertex\-CROWN is the resulting interface\. Figure[1](https://arxiv.org/html/2605.10974#S4.F1)illustrates where the Vertex\-Softmax primitive fits in the overall verification pipeline\.

Input perturbation set𝒳\\mathcal\{X\}x′∈\[x−ϵ,x\+ϵ\]x^\{\\prime\}\\in\[x\-\\epsilon,\\;x\+\\epsilon\]1Attention block affine boundspre\-activations and intermediate bounds2Per\-row score boxes andvalue\-side coefficient boundssr∈\[ℓr,ur\],zrL≤zr​\(x\)s\_\{r\}\\in\[\\ell\_\{r\},u\_\{r\}\],\\;z\_\{r\}^\{L\}\\leq z\_\{r\}\(x\)3Vertex\-Softmax row solvermin/max⁡c⊤​softmax⁡\(sr\),sr∈\[ℓr,ur\]\\min/\\max\\;c^\{\\top\}\\operatorname\{softmax\}\(s\_\{r\}\),\\;s\_\{r\}\\in\[\\ell\_\{r\},u\_\{r\}\]4Exact at fixed\-coefficientscore\-box interfaceCertified attention row output boundstight rowwise lower/upper bounds5Compose with remaining verifierrows, heads, residual, and MLP bounds6Final lower bound on class marginmt​\(x′\)=fy​\(x′\)−ft​\(x′\)m\_\{t\}\(x^\{\\prime\}\)=f\_\{y\}\(x^\{\\prime\}\)\-f\_\{t\}\(x^\{\\prime\}\); certified if\>0\>07Figure 1:Integration of Vertex\-Softmax into the verification pipeline\. Input perturbations are propagated to independent score boxes and value\-side coefficient lower bounds for each attention row\. Vertex\-Softmax computes exact directional softmax bounds at this rowwise score\-box interface, which are then composed with the remaining verifier to obtain a certified lower bound on the final class margin\.Suppose a scalar margin satisfies

m​\(x\)≥b\+∑i∑j=1Kai​\(x\)j​zi​j​\(x\)∀x∈𝒳,m\(x\)\\geq b\+\\sum\_\{i\}\\sum\_\{j=1\}^\{K\}a\_\{i\}\(x\)\_\{j\}z\_\{ij\}\(x\)\\qquad\\forall x\\in\\mathcal\{X\},\(14\)whereai​\(x\)=softmax⁡\(si​\(x\)\)a\_\{i\}\(x\)=\\operatorname\{softmax\}\(s\_\{i\}\(x\)\)\. Assume sound score and value\-side lower bounds

ℓi​j≤si​j​\(x\)≤ui​j,zi​jL≤zi​j​\(x\)∀x∈𝒳\.\\ell\_\{ij\}\\leq s\_\{ij\}\(x\)\\leq u\_\{ij\},\\qquad z\_\{ij\}^\{L\}\\leq z\_\{ij\}\(x\)\\qquad\\forall x\\in\\mathcal\{X\}\.\(15\)For proof references we also name the two parts separately:

ℓi​j≤si​j​\(x\)≤ui​j∀x∈𝒳,\\ell\_\{ij\}\\leq s\_\{ij\}\(x\)\\leq u\_\{ij\}\\qquad\\forall x\\in\\mathcal\{X\},\(16\)zi​jL≤zi​j​\(x\)∀x∈𝒳\.z\_\{ij\}^\{L\}\\leq z\_\{ij\}\(x\)\\qquad\\forall x\\in\\mathcal\{X\}\.\(17\)Letℬi=∏j\[ℓi​j,ui​j\]\\mathcal\{B\}\_\{i\}=\\prod\_\{j\}\[\\ell\_\{ij\},u\_\{ij\}\]and

Li=Lbox\(ziL,ℓi,ui\)=minsi∈ℬi∑j=1Ksoftmax\(si\)jzi​jL\.L\_\{i\}=L\_\{\\mathrm\{box\}\}\(z\_\{i\}^\{L\},\\ell\_\{i\},u\_\{i\}\)=\\min\_\{s\_\{i\}\\in\\mathcal\{B\}\_\{i\}\}\\sum\_\{j=1\}^\{K\}\\operatorname\{softmax\}\(s\_\{i\}\)\_\{j\}z\_\{ij\}^\{L\}\.\(18\)The layer bound is

LVC=b\+∑iLi\.L\_\{\\mathrm\{VC\}\}=b\+\\sum\_\{i\}L\_\{i\}\.\(19\)
Algorithm 2Vertex\-CROWN attention bound1:Input:input set

𝒳\\mathcal\{X\}, scalar margin

mm, attention row scores

sis\_\{i\}
2:Use CROWN/LiRPA to obtain sound row score bounds

\(ℓi,ui\)\(\\ell\_\{i\},u\_\{i\}\)
3:Obtain lower value coefficients

ziLz\_\{i\}^\{L\}and affine lower term

bbsatisfying \([14](https://arxiv.org/html/2605.10974#S4.E14)\)–\([17](https://arxiv.org/html/2605.10974#S4.E17)\)

4:foreach query row

iido

5:

Li←Lbox​\(ziL,ℓi,ui\)L\_\{i\}\\leftarrow L\_\{\\mathrm\{box\}\}\(z\_\{i\}^\{L\},\\ell\_\{i\},u\_\{i\}\)using Algorithm[1](https://arxiv.org/html/2605.10974#alg1)

6:endfor

7:return

LVC=b\+∑iLiL\_\{\\mathrm\{VC\}\}=b\+\\sum\_\{i\}L\_\{i\}

###### Proposition 4\.1\(Soundness of Vertex\-CROWN\)\.

Under \([14](https://arxiv.org/html/2605.10974#S4.E14)\), \([16](https://arxiv.org/html/2605.10974#S4.E16)\), and \([17](https://arxiv.org/html/2605.10974#S4.E17)\), Algorithm[2](https://arxiv.org/html/2605.10974#alg2)returns a sound lower bound:

LVC≤m​\(x\)∀x∈𝒳\.L\_\{\\mathrm\{VC\}\}\\leq m\(x\)\\qquad\\forall x\\in\\mathcal\{X\}\.\(20\)

In practice, ifLVC\>0L\_\{\\mathrm\{VC\}\}\>0, the model’s prediction is provably unchanged under every perturbation in𝒳\\mathcal\{X\}\. Tighter lower bounds certify more inputs and give a more informative picture of the model’s robustness\.

#### Self\-attention and suffix instantiation\.

For the ViT\-style blocks in the experiments, token embeddingsH​\(x\)H\(x\)produce affine queries, keys, and values

Qih=WQh​Hi\+bQh,Kjh=WKh​Hj\+bKh,Vjh=WVh​Hj\+bVh,Q\_\{i\}^\{h\}=W\_\{Q\}^\{h\}H\_\{i\}\+b\_\{Q\}^\{h\},\\qquad K\_\{j\}^\{h\}=W\_\{K\}^\{h\}H\_\{j\}\+b\_\{K\}^\{h\},\\qquad V\_\{j\}^\{h\}=W\_\{V\}^\{h\}H\_\{j\}\+b\_\{V\}^\{h\},\(21\)with scores

si​jh​\(x\)=dh−1/2​⟨Qih​\(x\),Kjh​\(x\)⟩\+μi​jh\.s\_\{ij\}^\{h\}\(x\)=d\_\{h\}^\{\-1/2\}\\langle Q\_\{i\}^\{h\}\(x\),K\_\{j\}^\{h\}\(x\)\\rangle\+\\mu\_\{ij\}^\{h\}\.\(22\)The score intervals can be obtained by CROWN/McCormick bounds on this scalar score module, or by the interval\-product fallback in Appendix[C](https://arxiv.org/html/2605.10974#A3)\.

For a target margin, letHi\+​\(x\)=Hi​\(x\)\+bO\+∑hWOh​∑jai​jh​\(x\)​Vjh​\(x\)H\_\{i\}^\{\+\}\(x\)=H\_\{i\}\(x\)\+b\_\{O\}\+\\sum\_\{h\}W\_\{O\}^\{h\}\\sum\_\{j\}a\_\{ij\}^\{h\}\(x\)V\_\{j\}^\{h\}\(x\)be the post\-attention residual state\. If the downstream suffix gives

mt​\(x\)≥βt\+∑iγt​i⊤​Hi\+​\(x\),m\_\{t\}\(x\)\\geq\\beta\_\{t\}\+\\sum\_\{i\}\\gamma\_\{ti\}^\{\\top\}H\_\{i\}^\{\+\}\(x\),\(23\)then the induced row coefficients are lower bounds of\(WOh\)⊤​γt​i\(W\_\{O\}^\{h\}\)^\{\\top\}\\gamma\_\{ti\}contracted withVjh​\(x\)V\_\{j\}^\{h\}\(x\), and the Vertex path has form

LVC,t=bt′\+∑h,iLbox​\(ct​i​h:,ℓi​h:,ui​h:\)\.L\_\{\\mathrm\{VC\},t\}=b\_\{t\}^\{\\prime\}\+\\sum\_\{h,i\}L\_\{\\mathrm\{box\}\}\(c\_\{tih:\},\\ell\_\{ih:\},u\_\{ih:\}\)\.\(24\)The target\-wise hybrid uses

Lhyb,t=max⁡\{LCROWN,t,LVC,t\},L\_\{\\mathrm\{hyb\},t\}=\\max\\\{L\_\{\\mathrm\{CROWN\},t\},L\_\{\\mathrm\{VC\},t\}\\\},\(25\)which is sound because both terms lower\-bound the same target margin\. The two paths complement each other: direct CROWN propagates tighter affine relaxations through the full computation graph, while Vertex\-CROWN solves the softmax subproblem exactly but relies on looser value\-side and suffix bounds\. Taking the per\-target maximum captures the best of both without sacrificing soundness\. Details, coefficient formulas, and the per\-target algorithm are in Appendix[C](https://arxiv.org/html/2605.10974#A3)\. The oracle cost isO​\(B​T​H​R​K​log⁡K\)O\(BTHRK\\log K\)for batch sizeBB, targetsTT, headsHH, query rowsRR, and keysKK, excluding score/value/suffix bound construction\.

## 5Experiments

The experiments test whether the exact score\-box primitive sharpens attention certificates at the verifier interface\. We progress from validating the solver itself, to scalable softmax comparisons on synthetic score boxes, to real\-data patch\-attention models, to full attention–residual–MLP blocks, and finally to comparisons against stronger optimized and search\-based baselines\.

Certified\-rate denominators differ by benchmark\. Synthetic rows are computed over all generated trials\. Patch\-attention rows in Table[4](https://arxiv.org/html/2605.10974#S5.T4)are conditional on clean\-correct examples\. Full\-block rows in Table[5](https://arxiv.org/html/2605.10974#S5.T5)are end\-to\-end certified accuracies over the listed evaluation prefixes, with clean\-incorrect examples counted as uncertified\. The exactness claim applies only to the fixed\-coefficient independent score\-box subproblem, not to end\-to\-end transformer verification\. The reported lower bound is the mean margin lower bound; and the gap is best attack margin minus certified lower bound\. All reported verifier tables use standard floating\-point PyTorch/auto\_LiRPA unless explicitly marked otherwise; the mathematical soundness statements are real\-arithmetic statements, with interval\-oracle checks in Appendix[D](https://arxiv.org/html/2605.10974#A4)\. Protocol and numerical\-status records are in Appendix Tables[6](https://arxiv.org/html/2605.10974#A5.T6)and[7](https://arxiv.org/html/2605.10974#A5.T7)\.

#### Solver and scalable softmax checks\.

The threshold solver agrees with exhaustive vertex enumeration up to numerical tolerance forK≤16K\\leq 16and remains practical atK=512K=512; Appendix Table[9](https://arxiv.org/html/2605.10974#A5.T9)and Figure[4](https://arxiv.org/html/2605.10974#A5.F4)give the timing details\. Table[3](https://arxiv.org/html/2605.10974#S5.T3)shows the main scalable\-softmax comparison\. Vertex\-Softmax gives the best mean lower bound and smallest attack gap for every testedK∈\{4,8,16,32,64,128\}K\\in\\\{4,8,16,32,64,128\\\}, while also being33–24×24\\timesfaster than Wei\-LSE \(e\.g\.,0\.080\.08s vs\.2\.02\.0s atK=128K=128\)\.

![Refer to caption](https://arxiv.org/html/2605.10974v1/x1.png)Figure 2:Scalable attention sweep atϵ=0\.02\\epsilon=0\.02\. Vertex\-Softmax gives the highest mean certified lower bound and the smallest gap to the best attack across the tested sequence lengths\. GaLileo\-style implementation baseline results forK≤16K\\leq 16are in Appendix Table[8](https://arxiv.org/html/2605.10974#A5.T8)\.Table 3:Scalable sweep atϵ=0\.02\\epsilon=0\.02over three seeds and 600 total trials per row\. Vertex\-Softmax gives the best mean lower bound and smallest attack gap at every testedKK\. Runtime is aggregate wall time\. An independent GaLileo\-style implementation baseline forK≤16K\\leq 16is in Appendix Table[8](https://arxiv.org/html/2605.10974#A5.T8)\(the original GaLileo code is not publicly available\)\.
#### Image attention certificates\.

Table[4](https://arxiv.org/html/2605.10974#S5.T4)evaluates small real\-data patch\-attention classifiers\. The strongest signal appears in high\-uncertainty regimes: atϵ=0\.03\\epsilon=0\.03, Vertex\-CROWN raises binary MNIST certification from20\.3%20\.3\\%to77\.8%77\.8\\%with 16 tokens and from46\.5%46\.5\\%to92\.5%92\.5\\%with 49 tokens\. These are regimes where standard CROWN leaves most inputs uncertified; replacing the softmax relaxation with the exact solver recovers the majority of them\. The 10\-class setting is harder, but Vertex\-CROWN still improves both certified rate and mean lower bound atϵ∈\{0\.02,0\.03\}\\epsilon\\in\\\{0\.02,0\.03\\\}; Appendix Table[13](https://arxiv.org/html/2605.10974#A5.T13)reports seed\-resampling stability checks for the main rate improvements\.

Table 4:Real\-data MNIST patch\-attention certificates\. Binary rows use classes0vs\.11; 10\-class rows use all MNIST classes\. The 16\-token model uses7×77\\times 7patches, and the 49\-token model uses4×44\\times 4patches\. Certification rates are conditional on clean\-correct examples: verification is run on up to the protocol’s listedNNcorrectly classified test examples per seed, so these rates are not end\-to\-end certified accuracies\. Results are averaged over three seeds for the 16\-token rows and two seeds for the 49\-token row\.
#### Full attention–residual–MLP blocks\.

Table[5](https://arxiv.org/html/2605.10974#S5.T5)tests whether the primitive’s gains survive a nonlinear suffix\. The CROWN\-suffix hybrid improves Fashion\-MNIST end\-to\-end certified rates and mean lower bounds across the robustness curve: atϵ=0\.02\\epsilon=0\.02it raises certification from5\.6%5\.6\\%to14\.0%14\.0\\%and improves the mean lower bound from−7\.784\-7\.784to−1\.382\-1\.382; atϵ=0\.03\\epsilon=0\.03the mean lower bound improves by over3333points\. CIFAR\-10 grayscale, included as a low\-accuracy stress setting, shows the same tightness direction\. Appendix Tables[12](https://arxiv.org/html/2605.10974#A5.T12),[13](https://arxiv.org/html/2605.10974#A5.T13), and[11](https://arxiv.org/html/2605.10974#A5.T11)give paired deltas, seed\-resampling stability checks, and runtime accounting\. The sort/sweep oracle is negligible relative to score, value, and suffix\-bound construction\.

#### Stronger baselines\.

![Refer to caption](https://arxiv.org/html/2605.10974v1/x2.png)Figure 3:Comparison against alpha\-CROWN and fixed\-budget ABCrown\-BaB on selected small attention blocks\. Vertex\-CROWN is competitive with alpha\-CROWN across settings and outperforms it in higher\-epsilon and higher\-dimensional configurations, while running3030–100×100\\timesfaster\. ABCrown\-BaB uses a 600s per\-instance budget; unknown, timeout, OOM, and internal\-error outcomes are counted as uncertified\.Against alpha\-CROWN and fixed\-budget ABCrown\-BaB on selected small attention blocks, Vertex\-CROWN matches or exceeds alpha\-CROWN atK=4,d=16,ϵ=0\.03K=4,d=16,\\epsilon=0\.03andK=6,d=16,ϵ=0\.03K=6,d=16,\\epsilon=0\.03, outperforms it in higher\-epsilon and higher\-dimensionalK=4K=4settings, and trails it on the residual block atϵ=0\.03\\epsilon=0\.03where optimizable slopes have more room to help\. With a 600 second ABCrown\-BaB budget, Vertex\-CROWN certifies62\.5%62\.5\\%versus50\.0%50\.0\\%onK=4,d=16,ϵ=0\.05K=4,d=16,\\epsilon=0\.05and50\.0%50\.0\\%versus29\.2%29\.2\\%onK=4,d=32,ϵ=0\.03K=4,d=32,\\epsilon=0\.03\. Notably, Vertex\-CROWN achieves these results in0\.030\.03–0\.070\.07s per trial, compared to1\.51\.5–3\.73\.7s for alpha\-CROWN and268268–395395s for ABCrown\-BaB\. Figure[3](https://arxiv.org/html/2605.10974#S5.F3)and Appendix Tables[14](https://arxiv.org/html/2605.10974#A5.T14)and[15](https://arxiv.org/html/2605.10974#A5.T15)give paired, aggregate, and fixed\-budget details\.

#### Practical guidance\.

Vertex\-CROWN is most effective when the softmax relaxation is the binding source of certificate looseness: high\-uncertainty regimes with wider score boxes, settings where alpha\-CROWN’s slope optimization has limited room, and architectures where the attention layer dominates the verification gap\. When suffix or value\-bound looseness dominates instead, the hybrid strategy can still recover the better of the two paths, but full\-block use incurs the substantial bound\-construction cost quantified in Appendix Table[11](https://arxiv.org/html/2605.10974#A5.T11)\.

Table 5:Full attention–residual–MLP block results\. Cert\. entries are end\-to\-end certified accuracies, reported as CROWN / Hybrid over the first 100 evaluation examples per seed with clean\-incorrect examples counted as uncertified\. Lower columns show CROWN / Hybrid mean margin lower bounds on the clean\-correct examples from the same evaluation prefix\.Δ\\Deltais the paired mean lower\-bound improvement of Hybrid over CROWN\. All rows use five seeds\.

## 6Limitations

Vertex\-Softmax eliminates one source of looseness, the softmax relaxation inside the score\-box subproblem, but the full verification pipeline has several other sources of slack that the primitive does not address\. Understanding these is important both for interpreting the experimental results and for identifying where future work can have the most impact\.

Vertex\-Softmax is exact only after the verifier has reduced an attention row to fixed coefficients and independent score intervals\. The remaining looseness comes from the surrounding verifier, not from the weighted\-softmax box oracle\. First, independent score boxes discard score correlations; if those correlations rule out the worst threshold vertex, exact box optimization is still conservative for the reachable set\. Second, value lower bounds discard score–value coupling; nonnegative softmax weights preserve soundness, but weak value bounds can dominate the final certificate\. Third, row\-wise minimization can combine worst cases that no single input attains simultaneously\. Fourth, nonlinear suffixes require additional relaxations, so the CROWN\-suffix hybrid in Table[5](https://arxiv.org/html/2605.10974#S5.T5)is tighter but slower than direct CROWN and still depends on suffix\-bound quality\. The experiments are one\-block ViT\-style models rather than deep transformers with layer normalization and many interacting blocks\. Appendix Table[10](https://arxiv.org/html/2605.10974#A5.T10)gives controlled slack\-decomposition diagnostics, and Appendix Table[11](https://arxiv.org/html/2605.10974#A5.T11)separates oracle cost from surrounding bound\-construction cost\.

## 7Conclusion

Vertex\-Softmax exactly solvesmins∈ℬ⁡c⊤​softmax⁡\(s\)\\min\_\{s\\in\\mathcal\{B\}\}c^\{\\top\}\\operatorname\{softmax\}\(s\)at the independent score\-box interface\. The optimum is attained by one ofK\+1K\+1sorted threshold vertices, giving an exactO​\(K​log⁡K\)O\(K\\log K\)primitive that replaces objective\-agnostic softmax relaxations with a direction\-aware row solver\. Integrated into Vertex\-CROWN, it produces large certified\-rate improvements on patch\-attention and full attention–residual–MLP models, and is competitive with or improves upon alpha\-CROWN and branch\-and\-bound baselines on selected attention blocks\.

The threshold structure also clarifies where further progress must come from\. Because Vertex\-Softmax exhausts the information at the independent score\-box interface, tighter end\-to\-end certificates require exploiting score correlations, score–value coupling, joint row composition, or tighter nonlinear suffix bounds\. Extending the exact\-optimization perspective to these richer interfaces, for instance solving correlated score polytopes or jointly optimizing over scores and values, is a natural next step toward closing the gap between local softmax exactness and global verifier tightness\.

## References

- Fast and precise certification of transformers\.InProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation,pp\. 466–481\.External Links:[Document](https://dx.doi.org/10.1145/3453483.3454056)Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p1.1)\.
- I\. Chaudhary, Q\. Hu, M\. Kumar, M\. Ziyadi, R\. Gupta, and G\. Singh \(2025\)Certifying counterfactual bias in LLMs\.InInternational Conference on Learning Representations,Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p1.1)\.
- J\. J\. Cherianet al\.\(2024\)Large language model validity via enhanced conformal prediction methods\.arXiv preprint arXiv:2406\.09714\.Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p1.1)\.
- W\. Dinkelbach \(1967\)On nonlinear fractional programming\.Management Science13\(7\),pp\. 492–498\.Cited by:[§3](https://arxiv.org/html/2605.10974#S3.p1.7)\.
- G\. Katz, D\. A\. Huang, D\. Ibeling, K\. Julian, C\. Lazarus, R\. Lim, P\. Shah, S\. Thakoor, H\. Wu, A\. Zeljić, D\. L\. Dill, M\. J\. Kochenderfer, and C\. Barrett \(2019\)The marabou framework for verification and analysis of deep neural networks\.InComputer Aided Verification,pp\. 443–452\.Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p2.1)\.
- A\. Kumar, C\. Agarwal, S\. Srinivas, A\. J\. Li, S\. Feizi, and H\. Lakkaraju \(2024\)Certifying LLM safety against adversarial prompting\.InConference on Language Modeling,Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p1.1)\.
- B\. H\. C\. Liao, C\. H\. Cheng, H\. Esen, and A\. Knoll \(2023\)Are transformers more robust? towards exact robustness verification for transformers\.InComputer Safety, Reliability, and Security,pp\. 89–103\.Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p2.1)\.
- Z\. Shi, Q\. Jin, Z\. Kolter, S\. Jana, C\. Hsieh, and H\. Zhang \(2025\)Neural network verification with branch\-and\-bound for general nonlinearities\.InTools and Algorithms for the Construction and Analysis of Systems,pp\. 315–335\.Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p2.1)\.
- Z\. Shi, H\. Zhang, K\. Chang, M\. Huang, and C\. Hsieh \(2020\)Robustness verification for transformers\.InInternational Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p1.1)\.
- V\. Tjeng, K\. Y\. Xiao, and R\. Tedrake \(2019\)Evaluating robustness of neural networks with mixed integer programming\.InInternational Conference on Learning Representations,Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p2.1)\.
- H\. Tranet al\.\(2020\)NNV: the neural network verification tool for deep neural networks and learning\-enabled cyber\-physical systems\.InComputer Aided Verification,pp\. 3–17\.Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p2.1)\.
- H\. Wanget al\.\(2025\)AgentSpec: customizable runtime enforcement for safe and reliable LLM agents\.arXiv preprint arXiv:2503\.18666\.Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p1.1)\.
- H\. Wang, C\. M\. Poskitt, J\. Wei, and J\. Sun \(2025\)ProbGuard: probabilistic runtime monitoring for LLM agent safety\.arXiv preprint arXiv:2508\.00500\.Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p1.1)\.
- S\. Wang, H\. Zhang, K\. Xu, X\. Lin, S\. Jana, C\. Hsieh, and J\. Z\. Kolter \(2021\)Beta\-crown: efficient bound propagation with per\-neuron split constraints for neural network robustness verification\.InAdvances in Neural Information Processing Systems,Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p1.1)\.
- D\. Wei, H\. Wu, M\. Wu, P\. Chen, C\. Barrett, and E\. Farchi \(2023\)Convex bounds on the softmax function with applications to robustness verification\.InProceedings of the 26th International Conference on Artificial Intelligence and Statistics,Proceedings of Machine Learning Research, Vol\.206,pp\. 6853–6878\.Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p1.1)\.
- K\. Xu, Z\. Shi, H\. Zhang, Y\. Wang, K\. Chang, M\. Huang, B\. Kailkhura, X\. Lin, and C\. Hsieh \(2020\)Automatic perturbation analysis for scalable certified robustness and beyond\.InAdvances in Neural Information Processing Systems,Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p1.1),[§1](https://arxiv.org/html/2605.10974#S1.p2.4)\.
- H\. Zhang, T\. Weng, P\. Chen, C\. Hsieh, and L\. Daniel \(2018\)Efficient neural network robustness certification with general activation functions\.InAdvances in Neural Information Processing Systems,Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p1.1),[§1](https://arxiv.org/html/2605.10974#S1.p2.4)\.
- Y\. Zhang, Y\. E\. Sun, A\. J\. E\. Lee, and J\. S\. Dong \(2025\)RvLLM: LLM runtime verification with domain knowledge\.arXiv preprint arXiv:2505\.18585\.Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p1.1)\.
- Y\. Zhang, L\. Shen, S\. Guo, and S\. Ji \(2024\)GaLileo: general linear relaxation framework for tightening robustness certification of transformers\.InProceedings of the AAAI Conference on Artificial Intelligence,Vol\.38,pp\. 21797–21805\.Cited by:[§1](https://arxiv.org/html/2605.10974#S1.SS0.SSS0.Px2.p1.1)\.
- Z\. Zhanget al\.\(2024\)SafetyBench: evaluating the safety of large language models\.arXiv preprint arXiv:2309\.07045\.Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p1.1)\.
- K\. Zhuet al\.\(2024\)PromptBench: a unified library for evaluation of large language models\.Journal of Machine Learning Research\.Cited by:[Appendix A](https://arxiv.org/html/2605.10974#A1.p1.1)\.

## Appendix AExtended Related Work

At LLM scale, the verification literature shifts toward different kinds of guarantees\. Erase\-and\-Check certifies wrapper behavior against bounded adversarial prompting\[Kumaret al\.,[2024](https://arxiv.org/html/2605.10974#bib.bib13)\]; distributional and conformal approaches give statistical guarantees over prompt distributions\[Chaudharyet al\.,[2025](https://arxiv.org/html/2605.10974#bib.bib14), Cherian and others,[2024](https://arxiv.org/html/2605.10974#bib.bib15)\]; empirical suites such as PromptBench and SafetyBench search for failures but are not sound certificates\[Zhu and others,[2024](https://arxiv.org/html/2605.10974#bib.bib16), Zhang and others,[2024](https://arxiv.org/html/2605.10974#bib.bib17)\]; and runtime monitors such as AgentSpec, RvLLM, and ProbGuard enforce explicit trace or action predicates during deployment\[Wang and others,[2025](https://arxiv.org/html/2605.10974#bib.bib18), Zhanget al\.,[2025](https://arxiv.org/html/2605.10974#bib.bib19), Wanget al\.,[2025](https://arxiv.org/html/2605.10974#bib.bib20)\]\. These approaches are practically important for frontier LLM systems, but they certify wrappers, distributions, tests, or traces rather than the worst\-case white\-box semantics of the transformer computation graph\. Vertex\-Softmax is complementary to all of these: it contributes a local exact primitive at the score\-box interface, not an end\-to\-end system for any of the above guarantee types\.

For transformers specifically, the exact MIQCP result ofLiaoet al\.\[[2023](https://arxiv.org/html/2605.10974#bib.bib6)\]applies to sparsemax attention rather than standard softmax attention\. Set\-based reachability methods\[Tran and others,[2020](https://arxiv.org/html/2605.10974#bib.bib11)\]can provide complete answers but have not yet been demonstrated at dense softmax scale\.

## Appendix BProof Details

This appendix proves Theorems[3\.1](https://arxiv.org/html/2605.10974#S3.Thmtheorem1)and[3\.2](https://arxiv.org/html/2605.10974#S3.Thmtheorem2), derives Corollary[3\.3](https://arxiv.org/html/2605.10974#S3.Thmtheorem3)from them, and finally establishes the soundness statement in Proposition[4\.1](https://arxiv.org/html/2605.10974#S4.Thmtheorem1)\. Throughout we use the change of variablesyj=esjy\_\{j\}=e^\{s\_\{j\}\},Lj=eℓjL\_\{j\}=e^\{\\ell\_\{j\}\},Uj=eujU\_\{j\}=e^\{u\_\{j\}\}, so thatFc​\(s\)=R​\(y\)F\_\{c\}\(s\)=R\(y\)withRRas in \([7](https://arxiv.org/html/2605.10974#S3.E7)\), andyyranges over the positive boxℬy=∏j=1K\[Lj,Uj\]⊂\(0,∞\)K\\mathcal\{B\}\_\{y\}=\\prod\_\{j=1\}^\{K\}\[L\_\{j\},U\_\{j\}\]\\subset\(0,\\infty\)^\{K\}\. Because the maps↦ys\\mapsto yis a coordinatewise bijection that sends vertices ofℬ\\mathcal\{B\}to vertices ofℬy\\mathcal\{B\}\_\{y\}, every statement below transfers toFcF\_\{c\}onℬ\\mathcal\{B\}without change\.

### B\.1Proof of Theorem[3\.1](https://arxiv.org/html/2605.10974#S3.Thmtheorem1)

We show thatRRattains its minimum overℬy\\mathcal\{B\}\_\{y\}at a vertex ofℬy\\mathcal\{B\}\_\{y\}\. The maximum statement follows by applying the same argument withccreplaced by−c\-c\.

###### Proof of Theorem[3\.1](https://arxiv.org/html/2605.10974#S3.Thmtheorem1)\.

*Step 1: one\-dimensional reduction\.*IfK=1K=1, thenR​\(y\)=c1R\(y\)=c\_\{1\}is constant onℬy\\mathcal\{B\}\_\{y\}, so every point is a minimizer; in particular, both endpoints, which are vertices, are minimizers\. Thus the claim is immediate\. AssumeK≥2K\\geq 2\.

Fix any indexi∈\{1,…,K\}i\\in\\\{1,\\ldots,K\\\}and any choice of valuesyj∈\[Lj,Uj\]y\_\{j\}\\in\[L\_\{j\},U\_\{j\}\]forj≠ij\\neq i\. Write

A=∑j≠icj​yj,D=∑j≠iyj\.A=\\sum\_\{j\\neq i\}c\_\{j\}y\_\{j\},\\qquad D=\\sum\_\{j\\neq i\}y\_\{j\}\.\(26\)Sinceyj\>0y\_\{j\}\>0for everyjj, we haveD\>0D\>0\. Along theiith coordinate,RRtakes the one\-dimensional form

ϕi​\(yi\)=ci​yi\+Ayi\+D,yi∈\[Li,Ui\]\.\\phi\_\{i\}\(y\_\{i\}\)=\\frac\{c\_\{i\}y\_\{i\}\+A\}\{y\_\{i\}\+D\},\\qquad y\_\{i\}\\in\[L\_\{i\},U\_\{i\}\]\.\(27\)Differentiating,

ϕi′​\(yi\)=ci​\(yi\+D\)−\(ci​yi\+A\)\(yi\+D\)2=ci​D−A\(yi\+D\)2\.\\phi\_\{i\}^\{\\prime\}\(y\_\{i\}\)=\\frac\{c\_\{i\}\(y\_\{i\}\+D\)\-\(c\_\{i\}y\_\{i\}\+A\)\}\{\(y\_\{i\}\+D\)^\{2\}\}=\\frac\{c\_\{i\}D\-A\}\{\(y\_\{i\}\+D\)^\{2\}\}\.\(28\)The denominator is strictly positive and the numerator is independent ofyiy\_\{i\}, soϕi\\phi\_\{i\}is either monotone on\[Li,Ui\]\[L\_\{i\},U\_\{i\}\]or constant there\. In every case, at least one ofLiL\_\{i\}orUiU\_\{i\}attainsmin\[Li,Ui\]⁡ϕi\\min\_\{\[L\_\{i\},U\_\{i\}\]\}\\phi\_\{i\}\.

*Step 2: coordinate\-by\-coordinate pushing\.*SinceRRis continuous andℬy\\mathcal\{B\}\_\{y\}is compact, the minimumR⋆=minℬy⁡RR^\{\\star\}=\\min\_\{\\mathcal\{B\}\_\{y\}\}Ris attained\. Pick any minimizery⋆∈ℬyy^\{\\star\}\\in\\mathcal\{B\}\_\{y\}and define a finite sequencey\(0\),y\(1\),…,y\(K\)y^\{\(0\)\},y^\{\(1\)\},\\ldots,y^\{\(K\)\}byy\(0\)=y⋆y^\{\(0\)\}=y^\{\\star\}and, fori=1,…,Ki=1,\\ldots,K, chooseyi\(i\)y^\{\(i\)\}\_\{i\}to be an endpoint of\[Li,Ui\]\[L\_\{i\},U\_\{i\}\]that minimizes \([27](https://arxiv.org/html/2605.10974#A2.E27)\) with all other coordinates fixed at their values iny\(i−1\)y^\{\(i\-1\)\}, settingyj\(i\)=yj\(i−1\)y^\{\(i\)\}\_\{j\}=y^\{\(i\-1\)\}\_\{j\}forj≠ij\\neq i\. By Step 1, each replacement satisfiesR​\(y\(i\)\)≤R​\(y\(i−1\)\)R\(y^\{\(i\)\}\)\\leq R\(y^\{\(i\-1\)\}\)\. Iterating,

R⋆≤R​\(y\(K\)\)≤R​\(y\(0\)\)=R⋆,R^\{\\star\}\\leq R\(y^\{\(K\)\}\)\\leq R\(y^\{\(0\)\}\)=R^\{\\star\},\(29\)soR​\(y\(K\)\)=R⋆R\(y^\{\(K\)\}\)=R^\{\\star\}\. By constructionyj\(K\)∈\{Lj,Uj\}y^\{\(K\)\}\_\{j\}\\in\\\{L\_\{j\},U\_\{j\}\\\}for everyjj, and thereforey\(K\)y^\{\(K\)\}is a vertex ofℬy\\mathcal\{B\}\_\{y\}\. Pulling back throughs↦ys\\mapsto yyields a vertex ofℬ\\mathcal\{B\}attaining the minimum ofFcF\_\{c\}\. ∎

Degenerate intervalsℓj=uj\\ell\_\{j\}=u\_\{j\}require no modification: the corresponding coordinate is forced to its common endpoint, which is still a vertex\.

### B\.2Proof of Theorem[3\.2](https://arxiv.org/html/2605.10974#S3.Thmtheorem2)

By Theorem[3\.1](https://arxiv.org/html/2605.10974#S3.Thmtheorem1), it suffices to minimizeRRover the2K2^\{K\}vertices ofℬy\\mathcal\{B\}\_\{y\}\. We show that at least one of those minimizers has threshold form in the sense of \([9](https://arxiv.org/html/2605.10974#S3.E9)\), which narrows attention to theK\+1K\+1candidatesy\(0\),…,y\(K\)y^\{\(0\)\},\\ldots,y^\{\(K\)\}\.

Reindex so thatc1≤c2≤⋯≤cKc\_\{1\}\\leq c\_\{2\}\\leq\\cdots\\leq c\_\{K\}, and denote the associated bounds byLj,UjL\_\{j\},U\_\{j\}\. This is the sorted orderc\(j\)c\_\{\(j\)\},L\(j\)L\_\{\(j\)\},U\(j\)U\_\{\(j\)\}used in the main text, and the value ofRRis invariant under this reindexing\.

###### Proof of Theorem[3\.2](https://arxiv.org/html/2605.10974#S3.Thmtheorem2)\.

*Step 1: linearization at the optimum\.*For everyρ∈ℝ\\rho\\in\\mathbb\{R\}and everyy∈ℬyy\\in\\mathcal\{B\}\_\{y\}, the common denominatorS​\(y\)=∑jyjS\(y\)=\\sum\_\{j\}y\_\{j\}is strictly positive, and

R​\(y\)−ρ=∑j=1K\(cj−ρ\)​yjS​\(y\)\.R\(y\)\-\\rho=\\frac\{\\sum\_\{j=1\}^\{K\}\(c\_\{j\}\-\\rho\)y\_\{j\}\}\{S\(y\)\}\.\(30\)Lety⋆∈ℬyy^\{\\star\}\\in\\mathcal\{B\}\_\{y\}be any minimizer ofRRand setρ=R​\(y⋆\)\\rho=R\(y^\{\\star\}\)\. Then \([30](https://arxiv.org/html/2605.10974#A2.E30)\) aty⋆y^\{\\star\}gives∑j\(cj−ρ\)​yj⋆=0\\sum\_\{j\}\(c\_\{j\}\-\\rho\)y^\{\\star\}\_\{j\}=0\. For everyy∈ℬyy\\in\\mathcal\{B\}\_\{y\}, minimality ofy⋆y^\{\\star\}givesR​\(y\)≥ρR\(y\)\\geq\\rho, so

∑j=1K\(cj−ρ\)​yj≥0=∑j=1K\(cj−ρ\)​yj⋆\.\\sum\_\{j=1\}^\{K\}\(c\_\{j\}\-\\rho\)y\_\{j\}\\geq 0=\\sum\_\{j=1\}^\{K\}\(c\_\{j\}\-\\rho\)y^\{\\star\}\_\{j\}\.\(31\)Thusy⋆y^\{\\star\}minimizes the linear functionaly↦∑j\(cj−ρ\)​yjy\\mapsto\\sum\_\{j\}\(c\_\{j\}\-\\rho\)y\_\{j\}overℬy\\mathcal\{B\}\_\{y\}\.

*Step 2: a linear minimizer has threshold form\.*The linear problem in \([31](https://arxiv.org/html/2605.10974#A2.E31)\) separates across coordinates\. For eachjj,

yj⋆∈arg​minyj∈\[Lj,Uj\]⁡\(cj−ρ\)⁡yj,y^\{\\star\}\_\{j\}\\in\\operatorname\*\{arg\\,min\}\_\{y\_\{j\}\\in\[L\_\{j\},U\_\{j\}\]\}\(c\_\{j\}\-\\rho\)y\_\{j\},\(32\)and so necessarily

yj⋆=\{Uj,cj<ρ,Lj,cj\>ρ,any point in​\[Lj,Uj\],cj=ρ\.y^\{\\star\}\_\{j\}=\\begin\{cases\}U\_\{j\},&c\_\{j\}<\\rho,\\\\ L\_\{j\},&c\_\{j\}\>\\rho,\\\\ \\text\{any point in \}\[L\_\{j\},U\_\{j\}\],&c\_\{j\}=\\rho\.\\end\{cases\}\(33\)Definem−=\|\{j:cj<ρ\}\|m^\{\-\}=\|\\\{j:c\_\{j\}<\\rho\\\}\|andm\+=\|\{j:cj≤ρ\}\|m^\{\+\}=\|\\\{j:c\_\{j\}\\leq\\rho\\\}\|\. Since the coefficients are sorted,cj<ρc\_\{j\}<\\rhoexactly forj≤m−j\\leq m^\{\-\}andcj\>ρc\_\{j\}\>\\rhoexactly forj\>m\+j\>m^\{\+\}\. On the tied block\{m−\+1,…,m\+\}\\\{m^\{\-\}\+1,\\ldots,m^\{\+\}\\\}the linear functional contributes zero, so replacingy⋆y^\{\\star\}on that block by any other feasible values preserves∑j\(cj−ρ\)​yj=0\\sum\_\{j\}\(c\_\{j\}\-\\rho\)y\_\{j\}=0and hence preservesR​\(y\)=ρR\(y\)=\\rhoby \([30](https://arxiv.org/html/2605.10974#A2.E30)\)\. In particular, define a threshold vertexy~\\tilde\{y\}by

y~j=\{Uj,j≤m\+,Lj,j\>m\+\.\\tilde\{y\}\_\{j\}=\\begin\{cases\}U\_\{j\},&j\\leq m^\{\+\},\\\\ L\_\{j\},&j\>m^\{\+\}\.\\end\{cases\}\(34\)Theny~\\tilde\{y\}is exactly the threshold pattern \([9](https://arxiv.org/html/2605.10974#S3.E9)\) withm=m\+m=m^\{\+\}, andR​\(y~\)=R​\(y⋆\)=minℬy⁡RR\(\\tilde\{y\}\)=R\(y^\{\\star\}\)=\\min\_\{\\mathcal\{B\}\_\{y\}\}R\.

*Step 3:K\+1K\+1candidates suffice\.*By Step 2, some indexm∈\{0,1,…,K\}m\\in\\\{0,1,\\ldots,K\\\}satisfiesR​\(y\(m\)\)=minℬy⁡RR\(y^\{\(m\)\}\)=\\min\_\{\\mathcal\{B\}\_\{y\}\}R\. Therefore

mins∈ℬ⁡Fc​\(s\)\\displaystyle\\min\_\{s\\in\\mathcal\{B\}\}F\_\{c\}\(s\)=miny∈ℬy⁡R​\(y\)\\displaystyle=\\min\_\{y\\in\\mathcal\{B\}\_\{y\}\}R\(y\)=minm=0,…,K⁡R​\(y\(m\)\)=minm=0,…,K⁡τm,\\displaystyle=\\min\_\{m=0,\\ldots,K\}R\\bigl\(y^\{\(m\)\}\\bigr\)=\\min\_\{m=0,\\ldots,K\}\\tau\_\{m\},\(35\)which is the claimed exactness identity\.

*Step 4: complexity\.*SortingcctakesO​\(K​log⁡K\)O\(K\\log K\)\. With the sorted order fixed, a left\-to\-right pass computes prefix sums ofU\(j\)U\_\{\(j\)\}andc\(j\)​U\(j\)c\_\{\(j\)\}U\_\{\(j\)\}, and a right\-to\-left pass computes suffix sums ofL\(j\)L\_\{\(j\)\}andc\(j\)​L\(j\)c\_\{\(j\)\}L\_\{\(j\)\}, each inO​\(K\)O\(K\)time\. Given these four arrays, everyτm\\tau\_\{m\}in \([10](https://arxiv.org/html/2605.10974#S3.E10)\) is a ratio of twoO​\(1\)O\(1\)lookups, so the full sweep overm=0,…,Km=0,\\ldots,KcostsO​\(K\)O\(K\)\. The total is thereforeO​\(K​log⁡K\)O\(K\\log K\), dominated by the sort\. ∎

For numerical stability, replacing\(ℓj,uj\)\(\\ell\_\{j\},u\_\{j\}\)by\(ℓj−a,uj−a\)\(\\ell\_\{j\}\-a,u\_\{j\}\-a\)rescales everyyjy\_\{j\}bye−ae^\{\-a\}, and therefore scales both the numerator and the denominator of everyτm\\tau\_\{m\}by the same factor\. Choosinga=maxj⁡uja=\\max\_\{j\}u\_\{j\}enforcesyj∈\(0,1\]y\_\{j\}\\in\(0,1\]for alljjand prevents overflow\.

### B\.3Proof of Corollary[3\.3](https://arxiv.org/html/2605.10974#S3.Thmtheorem3)

###### Proof of Corollary[3\.3](https://arxiv.org/html/2605.10974#S3.Thmtheorem3)\.

LetGGbe any sound score\-box\-only lower\-bound procedure\. By soundness,

G​\(c,ℓ,u\)≤Fc​\(s\)∀s∈ℬ\.G\(c,\\ell,u\)\\leq F\_\{c\}\(s\)\\qquad\\forall\\,s\\in\\mathcal\{B\}\.\(36\)The right\-hand side does not depend onGG, so we may take the infimum overs∈ℬs\\in\\mathcal\{B\}:

G​\(c,ℓ,u\)≤infs∈ℬFc​\(s\)\.G\(c,\\ell,u\)\\leq\\inf\_\{s\\in\\mathcal\{B\}\}F\_\{c\}\(s\)\.\(37\)The boxℬ\\mathcal\{B\}is compact andFcF\_\{c\}is continuous, so the infimum is attained and equalsmins∈ℬ⁡Fc​\(s\)\\min\_\{s\\in\\mathcal\{B\}\}F\_\{c\}\(s\)\. By Theorem[3\.2](https://arxiv.org/html/2605.10974#S3.Thmtheorem2),

mins∈ℬ⁡Fc​\(s\)=minm=0,…,K⁡τm=Lbox​\(c,ℓ,u\)\.\\min\_\{s\\in\\mathcal\{B\}\}F\_\{c\}\(s\)=\\min\_\{m=0,\\ldots,K\}\\tau\_\{m\}=L\_\{\\mathrm\{box\}\}\(c,\\ell,u\)\.\(38\)Combining the displays givesG​\(c,ℓ,u\)≤Lbox​\(c,ℓ,u\)G\(c,\\ell,u\)\\leq L\_\{\\mathrm\{box\}\}\(c,\\ell,u\)\. ∎

Algorithm[1](https://arxiv.org/html/2605.10974#alg1)is itself a concrete sound score\-box\-only procedure whose output equalsLbox​\(c,ℓ,u\)L\_\{\\mathrm\{box\}\}\(c,\\ell,u\), so the inequality in Corollary[3\.3](https://arxiv.org/html/2605.10974#S3.Thmtheorem3)is attained\. Among all sound procedures whose only inputs areccand the independent intervals, Vertex\-Softmax is therefore pointwise optimal at every\(c,ℓ,u\)\(c,\\ell,u\), not merely worst\-case optimal\.

### B\.4Proof of Proposition[4\.1](https://arxiv.org/html/2605.10974#S4.Thmtheorem1)

###### Proof of Proposition[4\.1](https://arxiv.org/html/2605.10974#S4.Thmtheorem1)\.

Fix an arbitraryx∈𝒳x\\in\\mathcal\{X\}and a rowii\. By \([16](https://arxiv.org/html/2605.10974#S4.E16)\),si​\(x\)∈ℬis\_\{i\}\(x\)\\in\\mathcal\{B\}\_\{i\}, sosi​\(x\)s\_\{i\}\(x\)is feasible for the minimization definingLiL\_\{i\}\. Therefore

Li≤∑j=1Ksoftmax\(si\(x\)\)jzi​jL\.L\_\{i\}\\leq\\sum\_\{j=1\}^\{K\}\\operatorname\{softmax\}\(s\_\{i\}\(x\)\)\_\{j\}z\_\{ij\}^\{L\}\.\(39\)The entries ofsoftmax⁡\(si​\(x\)\)\\operatorname\{softmax\}\(s\_\{i\}\(x\)\)are nonnegative, and by \([17](https://arxiv.org/html/2605.10974#S4.E17)\) we havezi​jL≤zi​j​\(x\)z\_\{ij\}^\{L\}\\leq z\_\{ij\}\(x\)for everyjj\. Multiplying termwise by the softmax weights and summing preserves the inequality:

∑j=1Ksoftmax\(si\(x\)\)jzi​jL≤∑j=1Ksoftmax\(si\(x\)\)jzi​j\(x\)\.\\sum\_\{j=1\}^\{K\}\\operatorname\{softmax\}\(s\_\{i\}\(x\)\)\_\{j\}z\_\{ij\}^\{L\}\\leq\\sum\_\{j=1\}^\{K\}\\operatorname\{softmax\}\(s\_\{i\}\(x\)\)\_\{j\}z\_\{ij\}\(x\)\.\(40\)Combining \([39](https://arxiv.org/html/2605.10974#A2.E39)\) and \([40](https://arxiv.org/html/2605.10974#A2.E40)\),LiL\_\{i\}lower\-bounds the signed row contribution at inputxx\. Summing over rows then gives

LVC\\displaystyle L\_\{\\mathrm\{VC\}\}=b\+∑iLi\\displaystyle=b\+\\sum\_\{i\}L\_\{i\}≤b\+∑i∑j=1Ksoftmax\(si\(x\)\)jzi​j\(x\)≤m\(x\),\\displaystyle\\leq b\+\\sum\_\{i\}\\sum\_\{j=1\}^\{K\}\\operatorname\{softmax\}\(s\_\{i\}\(x\)\)\_\{j\}z\_\{ij\}\(x\)\\leq m\(x\),\(41\)where the last inequality is exactly the margin interface \([14](https://arxiv.org/html/2605.10974#S4.E14)\)\. Sincex∈𝒳x\\in\\mathcal\{X\}was arbitrary,LVC≤m​\(x\)L\_\{\\mathrm\{VC\}\}\\leq m\(x\)throughout𝒳\\mathcal\{X\}\. IfLVC\>0L\_\{\\mathrm\{VC\}\}\>0, thenm​\(x\)\>0m\(x\)\>0for allx∈𝒳x\\in\\mathcal\{X\}, certifying the margin\. ∎

## Appendix CVertex\-CROWN Construction Details

For the architectures used in our experiments, the input image is first mapped to token embeddingsH​\(x\)∈ℝR×dH\(x\)\\in\\mathbb\{R\}^\{R\\times d\}\. For headhh, the queries, keys, and values are affine maps

Qih​\(x\)\\displaystyle Q\_\{i\}^\{h\}\(x\)=WQh​Hi​\(x\)\+bQh,\\displaystyle=W\_\{Q\}^\{h\}H\_\{i\}\(x\)\+b\_\{Q\}^\{h\},\(42\)Kjh​\(x\)\\displaystyle K\_\{j\}^\{h\}\(x\)=WKh​Hj​\(x\)\+bKh,\\displaystyle=W\_\{K\}^\{h\}H\_\{j\}\(x\)\+b\_\{K\}^\{h\},Vjh​\(x\)\\displaystyle V\_\{j\}^\{h\}\(x\)=WVh​Hj​\(x\)\+bVh\.\\displaystyle=W\_\{V\}^\{h\}H\_\{j\}\(x\)\+b\_\{V\}^\{h\}\.The attention score is

si​jh​\(x\)=1dh​⟨Qih​\(x\),Kjh​\(x\)⟩\+μi​jh,s\_\{ij\}^\{h\}\(x\)=\\frac\{1\}\{\\sqrt\{d\_\{h\}\}\}\\langle Q\_\{i\}^\{h\}\(x\),K\_\{j\}^\{h\}\(x\)\\rangle\+\\mu\_\{ij\}^\{h\},\(43\)whereμi​jh\\mu\_\{ij\}^\{h\}is a fixed mask or positional score term\. The experiments compute\[ℓi​jh,ui​jh\]\[\\ell\_\{ij\}^\{h\},u\_\{ij\}^\{h\}\]by applying auto\_LiRPA/CROWN to \([43](https://arxiv.org/html/2605.10974#A3.E43)\)\. A simple fallback is interval product bounding: from scalar boundsqi​rh∈\[q¯i​rh,q¯i​rh\]q\_\{ir\}^\{h\}\\in\[\\underline\{q\}\_\{ir\}^\{h\},\\overline\{q\}\_\{ir\}^\{h\}\]andkj​rh∈\[k¯j​rh,k¯j​rh\]k\_\{jr\}^\{h\}\\in\[\\underline\{k\}\_\{jr\}^\{h\},\\overline\{k\}\_\{jr\}^\{h\}\], set

p¯i​j​rh\\displaystyle\\underline\{p\}\_\{ijr\}^\{h\}=min⁡\{q¯​k¯,q¯​k¯,q¯​k¯,q¯​k¯\},\\displaystyle=\\min\\\{\\underline\{q\}\\,\\underline\{k\},\\underline\{q\}\\,\\overline\{k\},\\overline\{q\}\\,\\underline\{k\},\\overline\{q\}\\,\\overline\{k\}\\\},\(44\)p¯i​j​rh\\displaystyle\\overline\{p\}\_\{ijr\}^\{h\}=max⁡\{q¯​k¯,q¯​k¯,q¯​k¯,q¯​k¯\},\\displaystyle=\\max\\\{\\underline\{q\}\\,\\underline\{k\},\\underline\{q\}\\,\\overline\{k\},\\overline\{q\}\\,\\underline\{k\},\\overline\{q\}\\,\\overline\{k\}\\\},\(45\)where the four products use the corresponding\(i,j,r,h\)\(i,j,r,h\)bounds\. Then

ℓi​jh=μi​jh\+1dh​∑rp¯i​j​rh,ui​jh=μi​jh\+1dh​∑rp¯i​j​rh\\ell\_\{ij\}^\{h\}=\\mu\_\{ij\}^\{h\}\+\\frac\{1\}\{\\sqrt\{d\_\{h\}\}\}\\sum\_\{r\}\\underline\{p\}\_\{ijr\}^\{h\},\\qquad u\_\{ij\}^\{h\}=\\mu\_\{ij\}^\{h\}\+\\frac\{1\}\{\\sqrt\{d\_\{h\}\}\}\\sum\_\{r\}\\overline\{p\}\_\{ijr\}^\{h\}\(46\)is sound\. CROWN/McCormick multiplication relaxations can be substituted; Vertex\-Softmax only needs the certified scalar intervals\.

Let the attention\-residual state after the output projection be

Hi\+​\(x\)\\displaystyle H\_\{i\}^\{\+\}\(x\)=Hi​\(x\)\+bO\+∑hWOh​Oih​\(x\),\\displaystyle=H\_\{i\}\(x\)\+b\_\{O\}\+\\sum\_\{h\}W\_\{O\}^\{h\}O\_\{i\}^\{h\}\(x\),\(47\)Oih​\(x\)\\displaystyle O\_\{i\}^\{h\}\(x\)=∑jai​jh​\(x\)​Vjh​\(x\)\.\\displaystyle=\\sum\_\{j\}a\_\{ij\}^\{h\}\(x\)V\_\{j\}^\{h\}\(x\)\.For a target marginmt​\(x\)m\_\{t\}\(x\), suppose the downstream classifier or CROWN suffix gives an affine lower bound

mt​\(x\)≥βt\+∑iγt​i⊤​Hi\+​\(x\)∀x∈𝒳\.m\_\{t\}\(x\)\\geq\\beta\_\{t\}\+\\sum\_\{i\}\\gamma\_\{ti\}^\{\\top\}H\_\{i\}^\{\+\}\(x\)\\qquad\\forall x\\in\\mathcal\{X\}\.\(48\)Substituting \([47](https://arxiv.org/html/2605.10974#A3.E47)\) produces attention coefficients

ηt​i​h=\(WOh\)⊤​γt​i,ct​i​h​j≤ηt​i​h⊤​Vjh​\(x\)∀x∈𝒳\.\\eta\_\{tih\}=\(W\_\{O\}^\{h\}\)^\{\\top\}\\gamma\_\{ti\},\\qquad c\_\{tihj\}\\leq\\eta\_\{tih\}^\{\\top\}V\_\{j\}^\{h\}\(x\)\\quad\\forall x\\in\\mathcal\{X\}\.\(49\)WhenVjh​\(x\)V\_\{j\}^\{h\}\(x\)is affine in an input boxx∈\[xL,xU\]x\\in\[x^\{L\},x^\{U\}\], the lower bound in \([49](https://arxiv.org/html/2605.10974#A3.E49)\) is

LBx∈\[xL,xU\]⁡\[w⊤​x\+b\]=\(w\+\)⊤​xL\+\(w−\)⊤​xU\+b,\\operatorname\{LB\}\_\{x\\in\[x^\{L\},x^\{U\}\]\}\[w^\{\\top\}x\+b\]=\(w^\{\+\}\)^\{\\top\}x^\{L\}\+\(w^\{\-\}\)^\{\\top\}x^\{U\}\+b,\(50\)withw\+=max⁡\(w,0\)w^\{\+\}=\\max\(w,0\)andw−=min⁡\(w,0\)w^\{\-\}=\\min\(w,0\)\. The non\-attention pieces are gathered into

bt′=βt\+LBx∈𝒳⁡\[∑iγt​i⊤​Hi​\(x\)\+∑iγt​i⊤​bO\]\.b\_\{t\}^\{\\prime\}=\\beta\_\{t\}\+\\operatorname\{LB\}\_\{x\\in\\mathcal\{X\}\}\\left\[\\sum\_\{i\}\\gamma\_\{ti\}^\{\\top\}H\_\{i\}\(x\)\+\\sum\_\{i\}\\gamma\_\{ti\}^\{\\top\}b\_\{O\}\\right\]\.\(51\)The target\-wise Vertex\-CROWN lower bound is

LVC,t=bt′\+∑h,iLbox​\(ct​i​h:,ℓi​h:,ui​h:\)\.L\_\{\\mathrm\{VC\},t\}=b\_\{t\}^\{\\prime\}\+\\sum\_\{h,i\}L\_\{\\mathrm\{box\}\}\\\!\\left\(c\_\{tih:\},\\ell\_\{ih:\},u\_\{ih:\}\\right\)\.\(52\)
###### Proposition C\.1\(Soundness with affine suffix lower bounds\)\.

Fix a target classtt\. Suppose the suffix of an attention block admits a sound affine lower bound \([48](https://arxiv.org/html/2605.10974#A3.E48)\); the attention scores satisfyℓi​jh≤si​jh​\(x\)≤ui​jh\\ell\_\{ij\}^\{h\}\\leq s\_\{ij\}^\{h\}\(x\)\\leq u\_\{ij\}^\{h\}for allx∈𝒳x\\in\\mathcal\{X\}; and the value\-side coefficients satisfy \([49](https://arxiv.org/html/2605.10974#A3.E49)\)\. ThenLVC,tL\_\{\\mathrm\{VC\},t\}in \([52](https://arxiv.org/html/2605.10974#A3.E52)\) is a sound lower bound\. IfLCROWN,tL\_\{\\mathrm\{CROWN\},t\}is any other sound lower bound on the same target margin, thenmax⁡\{LCROWN,t,LVC,t\}\\max\\\{L\_\{\\mathrm\{CROWN\},t\},L\_\{\\mathrm\{VC\},t\}\\\}is sound as well\.

###### Proof\.

Start from \([48](https://arxiv.org/html/2605.10974#A3.E48)\) and substitute \([47](https://arxiv.org/html/2605.10974#A3.E47)\)\. The non\-attention affine terms are lower\-bounded bybt′b\_\{t\}^\{\\prime\}in \([51](https://arxiv.org/html/2605.10974#A3.E51)\)\. For each headhhand rowii, softmax weights are nonnegative and sum to one, so \([49](https://arxiv.org/html/2605.10974#A3.E49)\) gives

∑jai​jh​\(x\)​ηt​i​h⊤​Vjh​\(x\)≥∑jai​jh​\(x\)​ct​i​h​j\.\\sum\_\{j\}a\_\{ij\}^\{h\}\(x\)\\eta\_\{tih\}^\{\\top\}V\_\{j\}^\{h\}\(x\)\\geq\\sum\_\{j\}a\_\{ij\}^\{h\}\(x\)c\_\{tihj\}\.\(53\)The score vectorsih​\(x\)s\_\{i\}^\{h\}\(x\)is feasible for the score box\[ℓi​h:,ui​h:\]\[\\ell\_\{ih:\},u\_\{ih:\}\], so Theorem[3\.2](https://arxiv.org/html/2605.10974#S3.Thmtheorem2)yields

∑jai​jh​\(x\)​ct​i​h​j≥Lbox​\(ct​i​h:,ℓi​h:,ui​h:\)\.\\sum\_\{j\}a\_\{ij\}^\{h\}\(x\)c\_\{tihj\}\\geq L\_\{\\mathrm\{box\}\}\\\!\\left\(c\_\{tih:\},\\ell\_\{ih:\},u\_\{ih:\}\\right\)\.\(54\)Summing over rows and heads recovers \([52](https://arxiv.org/html/2605.10974#A3.E52)\)\. The maximum of two lower bounds on the same scalar margin is again a lower bound\. ∎

Algorithm 3Target\-wise CROWN/Vertex hybrid1:Input:input box

𝒳\\mathcal\{X\}, true class

yy, target set

𝒯=\{t:t≠y\}\\mathcal\{T\}=\\\{t:t\\neq y\\\}
2:foreach target

t∈𝒯t\\in\\mathcal\{T\}do

3:Compute direct CROWN margin lower bound

LCROWN,tL\_\{\\mathrm\{CROWN\},t\}
4:Construct score boxes

\(ℓi​h:,ui​h:\)\(\\ell\_\{ih:\},u\_\{ih:\}\)for all rows and heads

5:Construct suffix affine lower bound

\(βt,γt\)\(\\beta\_\{t\},\\gamma\_\{t\}\)over

H\+H^\{\+\}
6:Convert

γt\\gamma\_\{t\}to value coefficients

ct​i​h​jc\_\{tihj\}using \([49](https://arxiv.org/html/2605.10974#A3.E49)\)

7:

LVC,t←bt′\+∑h,iLbox​\(ct​i​h:,ℓi​h:,ui​h:\)L\_\{\\mathrm\{VC\},t\}\\leftarrow b\_\{t\}^\{\\prime\}\+\\sum\_\{h,i\}L\_\{\\mathrm\{box\}\}\(c\_\{tih:\},\\ell\_\{ih:\},u\_\{ih:\}\)
8:

Lhyb,t←max⁡\{LCROWN,t,LVC,t\}L\_\{\\mathrm\{hyb\},t\}\\leftarrow\\max\\\{L\_\{\\mathrm\{CROWN\},t\},L\_\{\\mathrm\{VC\},t\}\\\}
9:endfor

10:returncertified iff

mint∈𝒯⁡Lhyb,t\>0\\min\_\{t\\in\\mathcal\{T\}\}L\_\{\\mathrm\{hyb\},t\}\>0

## Appendix DNumerical Evaluation and Certificate Soundness

The exactness statements are real\-arithmetic statements\. The optimized implementation used in our experiments evaluates Algorithm[1](https://arxiv.org/html/2605.10974#alg1)with standard floating\-point PyTorch operations, including the stability shifta=maxj⁡uja=\\max\_\{j\}u\_\{j\}\. This is the usual implementation path for empirically comparing verifier bounds, but it is not by itself a proof\-carrying floating\-point certificate\.

For proof\-producing use, the sameK\+1K\+1threshold structure can be evaluated conservatively with outward\-rounded interval arithmetic\. After the stability shift, compute intervalsL^j\\widehat\{L\}\_\{j\}andU^j\\widehat\{U\}\_\{j\}enclosingexp⁡\(ℓj−a\)\\exp\(\\ell\_\{j\}\-a\)andexp⁡\(uj−a\)\\exp\(u\_\{j\}\-a\)\. For each thresholdmm, form interval enclosures for

Nm\\displaystyle N\_\{m\}=∑j≤mc\(j\)​U\(j\)\+∑j\>mc\(j\)​L\(j\),\\displaystyle=\\sum\_\{j\\leq m\}c\_\{\(j\)\}U\_\{\(j\)\}\+\\sum\_\{j\>m\}c\_\{\(j\)\}L\_\{\(j\)\},\(55\)Dm\\displaystyle D\_\{m\}=∑j≤mU\(j\)\+∑j\>mL\(j\)\.\\displaystyle=\\sum\_\{j\\leq m\}U\_\{\(j\)\}\+\\sum\_\{j\>m\}L\_\{\(j\)\}\.\(56\)BecauseDm\>0D\_\{m\}\>0, interval division yields an enclosure\[τ¯m,τ¯m\]\[\\underline\{\\tau\}\_\{m\},\\overline\{\\tau\}\_\{m\}\]of the exact threshold value\. Then

L¯box=minm=0,…,K⁡τ¯m≤Lbox​\(c,ℓ,u\)\\underline\{L\}\_\{\\mathrm\{box\}\}=\\min\_\{m=0,\\ldots,K\}\\underline\{\\tau\}\_\{m\}\\leq L\_\{\\mathrm\{box\}\}\(c,\\ell,u\)\(57\)is a conservative lower bound for the score\-box subproblem\. A high\-precision reference implementation based on PythonDecimalarithmetic with outward padding is provided in the supplementary material\. The reported GPU certified rates and lower bounds use the faster PyTorch implementation unless explicitly marked as interval\-certified\.

## Appendix EAdditional Experimental Evidence

This appendix collects the supporting evidence behind the main experimental claims\. To help navigate the material, here is a brief guide to what each subsection addresses and the key tables within it:

- •Protocol and numerical status\(Tables[6](https://arxiv.org/html/2605.10974#A5.T6)–[7](https://arxiv.org/html/2605.10974#A5.T7)\): Can these results be reproduced, and are the floating\-point outputs trustworthy?
- •GaLileo\-style baseline\(Table[8](https://arxiv.org/html/2605.10974#A5.T8)\): How does Vertex\-Softmax compare to the closest prior method on the same score\-box problem?
- •Solver correctness and slack\(Tables[9](https://arxiv.org/html/2605.10974#A5.T9)–[10](https://arxiv.org/html/2605.10974#A5.T10)\): Does theK\+1K\{\+\}1threshold solver match brute\-force enumeration, and once softmax is solved exactly, where does the remaining looseness come from?
- •Runtime accounting\(Table[11](https://arxiv.org/html/2605.10974#A5.T11)\): Is the hybrid verifier too expensive relative to direct CROWN?
- •Paired improvements and stability\(Tables[12](https://arxiv.org/html/2605.10974#A5.T12)–[13](https://arxiv.org/html/2605.10974#A5.T13)\): Are the gains broad\-based across images, and do they hold across training seeds?
- •Strong\-baseline details\(Tables[14](https://arxiv.org/html/2605.10974#A5.T14)–[15](https://arxiv.org/html/2605.10974#A5.T15)\): Full per\-trial comparisons with alpha\-CROWN and ABCrown\-BaB\.

### E\.1Protocol and numerical status

A natural concern with any verifier comparison is whether the evaluation is fair and the floating\-point outputs are trustworthy\. Table[6](https://arxiv.org/html/2605.10974#A5.T6)records the evaluation protocol, denominators, and hardware for each benchmark so that results can be reproduced\. Table[7](https://arxiv.org/html/2605.10974#A5.T7)addresses numerical soundness: it separates the proof\-producing interval\-oracle checks for the Vertex\-Softmax primitive from the standard floating\-point verifier outputs used for GPU\-scale experiments\.

Table 6:Experiment protocol summary\. All image inputs use clipped pixelℓ∞\\ell\_\{\\infty\}boxes in\[0,1\]\[0,1\]\. Unless otherwise noted, score boxes are computed via auto\_LiRPA/CROWN on the scalar score module, and all reported certificates are standard floating\-point verifier outputs\. Hardware is RTX 5090 except where marked “mixed\.” For learned patch\-attention rows and conditional appendix rows, the listedNNis the number of clean\-correct examples selected for certification per seed\. For the Fashion/CIFAR full\-block certificates in Table[5](https://arxiv.org/html/2605.10974#S5.T5),NNis the first 100 evaluation examples per seed and clean\-incorrect examples are counted as uncertified\. Synthetic rows compute rates over all listed trials\.BenchmarkScore / suffix methodSeedsNN/ seedClean acc\.Synthetic score boxesScalable sweepinterval\-product; no learned suffix3200 trialsn/aα\\alpha/ABCrown blockssynthetic blocks; CROWN score boxes3selectedn/aLearned patch\-attention modelsMNIST binary, 16 tok\.CROWN; linear classifier310000\.992MNIST binary, 49 tok\.CROWN; linear classifier25000\.993MNIST 10\-class, 16 tok\.CROWN; linear classifier35000\.875Residual MHACROWN; output proj\. \+ linear35000\.998Full attention–residual–MLP blocksMNIST blockCROWN; target\-wise suffix overH\+H^\{\+\}3–52000\.749Fashion\-MNIST blockCROWN; target\-wise suffix overH\+H^\{\+\}5100 eval0\.708/0\.672†CIFAR\-10 gray blockCROWN; target\-wise suffix overH\+H^\{\+\}5100 eval0\.346†0\.708 ford=32,h=4d\{=\}32,h\{=\}4; 0\.672 ford=16,h=2d\{=\}16,h\{=\}2\. ABCrown\-BaB uses a fixed 600s per\-instance budget\.Runtime claims use RTX 5090 rows only; Fashion/CIFAR rows use mixed GPUs\.Table 7:Numerical status checks\. The oracle interval rows validate the Vertex\-Softmax threshold primitive itself\. The Fashion\-MNIST rows use the exact evaluation\-denominator full\-block rerun atϵ=0\.02\\epsilon=0\.02: FP cert\. is counted over 500 evaluation examples, while near\-zero counts inspect the clean\-correct margins that were actually bounded\. These checks do not on their own constitute end\-to\-end outward\-rounded LiRPA certificates\.The interval\-oracle checks confirm that the Vertex\-Softmax primitive produces correct results to within numerical tolerance\. For the GPU\-scale experiments, no certified margins fall in the near\-zero band where floating\-point rounding could flip a certification decision\.

### E\.2GaLileo\-style implementation baseline

Table[8](https://arxiv.org/html/2605.10974#A5.T8)reports the GaLileo\-style implementation baseline forK≤16K\\leq 16\. Because the original GaLileo code is not publicly available, these results are from our independent reimplementation and are reported only as an implementation baseline, not as an official reproduction\. Vertex\-Softmax is tighter in every tested case\.

Table 8:GaLileo\-style implementation baseline atϵ=0\.02\\epsilon=0\.02, three seeds, 600 trials per row\. These results are from our independent reimplementation \(original code not publicly available\)\.
### E\.3Exact solver and slack diagnostics

Two questions arise about the Vertex\-Softmax primitive: does theK\+1K\+1threshold solver actually match exhaustive enumeration, and once it solves the softmax subproblem exactly, how much looseness remains from other sources? Table[9](https://arxiv.org/html/2605.10974#A5.T9)addresses the first: the threshold solver agrees with exhaustive search to within5×10−75\\times 10^\{\-7\}for all testedKK, while running orders of magnitude faster atK≥16K\\geq 16\. Table[10](https://arxiv.org/html/2605.10974#A5.T10)addresses the second by decomposing the total verification gap on controlled tiny instances into its constituent sources\.

![Refer to caption](https://arxiv.org/html/2605.10974v1/x3.png)Figure 4:Runtime scaling for the exact Vertex\-Softmax threshold solver\. Exhaustive enumeration is shown only where feasible\.Table 9:Threshold solver exactness and runtime\. Exhaustive enumeration is shown only where feasible\.Table 10:Slack\-decomposition diagnostics on controlled tiny instances\. Entries are mean lower\-bound gaps over random seeds; larger values mean more looseness from that source\. The softmax gap is Vertex\-Softmax minus Wei\-LSE on the same score boxes\. Grid\-based gaps use a dense two\-dimensional input grid and are diagnostics rather than proof\-producing certificates\.The slack decomposition confirms that once the softmax subproblem is solved exactly, the dominant remaining sources of looseness are value\-bound slack and, when present, suffix relaxation\. This supports the claim that Vertex\-Softmax removes the most accessible source of avoidable looseness at the score\-box interface\.

### E\.4Runtime accounting

A practical concern is whether the Vertex\-CROWN hybrid is too expensive relative to direct CROWN\. Table[11](https://arxiv.org/html/2605.10974#A5.T11)breaks down the wall time for the full\-block MNIST setting\. The Vertex\-Softmax sort/sweep itself is negligible \(0\.02%0\.02\\%of total time\); the cost of the hybrid comes almost entirely from constructing the score, value, and suffix bounds that feed into the oracle\.

Table 11:Coarse runtime accounting for the RTX 5090 full\-block MNIST settingd=32,h=4,m=64,ϵ=0\.02d=32,h=4,m=64,\\epsilon=0\.02\. Direct CROWN, Vertex path, and Hybrid totals are averaged over three seed runs with 200 certified images per seed\. The Vertex\-Softmax sort/sweep entry is estimated by scaling the measuredK=16K=16threshold microbenchmark to99targets,44heads, and1616query rows; the remaining Vertex\-path time is therefore attributed to score, value, and suffix\-bound construction\.
### E\.5Paired improvements and seed\-resampling stability

The main\-text tables report aggregate certified rates and mean lower bounds\. Here we ask two finer\-grained questions: does the hybrid improve bounds on most individual images \(not just on average\), and are the headline improvements stable across training seeds?

Table[12](https://arxiv.org/html/2605.10974#A5.T12)reports paired improvements from the same exact evaluation\-denominator reruns as Table[5](https://arxiv.org/html/2605.10974#S5.T5)\. Atϵ=0\.02\\epsilon=0\.02on Fashion\-MNIST, the hybrid improves the lower bound on99\.7%99\.7\\%of clean\-correct evaluated images, with a median improvement of4\.264\.26points, confirming that the gains are broad\-based rather than driven by a few outliers\. Table[13](https://arxiv.org/html/2605.10974#A5.T13)gives seed\-resampling intervals for the main certified\-rate improvements\. Because several rows have only two or three seeds, these intervals are descriptive stability checks rather than formal significance tests; nonetheless, the resampled intervals are comfortably above zero in every case\.

Table 12:Paired lower\-bound improvements for the non\-MNIST full\-block rows from the exact evaluation\-denominator reruns\. MeanΔ\\Deltais seed\-averaged to match Table[5](https://arxiv.org/html/2605.10974#S5.T5); medianΔ\\Deltaand fraction improved are computed over the clean\-correct evaluated images whose margins were bounded\.Table 13:Seed\-resampling stability checks for selected certified\-rate improvements using stored summaries\. Rows marked e2e use exact evaluation\-denominator rates; the remaining learned image\-model rows use conditional rates on clean\-correct certification subsets\. The intervals are percentile resampling intervals over training/evaluation seeds; rows with two or three seeds should be read as descriptive stability checks rather than formal significance tests\.
### E\.6Strong\-baseline details

The main text reports that Vertex\-CROWN is competitive with alpha\-CROWN and outperforms ABCrown\-BaB in selected settings\. Tables[14](https://arxiv.org/html/2605.10974#A5.T14)and[15](https://arxiv.org/html/2605.10974#A5.T15)provide the full per\-trial details behind those claims\.

Table[14](https://arxiv.org/html/2605.10974#A5.T14)shows paired diagnostics: on the two settings where Vertex\-CROWN most clearly outperforms alpha\-CROWN \(K=4,d=16,ϵ=0\.05K=4,d=16,\\epsilon=0\.05andK=4,d=32,ϵ=0\.03K=4,d=32,\\epsilon=0\.03\), Vertex\-CROWN produces a higher lower bound on2121–2323out of2424trials\. The “V\-only” column shows instances certified only by Vertex\-CROWN and not by alpha\-CROWN; in both settings, Vertex\-CROWN certifies several instances that alpha\-CROWN misses, while the reverse is rare\. Table[15](https://arxiv.org/html/2605.10974#A5.T15)consolidates the full certified rates, lower bounds, and runtimes across all tested settings and methods, including the residual\-MHA block where alpha\-CROWN’s optimizable slopes give it an advantage atϵ=0\.03\\epsilon=0\.03but not atϵ=0\.05\\epsilon=0\.05\.

Table 14:Paired strong\-baseline diagnostics from the long\-budget small\-attention detail CSVs\. Alpha\-CROWN and Vertex\-CROWN lower bounds are compared on the same trials\. ABCrown\-BaB reports status under a 600 second per\-instance budget; unknown, OOM, and internal\-error outcomes are counted as uncertified\.Table 15:Selected strong\-baseline results used in Figure[3](https://arxiv.org/html/2605.10974#S5.F3)\. ABCrown\-BaB uses a 600 second per\-instance budget and reports status, so no scalar lower bound is shown for those rows\. Residual\-MHA rows use the residual multi\-head block from the main comparison\.