Magnushammer: A Transformer-Based Approach to Premise Selection

Maciej MikulaSzymon TworkowskiSzymon AntoniakBartosz PiotrowskiAlbert Q. JiangJin Peng ZhouChristian SzegedyLukasz KucinskiPiotr MilosYuhuai Wu

article2024ICLR72 citations

Introduces Magnushammer, a transformer-based premise selection method that outperforms the symbolic Sledgehammer tool and increases automated theorem proving success on PISA from 57% to 71% with four times fewer model parameters.

Listen

Automated theorem proving and interactive proof assistants are essential tools for verifying complex mathematical reasoning and ensuring software correctness. However, a major bottleneck in formal verification is premise selection: the challenging task of retrieving a few relevant mathematical facts from libraries containing tens of thousands of lemmas to advance a proof. Traditional automation tools, such as Sledgehammer, rely on complex, hand-engineered symbolic heuristics and external provers. These traditional tools face diminishing returns as compute increases and require substantial engineering effort to adapt across different logical systems.

The article evaluates whether a purely data-driven, neural retrieval approach based on transformer models can outperform traditional symbolic methods on premise selection without requiring specialized domain engineering.

To address this question, the researchers developed Magnushammer, a generic transformer-based retrieval system. Magnushammer operates in two stages: first, an embedding-based contrastive selection stage rapidly narrows down tens of thousands of available facts to the top 1,024 candidates; second, a cross-attention reranking stage scores and reorders these candidates in the direct context of the current proof state. To train and evaluate the model, the authors created and open-sourced the largest formal premise selection dataset to date, comprising 4.4 million training pairs extracted from human-written proofs and machine-generated proofs in the Isabelle theorem prover.

The findings demonstrate that Magnushammer substantially outperforms established methods across standard benchmarks. In single-step proof automation on the PISA benchmark, Magnushammer achieved a 59.5% success rate compared to Sledgehammer's 38.3%, and achieved 34.0% versus 20.9% on the miniF2F competition benchmark. When integrated into Thor, a multi-step neural theorem proving system, Magnushammer established a new state of the art on PISA by lifting the overall proof rate from 57.0% to 71.0% while using a language model with four times fewer parameters. Furthermore, the approach exhibited strong data efficiency: a pre-trained Magnushammer model fine-tuned on just 0.1% of the training dataset (approximately 4,000 examples) still surpassed Sledgehammer. Even lightweight models with fewer than one million parameters outperformed the traditional baseline.

These results indicate that treating mathematical premises as standard text allows general deep-learning architectures to bypass the complex logic translations and external solvers that have historically limited theorem proving pipelines. By significantly improving retrieval precision, neural premise selection lowers the compute overhead and engineering cost needed to build automated assistants across diverse formal environments.

Organizations developing or deploying formal verification workflows should consider adopting neural retrieval pipelines as drop-in enhancements for existing hammer systems. Practitioners can also deploy the initial selection stage independently to enable fast, accelerator-free CPU inference using cached embeddings. Future initiatives should focus on testing Magnushammer across other interactive proof systems, such as Lean, and exploring end-to-end models that generate both proof tactics and premise arguments simultaneously.

While the findings demonstrate high reliability within the evaluated environments, the authors note that the current implementation relies strictly on textual representations provided by the proof assistant, omitting deeper semantic structures such as full type definitions. Confidence in the core performance gains remains high given consistent improvements across multiple compute budgets, model scales, and test suites.

Cornell University Google IDEAS NCBR Mistral AI University of Cambridge xAI automated theorem proving automation domain knowledge premise selection interactive theorem provers proof assistant

arXiv: 2303.04488

Paper: Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks, Patrick Lewis et al. (2020). Introduces Retrieval-Augmented Generation (RAG) using dense retrieval and transformer generation, providing foundational concepts for Magnushammer's dense premise retrieval methodology.
Paper: Attention Is All You Need, Ashish Vaswani et al. (2017). Establishes the core Transformer architecture, including self-attention and cross-attention mechanisms, upon which Magnushammer's two-stage retrieval and reranking design is built.
Paper: Measuring Mathematical Problem Solving With the MATH Dataset, Dan Hendrycks et al. (2021). Introduces the MATH dataset and benchmark framework for evaluating automated mathematical problem solving and reasoning in neural models.

Paper: LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks, Po-Nien Kung et al. (2026). Extends automated formal theorem proving by introducing an agentic proof-decomposition framework in Lean that complements Magnushammer's premise retrieval pipeline.
Paper: Search-o1: Agentic Search-Enhanced Large Reasoning Models, Xiaoxi Li et al. (2025). Generalizes neural retrieval during step-by-step reasoning by agentically interleaving web search into long-horizon reasoning trajectories.
Paper: Search-R1: Training LLMs to Reason and Leverage Search Engines with Reinforcement Learning, Bowen Jin et al. (2025). Applies reinforcement learning to train models to autonomously retrieve external information during multi-step reasoning tasks without explicit premise labels.
Paper: AI Co-Mathematician: Accelerating Mathematicians with Agentic AI, Daniel Zheng et al. (2026). Expands premise selection and formal proof automation into an interactive, end-to-end agentic workbench assisting mathematicians with literature search and formal drafting.

