Research map / Adversarial robustness and security / Certified and empirical robustness
No Soundness in the Real World: On the Challenges of the Verification of Deployed 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.
Shows that theoretically sound neural network verifiers (interval/polyhedra/zonotope based) are not practically sound for deployed networks, and demonstrates this with backdoored MNIST networks exploiting floating-point precision and operation order.
Problem
Formal verifiers guarantee robustness for the full-precision theoretical model, but deployed networks run in floating point in stochastic environments (operation order, precision, hardware), so verified guarantees may not hold for the deployed network.
Approach
Introduces the distinction between theoretical soundness and practical soundness, proves that interval-based and symbolic/zonotope bound propagation methods are not practically sound in stochastic floating-point environments, and builds deployment-sensitive backdoors (precision and expression-tree detectors) that evade state-of-the-art verifiers.
Key results
- Backdoored networks show near-0% vs 98.11% test accuracy depending on 32-bit vs 64-bit precision, confirming precision-triggered behavior change.
- Every tested sound verifier (MIPVerify, MN-BaB, β-CROWN BaB, GCP-CROWN, DeepPoly, DeepZ, RefinePoly, RefineZono) misses at least one of the precision or Order3 backdoors, so none is practically sound.
- Proofs show IBP and polyhedra/zonotope bound propagation can fail to cover the floating-point output for some expression trees, and finding the min/max expression tree is conjectured NP-hard.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use a 32-bit precision-triggered backdoor and switch inference precision between 32-bit and 64-bit | WK17a MNIST network · MNIST test set | accuracy: 0.11% (32-bit backdoor, 32-bit inference) vs 98.11% (64-bit inference); 98.11% (64-bit backdoor, 32-bit inference) vs 0. | Mixed |
| Use an expression-tree-triggered Order1 backdoor across deployment environments | WK17a MNIST network · MNIST test set, batch 1 and batch 10 across PyTorch/Flux CPU/GPU | accuracy: 0.11% and 98.11% across the environments in Table 2 | Mixed |
| Use an expression-tree-triggered Order2 backdoor across deployment environments | WK17a MNIST network · MNIST test set, batch 1 and batch 10 across PyTorch/Flux CPU/GPU | accuracy: 0.11% and 98.11% across the environments in Table 2 | Mixed |
| Use an expression-tree-triggered Order3 backdoor across deployment environments | WK17a MNIST network · MNIST test set, batch 1 and batch 10 across PyTorch/Flux CPU/GPU | accuracy: 98.11% in every listed environment | No clear effect |
| Evaluate a 32-bit precision-triggered backdoor without modeling deployment precision | MIPVerify, MN-BAB, β-CROWN BaB, GCP-CROWN, DeepPoly, DeepZ, RefinePoly, RefineZono · MNIST adversarial robustness verification | backdoor detection | Hurt |
| Evaluate the Order3 expression-tree backdoor with theoretical-sound verifiers | MIPVerify, MN-BAB, β-CROWN BaB, GCP-CROWN, DeepPoly, RefinePoly, RefineZono · MNIST adversarial robustness verification | backdoor detection | Hurt |
Surprising findings
- Simple orderings such as decreasing-order or decreasing-absolute-value summation do not guarantee bounding the minimum floating-point output.
- Verifiers that are claimed sound (e.g., DeepPoly, DeepZ) still report incorrect robust accuracy on backdoored networks.
Limitations
- The paper proposes no practically sound verifier; it only exposes the problem.
- Backdoors use very large weights and are fairly easy to detect; the attacks are demonstrated only on a small MNIST network with 100 test samples.
Experimental setup
Datasets: MNIST
Benchmarks: MNIST (first 100 test samples)
Metrics: verified robust accuracy test accuracy of backdoored networks
Baselines: MIPVerify MN-BaB β-CROWN BaB GCP-CROWN DeepPoly RefinePoly DeepZ RefineZono
Builds on: interval bound propagation DeepPoly CROWN Zombori et al. 2021 adversarial network construction MIPVerify
Closest papers by meaning
- Sound Verification of Deployed Neural Networks (NeurIPS 2026 · similarity 0.93)
- VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees (ICML 2024 · similarity 0.85)
- Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization (ICLR 2025 · similarity 0.85)
- Stress-Testing Neural Network Verifiers with Provably Robust Instances (NeurIPS 2026 · similarity 0.85)
- Training Verification-Friendly Neural Networks via Neuron Behavior Consistency (AAAI 2025 · similarity 0.85)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · 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.