초록
트랜스포머 기반 언어 모델을 자동 정리 증명에 적용하는 것을 탐구한다. 본 연구는 인간과 비교해 자동 정리 증명기의 주요한 한계 중 하나인 원초적인 수학적 용어 생성 문제를 언어 모델의 생성 능력을 통해 극복할 수 있다는 가능성을 동기로 삼고 있다. 우리는 메타마스(Metamath) 형식화 언어를 대상으로 하는 자동 증명기이자 증명 보조 도구인 GPT-f를 제안하고, 그 성능을 분석한다. GPT-f는 메타마스 주 라이브러리에 채택된 새로운 짧은 증명을 발견하였으며, 본 연구에 따르면 이는 딥러닝 기반 시스템이 공식 수학 커뮤니티에 의해 채택된 증명을 제안한 최초의 사례로 알려져 있다.