{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:06:30Z","timestamp":1784797590664,"version":"3.55.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Formal verification of transformers has become increasingly important due to their widespread deployment in safety-critical applications. Compared to classic neural networks, the inferences of transformers involve highly complex computations, such as dot products in self-attention layers, rendering their verification extremely difficult. Existing approaches explored over-approximation methods by constructing convex constraints to bound the output ranges of transformers, which can achieve high efficiency. However, they may sacrifice verification precision, and consequently introduce significant approximation error that leads to frequent occurrences of false alarms. In this paper, we propose a transformer verification approach that can achieve improved precision. At the core of our approach is a novel usage of ReLU, by which we represent a precise but non-linear bound for dot products such that we can further exploit the rich body of literature for convex relaxation of ReLU to derive precise bounds. We extend two classic approaches to the context of transformers, a rule-based one and an optimization-based one, resulting in two new frameworks for efficient and precise verification. We evaluate our approaches on different model architectures and robustness properties derived from two datasets about sentiment analysis, and compare with the state-of-the-art baseline approach. Compared to the baseline, our approach can achieve significant precision improvement for most of the verification tasks with acceptable compromise of efficiency, which demonstrates the effectiveness of our approach.<\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_25","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:47:27Z","timestamp":1784796447000},"page":"527-550","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Precise Verification of\u00a0Transformers Through ReLU-Catalyzed Abstraction Refinement"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-5820-1168","authenticated-orcid":false,"given":"Hengjie","family":"Liu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3854-9846","authenticated-orcid":false,"given":"Zhenya","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8083-4352","authenticated-orcid":false,"given":"Jianjun","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"25_CR1","doi-asserted-by":"publisher","unstructured":"Alzantot, M., Sharma, Y., Elgohary, A., Ho, B.J., Srivastava, M., Chang, K.W.: Generating natural language adversarial examples. In: Riloff, E., Chiang, D., Hockenmaier, J., Tsujii, J. (eds.) Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing, pp. 2890\u20132896. Association for Computational Linguistics, Brussels, Belgium (2018). https:\/\/doi.org\/10.18653\/v1\/D18-1316","DOI":"10.18653\/v1\/D18-1316"},{"key":"25_CR2","doi-asserted-by":"publisher","unstructured":"Bhargava, P., Drozd, A., Rogers, A.: Generalization in NLI: ways (not) to go beyond simple heuristics. In: Sedoc, J., Rogers, A., Rumshisky, A., Tafreshi, S. (eds.) Proceedings of the Second Workshop on Insights from Negative Results in NLP, pp. 125\u2013135. Association for Computational Linguistics, Online and Punta Cana, Dominican Republic (2021). https:\/\/doi.org\/10.18653\/v1\/2021.insights-1.18","DOI":"10.18653\/v1\/2021.insights-1.18"},{"key":"25_CR3","doi-asserted-by":"publisher","unstructured":"Bonaert, G., Dimitrov, D.I., Baader, M., Vechev, M.: Fast and precise certification of transformers. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pp. 466\u2013481. Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3453483.3454056","DOI":"10.1145\/3453483.3454056"},{"key":"25_CR4","doi-asserted-by":"publisher","unstructured":"Boudardara, F., Boussif, A., Meyer, P.J., Ghazel, M.: A review of abstraction methods toward verifying neural networks. ACM Trans. Embed. Comput. Syst. 23(4) (2024). https:\/\/doi.org\/10.1145\/3617508","DOI":"10.1145\/3617508"},{"key":"25_CR5","doi-asserted-by":"publisher","unstructured":"Brix, C., Bak, S., Johnson, T.T., Wu, H.: The fifth international verification of neural networks competition (VNN-COMP 2024): summary and results. arXiv preprint arXiv:2412.19985 (2024). https:\/\/doi.org\/10.48550\/arXiv.2412.19985","DOI":"10.48550\/arXiv.2412.19985"},{"issue":"3","key":"25_CR6","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10009-023-00703-4","volume":"25","author":"C Brix","year":"2023","unstructured":"Brix, C., M\u00fcller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the international verification of neural networks competition (VNN-COMP). Int. J. Softw. Tools Technol. Transf. 25(3), 329\u2013339 (2023). https:\/\/doi.org\/10.1007\/s10009-023-00703-4","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"25_CR7","unstructured":"Bunel, R., Turkaslan, I., Torr, P.H.S., Kumar, M.P., Lu, J., Kohli, P.: Branch and bound for piecewise linear neural network verification. J. Mach. Learn. Res. 21(1) (2020). https:\/\/jmlr.org\/papers\/volume21\/19-468\/19-468.pdf"},{"key":"25_CR8","doi-asserted-by":"publisher","unstructured":"Casadio, M., et al.: ANTONIO: towards a systematic method of generating NLP benchmarks for verification. In: Narodytska, N., Amir, G., Katz, G., Isac, O. (eds.) Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems. Kalpa Publications in Computing, vol.\u00a016, pp. 59\u201370. EasyChair (2023). https:\/\/doi.org\/10.29007\/7wxb","DOI":"10.29007\/7wxb"},{"issue":"1","key":"25_CR9","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1017\/S0956792525000099","volume":"37","author":"M Casadio","year":"2026","unstructured":"Casadio, M., et al.: NLP verification: towards a general methodology for certifying robustness. Eur. J. Appl. Math. 37(1), 180\u2013237 (2026). https:\/\/doi.org\/10.1017\/S0956792525000099","journal-title":"Eur. J. Appl. Math."},{"key":"25_CR10","doi-asserted-by":"publisher","unstructured":"Chiang, C.H., Lee, H.Y.: Are synonym substitution attacks really synonym substitution attacks? In: Rogers, A., Boyd-Graber, J., Okazaki, N. (eds.) Findings of the Association for Computational Linguistics: ACL 2023, pp. 1853\u20131878. Association for Computational Linguistics, Toronto, Canada (2023). https:\/\/doi.org\/10.18653\/v1\/2023.findings-acl.117","DOI":"10.18653\/v1\/2023.findings-acl.117"},{"key":"25_CR11","doi-asserted-by":"publisher","unstructured":"Devlin, J., Chang, M.W., Lee, K., Toutanova, K.: BERT: pre-training of deep bidirectional transformers for language understanding. In: Burstein, J., Doran, C., Solorio, T. (eds.) Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short Papers), pp. 4171\u20134186. Association for Computational Linguistics, Minneapolis, Minnesota (2019). https:\/\/doi.org\/10.18653\/v1\/N19-1423","DOI":"10.18653\/v1\/N19-1423"},{"key":"25_CR12","doi-asserted-by":"publisher","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy (SP), pp. 3\u201318 (2018). https:\/\/doi.org\/10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"25_CR13","doi-asserted-by":"publisher","unstructured":"Jiao, X., et al.: TinyBERT: distilling BERT for natural language understanding. In: Cohn, T., He, Y., Liu, Y. (eds.) Findings of the Association for Computational Linguistics: EMNLP 2020, pp. 4163\u20134174. Association for Computational Linguistics, Online (2020). https:\/\/doi.org\/10.18653\/v1\/2020.findings-emnlp.372","DOI":"10.18653\/v1\/2020.findings-emnlp.372"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"25_CR15","doi-asserted-by":"publisher","unstructured":"Katz, S.M., Corso, A.L., Strong, C.A., Kochenderfer, M.J.: Verification of image-based neural network controllers using generative models. In: 2021 IEEE\/AIAA 40th Digital Avionics Systems Conference (DASC), pp. 1\u201310 (2021). https:\/\/doi.org\/10.1109\/DASC52595.2021.9594360","DOI":"10.1109\/DASC52595.2021.9594360"},{"key":"25_CR16","doi-asserted-by":"publisher","unstructured":"Kaulen, K., et\u00a0al.: The 6th international verification of neural networks competition (VNN-COMP 2025): summary and results. arXiv preprint arXiv:2512.19007 (2025). https:\/\/doi.org\/10.48550\/arXiv.2512.19007","DOI":"10.48550\/arXiv.2512.19007"},{"key":"25_CR17","unstructured":"K\u00f6nig, M., Bosman, A.W., Hoos, H.H., van Rijn, J.N.: Critically assessing the state of the art in neural network verification. J. Mach. Learn. Res. 25(12), 1\u201353 (2024). http:\/\/jmlr.org\/papers\/v25\/23-0119.html"},{"key":"25_CR18","doi-asserted-by":"publisher","unstructured":"Liao, B.H.C., Cheng, C.H., Esen, H., Knoll, A.: Are transformers more robust? Towards exact robustness verification for transformers. In: Computer Safety, Reliability, and Security: 42nd International Conference, SAFECOMP 2023, Toulouse, France, 20\u201322 September 2023, Proceedings, pp. 89\u2013103. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-40923-3_8","DOI":"10.1007\/978-3-031-40923-3_8"},{"issue":"3\u20134","key":"25_CR19","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1561\/2400000035","volume":"4","author":"C Liu","year":"2021","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. Found. Trends Optim. 4(3\u20134), 244\u2013404 (2021). https:\/\/doi.org\/10.1561\/2400000035","journal-title":"Found. Trends Optim."},{"key":"25_CR20","doi-asserted-by":"publisher","unstructured":"Liu, H., Zhang, Z., Zhao, J.: Precise verification of transformers through ReLU-catalyzed abstraction refinement. Ext. Version (2026). https:\/\/doi.org\/10.48550\/arXiv.2605.14294. Available as an extended version with appendix","DOI":"10.48550\/arXiv.2605.14294"},{"key":"25_CR21","doi-asserted-by":"publisher","unstructured":"Liu, H., Zhang, Z., Zhao, J.: Precise verification of transformers through ReLU-catalyzed abstraction refinement (2026). https:\/\/doi.org\/10.5281\/zenodo.19841667","DOI":"10.5281\/zenodo.19841667"},{"key":"25_CR22","doi-asserted-by":"publisher","unstructured":"Samanta, S., Mehta, S.: Towards crafting text adversarial samples (2017). https:\/\/doi.org\/10.48550\/arXiv.1707.02812","DOI":"10.48550\/arXiv.1707.02812"},{"key":"25_CR23","doi-asserted-by":"publisher","unstructured":"Shi, Z., Jin, Q., Kolter, Z., Jana, S., Hsieh, C.J., Zhang, H.: Neural network verification with branch-and-bound for general nonlinearities. In: Tools and Algorithms for the Construction and Analysis of Systems: 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, 3\u20138 May 2025, Proceedings, Part I, pp. 315\u2013335. Springer, Heidelberg (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_17","DOI":"10.1007\/978-3-031-90643-5_17"},{"key":"25_CR24","unstructured":"Shi, Z., Zhang, H., Chang, K.W., Huang, M., Hsieh, C.J.: Robustness verification for transformers. In: International Conference on Learning Representations (2020). https:\/\/openreview.net\/forum?id=BJxwPJHFwS"},{"key":"25_CR25","doi-asserted-by":"publisher","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290354","DOI":"10.1145\/3290354"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Socher, R., et al.: Recursive deep models for semantic compositionality over a sentiment treebank. In: Yarowsky, D., Baldwin, T., Korhonen, A., Livescu, K., Bethard, S. (eds.) Proceedings of the 2013 Conference on Empirical Methods in Natural Language Processing, pp. 1631\u20131642. Association for Computational Linguistics, Seattle, Washington, USA (2013). https:\/\/aclanthology.org\/D13-1170\/","DOI":"10.18653\/v1\/D13-1170"},{"key":"25_CR27","unstructured":"Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, 6\u20139 May 2019. OpenReview.net (2019). https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"25_CR28","unstructured":"Vaswani, A., et al.: Attention is all you need. In: Guyon, I., et al. (eds.) Advances in Neural Information Processing Systems, vol.\u00a030. Curran Associates, Inc. (2017). https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2017\/file\/3f5ee243547dee91fbd053c1c4a845aa-Paper.pdf"},{"key":"25_CR29","doi-asserted-by":"publisher","unstructured":"Wegmann, A., Nguyen, D., Jurgens, D., Che, W., Nabende, J., Shutova, E.: Tokenization is sensitive to language variation. In: Pilehvar, M.T. (ed.) Findings of the Association for Computational Linguistics: ACL 2025, pp. 10958\u201310983. Association for Computational Linguistics, Vienna, Austria (2025). https:\/\/doi.org\/10.18653\/v1\/2025.findings-acl.572","DOI":"10.18653\/v1\/2025.findings-acl.572"},{"key":"25_CR30","unstructured":"Wei, D., Wu, H., Wu, M., Chen, P.Y., Barrett, C., Farchi, E.: Convex bounds on the softmax function with applications to robustness verification. In: Ruiz, F., Dy, J., van\u00a0de Meent, J.W. (eds.) Proceedings of The 26th International Conference on Artificial Intelligence and Statistics. Proceedings of Machine Learning Research, vol.\u00a0206, pp. 6853\u20136878. PMLR (2023). https:\/\/proceedings.mlr.press\/v206\/wei23c.html"},{"key":"25_CR31","unstructured":"Weng, L., et al.: Towards fast computation of certified robustness for ReLU networks. In: Dy, J., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol.\u00a080, pp. 5276\u20135285. PMLR (2018). https:\/\/proceedings.mlr.press\/v80\/weng18a.html"},{"key":"25_CR32","unstructured":"Xiao, T., Zhu, J.: Introduction to transformers: an NLP perspective (2023). https:\/\/arxiv.org\/abs\/2311.17633"},{"key":"25_CR33","unstructured":"Xu, K., et al.: Fast and complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In: International Conference on Learning Representations (2021). https:\/\/openreview.net\/forum?id=nVZtXBI6LNn"},{"key":"25_CR34","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS 2018, pp. 4944\u20134953. Curran Associates Inc., Red Hook, NY, USA (2018), https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2018\/file\/d04863f100d59b3eb688a11f95b0ae60-Paper.pdf"},{"key":"25_CR35","unstructured":"Zhang, X., Zhao, J., LeCun, Y.: Character-level convolutional networks for text classification. In: Proceedings of the 29th International Conference on Neural Information Processing Systems - Volume 1, NIPS 2015, pp. 649\u2013657. MIT Press, Cambridge, MA, USA (2015). https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2015\/file\/250cf8b51c773f3f8dc8b4be867a9a02-Paper.pdf"},{"key":"25_CR36","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Shen, L., Guo, S., Ji, S.: GaLileo: general linear relaxation framework for tightening robustness certification of transformers. In: Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Artificial Intelligence. AAAI\u201924\/IAAI\u201924\/EAAI\u201924. AAAI Press (2024). https:\/\/doi.org\/10.1609\/aaai.v38i19.30180","DOI":"10.1609\/aaai.v38i19.30180"},{"key":"25_CR37","doi-asserted-by":"publisher","unstructured":"Zhang, Z., Wu, Y., Liu, S., Liu, J., Zhang, M.: Provably tightest linear approximation for robustness verification of sigmoid-like neural networks. In: Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2022. Association for Computing Machinery, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3551349.3556907","DOI":"10.1145\/3551349.3556907"},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"Zhu, Z., Liu, F., Chrysos, G., Cevher, V.: Robustness in deep learning: the good (width), the bad (depth), and the ugly (initialization). In: Oh, A.H., Agarwal, A., Belgrave, D., Cho, K. (eds.) Advances in Neural Information Processing Systems (2022). https:\/\/openreview.net\/forum?id=m8vzptcFKsT","DOI":"10.52202\/068431-2616"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32526-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:47:38Z","timestamp":1784796458000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}