Cover for Magnushammer: A Transformer-Based Approach to Premise Selection

Abstract

This paper presents a novel approach to premise selection, a crucial reasoning task in automated theorem proving. Traditionally, symbolic methods that rely on extensive domain knowledge and engineering effort are applied to this task. In contrast, this work demonstrates that contrastive training with the transformer architecture can achieve higher-quality retrieval of relevant premises, without the engineering overhead. Our method, Magnushammer, outperforms the most advanced and widely used automation tool in interactive theorem proving called Sledgehammer. On the PISA and miniF2F benchmarks Magnushammer achieves $59.5\%$ (against $38.3\%$ ) and $34.0\%$ (against $20.9\%$ ) success rates, respectively. By combining \method with a language-model-based automated theorem prover, we further improve the state-of-the-art proof success rate from $57.0\%$ to $71.0\%$ on the PISA benchmark using $4$ x fewer parameters. Moreover, we develop and open source a novel dataset for premise selection, containing textual representations of (proof state, relevant premise) pairs. To the best of our knowledge, this is the largest available premise selection dataset, and the first one for the Isabelle proof assistant.

Topics

automated theorem proving automation domain knowledge encoder-decoder genetic selection isabelle/hol language model reasoning higher order logic

Keywords

premise selection interactive theorem provers proof assistant proof search proof reconstruction higher-order logic mathematical reasoning large language models

1 Introduction
2 Background: proof assistants, Isabelle, and Sledgehammer
3 Magnushammer
4 Datasets
5 Experiments
5.1 Experimental details
5.2 Results on PISA and miniF2F benchmarks
5.2.1 Scaling computational budget
5.3 Impact of training data
5.4 Ablations
6 Related work
7 Limitations and future work
References
A Isabelle environment
A.1 Visualization of the Isabelle environment
A.2 Alternative proof step generation with Sledgehammer
A.3 Example of a proof with tactics requiring premises
A.4 Sledgehammer setup
B Details of Magnushammer
B.1 Select stage
B.2 Rerank stage
B.3 Magnushammer
C Training details
C.1 Model architecture
C.2 Hyperparameter setup
C.3 Pre-training on language modeling
C.4 Fine-tuning for downstream tasks
C.5 Impact of re-ranking
C.6 Hardware
D Magnushammer evaluation
D.1 Computational budget
D.2 Thor + Magnushammer
E Additional experimental results
E.1 Supplemental details
E.2 Step tactic prompt
E.3 Number of premises used as a performance metric for premise selection.
E.4 Single-step proof rate bound
F Examples of proofs found by Magnushammer

Knowls

Knowl 1 — Magnushammer Two-Stage Premise Selection Framework
model/method
Magnushammer is a neural premise selection system designed for interactive theorem provers (ITPs) such as Isabelle. Rather than translating conjectures and facts into first-order logic for external automated theorem provers (ATPs) as done by traditional "hammer" tools like Sledgehammer, Magnushammer operates directly on the textual representations of proof states and available library premises via a two-stage transformer architecture:
1. SELECT Stage (Fast Dense Retrieval): Given a current proof state and a candidate pool of tens of thousands of premises (typically 30,000–50,000 available in a context), a bi-encoder representation model computes separate dense embeddings for the proof state and each premise. Premise embeddings are pre-computed and cached. The model retrieves the top $K_S = 1024$ most relevant premises using cosine similarity.
2. RERANK Stage (Cross-Attention Re-ranking): The $K_S$ candidate premises retrieved by SELECT are concatenated pairwise with the proof state text: (proof_state, premise). A cross-encoder model applies bidirectional self-attention across the combined tokens, projecting the final token embedding through a linear layer and sigmoid activation to produce an independent relevance probability for each pair. The premises are re-ordered by these scores to return the top $K_R$ ( $K_R = K_S$ ) ranked premises.
Both stages share the same underlying decoder-only transformer backbone (with rotary positional embeddings) while using specialized linear projection heads for state embedding, premise embedding, and binary relevance classification.
Knowl 2 — Multi-Task Training and Loss Formulations for Magnushammer
algorithm
Magnushammer trains its shared transformer backbone using alternating updates between the SELECT retrieval task and the RERANK classification task, accompanied by periodic hard-negative cache updates.

SELECT Loss Formulation

The SELECT stage is trained using a modified InfoNCE contrastive loss. For a batch containing $N$ proof states, $N$ ground-truth positive premises (one per proof state), and $M = 3N$ randomly sampled negative premises from the database that are not ground-truth facts for any state in the batch (yielding $N - 1 + M$ total negative premises per query $q$ ):

$\mathcal{L}_{\text{SELECT}}(q, k^+) = -\log \frac{\exp(s(q, k^+) / \tau)}{\exp(s(q, k^+) / \tau) + \sum_{i=1}^{N - 1 + M} \exp(s(q, k_i^-) / \tau)}$

where $s(q, k)$ denotes the cosine similarity between the linear projections of the proof state embedding and the premise embedding, and $\tau = 0.07$ is a fixed temperature parameter.

RERANK Loss Formulation

The RERANK stage is trained with binary cross-entropy loss over positive pairs $\mathcal{P}$ and hard-negative pairs $\mathcal{N}$ :

