Research map / Large language models / Agents, code and math
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
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 MUSTARD, a concept-seeded LLM (GPT-4) pipeline that generates math problems with informal and Lean 3 formal proofs, filters them with the Lean prover and error-driven revision, and releases a 7,335-point dataset used to fine-tune Llama 2-7B and GPT2-large with LoRA.
Problem
Obtaining large-scale, high-quality step-wise theorem-proving and math word problem data with verified intermediate steps is costly, since manual annotation is small-scale and rule-based synthesis yields meaningless proofs.
Approach
Sample Khan Academy math concept seeds, have GPT-4 generate problem, informal proof and Lean 3 formal proof in one pass, then use the Lean prover's error messages to iteratively revise the formal proof and keep only prover-validated samples; the number of revision rounds serves as a difficulty measure.
Key results
- Fine-tuning Llama 2-7B on valid MUSTARD data gives 16.00% relative gain on mathlib and miniF2F over random-subset fine-tuning, and 17.31% on MUSTARD-test (12.2 pass@1).
- Human evaluation shows prover-validated data significantly better on informal proof correctness (88.50 vs 73.50, p=0.00012) and IP-FP alignment (72.00 vs 54.00, p=0.00018).
- Averaged over settings, the paper reports 18.15% relative gain in ATP and 6.78% in MWP from fine-tuning on valid vs random data.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Fine-tune on MUSTARDSAUCE-valid rather than MUSTARDSAUCE-random | Llama 2-7B · Mathlib | pass@1: 7.5 -> 8.7; (+16.00%) | Helped |
| Fine-tune on MUSTARDSAUCE-valid rather than MUSTARDSAUCE-random | Llama 2-7B · miniF2F | pass@1: 2.5 -> 2.9; (+16.00%) | Helped |
| Fine-tune on MUSTARDSAUCE-valid rather than MUSTARDSAUCE-random | Llama 2-7B · MUSTARDSAUCE-valid test | pass@1: 10.4 -> 12.2; (+17.31%) | Helped |
| Fine-tune on MUSTARDSAUCE-valid rather than MUSTARDSAUCE-random | Llama 2-7B · GSM8K zero-shot | Maj1@1: 8.9 -> 9.1 | Helped |
| Fine-tune on all generated data instead of the valid subset | Llama 2-7B · Mathlib | pass@1: 8.7 -> 8.3 | Hurt |
| Fine-tune on all generated data instead of the valid subset | Llama 2-7B · GSM8K zero-shot | Maj1@1: 9.1 -> 9.0 | No clear effect |
| Add 1 prover-feedback correction (ablation) | GPT-4 formal proof generation · Theorem proving, elementary, 1 seed concept | pass@1: 26.0 -> 48.0 (+22.0) | Helped |
| Add 2 prover-feedback corrections (ablation) | GPT-4 formal proof generation · Theorem proving, elementary, 1 seed concept | pass@1: 26.0 -> 55.9 (+33.9) | Helped |
| Add 2 prover-feedback corrections (ablation) | GPT-4 formal proof generation · Word problem, elementary, 1 seed concept | pass@1: 38.0 -> 67.0 (+45.3) | Helped |
| Use step-by-step rather than all-at-once proof generation (ablation) | GPT-4 · Higher-education theorem proving | pass@1: 2.1 -> 3.0 | Mixed |
| Fine-tune on mathlib after MUSTARDSAUCE-valid rather than before it (ablation) | Llama 2-7B · MUSTARDSAUCE-valid test | pass@1: 13.8 -> 14.4 | Helped |
| Lean Prover validation of generated data | MUSTARDSAUCE data · Human evaluation, informal proof correctness | accuracy: 73.50 -> 88.50; p-value 0.00012 | Helped |
Surprising findings
- Fine-tuning on the full unfiltered 28,320-point set underperforms fine-tuning on the 7,335 prover-validated subset, suggesting quality beats quantity.
- Self-correction with Lean error messages raises pass rates substantially, e.g., elementary theorem proving from 26.0% to 55.9% after two correction steps.
Limitations
- Mild inconsistency remains between formal statements and proofs after prover validation, so filtering is not fully rigorous.
- Data generation and evaluation rely on proprietary GPT-4 and human checks on only 200 samples.
Experimental setup
Datasets: MUSTARD (generated) GSM8K MATH (PRM800K test split) mathlib miniF2F
Benchmarks: GSM8K MATH mathlib miniF2F MUSTARD-test
Metrics: maj1@1 pass@1 ROUGE-L human-rated accuracy per dimension p-value
Baselines: GPT2-large Llama 2-7B INT
Builds on: LoRA miniF2F GSM8K Lean Prover
Closest papers by meaning
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.90)
- FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence (NeurIPS 2026 · similarity 0.90)
- Lean-STaR: Learning to Interleave Thinking and Proving (ICLR 2025 · similarity 0.90)
- Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.89)
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.88)
- MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving (ICML 2025 · similarity 0.88)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.