Research map / Adversarial robustness and security / Certified and empirical robustness
LEVIS: Large Exact Verifiable Input Spaces for Neural Networks
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 LEVIS, a MIP-based framework (with a complementarity-constrained hybrid NLP-MIP speedup) that finds large exactly verifiable balls and unions of balls inside neural networks' verifiable input spaces.
Problem
Identifying the input region of a neural network that is provably free of adversarial examples is hard because the verifiable input space is high-dimensional, non-convex, and discontinuous, while existing verifiers only check outputs over a predefined input domain.
Approach
Approximate the verifiable space with exactly verified balls: LEVIS-alpha iteratively recenters a ball using directional MIP-found adversarial points until it touches two boundaries; LEVIS-beta collects many balls by exploring outward from found centers. A CC relaxation with a reduced MIP (integer variables only for undetermined neurons) speeds up the nearest-adversarial search.
Key results
- Hybrid CC-based NLP+reduced MIP achieves 7.82x speedup on MNIST (1.34 s vs 10.48 s) and 2.93x on CIFAR-10 (5.96 s vs 17.47 s) relative to MIP_CROWN, with optimality gaps of 0.004 and 0.0009.
- LEVIS-alpha yields verifiable-ball radii 3-9x larger than the EFC and Lipschitz baselines on DC-OPF, and the Lipschitz-based baseline radii are up to 10x smaller than the exact solver's radii.
- For DC-OPF, LEVIS-beta collects 52 verifiable balls with radii ranging from 0.10 to 23.58 (median 0.42).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use the hybrid NLP-reduced MIP solver instead of MIP_CROWN | LEVIS · MNIST | runtime: 10.48 -> 1.34; 7.82× | Helped |
| Use the hybrid NLP-reduced MIP solver instead of MIP_CROWN | LEVIS · CIFAR-10 | runtime: 17.47 -> 5.96; 2.93× | Helped |
| Solve the maximum verifiable ball directly instead of using the Lipschitz lower bound | LEVIS exact solver · DC-OPF, p = infinity | verifiable radius: 4.52 -> 16.24 | Helped |
| Solve the maximum verifiable ball directly instead of using the Lipschitz lower bound | LEVIS exact solver · DC-OPF, p = 1 | verifiable radius: 4.80 -> 47.28 | Helped |
| Solve the maximum verifiable ball directly instead of using the Lipschitz lower bound | LEVIS exact solver · DC-OPF, p = 2 | verifiable radius: 12.88 -> 28.12 | Helped |
| Iteratively refine the ball center | LEVIS-alpha · DC-OPF | verifiable radius: 3–9× larger than the baselines | Helped |
| Vary search angle, initialization shift, and random seed (ablation) | LEVIS-beta · MNIST | distribution of verifiable ball centers | Helped |
| Use the complementarity-constrained hybrid formulation instead of the full integer formulation | LEVIS solver · MNIST and CIFAR-10 | runtime: up to a 6-fold reduction in runtime | Helped |
Surprising findings
- Smaller-radius verifiable balls concentrate near the boundary of the verifiable region, reflecting natural shrinkage near edges.
- The MNIST network with 93% accuracy misclassifies a clean digit '7' as '3' under a perturbation of only 0.1 in pixel magnitude.
Limitations
- Convergence guarantee of LEVIS-alpha holds for convex verifiable regions; the paper notes it may fail for non-convex regions with bottlenecks.
- LEVIS-beta is not guaranteed to cover the full verifiable space; multi-directional search and parallel coverage are left for future work.
- Experiments use small three-layer networks, with MNIST radii estimated only for a single example initial point.
Experimental setup
Datasets: IEEE 9-bus DC-OPF dataset (1,000 samples) MNIST CIFAR-10
Benchmarks: IEEE 9-bus DC-OPF MNIST CIFAR-10
Metrics: runtime (seconds) speedup optimality gap verifiable ball radius
Baselines: MIP_CROWN Exact Fixed Center (EFC) Lipschitz-based lower bound (LLB)
Builds on: Big-M MILP encoding of ReLU OMLT CROWN IPOPT
Closest papers by meaning
- A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (NeurIPS 2019 · similarity 0.88)
- Towards General Robustness Verification of MaxPool-based Convolutional Neural Networks via Tightening Linear Approximation (CVPR 2024 · similarity 0.86)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.86)
- Tightening Robustness Verification of MaxPool-based Neural Networks via Minimizing the Over-Approximation Zone (CVPR 2025 · similarity 0.85)
- Verification of Neural Networks Against Convolutional Perturbations via Parameterised Kernels (AAAI 2025 · similarity 0.85)
- Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification (NeurIPS 2025 · similarity 0.85)
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.