@entry{bon-dim-baa-vec-21-aa-deept,
  author = {Bonaert, Gregory and Dimitrov, Dimitar I. and Baader, Maximilian and Vechev, Martin},
  title = {Fast and Precise Certification of Transformers},
  journal = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)},
  month = jun,
  pages = {466–481},
  doi = {10.1145/3453483.3454056},
  year = 2021,
  comment = {Uses AA, that they call zonotope. The ``transformers'' are NOT electrical transformers but some AI or neural network thing.},
  abstract = {We present DeepT, a novel method for certifying Transformer networks based on abstract interpretation. The key idea behind DeepT is our new Multi-norm Zonotope abstract domain, an extension of the classical Zonotope designed to handle $\ell_1$ and $\ell_2$-norm bound perturbations. We introduce all Multi-norm Zonotope abstract transformers necessary to handle these complex networks, including the challenging softmax function and dot product. Our evaluation shows that DeepT can certify average robustness radii that are 28$\times$ larger than the state-of-the-art, while scaling favorably. Further, for the first time, we certify Transformers against synonym attacks on long sequences of words, where each word can be replaced by any synonym. DeepT achieves a high certification success rate on sequences of words where enumeration-based verification would take 2 to 3 orders of magnitude more time.}
}