# Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

arXiv: https://arxiv.org/abs/2305.16366 · HTML: https://mlsanity.com/paper/2305.16366/

## Key facts

- Cited by 37 papers in the map (data through 14 Oct 2026).
- Placed in Discrete and text diffusion, one of 14 directions in Diffusion models.
- Builds on 39 of its 51 references that are in the map.
- First posted on arXiv 25 May 2023.

## Placed in

- Diffusion models / [Discrete and text diffusion](https://mlsanity.com/diffusion/discrete-and-text-diffusion/)

## Builds on (most cited first, 30 of 39)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift](https://mlsanity.com/paper/1502.03167/) (2015)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Structured Denoising Diffusion Models in Discrete State-Spaces](https://mlsanity.com/paper/2107.03006/) (2021)
- [Calibrate Before Use: Improving Few-Shot Performance of Language Models](https://mlsanity.com/paper/2102.09690/) (2021)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [What Makes Good In-Context Examples for GPT-3?](https://mlsanity.com/paper/2101.06804/) (2021)
- [Fantastically Ordered Prompts and Where to Find Them: Overcoming Few-Shot Prompt Order Sensitivity](https://mlsanity.com/paper/2104.08786/) (2021)
- [Learning To Retrieve Prompts for In-Context Learning](https://mlsanity.com/paper/2112.08633/) (2021)
- [Decomposed Prompting: A Modular Approach for Solving Complex Tasks](https://mlsanity.com/paper/2210.02406/) (2022)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Your Diffusion Model is Secretly a Zero-Shot Classifier](https://mlsanity.com/paper/2303.16203/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Selective Annotation Makes Language Models Better Few-Shot Learners](https://mlsanity.com/paper/2209.01975/) (2022)
- [Diffusion models as plug-and-play priors](https://mlsanity.com/paper/2206.09012/) (2022)
- [DIFUSCO: Graph-based Diffusion Solvers for Combinatorial Optimization](https://mlsanity.com/paper/2302.08224/) (2023)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Search on the Replay Buffer: Bridging Planning and Reinforcement Learning](https://mlsanity.com/paper/1906.05253/) (2019)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [In-context Examples Selection for Machine Translation](https://mlsanity.com/paper/2212.02437/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Maximum Entropy Gain Exploration for Long Horizon Multi-goal Reinforcement Learning](https://mlsanity.com/paper/2007.02832/) (2020)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [An Information-theoretic Approach to Prompt Engineering Without Ground Truth Labels](https://mlsanity.com/paper/2203.11364/) (2022)
- [Automatic Curriculum Learning through Value Disagreement](https://mlsanity.com/paper/2006.09641/) (2020)

## Built on by (most cited first, 30 of 37)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [G-LLaVA: Solving Geometric Problem with Multi-Modal Large Language Model](https://mlsanity.com/paper/2312.11370/) (2023)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Beyond Autoregression: Discrete Diffusion for Complex Reasoning and Planning](https://mlsanity.com/paper/2410.14157/) (2024)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [Provably safe systems: the only path to controllable AGI](https://mlsanity.com/paper/2309.01933/) (2023)
- [Lyra: Orchestrating Dual Correction in Automated Theorem Proving](https://mlsanity.com/paper/2309.15806/) (2023)
- [LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover](https://mlsanity.com/paper/2407.17227/) (2024)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs](https://mlsanity.com/paper/2502.00963/) (2025)
- [Mathesis: Towards Formal Theorem Proving from Natural Languages](https://mlsanity.com/paper/2506.07047/) (2025)
- [ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis](https://mlsanity.com/paper/2501.18310/) (2025)
- [Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification](https://mlsanity.com/paper/2410.19940/) (2024)
- [FormaRL: Enhancing Autoformalization with no Labeled Data](https://mlsanity.com/paper/2508.18914/) (2025)
- [From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems](https://mlsanity.com/paper/2503.01424/) (2025)
- [DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems](https://mlsanity.com/paper/2510.10815/) (2025)
- [3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes](https://mlsanity.com/paper/2410.11133/) (2024)
- [Premise Selection for a Lean Hammer](https://mlsanity.com/paper/2506.07477/) (2025)
- [Modeling Complex Mathematical Reasoning via Large Language Model based MathAgent](https://mlsanity.com/paper/2312.08926/) (2023)
- [ProofCompass: Enhancing Specialized Provers with LLM Guidance](https://mlsanity.com/paper/2507.14335/) (2025)
- [Cog-Rethinker: Hierarchical Metacognitive Reinforcement Learning for LLM Reasoning](https://mlsanity.com/paper/2510.15979/) (2025)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)

## Abstract (arXiv)

Large language models~(LLMs) present an intriguing avenue of exploration in the domain of formal theorem proving. Nonetheless, the full utilization of these models, particularly in terms of demonstration formatting and organization, remains an underexplored area. In an endeavor to enhance the efficacy of LLMs, we introduce a subgoal-based demonstration learning framework, consisting of two primary elements: Firstly, drawing upon the insights of subgoal learning from the domains of reinforcement learning and robotics, we propose the construction of distinct subgoals for each demonstration example and refine these subgoals in accordance with the pertinent theories of subgoal learning. Secondly, we build upon recent advances in diffusion models to predict the optimal organization, simultaneously addressing two intricate issues that persist within the domain of demonstration organization: subset selection and order determination. Through the integration of subgoal-based learning methodologies, we have successfully increased the prevailing proof accuracy from 38.9% to 44.3% on the miniF2F benchmark. Furthermore, the adoption of diffusion models for demonstration organization can lead to an additional enhancement in accuracy to 45.5%, or a 5× improvement in sampling efficiency compared with the long-standing state-of-the-art method. Our code is available at urlhttps://github.com/HKUNLP/subgoal-theorem-prover.