Goedel-Prover: 오픈 소스 자동 정리증명을 위한 프론티어 모델

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving

February 11, 2025

저자: Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, Chi Jin

cs.AI

초록

우리는 수학 문제에 대한 자동 형식 증명 생성에서 최첨단 성능을 달성하는 오픈 소스 대형 언어 모델인 Goedel-Prover를 소개합니다. 이 분야의 주요 과제는 형식화된 수학 문장과 증명의 부족이며, 이를 해결하기 위해 다음과 같은 방법을 사용합니다. 우리는 문장 형식화기를 훈련시켜 Numina의 자연어 수학 문제를 형식 언어(Lean 4)로 번역하여 164만 개의 형식적 문장 데이터셋을 작성합니다. 대형 언어 모델(Large Language Models)은 형식적 문장이 원래의 자연어 문제 내용을 정확하게 보존하는지 확인하는 데 사용됩니다. 그런 다음 일련의 증명기를 훈련시킴으로써 형식적인 증명의 대규모 데이터셋을 반복적으로 구축합니다. 각 증명기는 이전 것들이 증명하지 못한 많은 문장을 증명에 성공하며, 이러한 새로운 증명은 다음 증명기의 훈련 세트에 추가됩니다. 최종 증명기는 전체 증명 생성에서 모든 기존 오픈 소스 모델을 능가합니다. miniF2F 벤치마크에서 57.6%의 성공률(Pass@32)을 달성하여, 이전 최고의 오픈 소스 모델보다 7.6% 높습니다. PutnamBench에서 Goedel-Prover는 7개의 문제를 성공적으로 해결(Pass@512)하여 리더보드에서 1위를 차지합니다. 더불어, Lean Workbook 문제에 대해 29.7K개의 형식적인 증명을 생성하여, 이전 작업에서 생성된 15.7K를 거의 두 배로 늘립니다.

English

We introduce Goedel-Prover, an open-source large language model (LLM) that achieves the state-of-the-art (SOTA) performance in automated formal proof generation for mathematical problems. The key challenge in this field is the scarcity of formalized math statements and proofs, which we tackle in the following ways. We train statement formalizers to translate the natural language math problems from Numina into formal language (Lean 4), creating a dataset of 1.64 million formal statements. LLMs are used to check that the formal statements accurately preserve the content of the original natural language problems. We then iteratively build a large dataset of formal proofs by training a series of provers. Each prover succeeds in proving many statements that the previous ones could not, and these new proofs are added to the training set for the next prover. The final prover outperforms all existing open-source models in whole-proof generation. On the miniF2F benchmark, it achieves a 57.6% success rate (Pass@32), exceeding the previous best open-source model by 7.6%. On PutnamBench, Goedel-Prover successfully solves 7 problems (Pass@512), ranking first on the leaderboard. Furthermore, it generates 29.7K formal proofs for Lean Workbook problems, nearly doubling the 15.7K produced by earlier works.