ZonoGPT: Towards An Abstract Domain for Verifying Large GPT Models
Hai Duong, Thanh Le, ThanhVu Nguyen
cs.LG
Sep 28, 2026 · v1
cs.SE
TL;DR
Soundness theorems for the LayerNorm, GELU, MLP and attention zonotope transformers are mechanized in Lean 4 (e.g., ZonoGpt/LayerNorm.lean).
Abstract
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 \tool{} 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.
Problem
Existing neural network verifiers for transformers handle only small or simplified models. They also lose precision across deep stacks of blocks, so none scale to standard architectures such as GPT-2.
Approach
ZonoGPT is an abstract domain built on structured zonotopes. Shared generators capture cross-token relations, local generators capture token-specific relations, and per-block generator reduction keeps space complexity independent of network depth. It uses fused residual Taylor-expansion transformers for Attention and LayerNorm and an affine transform for GELU. The soundness of these transformers is mechanized in Lean 4.
Results
ZonoGPT verifies 1,339 of 2,880 instances on GPT-2 Small and Medium classifiers (up to 24 blocks, 300M+ parameters) trained on MNIST and SST. IBP and CoVeNN verify none of these instances, and DeepZ and alpha-beta-CROWN run out of memory.
| Tool | Solved | Time (s) |
|---|
| IBP | 0 | 688.8 |
| DeepZ | OOM | - |
| αβ-CROWN | OOM | - |
| CoVeNN | 0 | 569409.8 |
| ZonoGpt-A | 1339 | 157325.4 |
Total instances verified across all benchmarks (out of 2880)