Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

• URL: http://arxiv.org/abs/2508.03613v1
• Date: Tue, 05 Aug 2025 16:28:22 GMT
• Title: Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
• Abstract summary: Goedel-Prover-V2, a series of open-source language models, set a new state-of-the-art in automated theorem proving.<n>We generate synthetic tasks of increasing difficulty to train the model to master increasingly complex theorems.<n>Goedel-Prover-V2-32B achieves 88.1% on MiniF2F at pass@32 in standard mode and 90.4% in self-correction mode.
• Score: 95.91743732150233
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: We introduce Goedel-Prover-V2, a series of open-source language models that set a new state-of-the-art in automated theorem proving. Built on the standard expert iteration and reinforcement learning pipeline, our approach incorporates three key innovations: (1) Scaffolded data synthesis: We generate synthetic tasks of increasing difficulty to train the model to master increasingly complex theorems; (2) Verifier-guided self-correction: We enable the model to iteratively revise its proofs by leveraging feedback from the Lean compiler; (3) Model averaging: We merge model checkpoints to mitigate the decrease in model output diversity in later stages of training. Our small model, Goedel-Prover-V2-8B, reaches 84.6% pass@32 on MiniF2F and outperforms DeepSeek-Prover-V2-671B under the same metric, despite being 80X smaller. Our flagship model, Goedel-Prover-V2-32B, achieves 88.1% on MiniF2F at pass@32 in standard mode and 90.4% in self-correction mode, outperforming prior SOTA by a large margin. Additionally, our flagship model solves 86 problems on PutnamBench at pass@184, securing the first place among open-source models on the leaderboard, surpassing DeepSeek-Prover-V2-671B's record of solving 47 problems by pass@1024 with a significantly smaller model size and compute budget. At the time of its release (July-August 2025), Goedel-Prover-V2 achieves the strongest overall performance among all open-source theorem provers. It also ranks among the top-performing models--including closed-source systems with publicly reported performance--under a constrained test-time compute budget. Our models, code, and data are released at https://github.com/Goedel-LM/Goedel-Prover-V2.

Related papers

• Explorative Modeling: Unlocking a Third Pretraining Axis and End-to-End Generation [89.51408170909548]
  We introduce Explorative Modeling, a new paradigm that factors the training loop, exploring K candidate matches between model generations and data, and training on the best.<n>First, increasing exploration adds a third pretraining axis beyond parameters and data for existing generative models.<n>Second, XMs enable end-to-end reconstructive generative modeling, matching diffusion on control tasks with 16-256x fewer inference steps.
  arXiv  Detail & Related papers  (2026-07-29T18:25:17Z)
• Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation [27.324913853284404]
  Pythagoras-Prover is a compute-efficient family of Lean theorem provers built for practical compute budgets.<n>For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT.<n>We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements.
  arXiv  Detail & Related papers  (2026-06-10T18:43:11Z)
• Solve the Loop: Attractor Models for Language and Reasoning [4.8720589853137435]
  Looped Transformers offer a promising alternative to purely feed-forward computation.<n>We introduce Attractor Models, in which a backbone module first proposes output embeddings, then an attractor module refines them by solving for the fixed point.<n>We show that Attractor Models outperform existing models across two regimes, large-scale language-model pretraining and reasoning with tiny models.
  arXiv  Detail & Related papers  (2026-05-12T17:51:26Z)
• Three Roles, One Model: Role Orchestration at Inference Time to Close the Performance Gap Between Small and Large Agents [0.4666493857924357]
  We study whether inference-time scaffolding alone, without any additional training compute, can improve the performance of a small model in complex multi-step environments.<n>We evaluate Qwen3-8B on the AppWorld benchmark under both full-precision and 4-bit quantized configurations.<n>On full-precision inference, our scaffolded 8B model surpasses DeepSeek-Coder 33B Instruct (7.1%) from the original AppWorld evaluation.
  arXiv  Detail & Related papers  (2026-04-13T13:40:33Z)
