Convex Bounds on the Softmax Function with Applications to Robustness Verification

TL;DR

This paper introduces convex bounds on the softmax function to improve robustness verification of neural networks, especially transformers, by enabling more accurate convex optimization formulations.

Contribution

It provides new convex lower and upper bounds on the softmax function using exponential-reciprocal and log-sum-exp decompositions, improving over previous linear bounds.

Findings

Bounds are tighter than previous linear bounds.

Bounds are applicable to transformer verification.

Bounds improve robustness and uncertainty estimation.

Abstract

The softmax function is a ubiquitous component at the output of neural networks and increasingly in intermediate layers as well. This paper provides convex lower bounds and concave upper bounds on the softmax function, which are compatible with convex optimization formulations for characterizing neural networks and other ML models. We derive bounds using both a natural exponential-reciprocal decomposition of the softmax as well as an alternative decomposition in terms of the log-sum-exp function. The new bounds are provably and/or numerically tighter than linear bounds obtained in previous work on robustness verification of transformers. As illustrations of the utility of the bounds, we apply them to verification of transformers as well as of the robustness of predictive uncertainty estimates of deep ensembles.