Input-relational Verification of Transformers

Transformers have been driving significant advances across a wide range of applications, yet their deployment in safety-critical domains require rigorous formal verification. Most existing verification techniques are designed to assess perturbation tolerance around individual inputs and are therefore insufficient to ensure model robustness in a global context. To address this limitation, we first propose a self-composition-based approach that enables end-to-end application of local verification techniques. However, due to the complexity of the composed model, this approach turns out to exacerbate the approximation error of local verifiers significantly. In this paper, we show that exploiting cross-execution relationships in intermediate layers can substantially improve verification precision. Specifically, we construct McCormick envelopes for the cross-execution differences of attention-layer and propagate these relational constraints to the output layer, yielding tighter output bounds. We implement this approach in a tool, $\text{ReVerT}$, and develop two variants that prioritize efficiency and precision, respectively, to accommodate different verification requirements. We evaluate the approach on CCPP for regression and on Yelp and SST for classification. Across these benchmarks, the proposed methods produce tighter certified output bounds and certify more instances than the naive self-composition and the generic difference propagation, showing that our reasoning of the cross-execution differences is effective for achieving precise input-relational verification of Transformers.