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

• URL: http://arxiv.org/abs/2606.09377v2
• Date: Tue, 09 Jun 2026 11:54:13 GMT
• Title: Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism
• Abstract summary: Formal neural network verification is bounded in practice by GPU memory.<n>We adapt two techniques originally developed for large-scale model training to the auto_LiRPA / $,$-CROWN verification framework.<n>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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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 auto_LiRPA / $α,β$-CROWN verification framework. Tensor Parallelism (TP) shards both weight and $A$-matrices across GPUs, achieving ${\approx}2\times$ 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.

Related papers

• ChunkFT: Byte-Streamed Optimization for Memory-Efficient Full Fine-Tuning [58.54940026861599]
  textscChunkFT is a memory-efficient fine-tuning framework.<n>textscChunkFT enables gradient computation for arbitrary sub-tensors without modifying the network architecture.<n>textscChunkFT consistently outperforms existing memory-efficient baselines.
  arXiv  Detail & Related papers  (2026-05-20T13:44:44Z)
• Hierarchical Transformer Preconditioning for Interactive Physics Simulation [28.137076331332413]
  Hierarchical Transformer Preconditioner, a neural preconditioner anchored to a weak-admissibility H-matrix partition.<n>Network models the inverse through low-rank far-field factors.<n>Uses highway connections to propagate context across depth sparse.
  arXiv  Detail & Related papers  (2026-05-13T11:02:27Z)
• LBI: Parallel Scan Backpropagation via Latent Bounded Interfaces [1.8179911892344436]
  We introduce Latent Bounded Interfaces (LBI), an algorithmic formulation that makes scan-based backpropagation tractable.<n>LBI reduces the adjoint recursion to a suffix scan over $r times r$ Jacobians, cutting per-combine cost from $O(d3)$ to $O(r3)$.<n>We demonstrate that LBI maintains model quality across four architectures (Mamba-2, Mamba-3, Transformer, and a Mamba--Transformer hybrid) at 47--61M block parameters.
  arXiv  Detail & Related papers  (2026-05-09T22:46:46Z)
• EdgeLDR: Quaternion Low-Displacement Rank Neural Networks for Edge-Efficient Deep Learning [2.8496753993424817]
  EdgeLDR is a framework for quaternion block-circulant linear and convolutional layers that combines quaternion channel mixing with block-circulant parameter structure.<n>We present reference implementations of EdgeLDR layers and compare FFT-based computation against a naive spatial-domain realization of quaternion circulant products.
  arXiv  Detail & Related papers  (2026-01-08T21:04:07Z)
• GSPN-2: Efficient Parallel Sequence Modeling [101.33780567131716]
  Generalized Spatial Propagation Network (GSPN) addresses this by replacing quadratic self-attention with a line-scan propagation scheme.<n>GSPN-2 establishes a new efficiency frontier for modeling global spatial context in vision applications.
  arXiv  Detail & Related papers  (2025-11-28T07:26:45Z)
• Evolution Strategies at the Hyperscale [57.75314521465674]
  We introduce EGGROLL, an evolution strategies (ES) algorithm designed to scale backprop-free optimization to large population sizes.<n>ES is a set of powerful blackbox optimisation methods that can handle non-differentiable or noisy objectives.<n>EGGROLL overcomes these bottlenecks by generating random matrices $Ain mathbbRmtimes r, Bin mathbbRntimes r$ with $rll min(m,n)$ to form a low-rank matrix perturbation $A Btop$
  arXiv  Detail & Related papers  (2025-11-20T18:56:05Z)
• Arithmetic-Mean $μ$P for Modern Architectures: A Unified Learning-Rate Scale for CNNs and ResNets [9.94514344279733]
  Arithmetic-Mean $mu$P constrains not each individual layer but the network-wide average one-step pre-activation second moment to a constant scale.<n>We prove that, for one- and two-dimensional convolutional networks, the maximal-update learning rate satisfies $etastar(L)propto L-3/2$; with zero padding, boundary effects are constant-level as $Ngg k$.
  arXiv  Detail & Related papers  (2025-10-05T19:22:50Z)
• Communication-Efficient, 2D Parallel Stochastic Gradient Descent for Distributed-Memory Optimization [2.2596489829928452]
  This work generalizes work on 1D $s$-step SGD and 1D Federated SGD with Averaging (FedAvg) to yield a 2D parallel SGD method (HybridSGD)<n>We implement all algorithms in C++ and MPI and evaluate their performance on a Cray EX supercomputing system.
  arXiv  Detail & Related papers  (2025-01-13T17:56:39Z)
• Boosting the effective performance of massively parallel tensor network state algorithms on hybrid CPU-GPU based architectures via non-Abelian symmetries [0.0]
  Non-Abelian symmetry related tensor algebra based on Wigner-Eckhart theorem is fully detached from the conventional tensor network layer. We have achieved an order of magnitude increase in performance with respect to results reported in arXiv:2305.05581 in terms of computational complexity. Our solution has an estimated effective performance of 250-500 TFLOPS.
  arXiv  Detail & Related papers  (2023-09-23T07:49:53Z)
• Improved techniques for deterministic l2 robustness [63.34032156196848]
  Training convolutional neural networks (CNNs) with a strict 1-Lipschitz constraint under the $l_2$ norm is useful for adversarial robustness, interpretable gradients and stable training. We introduce a procedure to certify robustness of 1-Lipschitz CNNs by replacing the last linear layer with a 1-hidden layer. We significantly advance the state-of-the-art for standard and provable robust accuracies on CIFAR-10 and CIFAR-100.
  arXiv  Detail & Related papers  (2022-11-15T19:10:12Z)
• Unfolding Projection-free SDP Relaxation of Binary Graph Classifier via GDPA Linearization [59.87663954467815]
  Algorithm unfolding creates an interpretable and parsimonious neural network architecture by implementing each iteration of a model-based algorithm as a neural layer. In this paper, leveraging a recent linear algebraic theorem called Gershgorin disc perfect alignment (GDPA), we unroll a projection-free algorithm for semi-definite programming relaxation (SDR) of a binary graph. Experimental results show that our unrolled network outperformed pure model-based graph classifiers, and achieved comparable performance to pure data-driven networks but using far fewer parameters.
  arXiv  Detail & Related papers  (2021-09-10T07:01:15Z)
• VersaGNN: a Versatile accelerator for Graph neural networks [81.1667080640009]
  We propose textitVersaGNN, an ultra-efficient, systolic-array-based versatile hardware accelerator. textitVersaGNN achieves on average 3712$times$ speedup with 1301.25$times$ energy reduction on CPU, and 35.4$times$ speedup with 17.66$times$ energy reduction on GPU.
  arXiv  Detail & Related papers  (2021-05-04T04:10:48Z)
• Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification [151.62491805851107]
  We develop $beta$-CROWN, a bound propagation based verifier that can fully encode per-neuron splits. $beta$-CROWN is close to three orders of magnitude faster than LP-based BaB methods for robustness verification. By terminating BaB early, our method can also be used for incomplete verification.
  arXiv  Detail & Related papers  (2021-03-11T11:56:54Z)
• Deep Learning Meets Projective Clustering [66.726500395069]
  A common approach for compressing NLP networks is to encode the embedding layer as a matrix $AinmathbbRntimes d$. Inspired by emphprojective clustering from computational geometry, we suggest replacing this subspace by a set of $k$ subspaces.
  arXiv  Detail & Related papers  (2020-10-08T22:47:48Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.