Sari la conținut

Română · beta. Traducerea a fost făcută automat și este încă în curs de revizuire. Citește pagina în engleză

perspectiva aiqbenchSiguranță AI

analiza aiqbench

This research adapts training-scale parallelism techniques like Tensor Parallelism and Fully Sharded Data Parallelism to overcome GPU memory bottlenecks in formal neural network verification. While Tensor Parallelism reduces memory usage, it introduces a trade-off where bound tightness degrades due to algorithmic substitutions, whereas Fully Sharded Data Parallelism maintains bitwise-identical results to single-GPU baselines with significant memory savings. The findings highlight that per-neuron alpha tensors, rather than weight matrices, represent the primary memory constraint in current verification frameworks, guiding future optimization efforts.
Surse care acoperăarXiv, Quantum Zeitgeist
Ce este aceastaLectura unui model asupra articolului și a acoperirii conexe, scrisă pentru aiqbench. Nu sunt cuvintele publicației.

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

arXiv3 min de cititArticolul și perspectiva sunt în engleză.

arXiv:2606.09377v2 Announce Type: replace 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, $\alpha$-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 / $\alpha,\beta$-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 ($\beta$-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 $\alpha$-CROWN+BaB mode proves to be per-neuron alpha tensors, not weight matrices, pointing to the key direction for future work.

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, $\alpha$-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 / $\alpha,\beta$-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 ($\beta$-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 $\alpha$-CROWN+BaB mode proves to be per-neuron alpha tensors, not weight matrices, pointing to the key direction for future work.

Machine Learning (cs.LG); Artificial Intelligence (cs.AI)

arXiv:2606.09377 [cs.LG]

(or arXiv:2606.09377v2 [cs.LG] for this version)

https://doi.org/10.48550/arXiv.2606.09377 Focus to learn more arXiv-issued DOI via DataCite

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.

Text integral sub licența deschisă a publicației · 292 cuvinte

Subiecte conexe