$\mathcal{L}_{\text{RERANK}} = -\sum_{p \in \mathcal{P}} \log \text{score}(p) - \sum_{n \in \mathcal{N}} \log(1 - \text{score}(n))$

where $\text{score}(p) \in (0, 1)$ is the sigmoid output of the linear classification head. For each positive pair $(q, k^+)$ in a batch of size 64, 15 hard negatives are sampled from the top 1024 false-positive premises returned by the SELECT model.

Training Procedure
Input: Initial parameters $\theta$ , premise dataset $\mathcal{D}$ , negative refresh interval $T = 1000$
Output: Trained model parameters $\theta$
$\mathcal{D}_{\text{rerank}} \leftarrow \text{recompute_negatives_for_rerank}(\theta, \mathcal{D})$
step $\leftarrow 0$
while step < num_train_steps do
    batch_select $\leftarrow \mathcal{D}.\text{sample}()$
     $\theta \leftarrow \text{train_step}(\theta, \text{batch_select})$
    batch_rerank $\leftarrow \mathcal{D}_{\text{rerank}}.\text{sample}()$
     $\theta \leftarrow \text{train_step}(\theta, \text{batch_rerank})$
    step $\leftarrow \text{step} + 1$
    if step mod $T == 0$ then
         $\mathcal{D}_{\text{rerank}} \leftarrow \text{recompute_negatives_for_rerank}(\theta, \mathcal{D})$
    end if
end while
return $\theta$
Knowl 3 — Magnushammer Premise Selection Inference Algorithm
algorithm
During inference, Magnushammer takes a target proof state and a set of available candidate premises, producing a ranked list of relevant premises via two-stage filtering:
Input: proof_state, premises database $\mathcal{D}_{\text{prem}}$ , number of SELECT candidates $K_S = 1024$ , number of returned premises $K_R = 1024$
Output: top_premises of length $K_R$
state_embedding $\leftarrow \text{get_state_embedding}(\text{proof_state})$
premises_embeddings $\leftarrow \text{get_cached_embeddings}(\mathcal{D}_{\text{prem}})$
sim_scores $\leftarrow \text{state_embedding} \cdot \text{premises_embeddings}$
selected $\leftarrow \text{premises}[\text{argsort}(-\text{sim_scores})[:K_S]]$
batch $\leftarrow []$
for premise in selected do
batch.append((proof_state, premise))
end for
rerank_scores $\leftarrow \text{get_rerank_scores}(\text{batch})$
top_premises $\leftarrow \text{selected}[\text{argsort}(-\text{rerank_scores})[:K_R]]$
return top_premises
Knowl 4 — Single-Step Theorem Proving Evaluation Protocol and Computational Budget
algorithm
To evaluate a premise selection algorithm in an interactive theorem prover (e.g., Isabelle), retrieved premises are combined with proof tactics and executed in parallel.

Computational Budget Definition

The evaluation computational budget $C$ is defined as:

$C = |T| \times |K| \times T_{\text{timeout}}$

where $T$ is the set of tactics used (e.g., smt, metis, auto, simp, blast, meson, force, eval, presburger, linarith), $K$ is a list of candidate prefix lengths specifying how many top-ranked premises to provide to each tactic, and $T_{\text{timeout}} = 2\text{ s}$ is the per-step execution timeout. In standard single-step evaluations, $|T| = 36$ tactic configurations and $K = [2^0, 2^1, \dots, 2^{10}, 48, 96, 192]$ (14 values) are used, resulting in a budget $C \approx 1000$ .

Single-Step Evaluation Procedure
Input: theorem, premise selection model premsel_model, budget parameters $K_S, K_R$ , premises pool, top_k_premises_to_try $K$ , tactics_to_try $T$ , environment env
Output: Boolean solved
proof_state $\leftarrow \text{init_problem}(\text{env}, \text{theorem})$
top_premises $\leftarrow \text{premsel_model}(\text{proof_state}, \text{premises}, K_S, K_R)$
steps $\leftarrow []$
for $k$ in top_k_premises_to_try do
    top_k $\leftarrow \text{top_premises}[:k]$
    new_steps $\leftarrow \text{generate_steps}(\text{tactics_to_try}, \text{top_k})$
    steps.extend(new_steps)
end for
solved $\leftarrow \text{try_steps}(\text{env}, \text{steps})$
return solved

Knowl 5 — Machine-Augmented Proofs Library (MAPL) Dataset for Isabelle

data/table

The Machine-Augmented Proofs Library (MAPL) dataset consists of paired (proof_state, premise) data points extracted from the Archive of Formal Proofs (AFP) and the Isabelle Standard Library, using high-level textual representations rather than low-level logic representations (such as TPTP).

MAPL is split into two components:

Human Proofs Library (HPL): Ground-truth steps written by human formalizers.
Sledgehammer (SH) Partition: Alternative synthetic proof steps generated by running Sledgehammer on intermediate subgoals within human proofs. This augmentation expands data diversity and mitigates the occurrence of false negatives during contrastive learning.

Knowl 6 — Proof Success Rates on PISA and miniF2F Benchmarks

data/table

