Goedel-LM
/

Goedel-Prover-V2-8B

+---
+license: apache-2.0
+base_model:
+- Qwen/Qwen3-8B
+---
+<div align="center">
+    <h1> <a href="http://blog.goedel-prover.com"> <strong>Goedel-Prover-V2: The Strongest Open-Source Theorem Prover to Date</strong></a></h1>
+</div>
+<head>
+  <meta charset="UTF-8">
+  <style>
+    .badges {
+      display: flex;
+      justify-content: center;
+      gap: 0.5rem;  /* eliminate whitespace between badges */
+      padding: 0.8rem;
+    }
+    .badge {
+      display: inline-flex;       /* inline flex for pill layout */
+      align-items: center;        /* center icon & text vertically */
+      padding: 0.4rem 0.4rem;        /* larger badge size */
+      background: #333;
+      color: #fff;                 /* white text */
+      text-decoration: none;
+      font-family: sans-serif;
+      font-size: 0.8rem;          /* larger font */
+      border-radius: 999em;        /* full pill shape */
+      transition: background 0.15s;/* smooth hover */
+    }
+    .badge:hover {
+      background: #444;
+    }
+    .badge svg,
+    .badge .emoji {
+      width: 1.7em; /* scale icons with badge text */
+      height: 1.7em;
+      margin-right: 0.5em;
+      fill: currentColor; /* inherit badge color */
+    }
+  </style>
+</head>
+<body>
+  <div class="badges">
+    <a href="#" class="badge" target="_blank" rel="noopener">
+      <svg viewBox="-64 0 512 512" xmlns="http://www.w3.org/2000/svg">
+        <path d="M369.9 97.9L286 14C277 5 264.8-.1 252.1-.1H48C21.5 0 0 21.5 0 48v416c0 26.5 21.5
+                 48 48 48h288c26.5 0 48-21.5 48-48V131.9c0-12.7-5.1-25-14.1-34zM332.1 128H256V51.9l76.1
+                 76.1zM48 464V48h160v104c0 13.3 10.7 24 24 24h104v288H48zm250.2-143.7c-12.2-12-47-8.7
+                 -64.4-6.5-17.2-10.5-28.7-25-36.8-46.3 3.9-16.1 10.1-40.6 5.4-56-4.2-26.2-37.8-23.6
+                 -42.6-5.9-4.4 16.1-.4 38.5 7 67.1-10 23.9-24.9 56-35.4 74.4-20 10.3-47 26.2-51
+                 46.2-3.3 15.8 26 55.2 76.1-31.2 22.4-7.4 46.8-16.5 68.4-20.1 18.9 10.2 41 17 55.8
+                 17 25.5 0 28-28.2 17.5-38.7zm-198.1 77.8c5.1-13.7 24.5-29.5 30.4-35-19 30.3-30.4
+                 35.7-30.4 35zm81.6-190.6c7.4 0 6.7 32.1 1.8 40.8-4.4-13.9-4.3-40.8-1.8-40.8zm-24.4
+                 136.6c9.7-16.9 18-37 24.7-54.7 8.3 15.1 18.9 27.2 30.1 35.5-20.8 4.3-38.9 13.1-54.8
+                 19.2zm131.6-5s-5 6-37.3-7.8c35.1-2.6 40.9 5.4 37.3 7.8z"/>
+      </svg>arXiv (coming soon)</a><a href="http://blog.goedel-prover.com"
+         class="badge" target="_blank" rel="noopener">
+      <span class="emoji"><h1>🌐</h1></span>Website</a><a href="https://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B"
+         class="badge" target="_blank" rel="noopener">
+      <span class="emoji"><h1>🤗</h1></span>HuggingFace</a><a href="#"
+         class="badge" target="_blank" rel="noopener">
+      <svg viewBox="0 0 64 64" xmlns="http://www.w3.org/2000/svg">
+        <path d="M32.029,8.345c-13.27,0-24.029,10.759-24.029,24.033c0,10.617 6.885,19.624
+                 16.435,22.803c1.202,0.22 1.64-0.522 1.64-1.16c0-0.569-0.02-2.081-0.032-4.086
+                 c-6.685,1.452-8.095-3.222-8.095-3.222c-1.093-2.775-2.669-3.514-2.669-3.514
+                 c-2.182-1.492,0.165-1.462,0.165-1.462c2.412,0.171 3.681,2.477 3.681,2.477
+                 c2.144,3.672 5.625,2.611 6.994,1.997c0.219-1.553 0.838-2.612 1.526-3.213
+                 c-5.336-0.606-10.947-2.669-10.947-11.877c0-2.623 0.937-4.769 2.474-6.449
+                 c-0.247-0.608-1.072-3.051 0.235-6.36c0,0 2.018-0.646 6.609,2.464c1.917-0.533
+                 3.973-0.8 6.016-0.809c2.041,0.009 4.097,0.276 6.017,0.809c4.588-3.11
+                 6.602-2.464 6.602-2.464c1.311,3.309 0.486,5.752 0.239,6.36c1.54,1.68
+                 2.471,3.826 2.471,6.449c0,9.232-5.62,11.263-10.974,11.858c0.864,0.742
+                 1.632,2.208 1.632,4.451c0,3.212-0.029,5.804-0.029,6.591c0,0.644
+                 0.432,1.392 1.652,1.157c9.542-3.185 16.421-12.186 16.421-22.8c0-13.274
+                 -10.76-24.033-24.034-24.033"/>
+      </svg>Code (coming soon)</a>
+  </div>
+</body>
+## 1. Introduction
+We introduce Goedel-Prover-V2, an open-source language model series that achieves state-of-the-art performance in automated formal proof generation. Our models build on the standard expert iteration and reinforcement learning pipeline, with three novel methodologies: (1) data synthesis for curriculums, which creates and augments intermediate problems to bridge the gap between simple and difficult proofs; (2) compiler-guided self-correction, where the model is trained to iteratively correct its own proofs using lean compiler feedback, mimicking human problem-solving; and (3) model averaging.
+Our small model, Goedel-Prover-V2-8B, reaches 83.0% on MiniF2F test set at Pass@32, matching the performance of DeepSeek-Prover-V2-671B while being nearly 100 times smaller in model size.  Our flagship model, Goedel-Prover-V2-32B, achieves 88.0% on MiniF2F at Pass@32 and 90.4% with additional two rounds of self-correction (only increasing max output length from 32K to 40K), outperforming prior SOTA DeepSeek-Prover-V2-671B and concurrent work Kimina-Prover-72B by a large margin. Additionaly, Goedel-Prover-V2-32B solves 57 problems on PutnamBench with 32 sample budget and 2 rounds of self-correction per sample, securing the 1st on the leaderboard by beating DeepSeek-Prover-V2-671B's 47 by doing Pass@1024.
+## 2. Benchmark Performance
+<style>
+  .fig-row {
+    display: flex;
+    justify-content: space-between; /* spread them out */
+    align-items: flex-start;        /* align tops */
+    gap: 1rem;                      /* space between images */
+  }
+  .fig-row img {
+    display: block;
+    width: 100%;
+    height: auto;
+  }
+  .fig-row .panel {
+    /* override per‐panel width as needed */
+    /* e.g. .panel-1 { width:25%; } .panel-2 { width:40%; } etc. */
+  }
+  figure {
+    margin: 0;
+  }
+  figure figcaption {
+    text-align: center;
+    font-size: 0.9em;
+    margin-top: 0.75rem;
+    color: #555;
+  }
+ figure figcaption strong {
+    font-weight: bold;
+  }
+  /* Italicize the rest of the caption */
+  figure figcaption em {
+    font-style: italic;
+  }
+</style>
+<figure>
+  <div class="fig-row">
+    <div class="panel panel-1" style="width:100%;">
+      <img src="https://github.com/Goedel-LM/Goedel-Prover-V2/blob/main/assets/combined_performance_plots_varied_width.png?raw=true" alt="…">
+    </div>
+  </div>
+  <figcaption>
+    <strong>Figure 1</strong>: <em>Pass@32 performance on MiniF2F, PutnamBench, and our new FoMOBench containing 360 IMO-level problems.</em>  </figcaption>
+</figure>
+The charts above demonstrate the state-of-the-art performance of Goedel-Prover-V2. Goedel-Prover-V2+2 rounds of self-correction indicates that the model first do full proof generation and then correct the proof according to the lean compilation feedback.  <strong>Goedel-Prover-V2+2 rounds of self-correction only increases the max output length from 32K to 40K over other models.</strong>
+<strong>(Left)</strong> On the widely-used MiniF2F benchmark, our 8B model achieves 83.0%, matching much larger models, while our 32B model reaches 88.0% (90.4% with self-correction), outperforming all previous models.
+<strong>(Middle)</strong> On the challenging PutnamBench, our 32B model solves 43 problems, a significant leap over the previous best of 23.
+<strong>(Right)</strong> On our newly curated FoMOBench, which contains 360 IMO-level problems, our 32B model solves 73 problems, surpassing DeepSeek-Prover-V2-671B's 50.
+<div align="center">
+  <table style="margin: 0 auto;">
+    <thead>
+      <tr>
+        <th>#</th>
+        <th>Model</th>
+        <th>num‑solved</th>
+        <th>compute</th>
+      </tr>
+    </thead>
+    <tbody>
+      <tr><td>1</td><td>Goedel-Prover-V2-32B (two rounds of self-correction)</td><td>64</td><td>Pass@64</td></tr>
+      <tr><td>1</td><td>Goedel-Prover-V2-32B (two rounds of self-correction)</td><td>57</td><td>Pass@32</td></tr>
+      <tr><td>1</td><td>Goedel-Prover-V2-32B</td><td>43</td><td>Pass@32</td></tr>
+      <tr><td>2</td><td>DeepSeek‑Prover‑V2-671B</td><td>47</td><td>pass@1024</td></tr>
+      <tr><td>2</td><td>DeepSeek‑Prover‑V2-671B</td><td>22</td><td>pass@32</td></tr>
+      <tr><td>3</td><td>DSP+</td><td>23</td><td>pass@128</td></tr>
+      <tr><td>4</td><td>Kimina‑Prover‑7B‑Distill</td><td>10</td><td>pass@192</td></tr>
+    </tbody>
+  </table>
+    <!-- table caption -->
+    <caption align="bottom"><strong>Table 1</strong>: <em>PutnamBench leaderboard. Goedel-Prover-V2-32B secures the top rank with significantly less compute than the previous SOTA.  <strong>Goedel-Prover-V2 (self-correction) only increase the max output length from 32K to 40K over other models.</strong> Note that DeepSeek-Prover-V2-671B's score of 47 was achieved with a much larger sample budget (pass@1024).</em>
+</div>
+## 3. Compelling Scaling Performance
+<style>
+  .fig-row {
+    display: flex;
+    justify-content: space-between; /* spread them out */
+    align-items: flex-start;        /* align tops */
+    gap: 1rem;                      /* space between images */
+  }
+  .fig-row img {
+    display: block;
+    width: 100%;
+    height: auto;
+  }
+  .fig-row .panel {
+    /* override per‐panel width as needed */
+    /* e.g. .panel-1 { width:25%; } .panel-2 { width:40%; } etc. */
+  }
+  figure {
+    margin: 0;
+  }
+  figure figcaption {
+    text-align: center;
+    font-size: 0.9em;
+    margin-top: 0.75rem;
+    color: #555;
+  }
+ figure figcaption strong {
+    font-weight: bold;
+  }
+  /* Italicize the rest of the caption */
+  figure figcaption em {
+    font-style: italic;
+  }
+</style>
+<figure>
+  <div class="fig-row">
+    <div class="panel panel-1" style="width:80%;">
+      <img src="https://github.com/Goedel-LM/Goedel-Prover-V2/blob/main/assets/inference_scale_performance.png?raw=true" alt="…">
+    </div>
+  </div>
+  <figcaption>
+    <strong>Figure 2</strong>: <em>Performance on MiniF2F test set under different sample budgets.</em>
+  </figcaption>
+</figure>
+The scaling curves highlight our models' efficiency and effectiveness.
+<strong>(Left)</strong> The raw performance (Pass@K) shows that both our 8B and 32B models consistently improve as the number of samples (K) increases, demonstrating robust problem-solving capability.
+<strong>(Right)</strong> The compute-adjusted performance plot further reveals that our models are highly efficient, achieving strong results even at lower compute budgets compared to other models. This underscores the effectiveness of our training methodology.
+## 4. Model & Dataset Downloads
+We release Goedel-Prover-V2 in two model sizes: 8B and 32B parameters, which are trained on top of Qwen3-8B and Qwen3-32B respectively. We also release FoMOBench, which serves as a benchmark more close to the International Mathematics Olympiad (IMO).
+<div align="center">
+| Model | Download |
+| -------- | -------- |
+|    Goedel-Prover-V2-32B    |   [🤗Download](https://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B)    |
+|    Goedel-Prover-V2-8B    |   [🤗Download](https://huggingface.co/Goedel-LM/Goedel-Prover-V2-8B)    |
+</div>
+<div align="center">
+| Dataset | Download |
+| -------- | -------- |
+|    FoMOBench    |   [🤗Download](https://huggingface.co/datasets/Goedel-LM/FoMOBench)    |
+</div>
+## 5. Quick Start
+You can directly use [Huggingface's Transformers](https://github.com/huggingface/transformers) for model inference.
+```
+from transformers import AutoModelForCausalLM, AutoTokenizer
+import torch
+torch.manual_seed(30)
+model_id = "Goedel-LM/Goedel-Prover-V2-32B"
+tokenizer = AutoTokenizer.from_pretrained(model_id)
+model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
+formal_statement = """
+import Mathlib
+import Aesop
+set_option maxHeartbeats 0
+open BigOperators Real Nat Topology Rat
+theorem square_equation_solution {x y : ℝ} (h : x^2 + y^2 = 2*x - 4*y - 5) : x + y = -1 := by
+  sorry
+""".strip()
+prompt = """
+Complete the following Lean 4 code:
+```lean4
+{}```
+Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
+The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
+""".strip()
+chat = [
+  {"role": "user", "content": prompt.format(formal_statement)},
+]
+inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)
+import time
+start = time.time()
+outputs = model.generate(inputs, max_new_tokens=32768)
+print(tokenizer.batch_decode(outputs))
+print(time.time() - start)
+```
+### Cite
+```bibtex
+@misc{lin2025goedelproverv2,
+    title={Goedel-Prover-V2: The Strongest Open-Source Theorem Prover to Date},
+    author={Yong Lin and Shange Tang and Bohan Lyu and Ziran Yang and Jui-Hui Chung and Haoyu Zhao and Hongzhou Lin and Lai Jiang and Yihan Geng and Jiawei Ge and Jingruo Sun and Jiayun Wu and Jiri Gesi and David Acuna and Kaiyu Yang  and Yejin Choi and Danqi Chen and Sanjeev Arora and Chi Jin},
+    year={2025}
+}
+```