본 논문은 대규모 언어 모델(LLM)을 이용한 형식적 정리 증명에서 고품질 훈련 데이터 부족 문제를 해결하기 위해, 수학자들이 새로운 정리를 개발하는 방식에서 영감을 얻은 Self-play Theorem Prover (STP)를 제안합니다. STP는 추측 생성자와 증명자의 두 역할을 동시에 수행하며, 서로에게 훈련 신호를 제공하는 방식으로 동작합니다. 추측 생성자는 현재 증명자가 간신히 증명 가능한 수준의 추측을 반복적으로 생성하도록 훈련되며, 증명자는 표준 전문가 반복 학습을 통해 추측을 증명하려고 시도합니다. Lean 및 Isabelle 형식 검증기를 사용한 평가 결과, LeanWorkbook 데이터셋에서 28.5%의 정리를 증명하여 기존 최고 성능(13.2%)을 두 배 이상 능가하는 성과를 달성했습니다. 또한, miniF2F-test, Proofnet-test, PutnamBench 데이터셋에서도 최첨단 성능을 기록했습니다. 코드, 모델, 데이터셋은 공개되었습니다.
