고차 논리의 증명 연구
고차 논리의 상호작용형 증명 도구는 다양한 수학 이론을 형식화할 수 있다. HOList는 이를 딥러닝의 열린 증명 과제로 다루는 환경과 벤치마크를 제시했다.
강화 학습을 위한 환경
HOL Light에 기반한 공개 프레임워크를 강화 학습 환경으로 사용할 수 있도록 했다. 정리의 목록만 제공하는 것을 넘어 증명 과정과 상호작용할 연구 기반을 마련한 것이다.
수학 라이브러리에서 얻은 평가
HOL Light의 미적분 기초 정리와 케플러 추측의 형식 증명 등에서 어려운 자동 추론 평가를 구성했다. 기존에 형식화된 수학을 학습과 평가의 기반으로 활용했다.
DeepHOL의 초기 결과
연구는 심층 강화 학습을 사용하는 자동 증명기 DeepHOL을 함께 소개했다. 환경과 평가 및 모델을 연결해 고차 논리 정리 증명의 가능성을 살핀 초기 연구다.
관련 문서
miniF2F / LeanDojo / Lean 증명 도구 / 강화 학습 / 논리학 / 추론