Goedel-Prover: A Frontier Model for Open-Source Automated Theorem
  Proving
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.
67acb6af4335fbde70348fc1
Yong Lin
67acb6af4335fbde70348fc2
Shange Tang
claimed_verified
2025-03-24T08:55:48.351Z
669fa6ed3219ee9f3a645157
/avatars/0325f4e99e0c494ce2525c71884bc3b0.svg
Shange Tang
user
shangetang
67acb6af4335fbde70348fc3
Bohan Lyu
claimed_verified
2025-02-18T09:34:20.642Z
650267e7e751d03da933a24a
/avatars/f047a047d1de304cd97027463541bdf3.svg
Bohan22
user
Bohan22
67acb6af4335fbde70348fc4
Jiayun Wu
67acb6af4335fbde70348fc5
Hongzhou Lin
67acb6af4335fbde70348fc6
Kaiyu Yang
67acb6af4335fbde70348fc7
Jia Li
67acb6af4335fbde70348fc8
Mengzhou Xia
67acb6af4335fbde70348fc9
Danqi Chen
67acb6af4335fbde70348fca
Sanjeev Arora
67acb6af4335fbde70348fcb
Chi Jin
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem
  Proving
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.
Goedel-Prover, an open-source large language model, excels in automated formal proof generation through the iterative training of statement formalizers and provers, significantly outperforming existing models on various benchmarks.
large language model LLM formal proof generation statement formalizers formal language Lean 4 formal proofs miniF2F benchmark PutnamBench Lean Workbook problems