# ZonoGPT: Towards An Abstract Domain for Verifying Large GPT Models

arXiv: https://arxiv.org/abs/2609.34457 · HTML: https://mlsanity.com/paper/2609.34457/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 31 of its 54 references that are in the map.
- First posted on arXiv 28 Sep 2026.

## Builds on (most cited first, 30 of 31)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Scalable Diffusion Models with Transformers](https://mlsanity.com/paper/2212.09748/) (2022)
- [Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities](https://mlsanity.com/paper/2507.06261/) (2025)
- [Universal and Transferable Adversarial Attacks on Aligned Language Models](https://mlsanity.com/paper/2307.15043/) (2023)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Bias and Fairness in Large Language Models: A Survey](https://mlsanity.com/paper/2309.00770/) (2023)
- [Efficiently Scaling Transformer Inference](https://mlsanity.com/paper/2211.05102/) (2022)
- [DecodingTrust: A Comprehensive Assessment of Trustworthiness in GPT Models](https://mlsanity.com/paper/2306.11698/) (2023)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Certified Robustness to Adversarial Word Substitutions](https://mlsanity.com/paper/1909.00986/) (2019)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [An LLM can Fool Itself: A Prompt-Based Adversarial Attack](https://mlsanity.com/paper/2310.13345/) (2023)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [JailbreakRadar: Comprehensive Assessment of Jailbreak Attacks Against LLMs](https://mlsanity.com/paper/2402.05668/) (2024)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [PromptBench: A Unified Library for Evaluation of Large Language Models](https://mlsanity.com/paper/2312.07910/) (2023)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [A DPLL(T) Framework for Verifying Deep Neural Networks](https://mlsanity.com/paper/2307.10266/) (2023)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [Harnessing Neuron Stability to Improve DNN Verification](https://mlsanity.com/paper/2401.14412/) (2024)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [Evaluating and Improving Robustness in Large Language Models: A Survey and Future Directions](https://mlsanity.com/paper/2506.11111/) (2025)
- [Harmful Prompt Laundering: Jailbreaking LLMs with Abductive Styles and Symbolic Encoding](https://mlsanity.com/paper/2509.10931/) (2025)
- [FGGM: Formal Grey-box Gradient Method for Attacking DRL-based MU-MIMO Scheduler](https://mlsanity.com/paper/2510.26075/) (2025)

## Built on by (most cited first, 1 of 1)

- [Neural Network Verification for Deep Joint Source-Channel Coding](https://mlsanity.com/paper/2610.11994/) (2026)

## Abstract (arXiv)

Transformer-based models are widely used for reasoning, coding, and multimodal agentic tasks. To provide formal assurance of desirable behaviors, such as robustness, safety, and fairness, neural network verification techniques prove required properties and provide auditable guarantees before deployment. However, prior work remains limited to small or restricted Transformers, and maintaining precision across deep models remains challenging. In this work, we introduce ZonoGpt, an abstract domain for verifying large transformers that maintains a space complexity independent of network depth. ZonoGpt uses a structured zonotope and a generator reduction mechanism to efficiently preserve correlations. To maintain precision, it introduces block-specific fused transformations for Attention and LayerNorm that retain feature relations, along with an affine transform for GELU that preserves generator relations. These mechanisms enable ZonoGpt to be the first approach to verify standard architectures, scaling to official HuggingFace models up to GPT-2 Medium (24 blocks, 300M+ parameters) and successfully verifying 1,339 instances across text and vision tasks.