Precise Transformer Verification via ReLU-Catalyzed Abstraction Refinement

The research proposes using ReLU-catalyzed abstraction refinement to improve the precision of Transformer formal verification: representing the nonlinear boundary of the dot product with ReLU, then deriving exact output ranges with the aid of existing ReLU convex relaxations, and extending both rule-based and optimization-based methods into two verification frameworks. On robustness properties derived from two sentiment analysis datasets, compared against different model architectures and state-of-the-art baselines, precision improves significantly on most verification tasks, with an acceptable decrease in efficiency.