초록
기초 검증(foundationally verified)을 통해 프로그래머는 다양한 중요한 분야에서 높은 수준의 신뢰성(assurance)을 경험적으로 입증받은 소프트웨어를 구축할 수 있다. 그러나 대부분의 프로젝트에서는 기초 검증 소프트웨어를 개발하는 데 드는 비용이 여전히 지나치게 높은 편이다. 이는 고도로 훈련된 전문가들의 상당한 수작업이 필요하기 때문이다. 본 논문에서는 머신러닝 기술을 활용해 상호작용 정리 증명기(interactive theorem provers)에서 소프트웨어 정확성의 증명을 생성하는 증명 검색 시스템인 Proverbot9001을 제안한다. 우리는 대규모 실용적 증명 프로젝트인 CompCert 검증 C 컴파일러에서 발생하는 증명 과제(proof obligations)를 대상으로 Proverbot9001의 성능을 검증하였으며, 기존에 수작업으로 수행되던 증명을 효과적으로 자동화할 수 있음을 보였다. 특히, 솔버 기반 도구와 결합했을 경우, 테스트 데이터셋 내 27.5%의 정리 문장에 대해 자동으로 증명을 생성할 수 있었다. 추가적인 솔버 없이도, Coq에서 증명을 생성하는 기존 최고 수준의 머신러닝 모델보다 4배에 달하는 증명 완성률을 달성함으로써, 기존 기술 대비 획기적인 성능 향상을 입증하였다.