하이퍼트리 증명 검색: 신경망 정리 증명을 위한 접근법

우리는 변환기 기반 자동 정리 증명기(automated theorem prover)를 위한 온라인 학습 절차를 제안한다. 본 연구의 접근법은 최근 알파제로(AlphaZero)의 성공에 영감을 받아 개발된 새로운 탐색 알고리즘인 하이퍼트리 증명 탐색(HyperTree Proof Search, HTPS)을 활용한다. 제안하는 모델은 온라인 학습을 통해 과거의 증명 탐색 경험을 학습함으로써, 학습 분포와 거리가 먼 영역에도 일반화할 수 있다. 본 연구에서는 복잡도가 점차 증가하는 세 가지 환경에서 성능을 분석함으로써, 전체 파이프라인의 주요 구성 요소에 대한 세부적인 아블레이션(ablation)을 보고한다. 특히, HTPS만을 사용할 경우, 주석이 달린 증명 데이터로 훈련된 모델이 보류된 메타마스(Metamath) 정리 집합의 65.4%를 증명할 수 있음을 보여주며, 이는 기존 최고 성능인 GPT-f의 56.5%를 크게 상회한다. 이러한 미증명된 정리들에 대한 온라인 학습을 통해 정확도는 82.6%까지 향상된다. 유사한 계산 자원 예산 하에서, 리인(Lean) 기반의 미니F2F 커리큘럼 데이터셋에 대해 기존 최고 성능인 31%에서 42%로 증명 정확도를 개선하였다.