Magnushammer: A Transformer-Based Approach to Premise Selection

1 INTRODUCTION

• Existing hammers use ATPs, but their complex techniques for different logics and type systems make implementation challenging and limit their availability across proof assistants.Sledgehammer is prominent in Isabelle and helped create a significant portion of its proof corpus.Source: §1 · p. 2
• Magnushammer is a generic, data-driven transformer tool trained contrastively to retrieve and rerank premises with little domain-specific knowledge.SELECT retrieves by embedding similarity; RERANK scores proof-state–premise pairs with proof-state tokens attending to premise tokens.Source: §1 · p. 2
• 59.5% vs. 38.3%: Magnushammer’s PISA proof rate exceeds Sledgehammer’s, and replacing Sledgehammer in Thor raises PISA success from 57% to 71%.The paper also reports that the advantage persists across varying controlled compute budgets.Source: §1 · p. 2
• The authors open-source a 4.4M-instance dataset with 433K unique premises, which they describe as the largest available and first for Isabelle.They also report outperforming Sledgehammer with 4K training examples, or 0.1% of available training data.Source: §1 · p. 2
• The paper analyzes how Magnushammer’s performance depends on model size, dataset size, and inference-time compute, reporting superiority with moderate resources.The contribution summary also reports a 59.5% PISA proof rate against Sledgehammer’s 38.3%.Source: §1 · p. 2

2 BACKGROUND: PROOF ASSISTANTS, ISABELLE, AND SLEDGEHAMMER

• A proof step may use premises, and finding a handful of relevant facts is difficult when the current proof context contains tens of thousands.Proof states contain established facts and remaining goals; tactics can complete some proofs when supplied relevant premises.Source: §2 · p. 2
• Sledgehammer heuristically pre-selects facts, translates them with a conjecture for external ATPs, then reconstructs an Isabelle proof using extracted facts.External provers’ proofs are not trusted by Isabelle; their used facts are instead applied with Isabelle-native methods.Source: §2 · p. 3
• Sledgehammer’s relevance filtering uses handcrafted heuristics or classical machine learning, approaches the paper says are unlikely to efficiently use growing proof data.The paper also notes diminishing returns from increasing Sledgehammer’s compute and challenges adapting hammer logic projection and reconstruction beyond higher-order logic.Source: §2 · p. 3
• The authors argue that textual neural approaches can avoid logic projection, ATP solving, and proof reconstruction, with little or no feature engineering.They point to language-model scaling with model size and data as motivation for this direction.Source: §2 · p. 3

3 MAGNUSHAMMER

• SELECT embeds proof states and premises in a shared latent space, then uses cosine similarity to retrieve 1,024 candidates from typical contexts of 30K–50K premises.Cached premise embeddings allow inference to compute a proof-state embedding and compare it with the stored premises.Source: §3 · p. 4
• RERANK scores SELECT’s candidates as proof-state–premise pairs and returns the highest-scoring premises, trading greater accuracy for slower individual scoring.The pairwise input lets RERANK analyze each premise in the context of the current proof state.Source: §3 · p. 4
• SELECT uses modified InfoNCE training, while RERANK uses binary cross-entropy; both share a pretrained transformer backbone with specialized linear projections.The backbone is pretrained on GitHub and arXiv subsets of the Pile dataset.Source: §3 · p. 4
• SELECT training adds sampled negative premises beyond the other batch premises, typically using M = 3N; RERANK trains on 15 likely false positives per positive pair.RERANK’s negatives are sampled from the top 1,024 SELECT-ranked facts that were never used for that proof state.Source: §3 · p. 4
• At evaluation, retrieved premises are combined with tactics in parallel proof steps, using premise subsets sized by consecutive powers of two and a 2-second timeout.A theorem counts as successful if any tested proof step completes it.Source: §3 · p. 5
• Trying multiple premise subsets restricts the combinatorial search performed by ATPs and high-level ITP tactics.The paper notes that this practice is also used in automated theorem proving and is similar to Sledgehammer’s technique.Source: §3 · p. 5

4 DATASETS

