Threshold-Mass CROWN: Direction-Dependent Softmax Bounds for Transformer Verification

Attention is difficult to bound because its weights change together: increasing one score changes the probability assigned to every token. A robustness verifier must account for these interactions and their effect on the network's output. We introduce Threshold-Mass CROWN, which uses the coefficients supplied by backward verification to bound a weighted sum of attention probabilities as a whole. The method sorts tokens by these coefficients and bounds the total attention assigned to tokens above each cutoff in the ordering. These bounds combine into one affine function of the attention scores. Propagating this function toward the input can preserve relationships between scores that independent score ranges discard. We prove that this affine function is a lower bound throughout the allowed score ranges. For an attention row with $K$ tokens, sorting and cumulative sums take $O(K\log K)$ time and $O(K)$ working storage per coefficient vector. Across five independently trained one-block models, Threshold-Mass certifies 103 of 500 examples, compared with 49 for the CROWN-LSE baseline, at additional runtime cost. On a 200-property transformer benchmark, it certifies 143 properties. A control that performs the same additional calculation but returns the baseline bound certifies 127. The results show that retaining score relationships can improve certification, although stronger attention bounds alone remain insufficient for some more demanding architectures.