수학적 표현의 생성
사람의 증명과 비교할 때 자동 증명기의 어려움 가운데 하나는 필요한 수학적 표현을 새로 만들어 내는 것이다. 소개 연구는 언어 모델의 생성 능력으로 이 한계를 다룰 가능성을 탐구했다.
형식 언어 안에서의 탐색
Metamath의 형식화 언어를 대상으로 자동 증명기와 보조 도구를 제시했다. 자연어로 그럴듯한 설명을 만드는 작업과 달리 형식적인 증명을 찾는 문제를 다룬다.
언어 모델의 성능 분석
연구는 Transformer 기반 생성 모델을 증명 과정에 적용하고 결과를 분석했다. 코드나 자연어의 생성에서 쓰이는 모델을 수학적 증명 탐색으로 연결한 사례다.
라이브러리에 채택된 짧은 증명
초기 논문은 GPT-f가 찾은 새로운 짧은 증명이 주 Metamath 라이브러리에 받아들여졌다고 보고했다. 이는 새 정리를 발견했다는 의미보다 기존 주장에 대한 증명 경로를 새로 찾은 성과로 이해해야 한다.
관련 문서
miniF2F / HOList / LeanDojo / Lean 증명 도구 / 언어 모델 / 논리학