• The released dataset is, to the authors’ knowledge, Isabelle’s first high-quality dataset of this kind and the largest premise-selection dataset overall.It draws on the Archive of Formal Proofs and the Isabelle Standard library.Source: §4 · p. 5
• MAPL combines human-proof HPL data with SH data from Sledgehammer-generated alternative proofs, and contains over 4M data points.The dataset statistics distinguish MAPL from its HPL and SH partitions.Source: §4 · p. 5, Table 1 · p. 5
• Each human proof step contributes pairs of its preceding proof state and the premises used in that step.A step using n premises yields n training data points.Source: §4 · p. 5
• Adding alternative Sledgehammer proofs makes the dataset larger and more diverse and partially addresses false negatives in contrastive training.An unobserved alternative premise may be positive; alternative proofs partially remedy this issue.Source: §4 · p. 5
• Proof states and premises use high-level Isabelle text, making the dataset more suitable for language models and facilitating cross-proof-assistant pre-training.The representation also decreases the need for feature engineering.Source: §4 · p. 5

5.1 EXPERIMENTAL DETAILS

• PISA uses 1,000 problems and miniF2F has 488 high-school competition problems; proof success requires formal verification by Isabelle.The evaluation distinguishes single-step premise application from multi-step proof search using a language model.Source: §5.1 · p. 6
• Main empirical results use the 86M-parameter model, with Magnushammer outperforming Sledgehammer across a broad spectrum of computational budgets.The evaluation protocol combines tactics with ranked premises and estimates Sledgehammer's budget from CPU cores and timeout.Source: §5.1 · pp. 6–7, §5.2 · p. 7

5.2 RESULTS ON PISA AND MINIF2F BENCHMARKS

• 59.5% vs. 38.3% on PISA and 34.0% vs. 20.9% on miniF2F; Thor + Magnushammer reaches 71.0% vs. 57.0% on PISA.The single-step comparisons use a computational budget of 1000; the Thor experiments use a budget of 200.Source: §5.2 · p. 7

5.2.1 SCALING COMPUTATIONAL BUDGET

• Magnushammer outperforms Sledgehammer even with very limited computational resources and scales well, particularly in the medium-budget range.The section compares premise-selection quality across evaluation budgets.Source: §5.2.1 · p. 7

5.3 IMPACT OF TRAINING DATA

• The experiments compare HPL with MAPL using 38M-parameter models and a computational budget of 800.MAPL combines human-proof data with proofs generated by Sledgehammer.Source: §5.3 · p. 8
• With only 0.1% of MAPL—approximately 4K samples—Magnushammer already outperforms Sledgehammer.The effect of pre-training diminishes as the amount of training data increases.Source: §5.3 · p. 8, Figure 3 · p. 8
• Using the full datasets, fine-tuning on MAPL or HPL yields proof rates of 56.3% and 54.0%, respectively.The authors speculate that MAPL's larger size may matter for harder benchmarks and larger models.Source: §5.3 · p. 8

5.4 ABLATIONS

• A 920K-parameter model outperforms Sledgehammer, 40.7% vs. 38.3%; scaling layers is more beneficial than scaling embedding dimension.The model-size comparison uses MAPL-trained models and a computational budget of 800.Source: §5.4 · p. 8

• Classical premise-selection methods include Bayesian and kernel models, k-NN, and decision trees; these approaches require hand-engineered features.The passage notes faster, simpler training as an advantage of these methods.Source: §6 · p. 9
• Alemi et al. (2016) applied deep learning to premise selection without hand-designed features, but evaluated in automated theorem proving rather than a proof assistant.Their approach uses logistic loss and a shallow network over concatenated conjecture and premise embeddings; Magnushammer uses contrastive loss and cosine similarity.Source: §6 · p. 9
• Piotrowski and Urban (2020) model premise dependencies as sequences, but treat premises as opaque tokens rather than inspectable statements.Source: §6 · p. 9
• Generative theorem-proving models often generate premise names without inspecting statements; Magnushammer retrieves premises, avoiding the context-length challenge of long statements.The passage describes Thor as using Sledgehammer for premise selection and says Magnushammer can be used alongside other models.Source: §6 · p. 9
• Magnushammer combines SELECT retrieval with RERANK training; its approach shares in-batch negatives with HOList and uses retrieved premises as hard negatives for re-ranking.Concurrent work by Yang et al. (2023) also uses contrastive learning for Lean premise selection, but without a RERANK stage.Source: §6 · p. 9
• Existing evaluation datasets such as ProofNet and miniF2F do not provide training data; Magnushammer's dataset is published in high-level textual form rather than low-level structured languages.Source: §6 · pp. 9–10

