提出精确计算注意力分数上界的方法，显著提升模型验证精度。
Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization
- 发现最优解必在约束盒的顶点处，提出高效顶点搜索算法。
- 在多个数据集上验证率大幅提升，下界紧致性优于现有方法。
- 适合关注深度模型安全验证的研究者与工程师使用。
Transformer注意力的可认证验证需要对预得分区间上的softmax函数进行边界估计。现有方法独立于下游目标松弛softmax，导致不必要的松弛。本文证明该分数盒问题的精确最优解出现在约束盒的顶点上，并建立阈值结构定理：排序目标系数后，最优解仅需在线性数量候选中搜索，由此提出具有序列长度对数线性复杂度的Vertex-Softmax原语。进一步证明其为仅基于分数区间所能获得的最紧致有保证边界，明确指出需引入分数相关性或分数-值耦合等额外结构才能进一步改进。将Vertex-Softmax集成至基于CROWN凸松弛的验证器（类似Worst-case Neurons优化），在MNIST、Fashion-MNIST和CIFAR-10的注意力模型上显著提升认证率并大幅收紧下界，同时以远低于alpha-CROWN和分支定界基线的成本保持或超越其性能。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。