텐서 병렬성 (Tensor Parallelism) 및 완전 샤딩 데이터 병렬성 (Fully Sharded Data Parallelism)을

형식적 신경망 검증 (Formal neural network verification) — 특정 도메인 내의 extit{모든} 입력에 대해 네트워크가 안전 속성 (safety properties)을 만족함을 증명하는 것 — 은 실제 환경에서 GPU 메모리에 의해 제한됩니다. 경계 전파 (bound-propagation) 알고리즘 (IBP, CROWN, $α$-CROWN)의 표준 구현은 가중치 (weight) 및 완화 계수 (relaxation-coefficient) 행렬이 하나의 가속기(accelerator)에 완전히 상주할 것을 요구합니다. 우리는 대규모 모델 학습을 위해 원래 개발된 두 가지 병렬화 기술을 exttt{auto_LiRPA}/$α,β$-CROWN 검증 프레임워크에 맞게 조정했습니다. extbf{텐서 병렬성 (Tensor Parallelism, TP)}은 가중치와 $A$-행렬 모두를 GPU 전체에 샤딩 (sharding)하여, $P{=}2$일 때 피크 메모리 (peak-memory)를 약 $2 imes$ 감소시킵니다. VNN-COMP 2022 MNIST-FC 벤치마크에서 건전성 (soundness)이 확인되었으나, 샤딩된 구역 (sharded zones) 내부의 중간 경계 (intermediate bounds)에 대해 강제적인 IBP 대체가 이루어짐에 따라 샤딩된 구역의 수가 증가할수록 경계의 타이트함 (bound tightness)은 저하됩니다. extbf{완전 샤딩 데이터 병렬성 (Fully Sharded Data Parallelism, FSDP)}은 레이어별 exttt{AllGather}를 통해 가중치 행렬만을 샤딩하며, 단일 GPU 베이스라인과 extit{비트 단위로 동일한 (bitwise identical)} 경계를 생성합니다. 넓은 MLP (wide MLPs)에서 베이스라인 메모리는 80--90% 감소하고, 피크 메모리는 34--39% 감소합니다. FSDP는 완전 검증 ($β$-CROWN + Branch-and-Bound) 및 컨볼루션 레이어 ( exttt{BoundConv})와 깔끔하게 통합됩니다. FSDP 하에서 CIFAR-100 ResNet-large (VNN-COMP 2024)에 대해 완전한 extit{unsat} (불만족) 결과를 얻었습니다. 모든 실험을 통해 $α$-CROWN+BaB 모드에서의 메모리 병목 (memory bottleneck)은 가중치 행렬이 아니라 뉴런당 알파 텐서 (per-neuron alpha tensors)임이 증명되었으며, 이는 향후 연구를 위한 핵심 방향을 제시합니다.