Research map / Large language models / Agents, code and math

Subgoal-based Demonstration Learning for Formal Theorem Proving

ICML 2024 · Large language models › Agents, code and math · approach: Retrieval-augmented formal theorem proving

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Proposes subgoal-based demonstration learning for LLM formal theorem proving in Isabelle, refining subgoal proofs with a prover and organizing in-context demonstrations (selection and order) via a graph discrete diffusion model, reaching 45.5% on miniF2F-test.

Problem

LLM-based formal theorem proving is sensitive to the format and selection/ordering of in-context demonstration examples, and informal proofs are poorly suited to LLMs; the joint subset selection and ordering problem is combinatorially hard.

Approach

Replace informal proofs with subgoal-based proofs refined iteratively with an LLM and Isabelle verification (guided by subgoal learning theory), and treat demonstration subset selection plus ordering as a graph diffusion problem trained on successful demonstration organizations.

Key results

• Full method reaches 45.5% pass rate on miniF2F-test, versus 38.9% for DSP (540B Minerva) and 44.1% for the diffusion-only ablation.
• Subgoal-based proof raises pass rate from 38.9% to 44.1% on miniF2F-test (ablation without diffusion, subgoal removed reported as 40.6%).
• With diffusion reorganization, 94 problems (38.5%) solved with only 20 LLM calls, comparable to DSP at 100 calls.

Measured effects reported in the paper

Surprising findings

• Human-written informal proofs were found to be poorly compatible with LLMs, and subgoal-based proofs help more than expected in ablations.

Limitations

• Diffusion model trained on miniF2F-valid successes, so validation results use cumulative pass rate and are not directly comparable to test results.
• Relies on ChatGPT API and Isabelle with Sledgehammer; performance depends on the proprietary LLM.
• Diffusion gains diminish as the number of LLM calls increases to 100.

Experimental setup

Datasets: miniF2F

Benchmarks: miniF2F

Metrics: pass rate cumulative pass rate number of problems solved vs LLM calls

Baselines: Sledgehammer Sledgehammer+heuristic Thor Thor + expert iteration DSP LEGO-Prover Lyra Top-K demonstration selection GNN demonstration selection

Builds on: Draft, Sketch, and Prove (DSP) Thor Sledgehammer discrete diffusion models for NP-complete problems subgoal learning (Zhang et al., 2021)

Closest papers by meaning

• Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.90)
• Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers (ICML 2026 · similarity 0.89)
• LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.89)
• ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.89)
• LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 2025 · similarity 0.88)
• MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.88)