Goedel-Prover-V2 - An open-source theorem proving model by Princeton, Tsinghua, and others

What is Goedel-Prover-V2

Goedel-Prover-V2 is an open-source theorem prover jointly launched by top institutions such as Princeton University, Tsinghua University, and NVIDIA. Goedel-Prover-V2 significantly improves the performance of automated formal proof generation through innovative techniques such as scaffolded data synthesis, verifier-guided self-correction, and model averaging. The model includes two parameter versions: 32B and 8B. The 32B model achieves a 90.4% Pass@32 score on the MiniF2F benchmark, surpassing the 671BDeepSeek-Prover-V2. Goedel-Prover-V2 ranks first on the PutnamBench and MathOlympiadBench benchmarks, demonstrating strong theorem proving capabilities. The release of Goedel-Prover-V2 provides a new milestone for AI research in the field of mathematical theorem proving.

Main features of Goedel-Prover-V2

• Automatic proof generation: Generates formal proofs for complex mathematical problems.
• Self-correction capability: Through feedback from the Lean compiler, the model can iteratively correct its own proofs and improve proof quality.
• Efficient training and optimization: Uses scaffolded data synthesis and model averaging techniques to improve training efficiency and model performance.
• Open source and scalability: Provides open-source models and datasets, making it easy for researchers to further develop and improve them.

Technical principles of Goedel-Prover-V2

• Scaffolded Data Synthesis: Automatically generates proof tasks with gradually increasing difficulty, helping the model progressively transition from simple problems to complex ones. By generating intermediate-difficulty problems, it fills the gap between simple and complex problems and provides denser training signals.
• Verifier-Guided Self-Correction: The model uses feedback from the Lean compiler to learn how to iteratively correct its own proofs. It closely simulates the correction process of humans when refining proofs, improving the accuracy and reliability of proofs.
• Model Averaging: By averaging model checkpoints from multiple training stages, it restores the diversity of the model. It significantly improves the model's overall performance under larger Pass@K values and enhances robustness.

Performance of Goedel-Prover-V2

• MiniF2F benchmark：
  • 32B model：
    • Pass@32: Achieves 90.4%, significantly outperforming DeepSeek-Prover-V2-671B's 82.4%.
    • Self-correction mode: In self-correction mode, the Pass@32 score is further improved to 90.4%.
  • 8B model：
    • Pass@32: Achieves 83.3%, comparable to DeepSeek-Prover-V2-671B's 82.4%, but with a model size nearly 100 times smaller.
• PutnamBench benchmark：
  • 32B model：
    • Pass@64: Solves 64 problems, ranking first.
    • Pass@32: Solves , 57 problems, significantly outperforming DeepSeek-Prover-V2-671B's 47 problems.
  • 8B model：
    • Pass@32: Also performs very well, comparable to DeepSeek-Prover-V2-671B.
• MathOlympiadBench benchmark：
  • 32B model: Solves 73 problems, significantly outperforming DeepSeek-Prover-V2-671B's 50 problems.
  • 8B model: Performs very close as well, demonstrating strong theorem proving capabilities.

Project address of Goedel-Prover-V2

• Project website：https://blog.goedel-prover.com/
• HuggingFace Model Hub：
  • https://huggingface.co/Goedel-LM/Goedel-Prover-V2-8B
  • https://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B

Application scenarios of Goedel-Prover-V2

• Mathematical theorem proving: Automatically generate formal proofs of mathematical theorems, helping mathematicians verify conjectures, explore new mathematical theories, and accelerate the progress of mathematical research.
• Software and hardware verification: In software development and hardware design, verify the correctness of algorithms, program logic, and circuit designs. Use formal proofs to ensure the reliability of software and hardware systems, reduce errors and vulnerabilities, and improve system security.
• Education: As an auxiliary tool for mathematics education, provide students with examples of formal proofs to help them better understand and master mathematical concepts and theorems.
• Artificial intelligence and machine learning: In the fields of artificial intelligence and machine learning, verify the mathematical foundations and algorithmic logic of models to ensure their reliability and accuracy.
• Scientific research and engineering: Verify mathematical models and theories in scientific research, helping scientists and engineers ensure the feasibility and reliability of design solutions.