Vertex-Softmax：通过精确 Softmax 优化进行严格变压器验证

arXiv:2605.10974v1 公告类型：新 摘要：变压器注意力的认证验证需要将 softmax 函数限制在 pre-softmax 分数的区间约束上。现有的验证者独立于下游目标放松了 softmax，留下了可以避免的松弛。我们证明了这个分数框问题的精确最优值是在约束框的顶点处获得的，并建立了一个阈值结构定理，表明在对目标系数进行排序后，最优值仅存在于线性多个候选者中，从而产生在序列长度上具有对数线性复杂度的 Vertex-Softmax 原语。我们进一步证明了形式最优性结果，表明 Vertex-Softmax 是仅从分数区间即可获得的最紧密的声音界限，准确地描述了进一步改进需要哪些附加结构（分数相关性、分数值耦合）。 Vertex-Softmax 集成到具有正式稳健性保证的基于 CROWN 凸松弛（针对最坏情况神经元的优化）式验证器中，显着提高了认证率，并大幅收紧了 MNIST、Fashion-MNIST 和 CIFAR-10 注意力模型的下限，同时以一小部分成本始终匹配或优于 alpha-CROWN 和分支定界基线。