신경망이 지정된 입력 범위에서 안전 속성을 항상 만족하는지 수학적으로 증명하는 형식 검증(formal verification) 분야에서 GPU 메모리 한계를 돌파하는 새로운 접근법이 제시됐다. 표준적인 경계 전파 알고리즘은 가중치 행렬 전체를 단일 가속기에 올려야 해 대규모 모델 검증이 사실상 불가능했는데, 연구진은 대규모 모델 학습에 쓰이던 두 가지 병렬화 기법을 검증 프레임워크에 이식하는 방법을 개발했다.
첫 번째 기법인 텐서 병렬화(TP)는 가중치 행렬과 완화 계수 행렬을 여러 GPU에 분산해 GPU 2개 구성에서 최고 메모리 사용량을 절반 수준으로 줄였다. 다만 분산 구역 수가 늘어날수록 중간 경계의 정밀도가 저하되는 한계가 있었다. 두 번째 기법인 완전 분산 데이터 병렬화(FSDP)는 가중치 행렬만 분산하고 층별로 수집하는 방식이어서, 단일 GPU 기준선과 비트 수준에서 동일한 검증 결과를 내면서도 기저 메모리를 80~90%, 최고 메모리를 34~39% 감소시켰다. FSDP는 완전 검증 모드와 합성곱 층에도 문제없이 적용됐으며, CIFAR-100 기반 대형 신경망에서 완전 비충족(unsat) 결과를 도출하는 데 성공했다.
실험 전반을 통해 병목이 가중치 행렬이 아니라 뉴런별 알파 텐서에 있음이 확인됐으며, 연구진은 이를 향후 연구의 핵심 방향으로 제시했다. 두 기법을 함께 검토한 이번 연구는 대규모 모델 훈련에서 검증된 인프라 기술이 안전성 증명 분야에도 유의미하게 이전될 수 있음을 보여준다는 점에서 실용적 의의가 있다.
AI 시스템의 안전성 보증 수요가 높아지는 상황에서 이 연구는 지금까지 메모리 한계로 검증이 어려웠던 대형 신경망으로 형식 검증 적용 범위를 넓히는 발판을 마련한다. 특히 FSDP가 결과 정확도를 유지하면서 메모리 절감을 달성했다는 점은 실제 배포 환경에서의 활용 가능성을 높인다.
