QED-Nano: Teaching a Tiny Model to Prove Hard Theorems

• URL: http://arxiv.org/abs/2604.04898v1
• Date: Mon, 06 Apr 2026 17:44:25 GMT
• Title: QED-Nano: Teaching a Tiny Model to Prove Hard Theorems
• Abstract summary: We build QED-Nano, a 4B model post-trained for Olympiad-level proofs.<n>We release the full QED-Nano pipeline, including the QED-Nano and QED-Nano-SFT models, the FineProofs-SFT and FineProofs-RL datasets, and the training and evaluation code.
• Score: 34.119608370222245
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Proprietary AI systems have recently demonstrated impressive capabilities on complex proof-based problems, with gold-level performance reported at the 2025 International Mathematical Olympiad (IMO). However, the training pipelines behind these systems remain largely undisclosed, and their reliance on large "internal" models and scaffolds makes them expensive to run, difficult to reproduce, and hard to study or improve upon. This raises a central question: can small, open models also be trained to achieve competitive reasoning performance on difficult Olympiad-level math? In this paper, we answer this question by building QED-Nano, a 4B model post-trained for Olympiad-level proofs. Our training recipe has three stages: (1) supervised fine-tuning to imbue good proof-writing styles by distilling from DeepSeek-Math-V2, (2) reinforcement learning (RL) with rubric-based rewards, and (3) expanding RL with a reasoning cache, which decomposes long proofs into iterative summarize-and-refine cycles and enables stronger test-time reasoning. QED-Nano surpasses the proof-generation performance of much larger open models, including Nomos-1 and GPT-OSS-120B, and approaches the performance of proprietary models like Gemini 3 Pro, at a fraction of the inference cost. To support further research on open mathematical reasoning, we release the full QED-Nano pipeline, including the QED-Nano and QED-Nano-SFT models, the FineProofs-SFT and FineProofs-RL datasets, and the training and evaluation code.

Related papers

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• Achieving Gold-Medal-Level Olympiad Reasoning via Simple and Unified Scaling [108.48818215929494]
  We introduce a simple and unified recipe for converting a post-trained reasoning backbone into a rigorous olympiad-level solver.<n>We train a 30B-A3B backbone with SFT on around 340K sub-8K-token trajectories followed by 200 RL steps.<n>The resulting model, SU-01, supports stable reasoning on difficult problems with trajectories exceeding 100K tokens.
  arXiv  Detail & Related papers  (2026-05-13T10:13:26Z)
• Answer First, Reason Later: Aligning Search Relevance via Mode-Balanced Reinforcement Learning [7.006180736433431]
  Building a search relevance model that achieves both low latency and high performance is a long-standing challenge in the search industry.<n>We propose a novel textbfAnswer-First, Reason Later (AFRL) paradigm.<n>This paradigm requires the model to output the definitive relevance score in the very first token, followed by a structured logical explanation.
  arXiv  Detail & Related papers  (2026-02-10T17:28:12Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  Large Language Models (LLMs) have demonstrated strong math reasoning abilities through Reinforcement Learning with *Verifiable Rewards* (RLVR)<n>Many advanced mathematical problems are proof-based, with no guaranteed way to determine the authenticity of a proof by simple answer matching.<n>To enable automatic verification, a Reward Model (RM) capable of reliably evaluating full proof processes is required.
  arXiv  Detail & Related papers  (2026-02-02T17:42:53Z)
• Knowledge Graphs are Implicit Reward Models: Path-Derived Signals Enable Compositional Reasoning [4.464939140209426]
  We propose a bottom-up learning paradigm in which models are grounded in axiomatic domain facts and compose them to solve complex, unseen tasks.<n>By deriving novel reward signals from knowledge graph paths, we provide verifiable, scalable, and grounded supervision.<n>Our experiments show that path-derived rewards act as a "compositional bridge", enabling our model to significantly outperform larger models.
  arXiv  Detail & Related papers  (2026-01-21T16:38:59Z)
• ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations [14.748476989228214]
  We introduce Proofr, the first language model trained to simplify Lean proofs without requiring additional human supervision.<n>Provr is trained via expert iteration and reinforcement learning, using Lean to verify simplifications and provide training signal.<n>Provr substantially compresses proofs generated by state-of-the-art RL-trained provers on standard benchmarks.
  arXiv  Detail & Related papers  (2025-10-17T14:45:30Z)
• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
  In this work, we propose textbfSeed-Prover, a lemma-style whole-proof reasoning model.<n>To solve IMO-level contest problems, we design three test-time inference strategies that enable both deep and broad reasoning.<n>Seed-Prover proves $78.1%$ of formalized past IMO problems, saturates MiniF2F, and achieves over 50% on PutnamBench, outperforming the previous state-of-the-art by a large margin.
  arXiv  Detail & Related papers  (2025-07-31T17:00:30Z)
• 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)
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving [33.61458249318183]
  Self-play Theorem Prover (STP) takes on two roles, conjecturer and prover.<n>STP simultaneously takes on two roles, conjecturer and prover.<n>We evaluate with both Lean and Isabelle formal versifiers.
  arXiv  Detail & Related papers  (2025-01-31T23:01:48Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)

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.