Research map / Learning theory and algorithms / Combinatorial and search optimization
Exponent Relaxation of Polynomial Zonotopes and Its Applications in Formal Neural Network Verification
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes exponent relaxation that restructures polynomial zonotopes by merging dependent generators with similar exponents (graph-guided), giving tighter and cheaper order reduction, zonotope enclosure, and range bounds for neural network reachability.
Problem
Polynomial zonotopes tightly enclose neural network output sets, but their complexity (monomial dependencies) makes subsequent operations such as interval bounds, zonotope enclosure, order reduction and intersection checking expensive and outer-approximative.
Approach
Relax exponents of dependent generators with similar exponents so that they can be merged, adding a single independent generator to bound the approximation error; a graph-based greedy selection chooses which generators to merge with polynomial-time complexity.
Key results
- On an MNISTFC image with perturbation 0.075, the proposed approach verifies the property in 0.27s without splitting, versus 23.22s for polynomial zonotope with splitting; the plain zonotope returns UNKNOWN.
- Across randomly generated sigmoid and ReLU networks, ratios of order reduction, zonotope enclosure, interval bounds and support function are all below 1 (e.g., 0.2909 to 1.5905 range in the sigmoid case), indicating tighter results without splitting.
- Exponent relaxation runs in polynomial time, O((h+q)hn + h^2 p), and often matches or beats recursive splitting while maintaining a single set.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| apply exponent relaxation with η = 1 before final order reduction and specification checking | Polynomial zonotope neural-network verification · MNISTFC | verification result | Helped |
| apply exponent relaxation with η = 1 before final order reduction and specification checking | Polynomial zonotope neural-network verification · MNISTFC | verification time: 0.16s -> 0.27s; 23.22s -> 0.27s | Helped |
| apply exponent relaxation before subsequent order reduction and enclosure operations | Random neural-network output sets · Random networks with sigmoid and ReLU activations | operation ratio | Helped |
| vary the exponent threshold η (ablation) | Exponent relaxation · Polynomial zonotope restructuring | zonotope enclosure tightness | Helped |
| vary the exponent threshold η (ablation) | Exponent relaxation · Polynomial zonotope restructuring | outer-approximation | Mixed |
Surprising findings
- In several random networks the single-set approach yields tighter results than recursive splitting on some metrics, despite splitting usually being expected to be tighter.
Limitations
- Exponent relaxation induces a small outer-approximation, and the tradeoff depends on the threshold eta.
- Only evaluated on feed-forward networks with ReLU/sigmoid activations and random networks plus one MNISTFC example.
Experimental setup
Datasets: MNISTFC
Benchmarks: MNISTFC
Metrics: verification time volume ratio of zonotope enclosure interval bounds volume ratio support function ratio order reduction ratio
Baselines: zonotope enclosure (Singh et al. 2018) polynomial zonotope with recursive splitting (Kochdumper et al. 2023)
Builds on: polynomial zonotope abstraction refinement with higher-order polynomials zonotope enclosure
Closest papers by meaning
- Parameterized Hardness of Zonotope Containment and Neural Network Verification (ICLR 2026 · similarity 0.89)
- Zonotope Domains for Lagrangian Neural Network Verification (NeurIPS 2022 · similarity 0.88)
- Sound and Complete Verification of Polynomial Networks (NeurIPS 2022 · similarity 0.87)
- Identifiability of Deep Polynomial Neural Networks (NeurIPS 2025 · similarity 0.85)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.85)
- Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization (ICLR 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.