Other proof assistants

• Magnushammer makes no assumptions about proof-state or premise structure, and the authors conjecture it could work in other proof assistants because it is agnostic to their logic or type system.Evaluation in Lean on ProofNet and miniF2F is planned.Source: §7 · p. 10

Richer proof and premise representations

• Magnushammer uses Isabelle’s textual proof state, which omits complete semantic information about referenced objects; adding function definitions and object types might improve performance.The authors identify richer proof and premise representations as a direction for future work.Source: §7 · p. 10

Modelling full proof steps

• Combining language models with external premise selection tools improves theorem-proving performance, motivating a single model that generates proof steps with relevant premises.The proposed direction could model dependencies between returned premises; retrieval-augmented language models are suggested as a possible aid.Source: §7 · p. 10

REPRODUCIBILITY STATEMENT

• The backbone pre-training data, Isabelle downstream-training data, and evaluation benchmarks are identified as freely available resources.PISA also implements the Isabelle interface used in the experiments; appendices document model, loss, hyperparameter, hardware, and evaluation details.Source: REPRODUCIBILITY STATEMENT · p. 10

A ISABELLE ENVIRONMENT

• The appendix illustrates Isabelle with a theorem stating that a natural-number self-map satisfying f(f(n)) < f(n+1) is the identity, proved by induction and refinement.The example comes from the Archive of Formal Proofs entry Fun With Functions.Source: §A.1 · p. 18

A.1 VISUALIZATION OF THE ISABELLE ENVIRONMENT

• In the illustrated proof, the orange frame marks the theorem statement and the green frame the proof; most lines first formulate a proposition and then prove it.Figure A.2 breaks down a line into a proposition, a proof step, the resulting proof state, and the full premise statement.Source: Figure A.1 · p. 18, Figure A.2 · p. 18

A.2 ALTERNATIVE PROOF STEP GENERATION WITH SLEDGEHAMMER

• Alternative proof steps are generated by replacing intermediate propositions, including nested ones, with Sledgehammer steps; successful steps are recorded and both proof versions retained.The process supplies examples for the dataset described in Section 4.Source: §A.2 · p. 19

A.3 EXAMPLE OF A PROOF WITH TACTICS REQUIRING PREMISES √

• The example proof of 2 /∈Q includes premise-using tactics such as metis, smt, fastforce, blast, and auto.One illustrated metis step uses the premises Rats cases’ and less irrefl.Source: Figure A.4 · p. 19, §A.3 · p. 19

A.4 SLEDGEHAMMER SETUP

• Sledgehammer was run in Isabelle 2021-1 with a default 30-second timeout, several settings, and on-machine provers; its reported proof rate is the union across runs.The computation-budget estimate assumes S = 10 CPU cores, which the authors say is realistic for their 96-core machines.Source: §A.4 · p. 20

B.1 SELECT STAGE

• SELECT is trained with the InfoNCE loss, using a proof state as query, a dataset premise as positive, and other premises as negatives, scored by cosine similarity.The temperature parameter τ is positive and non-trainable.Source: §B.1 · p. 20

B.2 RERANK STAGE

• Pairwise relevance classification is too costly across all premises, so RERANK applies it to a small SELECT-retrieved set using cross-entropy.Training samples positive pairs and negatives drawn from SELECT’s top 1024 likely false positives.Source: §B.2 · p. 20

B.3 MAGNUSHAMMER

• Magnushammer alternates SELECT and RERANK update steps with a shared transformer backbone, recomputing the top 1024 premises for reranking every 1000 steps.The periodic recomputation is used for efficiency because calculating SELECT’s negative premises is costly.Source: §B.3 · p. 20

C.1 MODEL ARCHITECTURE

• The decoder-only transformer uses separate proof-state and premise projections with a shared backbone, while RERANK projects the last-token embedding to a relevance score.The described models have 12 layers; the 38M model uses D = 512 and the 86M model D = 768.Source: §C.1 · pp. 20–21

C.2 HYPERPARAMETER SETUP

• Hyperparameter sweeps found no significant result differences; the selected settings include learning rate 2e−4, SELECT batch size 256, and 15 RERANK negatives per proof state.Other selected settings include dropout 0.1 and an InfoNCE temperature of 0.07.Source: §C.2 · p. 21

C.3 PRE-TRAINING ON LANGUAGE MODELING

