Goedel-Prover: Een vooruitstrevend model voor open-source geautomatiseerd stellingbewijs.

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

February 11, 2025

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

cs.AI

Samenvatting

We introduceren Goedel-Prover, een open-source groot taalmodel (LLM) dat de state-of-the-art (SOTA) prestaties behaalt in geautomatiseerde formele bewijsvoering voor wiskundige problemen. De belangrijkste uitdaging in dit vakgebied is het gebrek aan geformaliseerde wiskundige verklaringen en bewijzen, die we op de volgende manieren aanpakken. We trainen verklaringsformaliseerders om de natuurlijke taal wiskundige problemen van Numina naar formele taal (Lean 4) te vertalen, waarbij we een dataset van 1,64 miljoen formele verklaringen creëren. LLM's worden gebruikt om te controleren of de formele verklaringen nauwkeurig de inhoud van de oorspronkelijke natuurlijke taal problemen behouden. Vervolgens bouwen we iteratief een grote dataset van formele bewijzen door een reeks bewijzers te trainen. Elke bewijzer slaagt erin om veel verklaringen te bewijzen die de vorige niet konden, en deze nieuwe bewijzen worden toegevoegd aan de trainingsset voor de volgende bewijzer. De uiteindelijke bewijzer presteert beter dan alle bestaande open-source modellen in het genereren van volledige bewijzen. Op de miniF2F benchmark behaalt het een succespercentage van 57,6% (Pass@32), wat het vorige beste open-source model met 7,6% overtreft. Op PutnamBench lost Goedel-Prover succesvol 7 problemen op (Pass@512), waarbij het eerste staat op de ranglijst. Bovendien genereert het 29,7K formele bewijzen voor Lean Workbook problemen, bijna het dubbele van de 15,7K geproduceerd door eerdere werken.

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.