본 논문은 심층 신경망(DNN) 검증기의 신뢰성을 높이기 위한 연구를 다룹니다. 기존 DNN 검증기들은 오류와 수치 부정확성에 취약하다는 문제점이 있었으며, 이를 해결하기 위해 결과에 대한 독립적인 알고리즘 검증이 가능한 인증서 생성 기능을 추가하는 시도가 있었습니다. 하지만 기존의 C++ 기반 Marabou 인증서 검증 구현은 여전히 신뢰성 문제(예: 부동 소수점 계산의 정확도, 구현의 건전성 보장)를 가지고 있습니다. 본 논문에서는 산업용 함수형 프로그래밍 언어이자 대화형 정리 증명기(ITP)인 Imandra를 사용하여 Marabou 인증서 검증을 재구현함으로써 인증서 정확성에 대한 완전한 증명을 얻는 방법을 제시합니다. 이를 통해 Marabou 증명에 대한 더 강력한 독립적인 보장을 제공하고, ITP에서 DNN 검증기의 광범위한 채택을 위한 길을 열게 됩니다.
