자율주행 자동차의 이미지 기반 신경망 제어기에 대한 기존의 형식적 검증 방법은 고차원 입력, 계산 비효율성, 설명 가능성 부족으로 어려움을 겪습니다. 고차원 이미지 데이터 처리의 계산 집약성과 신경망의 블랙박스 특성으로 안전성과 신뢰성을 보장하기 어렵습니다. 본 논문에서는 고차원 이미지를 설명 가능한 저차원 잠재 공간으로 인코딩하는 변분 오토인코더(VAE)를 활용하는 SEVIN(Scalable and Explainable Verification of Image-Based Neural Network Controllers) 프레임워크를 제안합니다. 잠재 변수에 해당 제어 동작을 주석으로 달아 볼록 다면체를 생성하여 검증을 위한 구조화된 입력 공간으로 사용함으로써 계산 복잡성을 크게 줄이고 확장성을 높입니다. VAE의 디코더를 신경망 제어기와 통합하여 이러한 설명 가능한 다면체를 사용하여 형식적이고 강건한 검증을 수행합니다. 데이터셋을 확장하고 환경 변화를 포착하도록 VAE를 재훈련하여 실제 환경의 섭동에 대한 강건성 검증도 포함합니다. 실험 결과, SEVIN은 효율적이고 확장 가능한 검증을 달성하는 동시에 제어기 동작에 대한 설명 가능한 통찰력을 제공하여 형식적 검증 기법과 안전 중요 시스템의 실제 응용 간의 간극을 해소합니다.