Magnushammer (86M non-embedding parameters) was evaluated on the PISA benchmark (1000 test problems from the Archive of Formal Proofs) and the miniF2F benchmark (488 competition-level mathematics problems across validation and test splits) in both single-step execution and multi-step proof search (Thor + Magnushammer).

Task (PISA)	Method	Proof rate (%)
Single-step	BM25	30.6
Single-step	TF-IDF	31.8
Single-step	OpenAI embed. (text-embedding-ada-002)	36.1
Single-step	Sledgehammer	38.3
Single-step	Magnushammer (86M)	59.5
Multi-step	LISA	33.2
Multi-step	Thor (700M) + Sledgehammer	57.0
Multi-step	Thor + Magnushammer	71.0

Task (miniF2F)	Method	Valid (%)	Test (%)
Single-step	Sledgehammer	9.9	10.4
Single-step	Sledgehammer + heuristics	18.0	20.9
Single-step	Magnushammer (86M)	33.6	34.0
Multi-step	Thor + Sledgehammer	28.3	29.9
Multi-step	Thor + Sledgehammer + auto	37.3	35.2
Multi-step	Thor + Magnushammer	36.9	37.3
Multi-step	DSP (Minerva 62B)	43.9	39.3

In the single-step setting, Magnushammer outperforms Sledgehammer by +21.2 percentage points on PISA and +13.1 percentage points on miniF2F test. When integrated with Thor in the multi-step setting, Magnushammer establishes a state-of-the-art success rate of 71.0% on PISA.

Knowl 7 — Multi-Step Theorem Proving Integration with Thor
model/method
To tackle complex, multi-step formal proofs, Magnushammer is integrated into the language-model-based Best-First Search (BFS) framework of Thor. During the proof search:
1. A generative language model samples candidate proof steps conditioned on the current proof state.
2. When the language model emits a special <hammer> token, Magnushammer is invoked rather than Sledgehammer to select relevant premises from the context library.
3. Candidate single-step tactic combinations are constructed using the top retrieved premises and executed with a 2-second timeout per step.
4. If an execution closes the proof, search completes successfully. Otherwise, at most $s = 2$ non-closed valid successor proof states resulting from successful tactic applications are inserted into the BFS priority queue (maximum queue capacity of 32).
5. The search terminates when the theorem is proven, 300 language model queries are exhausted, a wall-clock timeout of 500 s is reached, or the queue becomes empty.

Knowl 8 — Data Scaling and Pre-Training Efficiency of Magnushammer

data/table

The table below evaluates the impact of training dataset volume, dataset source (HPL vs. MAPL), and language model pre-training (pre-trained on GitHub and arXiv subsets of the Pile vs. trained from scratch) on the PISA benchmark proof success rate, using a 38M non-embedding parameter model and a computation budget of $C = 800$ .

Dataset	Fraction	Pre-trained	Proof rate (%)
MAPL	0.1% ( 4K samples)	Yes	39.2
HPL	0.1%	Yes	34.9
MAPL	0.1%	No	16.8
MAPL	1.0%	Yes	47.7
HPL	1.0%	Yes	42.7
MAPL	1.0%	No	29.0
MAPL	10.0%	Yes	53.2
HPL	10.0%	Yes	49.4
MAPL	10.0%	No	48.5
MAPL	100.0%	Yes	56.3
HPL	100.0%	Yes	54.0
MAPL	100.0%	No	53.0

When pre-trained, fine-tuning Magnushammer on as little as 0.1% of MAPL (~4,000 samples) achieves a 39.2% proof rate, which exceeds Sledgehammer's full baseline performance (38.3%). While pre-training provides significant gains in low-data regimes (+22.4% at 0.1% fraction), its relative benefit narrows as the full 4.4M-example dataset is utilized (+3.3% at 100%).

Knowl 9 — Transformer Capacity and Architecture Scaling on PISA

data/table

The performance of Magnushammer scales with transformer depth (number of layers $L$ ), width (embedding dimension $D$ ), parameter count, and language model pre-training. All evaluations were conducted on the PISA benchmark with a compute budget of $C = 800$ after fine-tuning on MAPL.

Transformer ( $L, D$ )	#Parameters	Pre-trained	Proof rate (%)
(1, 256)	920K	No	40.7
(1, 512)	3.7M	No	43.9
(2, 256)	1.7M	No	47.0
(2, 512)	6.8M	No	48.4
(2, 768)	15.4M	No	49.9
(6, 512)	19.2M	No	52.5
(6, 512)	19.2M	Yes	53.3
(6, 768)	43.7M	No	52.1
(12, 512)	38.3M	No	52.6
(12, 512)	38.3M	Yes	56.3
(12, 768)	86.2M	Yes	57.0

Even a minimal single-layer transformer with 920K parameters trained from scratch achieves a 40.7% proof rate, exceeding Sledgehammer (38.3%). Increasing model depth ( $L$ ) yields greater improvements than increasing embedding dimension ( $D$ ) for comparable parameter budgets (e.g., $(12, 512)$ at 38.3M parameters outperforms $(6, 768)$ at 43.7M parameters).

Knowl 10 — SELECT-Only Premise Selection Performance and Inference Efficiency
empirical result
Operating Magnushammer in a "SELECT-only" mode (bypassing the cross-encoder RERANK stage entirely and scoring solely by cosine similarity of dense embeddings) achieves a 54.2% single-step proof success rate on PISA using the 38M parameter model, compared to 56.3% for the full two-stage SELECT + RERANK pipeline.