• The decoder-only models are pre-trained for 1M steps on GitHub and arXiv subsets of the Pile, with a context length of 2048.The global batch contains 32 sequences, or 65,536 tokens, and the learning rate follows a warmup then cosine schedule.Source: §C.3 · p. 21

C.4 FINE-TUNING FOR DOWNSTREAM TASKS

• Downstream fine-tuning starts from a pre-trained language model, removes its language-modeling head, and adds projections for proof-state embeddings, premise embeddings, and RERANK relevance scores.For proof-step generation, the authors apply the algorithm used to train Thor.Source: §C.4 · pp. 21–22

C.5 IMPACT OF RE-RANKING

• On the 38M model, SELECT-only achieves a 54.2% proof rate, comparable to 56.3% for Magnushammer; it needs one forward pass and permits cached-premise CPU inference without accelerators.The SELECT-only method omits RERANK and is described as a computationally appealing alternative.Source: §C.5 · p. 22

C.6 HARDWARE

• Pre-training, fine-tuning, and evaluation use Google Cloud TPU virtual machines, each with 8 TPU v3 cores, 96 CPU cores, and over 300GB of RAM.The Isabelle environment is allocated 32 CPU cores.Source: §C.6 · p. 22

D MAGNUSHAMMER EVALUATION

• Algorithm 3 retrieves premises, generates proof steps with ten listed tactics, and checks those steps in the ITP environment; BM25 is evaluated using the same procedure.The tactics are smt, metis, auto, simp, blast, meson, force, eval, presburger, and linarith.Source: D MAGNUSHAMMER EVALUATION · p. 22, §D.1 · p. 22

D.1 COMPUTATIONAL BUDGET

• The main evaluation uses 14 premise counts, 36 tactics, and a 2-second timeout per tactic, for computational budget C ≈1000; ablations use powers of two and C ≈800.The main counts include powers of two from 2^0 to 2^10 and 48, 96, and 192.Source: §D.1 · p. 22

D.2 THOR + MAGNUSHAMMER

• Thor integration replaces Sledgehammer when the language model emits <hammer>, then adds up to two resulting proof states to the BFS queue.Proof search ends at a valid proof, 300 language-model queries, 500 seconds of wall time, or an empty queue; the queue limit is 32.Source: §D.2 · p. 23

E.1 SUPPLEMENTAL DETAILS

• The supplemental Table 4 relates training data to proof rate, while Table 5 reports PISA proof rates across Transformer layer counts and embedding dimensions.The supplied captions specify table scope but not cell values.Source: Table 4 · p. 23, §E.1 · p. 23, Table 5 · p. 24

E.2 STEP TACTIC PROMPT

• Tactic prompts do not significantly improve results, but the authors report that they rank premises needed to close proofs higher.Table 6 and Figure A.5 compare accumulated proof rates as the number of premises used to generate tactic steps increases.Source: §E.2 · p. 23, Table 6 · p. 24, Figure A.5 · p. 24

E.3 NUMBER OF PREMISES USED AS A PERFORMANCE METRIC FOR PREMISE SELECTION.

• The proposed retrieval metric counts problems solved using at most k premises, with fewer premises indicating that necessary facts rank higher and unnecessary facts lower.Each increase in k adds one step per tactic to try.Source: §E.3 · p. 25

E.4 SINGLE-STEP PROOF RATE BOUND

• 65.5% of proofs are closed by the union of Magnushammer variants, Sledgehammer, BM25, and other models when evaluated from the root state in one step.The ensemble includes Magnushammer-86M, Magnushammer-38M, Magnushammer-SELECT, Sledgehammer, BM25, and models from Section 5.4.Source: §E.4 · p. 25

F EXAMPLES OF PROOFS FOUND BY MAGNUSHAMMER

• Magnushammer passes retrieved premises directly to Isabelle tactics, whereas Sledgehammer relies on external provers and can fail when preselection supplies too few or too many premises.Magnushammer proofs typically use more premises and are longer when both systems solve a theorem.Source: F EXAMPLES OF PROOFS FOUND BY… · p. 25
• In one example, Magnushammer retrieved premises for an smt proof where Sledgehammer did not, illustrating the systems’ difference in premise selection.The example theorem is unit disc fix moebius uminus.Source: F EXAMPLES OF PROOFS FOUND BY… · pp. 25–26