HolStep: 고차 논리 정리 증명을 위한 기계 학습 데이터셋

대규모 컴퓨터가 이해할 수 있는 증명은 수백만 개의 중간 논리 단계로 구성됩니다. 이러한 단계의 대부분은 중간 목표에 적용된 수동으로 선택되고 수동으로 안내되는 휴리스틱에서 비롯됩니다. 지금까지 기계 학습은 일반적으로 이러한 단계를 필터링하거나 생성하는 데 사용되지 않았습니다. 본 논문에서는 고차 논리(Higher-Order Logic, HOL) 증명을 기반으로 하는 새로운 데이터셋을 소개합니다. 이 데이터셋은 BSD 라이선스 하에 공개적으로 이용 가능하도록 제공됩니다. 또한 이 데이터셋에서 수행할 수 있는 다양한 기계 학습 작업들을 제안하고, 그것들이 정리 증명에 미치는 중요성을 논의합니다. 우리는 이러한 작업에 적합한 간단한 베이스라인 기계 학습 모델(로지스틱 회귀, 컨벌루션 신경망, 순환 신경망 등을 포함)을 벤치마킹합니다. 우리의 베이스라인 모델들의 결과는 기계 학습을 HOL 정리 증명에 적용하는 가능성을 보여줍니다.