While the two-stage model provides superior accuracy, SELECT-only mode requires only a single neural network forward pass to embed the target proof state followed by inner products against pre-cached premise embeddings. This makes SELECT-only execution computationally lightweight and capable of running premise retrieval entirely on CPU architectures without GPU/TPU accelerators.

Coverage note — Qualitative proof step examples from Appendix F and the tactic-prompted premise selection ablation from Appendix E.2 were omitted, as they represent minor illustrative examples and secondary metric variants that are not central to the primary method or its benchmark results.

References

1.Jesse Alama, Daniel Kóhlwein, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Premise selection for mathematics by corpus analysis and kernel methods. CoRR, abs/1108.3446, 2011. URL http://arxiv.org/abs/1108.3446.
2.Jesse Alama, Tom Heskes, Daniel Kóhlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason., 52(2): 191–213, 2014. doi: 10.1007/s10817-013-9286-5. URL https://doi.org/10.1007/s10817-013-9286-5.
3.Alexander A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, and Josef Urban. DeepMath – deep sequence models for premise selection. CoRR, abs/1606.04442, 2016. URL http://arxiv.org/abs/1606.04442.
4.Zhangir Azerbayev, Bartosz Piotrowski, and Jeremy Avigad. ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems. In Advances in Neural Information Processing Systems 35, 2nd MATH-AI Workshop at NeurIPS'22, 2022. URL https://mathai2022.github.io/papers/20.pdf.
5.Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 454–463. PMLR, 2019. URL http://proceedings.mlr.press/v97/bansal19a.html.
6.Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems – 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 415–442. Springer, 2022. doi: 10.1007/978-3-030-99524-9_24. URL https://doi.org/10.1007/978-3-030-99524-9_24.
7.Yves Bertot. A short presentation of coq. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 12–16. Springer, 2008. doi: 10.1007/978-3-540-71067-7_3. URL https://doi.org/10.1007/978-3-540-71067-7_3.
8.Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. J. Autom. Reason., 51(1):109–128, 2013. doi: 10.1007/s10817-013-9278-5. URL https://doi.org/10.1007/s10817-013-9278-5.
9.Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kóhlwein, and Josef Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reason., 57(3):219–244, 2016. doi: 10.1007/s10817-016-9362-8. URL https://doi.org/10.1007/s10817-016-9362-8.
10.Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement day. In Jürgen Giesl and Reiner Hähnle, editors, Automated Reasoning, pages 107–121, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. ISBN 978-3-642-14203-1.
11.Sebastian Borgeaud, Arthur Mensch, Jordan Hoffmann, Trevor Cai, Eliza Rutherford, Katie Millican, George van den Driessche, Jean-Baptiste Lespiau, Bogdan Damoc, Aidan Clark, Diego de Las Casas, Aurelia Guy, Jacob Menick, Roman Ring, Tom Hennigan, Saffron Huang, Loren Maggiore, Chris Jones, Albin Cassirer, Andy Brock, Michela Paganini, Geoffrey Irving, Oriol Vinyals, Simon Osindero, Karen Simonyan, Jack W. Rae, Erich Elsen, and Laurent Sifre. Improving language models by retrieving from trillions of tokens. In Kamalika Chaudhuri, Stefanie Jegelka, Le Song, Csaba Szepesvári, Gang Niu, and Sivan Sabato, editors, International Conference on Machine Learning, ICML 2022, 17-23 July 2022, Baltimore, Maryland, USA, volume 162 of Proceedings of Machine Learning Research, pages 2206–2240. PMLR, 2022. URL https://proceedings.mlr.press/v162/borgeaud22a.html.
12.Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. CoRR, abs/2005.14165, 2020. URL https://arxiv.org/abs/2005.14165.
13.Ting Chen, Simon Kornblith, Mohammad Norouzi, and Geoffrey E. Hinton. A simple framework for contrastive learning of visual representations. In Proceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event, volume 119 of Proceedings of Machine Learning Research, pages 1597–1607. PMLR, 2020. URL http://proceedings.mlr.press/v119/chen20j.html.
14.Alexis Conneau and Guillaume Lample. Cross-lingual language model pretraining. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32. Curran Associates, Inc., 2019. URL https://proceedings.neurips.cc/paper/2019/file/c04c19c2c2474dbf5f7ac4372c5b9af1-Paper.pdf.
15.Lukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for dependent type theory. J. Autom. Reason., 61(1-4):423–453, 2018. doi: 10.1007/s10817-018-9458-4. URL https://doi.org/10.1007/s10817-018-9458-4.
16.Nicolaas Govert De Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. In Symposium on automatic demonstration, pages 29–61. Springer, 1970.
17.Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-78800-3.
18.Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction – CADE-25 – 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378–388. Springer, 2015. doi: 10.1007/978-3-319-21401-6_26. URL https://doi.org/10.1007/978-3-319-21401-6_26.
19.Gabriel Ebner. Integration of general-purpose automated theorem provers in Lean, 2020. https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_ebner.pdf.
20.Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy. The Pile: An 800GB dataset of diverse text for language modeling. CoRR, abs/2101.00027, 2021. URL https://arxiv.org/abs/2101.00027.
21.Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 49–57. ACM, 2015. doi: 10.1145/2676724.2693173. URL https://doi.org/10.1145/2676724.2693173.
22.Zarathustra Amadeus Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban. The Isabelle ENIGMA. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 16:1–16:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi: 10.4230/LIPIcs.ITP.2022.16.
23.Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. J. Formaliz. Reason., 3(2):153–245, 2010. doi: 10.6092/issn.1972-5787/1980. URL https://doi.org/10.6092/issn.1972-5787/1980.
24.Jesse Michael Han, Tao Xu, Stanislas Polu, Arvind Neelakantan, and Alec Radford. Contrastive finetuning of generative language models for informal premise selection. 6th Conference on Artificial Intelligence and Theorem Proving, 2021.
25.Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL https://openreview.net/forum?id=rpxJc9j04U.
26.John Harrison. HOL light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1166 of Lecture Notes in Computer Science, pages 265–269. Springer, 1996. doi: 10.1007/BFb0031814. URL https://doi.org/10.1007/BFb0031814.
27.Jordan Hoffmann, Sebastian Borgeaud, Arthur Mensch, Elena Buchatskaya, Trevor Cai, Eliza Rutherford, Diego de Las Casas, Lisa Anne Hendricks, Johannes Welbl, Aidan Clark, Tom Hennigan, Eric Noland, Katie Millican, George van den Driessche, Bogdan Damoc, Aurelia Guy, Simon Osindero, Karen Simonyan, Erich Elsen, Jack W. Rae, Oriol Vinyals, and Laurent Sifre. Training compute-optimal large language models. CoRR, abs/2203.15556, 2022. doi: 10.48550/arXiv.2203.15556. URL https://doi.org/10.48550/arXiv.2203.15556.
28.Jeremy Howard and Sebastian Ruder. Universal language model fine-tuning for text classification. In Iryna Gurevych and Yusuke Miyao, editors, Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics, ACL 2018, Melbourne, Australia, July 15-20, 2018, Volume 1: Long Papers, pages 328–339. Association for Computational Linguistics, 2018. doi: 10.18653/v1/P18-1031. URL https://aclanthology.org/P18-1031/.
29.Gautier Izacard, Mathilde Caron, Lucas Hosseini, Sebastian Riedel, Piotr Bojanowski, Armand Joulin, and Edouard Grave. Towards unsupervised dense information retrieval with contrastive learning. CoRR, abs/2112.09118, 2021. URL https://arxiv.org/abs/2112.09118.
30.Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. LISA: Language models of ISAbelle proofs. 6th Conference on Artificial Intelligence and Theorem Proving, 2021.
31.Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźć, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances in Neural Information Processing Systems, 2022a. URL https://openreview.net/forum?id=fUeOyt-2EOp.
32.Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. CoRR, abs/2210.12283, 2022b. doi: 10.48550/arXiv.2210.12283.
33.Cezary Kaliszyk and Josef Urban. HOL(y)Hammer: Online ATP service for HOL Light. Math. Comput. Sci., 9(1):5–22, 2015a. doi: 10.1007/s11786-014-0182-0. URL https://doi.org/10.1007/s11786-014-0182-0.
34.Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. Journal of Automated Reasoning, 55(3): 245–256, 2015b.
35.Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A machine learning dataset for higher-order logic theorem proving. CoRR, abs/1703.00426, 2017. URL http://arxiv.org/abs/1703.00426.
36.Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B. Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei. Scaling laws for neural language models. CoRR, abs/2001.08361, 2020. URL https://arxiv.org/abs/2001.08361.
37.Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification – 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 1–35. Springer, 2013. doi: 10.1007/978-3-642-39799-8_1. URL https://doi.org/10.1007/978-3-642-39799-8_1.
38.Alex Krizhevsky, Ilya Sutskever, and Geoffrey E. Hinton. ImageNet classification with deep convolutional neural networks. In Peter L. Bartlett, Fernando C. N. Pereira, Christopher J. C. Burges, Léon Bottou, and Kilian Q. Weinberger, editors, Advances in Neural Information Processing Systems 25: 26th Annual Conference on Neural Information Processing Systems 2012. Proceedings of a meeting held December 3-6, 2012, Lake Tahoe, Nevada, United States, pages 1106–1114, 2012. URL https://proceedings.neurips.cc/paper/2012/hash/c399862d3b9d6b76c8436e924a68c45b-Abstract.html.
39.Daniel Kóhlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning – 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 378–392. Springer, 2012. doi: 10.1007/978-3-642-31365-3_30. URL https://doi.org/10.1007/978-3-642-31365-3_30.
40.Daniel Kóhlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. MaSh: Machine learning for Sledgehammer. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving – 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 35–50. Springer, 2013. doi: 10.1007/978-3-642-39634-2_6. URL https://doi.org/10.1007/978-3-642-39634-2_6.
41.Guillaume Lample, Timothée Lacroix, Marie Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. HyperTree proof search for neural theorem proving. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances in Neural Information Processing Systems, 2022. URL https://openreview.net/forum?id=J4pX8Q8cxHH.
42.Aitor Lewkowycz, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances in Neural Information Processing Systems, 2022. URL https://openreview.net/forum?id=IFXTZERXdM7.
43.Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. IsarStep: A benchmark for high-level mathematical reasoning. In International Conference on Learning Representations, 2021. URL https://openreview.net/forum?id=Pzj6fzU6wkj.
44.Jia Meng and Lawrence C. Paulson. Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log., 7(1):41–57, 2009. doi: 10.1016/j.jal.2007.07.004.
45.Yutaka Nagashima and Yilun He. PaMpeR: Proof Method Recommendation system for Isabelle/HOL, 2018. URL https://arxiv.org/abs/1806.07239.
46.Arvind Neelakantan, Tao Xu, Raul Puri, Alec Radford, Jesse Michael Han, Jerry Tworek, Qiming Yuan, Nikolas Tezak, Jong Wook Kim, Chris Hallacy, Johannes Heidecke, Pranav Shyam, Boris Power, Tyna Eloundou Nekoul, Girish Sastry, Gretchen Krueger, David Schnurr, Felipe Petroski Such, Kenny Hsu, Madeleine Thompson, Tabarak Khan, Toki Sherbakov, Joanne Jang, Peter Welinder, and Lilian Weng. Text and code embeddings by contrastive pre-training, 2022.
47.Tobias Nipkow. Fun with functions. Archive of Formal Proofs, August 2008. ISSN 2150-914x. https://isa-afp.org/entries/FunWithFunctions.html, Formal proof development.
48.Rodrigo Frassetto Nogueira and Kyunghyun Cho. Passage re-ranking with BERT. CoRR, abs/1901.04085, 2019. URL http://arxiv.org/abs/1901.04085.
49.Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 2967–2974. AAAI Press, 2020. URL https://ojs.aaai.org/index.php/AAAI/article/view/5689.
50.Lawrence C. Paulson. Isabelle: The next 700 theorem provers. CoRR, cs.LO/9301106, 1993. URL https://arxiv.org/abs/cs/9301106.
51.Lawrence Charles Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In IWIL@LPAR, 2012.
52.Bartosz Piotrowski and Josef Urban. ATPboost: Learning premise selection in binary setting with ATP feedback. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning – 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 566–574. Springer, 2018. doi: 10.1007/978-3-319-94205-6_37. URL https://doi.org/10.1007/978-3-319-94205-6_37.
53.Bartosz Piotrowski and Josef Urban. Stateful premise selection by recurrent neural networks. In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 409–422. EasyChair, 2020. doi: 10.29007/j5hd. URL https://doi.org/10.29007/j5hd.
54.Bartosz Piotrowski, Ramon Fernández Mir, and Edward W. Ayers. Machine-learned premise selection for Lean. In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings, volume 14278 of Lecture Notes in Computer Science, pages 175–186. Springer, 2023. doi: 10.1007/978-3-031-43513-3_10. URL https://doi.org/10.1007/978-3-031-43513-3_10.
55.Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393.
56.Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. URL https://openreview.net/pdf?id=-P7G-8dmSh4.
57.Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Language models are unsupervised multitask learners. OpenAI blog, 1(8):9, 2019.
58.Alec Radford, Jong Wook Kim, Chris Hallacy, Aditya Ramesh, Gabriel Goh, Sandhini Agarwal, Girish Sastry, Amanda Askell, Pamela Mishkin, Jack Clark, Gretchen Krueger, and Ilya Sutskever. Learning transferable visual models from natural language supervision. CoRR, abs/2103.00020, 2021. URL https://arxiv.org/abs/2103.00020.
59.Stephen E. Robertson and Hugo Zaragoza. The probabilistic relevance framework: BM25 and beyond. Found. Trends Inf. Retr., 3(4):333–389, 2009. doi: 10.1561/1500000019.
60.Joshua David Robinson, Ching-Yao Chuang, Suvrit Sra, and Stefanie Jegelka. Contrastive learning with hard negative samples. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https://openreview.net/forum?id=CR1XOQ0UTh-.
61.Stephan Schulz. System description: E 0.81. In David Basin and Michaçl Rusinowitch, editors, Automated Reasoning, pages 223–228, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. ISBN 978-3-540-25984-8.
62.Jianlin Su, Yu Lu, Shengfeng Pan, Bo Wen, and Yunfeng Liu. Roformer: Enhanced transformer with rotary position embedding. CoRR, abs/2104.09864, 2021. URL https://arxiv.org/abs/2104.09864.
63.G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017.
64.Terence Tao. Solving mathematical problems: A personal perspective. Oxford University Press, 2010.
65.Nandan Thakur, Nils Reimers, Andreas Rücklé, Abhishek Srivastava, and Iryna Gurevych. BEIR: A heterogenous benchmark for zero-shot evaluation of information retrieval models. CoRR, abs/2104.08663, 2021. URL https://arxiv.org/abs/2104.08663.
66.Szymon Tworkowski, Maciej Mikuła, Tomasz Odrzygóźć, Konrad Czechowski, Szymon Antoniak, Albert Jiang, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Formal premise selection with language models. AITP 2022, 2022. URL http://aitp-conference.org/2022/abstract/AITP_2022_paper_32.pdf.
67.Josef Urban and Jan Jakubův. First neural conjecturing datasets and experiments. In Christoph Benzmüller and Bruce R. Miller, editors, Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pages 315–323. Springer, 2020. doi: 10.1007/978-3-030-53518-6_24. URL https://doi.org/10.1007/978-3-030-53518-6_24.
68.Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří VyskočIL. MaLARea SG1 – machine learner for automated reasoning with semantic guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, pages 441–456, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-71070-7.
69.Aaron van den Oord, Yazhe Li, and Oriol Vinyals. Representation learning with contrastive predictive coding. CoRR, abs/1807.03748, 2018. URL http://arxiv.org/abs/1807.03748.
70.Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. CoRR, abs/1706.03762, 2017. URL http://arxiv.org/abs/1706.03762.
71.Ben Wang and Aran Komatsuzaki. GPT-J-6B: A 6 Billion Parameter Autoregressive Language Model. https://github.com/kingoflolz/mesh-transformer-jax, May 2021.
72.Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. CoRR, abs/1709.09994, 2017. URL http://arxiv.org/abs/1709.09994.
73.Christoph Weidenbach. Combining superposition, sorts and splitting. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 1965–2013. Elsevier and MIT Press, 2001. doi: 10.1016/b978-044450813-3/50029-1. URL https://doi.org/10.1016/b978-044450813-3/50029-1.
74.Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances in Neural Information Processing Systems, 2022a. URL https://openreview.net/forum?id=IUikebJ1Bf0.
75.Yuhuai Wu, Markus Norman Rabe, DeLesley Hutchins, and Christian Szegedy. Memorizing transformers. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022b. URL https://openreview.net/forum?id=TrjbxzRcnf-.
76.Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 6984–6994. PMLR, 2019. URL http://proceedings.mlr.press/v97/yang19a.html.
77.Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. CoRR, abs/2306.15626, 2023. doi: 10.48550/arXiv.2306.15626. URL https://doi.org/10.48550/arXiv.2306.15626.
78.Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: A cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv.

