Source-linked AI summary
ZonoGPT: Towards An Abstract Domain for Verifying Large GPT Models
Hai Duong, Thanh Le, ThanhVu Nguyen
TL;DR
Widely used Transformer models need formal verification, yet maintaining precision across deep models remains challenging. ZONOGPT combines structured zonotopes with block-specific transformations and verifies 1,339 instances across text and vision, scaling to GPT-2 Medium.
Problem
Formal verification is relevant to widely used Transformer models, but maintaining precision across deep models remains challenging.
Source: §1 · p. 1Method
ZONOGPT uses structured zonotopes with generator reduction and block-specific fused or affine transformations tailored to Transformer components.
Source: §1 · p. 2Results
Across 2,880 text and vision instances, ZONOGPT verified 1,339 (46.5%) and scaled to official HuggingFace models up to GPT-2 Medium (24 blocks, 300M+ parameters).
Source: §1 · p. 2Takeaways & Limitations
The work demonstrates verification of standard HuggingFace GPT-2 architectures adapted for vision under full-dimensional input perturbations, including GPT-2 Medium.
Source: §1 · p. 2The demonstrated models remain small compared with the largest GPT models, with scale reaching up to GPT-2 Medium.
Source: §1 · p. 2
Abstract
from arXiv · showhide
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.
1 Introduction
Formal verification can provide auditable guarantees for widely used Transformer models, but existing methods struggle with standard architectures and precision across deep models. ZONOGPT combines structured zonotopes and block-specific transformations, verifies 1,339 instances, and scales to GPT-2 Medium.
1 Introduction
- Prior verification tools were limited to small or restricted Transformers, while precision loss across successive nonlinear layers remained a challenge.Existing work handled at most three small simplified blocks or scaled to 12 blocks with much smaller configurations; tightening isolated operations did not address accumulated over-approximation error.Source: §1 · pp. 1–2
- ZONOGPT uses structured zonotopes and generator reduction to preserve token and feature relations with space complexity independent of network depth.Its fused attention transform jointly over-approximates skip and attention branches; fused LayerNorm and affine GELU transformations preserve feature or generator relations.Source: §1 · p. 2
- 1,339 of 2,880 text and vision instances (46.5%) were verified, with scaling to official HuggingFace models up to GPT-2 Medium (24 blocks, 300M+ parameters).As perturbation increases, fused attention verifies 867 instances (40.1%) for deep configurations (4+ blocks), while unfused variants verify fewer than 1%.Source: §1 · p. 2
- The demonstrated models remain small compared with the largest GPT models, reaching up to GPT-2 Medium (24 blocks, 300M+ parameters).The authors describe this scale as a first step toward verifying larger GPT models.Source: §1 · p. 2
2 Background
The background frames verification as checking whether a network satisfies a property and describes zonotopes as a relational abstraction. ZONOGPT builds on that representation and uses residual Taylor expansion to construct bounds for attention and LayerNorm.
2 Background
- Neural network verification asks whether a property relating network inputs and outputs is valid, searching for a counterexample that satisfies the input condition but violates the output condition.If no such counterexample exists, the property is valid; otherwise, it is invalid.Source: §2 · p. 2
- A zonotope represents a center plus generator-weighted perturbations, and shared coefficients let it preserve relations among outputs.Affine transformations are exact, while nonlinear operations add generators to bound approximation error and can increase computational complexity.Source: §2 · p. 2
- ZONOGPT combines shared generators for cross-token relations with token-local generators, then reduces their number after each block to avoid growth across network depth.The representation preserves relations needed by Transformer operations while keeping generator counts limited.Source: §2 · p. 2
- Residual Taylor expansion supplies the output-zonotope construction that ZONOGPT uses for attention and LayerNorm.For a residual A(x) = x + B(x), the expansion separates the center value and linearized change from a nonlinear error term.Source: §2 · pp. 2–3
3 Motivating Example
The motivating example shows that fused attention yields a tighter bound that verifies a property the operator-wise bound cannot. ZONOGPT also stores the GPT-2-small input with far less memory than DEEPZ and has a space bound independent of network depth.
3 Motivating Example
- 2.25 GiB for ZONOGPT versus 1152 GiB for DEEPZ on a GPT-2-small input with S = 512 and d = 768.ZONOGPT stores eight input coefficients rather than DEEPZ’s 16 in the smaller running example.Source: §3 · p. 3
- O(Sd(m + q + 1)) coefficients are required between components, independent of network depth, versus O(LS^2d^2) for DEEPZ across L blocks.ZONOGPT retains at most m shared and q local generators per token.Source: §3 · p. 3
- [−1.24, 1.98] cannot verify [A(X)]1,1 > 0, while operator-wise DEEPZ introduces fresh generators at nonlinear operators.The attention output grows to 34 generators in the operator-wise example.Source: §3 · pp. 3–4
- [A(X)]1,1 ∈ [0.11, 0.69] verifies [A(X)]1,1 > 0 under the stated ℓ∞ perturbation.The example uses two tokens, hidden size two, and radius 0.02.Source: §3 · pp. 3–4
4 The ZONOGPT Approach
ZONOGPT propagates bounds through Transformers using structured zonotopes that preserve selected dependencies while limiting generator growth. It combines fused attention and LayerNorm transforms with sequential MLP processing, then reduces generators to control space use.
4 The ZONOGPT Approach
- The bound-propagation procedure initializes local input generators, uses fused attention and sequential MLP transforms, reduces generators, and returns output bounds.It limits shared generators to m and local generators to q per token.Source: §4 · p. 4
4.1 Structured Representation
- Shared generators represent cross-token relations, local generators represent token-specific relations, and intervals bound remaining terms without depth-dependent generator growth.Inputs initially use local generators because each input coordinate affects only its token; attention later mixes tokens.Source: §4.1 · p. 5, §4 · p. 5
4.2 Fused Attention Block Transform
- Fused attention propagates each input generator through the complete attention residual, preserving relations before bounding the remaining nonlinear error.The output combines the center evaluation, Jacobian image, and nonlinear remainder bound.Source: §4.2 · p. 5
4.3 MLP Block Transform
- The MLP applies fused LayerNorm, then propagates affine maps and elementwise GELU sequentially before combining the block with the skip connection.Unlike attention, the MLP has no bilinear products such as QK⊤ and PV.Source: §4.3 · p. 6
4.3.1 LayerNorm
- ZONOGPT bounds the complete LayerNorm as one fused transform because its mean and variance depend on the same token features.The Taylor expansion produces a structured zonotope using the center and Jacobian images of shared and local generators.Source: §4.3.1 · p. 7
4.3.2 GELU
- GELU is bounded coordinate-wise by an affine term and an error interval, preserving the input generators in the affine part.The error interval is centered at m = (rlb + rub)/2 with radius d = (rub − rlb)/2.Source: §4.3.2 · p. 7
4.4 Zonotope Conversion and Reduction
- After each block, ZONOGPT converts interval radii to local generators, retains at most m shared and q local generators per token, and adds discarded shared-generator magnitudes to the interval radius.The reduction construction is stated to produce a zonotope containing the original.Source: §4.4 · p. 7
4.5 Complexity
- Between components, storage is O(Sd(m + q + 1)); attention adds O(Sd^2) temporary coefficients, while softmax space O(HS^2d) dominates attention-matrix storage.The section also defines time complexity in terms of full-component JVP, source-token attention JVP, and nonlinear-remainder-bound costs.Source: §4.5 · p. 8
5 Evaluation
Evaluation across MNIST and SST benchmarks finds that ZONOGPT verifies instances where the baselines verify none, while fusion choices trade verification precision against runtime. The study also compares verification across perturbation radii and runtime distributions.
5.1 Experimental Design
- The evaluation used GPT-2 classifiers trained on MNIST and SST, generating 2,880 instances across networks and perturbation radii.The baselines were IBP, DEEPZ, αβ-CROWN, and COVENN; the compared ZONOGPT variants fused neither, one, or both blocks.Source: §5.1 · pp. 8–9
5.2 RQ1: Overall Verification Performance
- 46.5% of the 2,880 MNIST and SST instances were certified by ZONOGPT-A, while every baseline verified none.DEEPZ and αβ-CROWN exceeded memory limits; IBP and COVENN produced loose bounds.Source: §5.2 · p. 9
5.3 RQ2: Fused Transformation Effectiveness
- At ϵ = 10−4, ZONOGPT-A verified 305 instances versus ZONOGPT-F’s 228; at ϵ = 5 × 10−4, it certified 68 versus 9.The variants with fused attention scaled to larger perturbations, and ZONOGPT-A performed consistently better across radii.Source: §5.3 · p. 9
5.4 RQ3: Runtime Analysis
- IBP finished in under 1s, while COVENN had median runtime > 150s; among ZONOGPT variants, MLP fusion reduced runtime but attention fusion added computation.ZONOGPT-M ran in 3s versus ZONOGPT-D’s 11s, while ZONOGPT-F ran in 21s versus ZONOGPT-A’s 38s.Source: §5.4 · pp. 9–10
6 Conclusion
ZONOGPT verifies standard HuggingFace GPT-2 Medium, and the paper identifies cached attention states for autoregressive decoding and adaptation to Diffusion as future work. The appendix also presents a soundness theorem for its fused LayerNorm transform.
6 Conclusion
- ZONOGPT successfully verified standard HuggingFace GPT-2 Medium; future work includes cached attention states for autoregressive decoding and adaptation to Diffusion.The authors describe this as a first step toward verifying larger GPT models.Source: §6 · p. 10
A.1 Fused LayerNorm Transform
- The appendix states a LayerNorm soundness theorem for Π = I − 11⊤/d and τ > 0.For an input zonotope, the construction computes nonnegative bounds for the theorem’s quantities.Source: §A.1 · p. 13
The resulting zonotope
The LayerNorm construction separates the first-order change from nonlinear error while retaining input-generator relations in the resulting zonotope.
The resulting zonotope
- LayerNorm’s linear change is computed by differentiating its expression at Δ = 0 and substituting the zonotope-generator representation.The proof treats the change from the center and its corresponding centered change.Source: The resulting zonotope · p. 13
- The nonlinear error is obtained by subtracting LN(c) and JLN(c)Δ, with the residual terms expressed through ρ and its derivative.The expansion separates the linear change from the nonlinear error computation.Source: The resulting zonotope · p. 13
- The output retains every input symbol in the Jacobian images, placing only the nonlinear error eN in the interval.The Taylor construction also requires a positive lower bound for the argument of ρ.Source: The resulting zonotope · p. 14
A.2 Affine GELU Transform
The affine GELU transform bounds the activation over each preactivation interval and constructs an output zonotope that preserves input noise symbols.
A.2 Affine GELU Transform
- Over each preactivation interval [ℓ, u], ZONOGPT bounds GELU using linear lower and upper bounds that share coefficient a and bound the residual q(t) = g(t) − at.For ℓ < u, the method partitions the interval and bounds interpolation error on each subinterval.Source: §A.2 · pp. 14–15
- The output zonotope retains the input generators and adds local columns for coordinate-wise GELU variation.The new columns are local because GELU acts independently on each token and coordinate.Source: §A.2 · p. 15
- The soundness argument combines interpolation-error and global ReLU-gap bounds to show every GELU output belongs to the constructed zonotope.The implementation uses K = 32 equal subintervals.Source: §A.2 · p. 15
A.3 Fused MLP Transform
The fused MLP transform constructs an output zonotope from the residual’s center, Jacobian images, and a bounded nonlinear remainder. It preserves generator symbols while bounding the remaining error.
A.3 Fused MLP Transform
- The construction evaluates the complete MLP residual at c, propagates input generators through JM(c), and uses RM as the remainder bound.The Jacobian images retain input symbols, and tokenwise processing keeps each local image at its source token.Source: §A.3 · p. 16
- The nonlinear-error bound combines LayerNorm’s remainder with GELU curvature, under bounds on rN, RN, and Cg over the specified preactivation interval.The mechanized proof also establishes end-to-end soundness for the sequential MLP implementation.Source: §A.3 · p. 16
- The output zonotope is sound: for inputs in Z satisfying Theorem 5’s bounds, the fused MLP maps every input into ZM.Its center is M(c), its generators are Jacobian images, and its interval field bounds the nonlinear remainder.Source: §A.3 · p. 16
A.3.1 MLP nonlinear-error computation
The appendix bounds nonlinear errors for the MLP and attention transforms, then uses those bounds to establish soundness of the fused attention output zonotope.
A.3.1 MLP nonlinear-error computation
- The MLP remainder RM combines transported LayerNorm error with GELU’s second-order Taylor error, using a curvature bound on the preactivation interval.The mechanized curvature bound is computable, and the Taylor bound requires differentiability of g and g′.Source: §A.3.1 · pp. 17–18
A.4 Fused Attention Transform
- The attention transform propagates LayerNorm and projection radii through QK⊤, softmax, and the attention-value product to bound nonlinear error.The attention-radius computation is mechanized with τ > 0 as its only hypothesis.Source: §A.4 · pp. 18–19
A.5 Fused attention soundness
- The fused attention output zonotope contains A(Z): its center represents A(c), its generators retain Jacobian terms, and bA bounds the remaining terms.The soundness proof requires a zero interval field in the input zonotope; its mechanized theorem assumes τ > 0.Source: §A.5 · pp. 19–20
B Related Work
Prior verification methods face limits in model scale, transformer scope, or precision across components. ZONOGPT combines generator reduction and fused transforms to address these limitations for standard GPT-2 architectures.
B Related Work
- Existing transformer verification covers small or restricted models, while none of the described tools scale to standard architectures such as GPT-2.Prior approaches simplify LayerNorm, use smaller configurations or restricted perturbations, or tighten individual attention operations.Source: B Related Work · p. 20
- ZONOGPT reduces shared and local generators after each block to keep space complexity independent of network depth.This addresses DEEPZ’s generator growth with network size.Source: B Related Work · p. 20
- ZONOGPT fuses the attention residual transform to retain relations between components rather than bounding attention operations separately.The related-work discussion contrasts this with COVENN’s decomposition, whose interval bounds lose precision between components.Source: B Related Work · p. 20
- ZONOGPT bounds standard LayerNorm and GELU to verify GPT-2 architectures, addressing prior use of simplified LayerNorm or restricted model configurations.Source: B Related Work · p. 20
C Benchmark Details
The benchmark evaluates GPT-2 classifiers on MNIST and SST across model sizes and perturbation settings. Generator reduction applies a combined shared-and-local limit during propagation.
C Benchmark Details
- The benchmark uses causal GPT-2 blocks at Small and Medium sizes, with 2, 4, 8, and 12 blocks for Small and 2, 4, 8, and 24 for Medium.MNIST images are mapped from rows to tokens; SST perturbations apply to token embeddings rather than token IDs.Source: C Benchmark Details · p. 20
- For MNIST, four correctly classified test images are selected per model and radius; for SST, 18 correctly classified validation sentences are selected per model and radius.Each SST sentence receives two specifications, perturbing either one or three token embeddings; sampling uses seed 0.Source: C Benchmark Details · p. 20
- The combined generator limit C is 6,241 and 4,681 for MNIST Small and Medium, and 5,461 and 4,096 for SST Small and Medium, respectively.Shared and local generator counts are computed dynamically while their sum remains at most C after each reduction.Source: C Benchmark Details · p. 21