본 논문은 신경망의 안전성과 신뢰성을 보장하기 위한 형식적 검증 방법론에 초점을 맞추고 있다. 특히, 공정성이나 전역적 강건성과 같이 전체 입력 공간에 적용되는 속성을 고려할 때, 현실 세계에서 발생하지 않는 입력에 대한 검증을 피해야 하는 문제점을 해결하고자 한다. 이를 위해, VeriFlow 아키텍처를 제안한다. VeriFlow는 관심 있는 데이터 분포에 검증 범위를 제한할 수 있도록 설계된 흐름 기반 밀도 모델이다. 이 모델은 조각별 선형 변환을 통해 선형 산술 기반 검증 도구를 사용할 수 있게 하며, 데이터 분포의 상위 밀도 레벨 집합(UDL)을 잠재 공간에서 선형 제약으로 정의할 수 있게 한다.
