Research map / Large language models / Agents, code and math
Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation
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.
Alchemy synthesizes ~6M new Mathlib theorems by symbolically mutating existing statements with rw/apply invocable theorems, then uses them for continual pretraining and SFT of Llama-3-8B and deepseek-coder-7B provers.
Problem
Neural theorem provers for Lean are limited by scarce formal training data, as Mathlib has only about 110k theorems compared with abundant natural text.
Approach
Synthesize new Lean theorems directly in symbolic space: for each Mathlib theorem, find invocable theorems via rw and apply tactics in the Lean environment, mutate the statement by replacing components with equivalent forms or antecedents, and build proofs with a `have` tactic that is verified by Lean.
Key results
- Mathlib theorems grow from 110,657 to about 6.3M (about x25 for rw and x44 for apply); novel_premises pass rate for Llama3-8b rises from 38.52 to 43.22 with rw+apply data.
- deepseek-coder-7b-base-v1.5 novel_premises rises from 39.24 to 43.46 (+4.22) with rw+apply data.
- miniF2F-test for Llama3-8b rises from 34.01 to 36.48 with Mathlib-train + rw + apply.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add rw and apply synthetic data | Llama3-8b · Leandojo novel_premises | proving success: 38.52 -> 43.22 | Helped |
| Add rw and apply synthetic data | deepseek-coder-base-v1.5-7B · Leandojo novel_premises | proving success: 39.24 -> 43.46 | Helped |
| Add rw synthetic data | Llama3-8b · miniF2F-test | proving success: 34.01 -> 35.24 | Helped |
| Add apply synthetic data | Llama3-8b · miniF2F-test | proving success: 34.01 -> 36.07 | Helped |
| Add rw and apply synthetic data | Llama3-8b · miniF2F-test | proving success: 34.01 -> 36.48 | Helped |
| Add continual pretraining on augmented corpus (ablation) | Llama3-8b, SFT on Mathlib-train · Leandojo novel_premises | proving success: 38.52 -> 42.56 | Helped |
| Add continual pretraining on augmented corpus (ablation) | Llama3-8b, SFT on Mathlib-train + rw + apply · Leandojo novel_premises | proving success: 41.95 -> 43.22 | Helped |
| Add have state-tactic pairs to Mathlib-train (ablation) | Llama3-8b · Leandojo novel_premises | proving success: 38.52 -> 41.29 | Helped |
| Add have state-tactic pairs alongside apply data (ablation) | Llama3-8b · Leandojo novel_premises | proving success: 40.02 -> 38.34 | Hurt |
| Increase single-tactic SFT data quantity (ablation) | Llama-3-8B · Leandojo | proving success | No clear effect |
Surprising findings
- Adding state-tactic pairs for the `have` tactic lowered or failed to improve performance relative to single-tactic data, showing complex effects.
- Single-tactic augmentation shifts the model's tactic preference, and out-of-distribution gains on miniF2F are smaller than in-distribution gains.
Limitations
- Only two symbolic rules (rw and apply) are used, limiting diversity and quality of synthetic data.
- Synthesis is computationally costly and O(n^2), with heavy memory demands from LeanDojo.
- Top-down synthesis depends on seed theorems, restricting diversity; out-of-distribution gain on miniF2F is smaller.
Experimental setup
Datasets: Mathlib4 LeanDojo Benchmark miniF2F
Benchmarks: LeanDojo Benchmark random split LeanDojo Benchmark novel_premises split miniF2F-test
Metrics: pass rate theorems proved count
Baselines: tidy GPT-4 ReProver llmstep deepseek-coder-base-7b-v1.5
Builds on: ReProver LeanDojo Mathlib Llama-Factory
Closest papers by meaning
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.89)
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.89)
- miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · similarity 0.89)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.88)
- BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving (AAAI 2024 · similarity 0.88)
- LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 2025 · similarity 0.87)
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.