Citation

MLA

Mikuła, M., et al. “Magnushammer: A Transformer-Based Approach to Premise Selection”. arXiv, 2023, http://arxiv.org/abs/2303.04488v3.

APA

Mikuła, M., Tworkowski, S., Antoniak, S., Piotrowski, B., Jiang, A. Q., Zhou, J. P., Szegedy, C., Kuciński, Ł., Miłoś, P., & Wu, Y. (2023). Magnushammer: A Transformer-Based Approach to Premise Selection. arXiv. http://arxiv.org/abs/2303.04488v3

Chicago

Mikuła, M., S. Tworkowski, S. Antoniak, et al. 2023. “Magnushammer: A Transformer-Based Approach to Premise Selection”. arXiv. http://arxiv.org/abs/2303.04488v3.

Harvard

Mikuła, M. et al. (2023) “Magnushammer: A Transformer-Based Approach to Premise Selection”, arXiv [Preprint]. Available at: http://arxiv.org/abs/2303.04488v3.

Vancouver

1. Mikuła M, Tworkowski S, Antoniak S, Piotrowski B, Jiang AQ, Zhou JP, Szegedy C, Kuciński Ł, Miłoś P, Wu Y (2023) Magnushammer: A Transformer-Based Approach to Premise Selection. arXiv

