Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

LM-Provers, Yuxiao Qu, Amrith Setlur, Jasper Dekoninck, Edward Beeching, Jia Li, Ian Wu, Lewis Tunstall, Aviral Kumar

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.

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

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.

Paper Structure

This paper contains 33 sections, 60 equations, 7 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Step I: Dataset Construction and Grading Schemes
  4. Step II: Training Recipe
  5. Core Reinforcement Learning Approach
  6. RL for Continual Improvement at Test Time via Reasoning Cache
  7. Initializing Proof-Writing Capabilities via Supervised Fine-Tuning
  8. Results
  9. Discussion, Conclusion, and Perspectives on Future Work
  10. Grading Protocol
  11. Test-Time Scaffolds
  12. SFT Ablations
  13. Filtering with GPT-nano
  14. Grader Prompts
  15. Grading Scheme Examples
  16. ...and 18 more sections

Figures (7)

  • Figure 1: IMO-ProofBench imobench grade as a function of model size. QED-Nano outperforms open models of similar size and remains competitive with much larger systems.
  • Figure 2: Example of a grading scheme.
  • Figure 3: RL training curves with rubric-based rewards (left) and corresponding evaluation metrics on IMO-ProofBench and ProofBench (right)
  • Figure 4: Training reward as a function of optimization steps for standard RL and RL with RC.
  • Figure 5: Per-turn mean reward during RC training.
  • ...and 2 more figures