Research map / Large language models / Agents, code and math
Magnushammer: A Transformer-Based Approach to Premise Selection
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.
Magnushammer uses a two-stage contrastive transformer retriever (Select then Rerank) for premise selection in Isabelle, releasing a 4.4M-example Isabelle premise dataset, and combined with Thor it reaches 71.0% on PISA.
Problem
Premise selection for automated theorem proving in proof assistants, where symbolic hammers like Sledgehammer require heavy domain engineering and are hard to port to new proof assistants.
Approach
Treat proof states and premises as text and train a transformer contrastively for cosine-similarity retrieval (Select), then re-rank the top candidates with a joint proof-state-premise cross-scoring head (Rerank), trained with alternating updates on a shared backbone.
Key results
- Magnushammer achieves 59.5% proof rate on PISA single-step vs 38.3% for Sledgehammer.
- Thor + Magnushammer reaches 71.0% on PISA multi-step, up from Thor's 57.0%.
- On miniF2F test, single-step Magnushammer achieves 34.0% vs 20.9% for Sledgehammer with heuristics.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Replace Sledgehammer with Magnushammer for single-step premise selection | PISA theorem proving · PISA single-step | proof success rate (%): 38.3 -> 59.5 | Helped |
| Replace Sledgehammer with Magnushammer in Thor | Thor · PISA multi-step | proof success rate (%): 57.0 -> 71.0 | Helped |
| Replace Sledgehammer with Magnushammer for single-step premise selection | miniF2F · miniF2F test single-step | proof success rate (%): 20.9 -> 34.0 | Helped |
| Replace Sledgehammer with Magnushammer in Thor | Thor · miniF2F test multi-step | proof success rate (%): 29.9 -> 37.3 | Helped |
| Remove the Rerank stage (ablation) | Magnushammer · PISA, budget 800 | proof success rate (%): 56.3% -> 54.2% | Hurt |
| Train on MAPL instead of HPL (ablation) | Magnushammer · PISA, budget 800 | proof success rate (%): 54.0% -> 56.3% | Helped |
| Add language-model pre-training (ablation) | Magnushammer trained on MAPL · PISA, budget 800 | proof success rate (%): 53.0 -> 56.3 | Helped |
| Use 0.1% of MAPL instead of 100% of MAPL (ablation) | Pre-trained Magnushammer · PISA, budget 800 | proof success rate (%): 56.3 -> 39.2 | Hurt |
| Use 0.1% MAPL instead of 0.1% HPL (ablation) | Pre-trained Magnushammer · PISA, budget 800 | proof success rate (%): 34.9 -> 39.2 | Helped |
| Increase model size from 920K to 86.2M parameters (ablation) | Magnushammer · PISA, budget 800 | proof success rate (%): 40.7 -> 57.0 | Helped |
| Add a tactic prompt (ablation) | Magnushammer premise selection · PISA | proof success rate (%): 55.60 -> 56.19 | No clear effect |
Surprising findings
- A tiny 920K-parameter model already outperforms Sledgehammer (40.7% vs 38.3%) on PISA.
- Select-only retrieval without reranking reaches 54.2% vs 56.3% with reranking on the 38M model.
Limitations
- Evaluated only on Isabelle; cross-prover generalization (Lean) is future work.
- Proof states lack full semantic information such as function definitions and types.
- Retrieval and generation are not yet integrated into a single model.
Experimental setup
Datasets: MAPL HPL SH partition Archive of Formal Proofs Isabelle Standard library GitHub and arXiv subsets of the Pile
Benchmarks: PISA miniF2F
Metrics: proof success rate
Baselines: Sledgehammer Sledgehammer + heuristics BM25 TF-IDF OpenAI text-embedding-ada-002 Thor Thor + Sledgehammer LISA DSP Thor + auto
Builds on: InfoNCE Thor Sledgehammer Contriever HOList
Closest papers by meaning
- BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving (AAAI 2024 · similarity 0.90)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.89)
- FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence (NeurIPS 2026 · similarity 0.88)
- A Minimal Agent for Automated Theorem Proving (ICML 2026 · similarity 0.88)
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.88)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 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.