Generative language modeling for automated theorem proving

Motivation

• Known: 기존 딥러닝 기반 정리 증명 연구는 주로 premise selection과 proof guidance에 CNN, RNN, GNN을 활용했으며(DeepMath, FormulaNet, HOList), Metamath 환경에서는 Holophrasm과 MetaGen-IL 같은 RNN 기반 모델이 사용되어 왔다.
• Gap: 자동 정리 증명기가 인간에 비해 갖는 주요 한계인 새로운 수학적 항(term)의 생성 능력이 language model의 생성 능력으로 보완될 수 있는지, 그리고 Transformer 기반 생성 모델이 formal reasoning 과제에 실제로 얼마나 효과적인지는 충분히 검증되지 않았다.
• Why: 추론(reasoning)은 AlphaGo/AlphaZero를 제외하면 신경망 연구에서 상대적으로 성공 사례가 적은 영역이며, 자동 정리 증명은 검증 가능성과 자동 데이터 생성이 가능해 reasoning 연구를 위한 유망한 테스트베드가 될 수 있다.
• Approach: GPT-f라는 transformer 기반 자동 증명기 및 proof assistant를 Metamath 환경에 구축하고, generative pre-training과 value function을 결합한 반복적 자기개선(self-improvement) 전략으로 증명 탐색 성능을 향상시켰다.

Achievement

1. 성능 검증: generative pre-training이 성능을 크게 향상시키며, arXiv 같은 수학 데이터로 사전학습하는 것이 일반 웹 텍스트 사전학습보다 우수함을 확인했다.
2. 모델 크기 상관관계: Metamath 데이터셋 규모가 상대적으로 작음에도 모델 크기가 커질수록 성능이 향상됨을 발견했다.
3. 자기개선 전략: 언어 모델이 생성한 statement들에 대해 value function을 반복적으로 학습시키는 것이 prover 성능을 개선하며, 이는 prover가 생성한 증명으로 계속 학습하는 지속적 자기개선 전략으로 이어질 수 있음을 보였다.
4. SOTA 달성: held-out 테스트셋 기준 56.22%의 증명을 닫아 기존 SOTA인 MetaGen-IL의 21.16%를 크게 상회했다.
5. 실제 채택: GPT-f가 발견한 새로운 짧은 증명이 Metamath 메인 라이브러리(set.mm)에 실제로 채택되어, 딥러닝 기반 시스템이 formal mathematics 커뮤니티에 기여한 최초 사례가 되었다.

How

Proof search consists in maintaining a proof tree where multiple tactics are explored for

• Metamath를 formal environment로 채택: 검증이 빠르고, proof step이 context-free하며, 간결한 subgoal 표현이 가능하다는 장점 활용
• Backward proving 방식으로 목표(goal)에서 시작해 axiom까지 도달하는 proof tree를 구성 (Fig 1)
• transformer 언어 모델을 사용해 각 단계에서 적용할 proof step(정리 선택 및 substitution)을 생성
• arXiv 등 수학 관련 코퍼스로 generative pre-training 수행 후 Metamath 데이터로 fine-tuning
• 생성된 statement들에 대해 value function을 반복적으로 학습시켜 proof search를 안내하고, 모델이 생성한 증명을 다시 학습 데이터로 활용하는 self-improvement loop 구축
• IMO 1972 problem B2 등 실제 문제를 GPT-f 보조로 formalization하여 사례 연구 제시

Originality

• 기존 premise selection이나 proof guidance 중심의 접근과 달리, 생성형 언어 모델을 직접 활용해 substitution 및 proof step 자체를 생성하는 방식을 formal theorem proving에 적용
• 수학 코퍼스(arXiv) 기반 사전학습이 정리 증명 성능에 미치는 영향을 최초로 체계적으로 분석
• 언어 모델이 생성한 statement에 대해 value function을 반복 학습시켜 self-improvement를 이끄는 프레임워크 제시
• 딥러닝 시스템이 생성한 증명이 실제 formal mathematics 커뮤니티 라이브러리에 채택된 최초 사례로서 실질적 파급력을 입증

Limitation & Further Study

• Metamath는 저수준(low-level) 증명 스텝을 사용하는 시스템으로 de-bruijn factor가 커서(~10-20) 증명이 길어지고 탐색 오류가 누적될 가능성이 있어, Lean이나 Coq 같은 고수준 tactic 기반 시스템으로의 일반화 가능성에 대한 추가 검증이 필요함
• Metamath 자체가 툴링이 미비하고 수학 커뮤니티에서 폭넓게 채택되지 않은 "DIY" 시스템이라는 한계가 있어 실제 적용 범위가 제한적일 수 있음
• self-improvement 루프의 장기적 안정성과 확장성(다양한 도메인 및 더 어려운 정리로의 일반화)에 대한 심층 분석이 부족함
• 후속 연구로 Lean, Coq, HOL Light 등 고수준 formal system에 동일 접근법을 확장 적용하는 연구가 필요함

Evaluation

총평: Transformer 기반 생성 언어 모델을 자동 정리 증명에 성공적으로 적용하여 SOTA를 크게 경신하고, 실제 formal mathematics 커뮤니티에 기여한 최초의 딥러닝 시스템이라는 점에서 매우 의미 있는 이정표적 연구이다.