# Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism

arXiv: https://arxiv.org/abs/2606.09377 · HTML: https://mlsanity.com/paper/2606.09377/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 26 references that are in the map.
- First posted on arXiv 8 Jun 2026.

## Builds on (most cited first, 13 of 13)

- [Megatron-LM: Training Multi-Billion Parameter Language Models Using Model Parallelism](https://mlsanity.com/paper/1909.08053/) (2019)
- [ZeRO: Memory Optimizations Toward Training Trillion Parameter Models](https://mlsanity.com/paper/1910.02054/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results](https://mlsanity.com/paper/2212.10376/) (2022)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Input Validation for Neural Networks via Runtime Local Robustness Verification](https://mlsanity.com/paper/2002.03339/) (2020)
- [Optimized Symbolic Interval Propagation for Neural Network Verification](https://mlsanity.com/paper/2212.08567/) (2022)
- [Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation](https://mlsanity.com/paper/2505.05235/) (2025)

## Abstract (arXiv)

Formal neural network verification -- proving that a network satisfies safety properties for *all* inputs in a specified domain -- is bounded in practice by GPU memory: standard implementations of bound-propagation algorithms (IBP, CROWN, α-CROWN) require weight and relaxation-coefficient matrices to reside entirely on one accelerator. We adapt two parallelism techniques originally developed for large-scale model training to the autoLiRPA / α,β-CROWN verification framework. Tensor Parallelism (TP) shards both weight and A-matrices across GPUs, achieving ≈2× peak-memory reduction at P=2; soundness is confirmed on VNN-COMP 2022 MNIST-FC benchmarks, though bound tightness degrades with the number of sharded zones due to forced IBP substitution for intermediate bounds inside sharded zones. Fully Sharded Data Parallelism (FSDP) shards only weight matrices with a per-layer AllGather, producing bounds that are bitwise identical to the single-GPU baseline: baseline memory drops by 80--90%, peak memory by 34--39% on wide MLPs. FSDP integrates cleanly with complete verification (β-CROWN + Branch-and-Bound) and with convolutional layers (BoundConv); a complete unsat result is obtained for CIFAR-100 ResNet-large (VNN-COMP 2024) under FSDP. Across all experiments the memory bottleneck in α-CROWN+BaB mode proves to be per-neuron alpha tensors, not weight matrices, pointing to the key direction for future work.