Research map / Large language models / Instruction and fine-tuning
miniCTX: Neural Theorem Proving with (Long-)Contexts
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.
Introduces miniCTX, a Lean 4 benchmark of 762 temporally split theorems from six real projects that tests theorem proving with long file context, plus the NTP-Toolkit extraction tool and a file-tuning baseline.
Problem
Existing neural theorem provers are trained on proof states only and evaluated on standalone competition problems or Mathlib theorems, so they cannot use new definitions, lemmas, comments, or file context that real formalization projects depend on, and evaluations risk data contamination.
Approach
Benchmark theorems from real Lean repositories with their preceding file context (and cross-file premises), using temporal splits to avoid training contamination, and propose file-tuning, which fine-tunes a tactic generator on (file context, proof state, tactic) triples instead of proof states alone.
Key results
- File-tuned DeepSeek-Coder-1.3b reaches 35.94% average on miniCTX-test versus 19.53% for state-tactic tuning.
- GPT-4o with preceding file context reaches 27.08% average versus 11.72% for full proof without context.
- On miniF2F-test, file-tuning improves only marginally over state-tactic tuning (33.61% vs 32.79%).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| fine-tune with preceding file context instead of proof states alone | DeepSeek-Coder-1.3b · miniCTX-test Avg. | proof rate: 19.53% vs. 35.94% | Helped |
| provide preceding file context | GPT-4o · miniCTX-test Avg. | proof rate: 11.72% vs. 27.08% | Helped |
| add retrieved premises to preceding file context | GPT-4o · PFR, PFR-cross, and SciLean | proof rate: PFR: 5.56 -> 7.41; PFR-cross: 34.88 -> 39.53; SciLean: 17.39 -> 21.74 | Helped |
| add retrieved premises | File tuning · PFR-cross | proof rate: 44.19 -> 16.28 | Hurt |
| add retrieved premises | File tuning · miniCTX-test Avg. | proof rate: 35.94 -> 30.21 | Hurt |
| fine-tune with preceding file context instead of proof states alone | DeepSeek-Coder-1.3b · miniF2F-test | proof rate: 32.79% vs. 33.61% | Helped |
| add environment context to no context (ablation) | File tuning · PFR.ForMathlib.Entropy.Basic | proof rate: 14.12\% -> 25.88\% | Helped |
| add environment context to no context (ablation) | GPT-4o · PFR.ForMathlib.Entropy.Basic | proof rate: 8.24\% -> 2.35\% | Hurt |
| add definitions to environment context (ablation) | File tuning · PFR.ForMathlib.Entropy.Basic | proof rate: 25.88\% -> 24.71\% | Hurt |
| add definitions to environment context (ablation) | GPT-4o · PFR.ForMathlib.Entropy.Basic | proof rate: 2.35\% -> 9.41\% | Helped |
| add lemma statements (ablation) | File tuning · PFR.ForMathlib.Entropy.Basic | proof rate: 24.71\% -> 27.06\% | Helped |
| add lemma statements (ablation) | GPT-4o · PFR.ForMathlib.Entropy.Basic | proof rate: 9.41\% -> 22.35\% | Helped |
Surprising findings
- Premise selection via LeanDojo retriever does not consistently help the file-tuned model and even hurts on PFR_cross.
- Models rely heavily on automation tactics: disabling simp/linarith on Math2001 drops file-tuned performance from 41.18% to 27.45%.
Limitations
- File-tuning truncates context to 1024 tokens, discarding useful information in long contexts.
- Performance remains low on challenging proofs longer than five lines (about 19%) and on PFR proofs.
- Premise selection integration with in-file context is inconsistent.
Experimental setup
Datasets: Mathlib (2023 snapshot) miniF2F Math2001
Benchmarks: miniCTX-test miniF2F-test Math2001
Metrics: pass@8 proof rate proof success rate
Baselines: GPT-4o full proof GPT-4o with context State-tactic prompting State-tactic tuning LeanDojo premise retriever
Builds on: LeanDojo ReProver lean-training-data Lean REPL GPT-f
Closest papers by meaning
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.91)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.90)
- Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation (ICLR 2025 · similarity 0.89)
- Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.89)
- REFACTOR: Learning to Extract Theorems from Proofs (ICLR 2024 · similarity 0.89)
- Lean-STaR: Learning to Interleave Thinking and Proving (ICLR 2025 · similarity 0.89)
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.