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

The paper presents advancements in formal neural network verification by integrating Tensor Parallelism (TP) and Fully Sharded Data Parallelism (FSDP) into the auto_LiRPA / $\alpha,\beta$-CROWN framework. TP achieves approximately 2x peak-memory reduction at P=2, while FSDP reduces baseline memory usage by 80-90% and peak memory by 34-39% on wide MLPs, confirming soundness on VNN-COMP benchmarks. These techniques enable practitioners to overcome GPU memory limitations in verification tasks, enhancing the scalability of safety property proofs for larger networks.