顶点 Softmax：通过精确 Softmax 优化实现紧密的 Transformer 验证
机器学习
2026-05-13 v1 人工智能
摘要
Transformer 注意力的认证验证需要对预 Softmax 分数施加区间约束下的 Softmax 函数进行上界。现有验证器对 Softmax 进行松弛，且不依赖于下游目标，留下了可避免的间隙。我们证明了该得分盒问题的确切最优点位于约束盒的顶点，并建立了一个阈值结构定理表明，经过排序目标系数后，最优解仅包含线性数量的候选者，由此得到 Vertex-Softmax 原语，其在序列长度上的复杂度为对数线性。我们进一步证明了 Vertex-Softmax 是从得分区间alone 可获得的最紧致的 sound 边界，精确描述了为获得进一步改进所需的额外结构（得分相关性、得分-值耦合）。集成到基于 CROWN 凸松弛优化的最差神经元式验证器中，Vertex-Softmax 在 MNIST、Fashion-MNIST 和 CIFAR-10 注意力模型上显著提高了认证通过率，大幅紧缩了下界，而在保持成本低廉的同时持续匹配或超越 alpha-CROWN 和分支定界基线。
引用
@article{arxiv.2605.10974,
title = {Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization},
author = {Navid Rezazadeh and Arash Gholami Davoodi},
journal= {arXiv preprint arXiv:2605.10974},
year = {2026}
}