초록
인간은 고차원적인 추론과 문제 특유의 통찰력을 바탕으로 정리를 증명합니다. 증명 보조 도구는 인간의 수학적 추론을 닮은 형식을 제공하며, 정리를 고차 논리로 표현하고 증명을 고차 전략으로 나타냅니다. 그러나 인간 전문가들은 증명 보조 도구에 전략을 수동으로 입력하여 증명을 구성해야 합니다. 본 논문에서는 기계 학습을 활용해 증명 보조 도구와의 상호작용을 자동화하는 문제를 연구합니다. 우리는 Coq 증명 보조 도구로 개발된 123개 프로젝트에서 71,000건의 인간이 작성한 증명을 포함하는 대규모 데이터셋 및 학습 환경인 CoqGym을 구축했습니다. 또한 ASTactic이라는 딥러닝 기반 모델을 개발하여, 추상 문법 트리(Abstract Syntax Trees, ASTs) 형태의 프로그램으로 전략을 생성합니다. 실험 결과, CoqGym에서 훈련된 ASTactic는 효과적인 전략을 생성할 수 있으며, 자동화된 방법으로 이전에 증명되지 않았던 새로운 정리를 증명하는 데 사용될 수 있음을 확인하였습니다. 코드는 https://github.com/princeton-vl/CoqGym에서 이용 가능합니다.