BibTeX

@article{mikua2023magnushammer,
  title = {Magnushammer: A Transformer-Based Approach to Premise Selection},
  author = {Mikuła, Maciej and Tworkowski, Szymon and Antoniak, Szymon and Piotrowski, Bartosz and Jiang, Albert Qiaochu and Zhou, Jin Peng and Szegedy, Christian and Kuciński, Łukasz and Miłoś, Piotr and Wu, Yuhuai},
  year = {2023},
  journal = {arXiv},
  url = {http://arxiv.org/abs/2303.04488v3},
  eprint = {2303.04488}
}

Metadata:arXiv

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF

License: Published with permission

Dataset	Data points	Unique proof states	Unique premises
HPL	1.1M	570K	300K
SH	3.3M	500K	306K
MAPL	4.4M	570K	433K

Magnushammer: A Transformer-Based Approach to Premise Selection

Abstract

Topics

Keywords

Table of Contents

Knowls

Knowl 1 — Magnushammer Two-Stage Premise Selection Framework

Knowl 2 — Multi-Task Training and Loss Formulations for Magnushammer

SELECT Loss Formulation

RERANK Loss Formulation

Training Procedure

Knowl 3 — Magnushammer Premise Selection Inference Algorithm

Knowl 4 — Single-Step Theorem Proving Evaluation Protocol and Computational Budget

Computational Budget Definition

Single-Step Evaluation Procedure

Knowl 5 — Machine-Augmented Proofs Library (MAPL) Dataset for Isabelle

Knowl 6 — Proof Success Rates on PISA and miniF2F Benchmarks

Knowl 7 — Multi-Step Theorem Proving Integration with Thor

Knowl 8 — Data Scaling and Pre-Training Efficiency of Magnushammer

Knowl 9 — Transformer Capacity and Architecture Scaling on PISA

Knowl 10 — SELECT-Only Premise Selection Performance and Inference Efficiency

References

Citation

BibTeX

Access the Paper