HOList: 고차 정리 증명을 위한 기계 학습 환경

우리는 고차 논리에 대한 환경, 벤치마크 및 딥러닝 기반의 자동 정리 증명기를 제시합니다. 고차 상호작용형 정리 증명기는 임의의 수학 이론을 형식화할 수 있어 딥러닝에게 흥미롭고 개방적인 도전 과제를 제공합니다. 우리는 HOL Light 정리 증명기 기반의 강화 학습 환경으로 사용될 수 있는 오픈 소스 프레임워크를 제공합니다. HOL Light는 미적분학과 케플러 추측의 형식적 증명을 포함하는 광범위한 기본 수학 정리를 다루고 있으며, 이를 바탕으로 자동 추론을 위한 도전적인 벤치마크를 도출하였습니다. 또한, 이 벤치마크에서 우수한 초기 결과를 보인 딥러닝 기반의 강화 학습 자동 정리 증명기인 DeepHOL을 소개합니다.