Generative language modeling for automated theorem proving

Essence

트랜스포머 기반 생성 언어 모델을 자동 정리 증명(automated theorem proving)에 적용하여, 신경망이 형식 수학 추론 작업을 수행할 수 있음을 최초로 입증한 연구이다. GPT-f 시스템은 Metamath 라이브러리에 채택된 새로운 증명들을 생성함으로써, 딥러닝 기반 시스템이 공식 수학 커뮤니티에 기여한 첫 사례가 되었다.

Motivation

Known: AlphaGo/AlphaZero를 제외한 신경망 기반 시스템들은 주로 지각(vision), 번역, 음성 인식 등에서만 성공했으며, 추론(reasoning) 작업에서는 두드러진 성과가 없음
Gap: 자동 정리 증명 시스템은 인간과 달리 새로운 수학적 항(mathematical terms)을 생성하는 데 어려움을 겪음. 기존 방법들(premise selection, proof guidance)은 단편적 접근만 가능
Why: 정리 증명은 (1) 일반적 추론 능력 필요, (2) 빠른 정확성 검증 가능, (3) 자동 데이터 생성 가능이라는 점에서 신경망 추론 연구에 이상적인 도메인
Approach: Metamath 형식 시스템을 대상으로 GPT-2/GPT-3 스타일의 디코더 전용 트랜스포머를 적용하여 증명 단계(proof step)를 생성하는 방식으로 접근

Achievement

성과1 - 최고 성능 달성: Metamath 환경에서 새로운 최고 성능 기록 (56.22% vs 기존 21.16%)
성과2 - 실제 커뮤니티 기여: 생성된 증명이 Metamath 라이브러리에 채택됨 (신경망 시스템 최초)
성과3 - 학습 효과 검증:
- 수학 데이터(arXiv) 사전학습이 일반 웹 데이터보다 우수
- 모델 크기 증가가 성능 향상과 정상 상관관계 (작은 데이터셋에도 불구하고)
- 가치함수(value function) 반복 학습이 성능 개선 달성

How

증명 탐색(proof search)은 다양한 전술(tactics)을 탐색하는 증명 트리를 유지

핵심 방법론:

형식 환경 선택: Metamath set.mm (∼38k 증명, ZFC 집합론 기반)
- 장점: 빠른 검증, 문맥 자유적 목표 표현, 깨끗한 부분목표 표현
- 한계: 저수준 증명 단계 (de-bruijn factor ~10-20)
데이터셋 구성: 증명 단계 ∼300만개, 정리 ∼38k개
- GOAL, PROOFSTEP, 부모 목표 참조로 트리 구조 인코딩
- 훈련/검증/테스트 분할 (∼90k 단계씩)
모델 아키텍처:
- 디코더 전용 트랜스포머 (GPT-2/GPT-3 유사)
- 최대 36 레이어, 774M 매개변수
증명 생성 프로세스:
1. 후진 증명(backward proving): 증명할 명제에서 시작
2. 각 단계에서 적용 가능한 정리와 변수 대체(substitution) 생성
3. 언어 모델이 중간 항(intermediary terms) 자동 생성
4. 부분목표가 공리/이미 증명된 정리와 일치할 때까지 반복

Originality

처음의 시도: 트랜스포머를 형식 증명의 전체 증명 생성에 직접 적용 (기존 연구는 전제 선택이나 증명 지도(proof guidance) 같은 보조 작업만 수행)
신경망 기여 실증: 생성된 증명이 실제 공식 수학 라이브러리에 채택된 최초 사례
사전학습 효과 검증: 수학 특화 사전학습(arXiv)의 우월성을 정량적으로 입증
확장성 발견: 작은 데이터셋(3M 단계)에도 모델 크기 스케일링이 성능 향상을 가져옴을 보임