Verified-Intelligence/auto_LiRPA

해결하는 문제

auto_LiRPA는 신경망의 형식적 강건성을 검증하는 방법을 제공합니다. 입력 데이터나 모델 가중치에 변형이 가해졌을 때, 모델의 출력 범위(경계)를 보장할 수 있도록 하여, 특정 제약 조건 하에서 네트워크의 예측이 안정적이고 예측 가능하게 유지됨을 보장합니다.

작동 방식

이 라이브러리는 PyTorch 계산 그래프 위에서 작동하는 그래프 알고리즘으로, Linear Relaxation 기반 Perturbation Analysis (LiRPA) 알고리즘을 일반화합니다. 사용자는 표준 nn.Module로 모델을 정의하고, 라이브러리는 그래프를 탐색하여 임의의 노드에 대한 경계를 자동으로 도출하고 계산합니다. 구현이 미분 가능하므로, 네트워크 파라미터를 최적화하여 "증명 가능한 방어"(증명 가능한 강건성을 갖춘 모델)를 생성하는 데 사용할 수 있습니다.

대상 사용자

AI 모델의 형식적 강건성을 입증해야 하는 연구자 및 개발자에게 적합합니다. 특히 비전 모델(ResNet, DenseNet), 시퀀스 모델(LSTM, Transformers), 리아푸노프 안정성을 위한 신경 컨트롤러를 다루는 분들에게 적합합니다.

주요 특징

• 광범위한 알고리즘 지원: CROWN, DeepPoly, $α$-CROWN, $β$-CROWN, IBP 및 하이브리드 접근 방식을 포함한 다양한 기법을 구현합니다.
• 자동 도출: 사용자가 복잡한 LiRPA 경계를 수동으로 도출할 필요 없이, 자동 미분과 유사하게 처리합니다.
• 다양한 모델 지원: ReLU, sigmoid, tanh, maxpool 등의 다양한 활성화 함수와 Transformers, LSTMs와 같은 복잡한 아키텍처를 지원합니다.
• 고성능: 메모리 효율적인 GPU 구현과 멀티 GPU 지원을 통해 ImageNet과 같은 대규모 데이터셋에 확장 가능합니다.
• 왕관의 성공: $α, β$-CROWN의 핵심 라이브러리로, 2021년부터 2025년까지 VNN-COMP 경진대회에서 일관되게 우승했습니다.