• Efficient Multi-Model Orchestration for Self-Hosted Large Language Models [2.3275796286410677]
  Pick and Spin is a framework that makes self-hosted orchestration and economical.<n>It integrates a unified Helm-based deployment system, adaptive scale-to-zero automation, and a hybrid routing module.<n>It achieves up to 21.6% higher success rates, 30% lower latency, and 33% lower cost per query compared with static deployments of the same models.
  arXiv  Detail & Related papers  (2025-12-26T22:42:40Z)
• URPO: A Unified Reward & Policy Optimization Framework for Large Language Models [10.511836918064724]
  We propose a novel framework that unifies instruction-following ("player") and reward modeling ("referee") within a single model and a single training phase.<n>Our method recasts all alignment data-including preference pairs, verifiable reasoning, and open-ended instructions-into a unified generative format.<n>Experiments on the Qwen2.5-7B model demonstrate URPO's superiority.
  arXiv  Detail & Related papers  (2025-07-23T13:52:27Z)
• Navigating the Accuracy-Size Trade-Off with Flexible Model Merging [15.497612580389479]
  We propose FlexMerge, a novel data-free model merging framework.<n>It flexibly generates merged models of varying sizes, spanning the full spectrum from a single merged model to retaining all fine-tuned models.<n>Using FlexMerge, we systematically characterize the accuracy-size trade-off of different algorithms.
  arXiv  Detail & Related papers  (2025-05-29T07:50:32Z)
• Skywork Open Reasoner 1 Technical Report [51.403686909760914]
  We present Skywork-OR1, an effective and scalable reinforcement learning (RL) implementation for long Chain-of-Thought (CoT) models.<n>Building on the DeepSeek-R1-Distill model series, our RL approach achieves notable performance gains.<n>Our Skywork-OR1-32B model surpasses both DeepSeek-R1 and Qwen3-32B on the AIME24 and AIME25 benchmarks.
  arXiv  Detail & Related papers  (2025-05-28T12:56:04Z)
• DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition [24.50773495427783]
  We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4.<n>The model achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench.<n>In addition to standard benchmarks, we introduce ProverBench, a collection of 325 formalized problems, to enrich our evaluation, including 15 selected problems from the recent AIME competitions.
  arXiv  Detail & Related papers  (2025-04-30T16:57:48Z)
• S*: Test Time Scaling for Code Generation [55.11863577956177]
  We propose S*, the first hybrid test-time scaling framework for code generation.<n>S* substantially improves the coverage and selection accuracy of generated code.
  arXiv  Detail & Related papers  (2025-02-20T09:18:53Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  We introduce Goedel-Prover, an open-source language model that achieves state-of-the-art (as of April 5 2025) performance in automated formal proof generation for mathematical problems.<n>First, we train LLMs to convert natural language math problems from the Numina dataset to equivalent formal statements in Lean 4.<n>Next, we develop a large dataset of formal proofs by training a series of provers.<n>Finally, we obtain the dataset Goedel-Pset-v1-solved, which contains proofs for over 800K statements from Goedel-Pset-v1
  arXiv  Detail & Related papers  (2025-02-11T15:27:35Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a procedure that equips LLMs with automation methods at various granularities.<n>Our method is validated on the miniF2F benchmark using the open-source deep-math-7b-base model and the Isabelle proof assistant.<n>We also implement a Lean 4 version of ProofAug that can improve the pass@1 performance of Kimina-Prover-seek-Distill-1.5B from 44.3% to 50.4%.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• ReNO: Enhancing One-step Text-to-Image Models through Reward-based Noise Optimization [59.72782742378666]
  We propose Reward-based Noise Optimization (ReNO) to enhance Text-to-Image models at inference. Within a computational budget of 20-50 seconds, ReNO-enhanced one-step models consistently surpass the performance of all current open-source Text-to-Image models.
  arXiv  Detail & Related papers  (2024-06-06T17:56:40Z)
• CodingTeachLLM: Empowering LLM's Coding Ability via AST Prior Knowledge [0.0]
  We introduce CodingTeachLLM, a large language model (LLM) designed for coding teaching.<n>Our model realizes the structural disassembly and incremental guided output of educational knowledge.<n>Our model also achieves state-of-the-art in code abilities compared to open-source models.
  arXiv  Detail & Related papers  (2024-03-13T05:38:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.