Magnushammer: A Transformer-Based Approach to Premise Selection
Authors: Maciej Mikuła
Szymon Tworkowski
Szymon Antoniak
Bartosz Piotrowski
Albert Q. Jiang
Jin Peng Zhou
Christian Szegedy
Łukasz Kuciński
Piotr Miłoś
Yuhuai Wu
Venue: ICLR 2024 poster (2024)
Keywords: transformers
interactive theorem proving
automated reasoning
contrastive learning
premise selection
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: Contrastively trained transformers outperform state-of-the-art symbolic methods for premise selection, a challenging reasoning task of selecting relevant facts for proving new theorems in formal mathematics.

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 knowledge or feature 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 Magnushammer 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 dataset of this kind for the Isabelle proof assistant.

Published as a conference paper at ICLR 2024
MAGNUSHAMMER: A TRANSFORMER-BASED APPROACH TO PREMISE SELECTION
Maciej Mikula" Google DeepMind
Szymon Tworkowski XAIt
Szymon Antoniak" Mistral AIT
Bartosz Piotrowski IDEAS NCBR
Albert Qiaochu Jiang University of Cambridge
Jin Peng Zhou Cornell University
Christian Szegedy xAI
Lukasz Kuciński IDEAS NCBR, IMPAN
Piotr Miloć
Yuhuai Wu
IDEAS NCBR, IMPAN
xAI
ABSTRACT
This paper presents a novel approach to premise selection, a crucial reasoning task in automated theorem proving. Traditionally, symbolic methods that rely on exten- sive 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 engineer- ing 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 Mag- nushammer with language-model-a improve the tate-of-the-an art proof success rate from 57.0% to 71.0% on the PISA benchmark using 4x 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.
automated theorem prover, we further
INTRODUCTION
Automating mathematical reasoning has been central theme of artificial intelligence since its
x
x
X
earliest days (De Bruijn 1970). Recently, ma-
Proof Rate (%6)
chine learning has led to significant advance-
40
ments in both informal (Lewkowycz et (022)
and formal mathematical reasoning (Kaliszyk
30
and Urban 20155 Alemi et al. 2016, Polu and
20
Sutskever 2020 Han et al. [2022). The latter ap-
Magnoshammer Sledgehammer BK25
proach, adopted in this paper, allows mechanical verification of proofs by proof assistants.
0
100
200
300
400
500
600
700
800
Compute Budget
Modern mathematics development is gradual: feeds upon huge body of already established knowledge and constantly adds to it. Proving a mathematical statement requires retrieval of facts from the knowledge base that can advance the proof. In automated reasoning literature, this retrieval process is known as premise selection.
Figure 1: Proof success rate for varying computa- tional budget for Magnushammer, Sledgehammer, and BM25. Magnushammer shows remarkable scalability. See Sections for for the definition of computational budget and Section 5.2. for con- figurations depicted in this figure.
"Equal contribution.
I Work performed while at the University of Warsaw. Work performed while Google Research.

---

Published as a conference paper at ICLR 2024
Many tools have been developed to tackle premise selection (Alama al. 2011 Kühlwein et al. 2012 Kaliszyk et al.) 2017; Bansal et al. 2019). including a broad class known as "hammers." which
leverage powerful automated theorem provers (ATPs) determine useful premises (Paulson and Blanchette| 2012 Gauthier and Kaliszyk 2015 Kaliszyk and Urban 2015a Czajka and Kaliszyk 2018). One such tool, Sledgehammer (SH) (Paulson and Blanchette] 2012), has gained prominence
Isabelle (Paulson [193)). where it helped to create a significant portion of Isabelle's ' proof corpus. Hammers are not yet available in all proof assistants (Ebner 2020); implementing them is challenging due to the complex techniques required for different logics and type systems. There is need for an effective premise selection tool that requires less adaptation to work for different proof assistants.
In this study, we provide generic, data-driven, transformer- selection tool: Magnushammer. It constitutes a novel way to tackle the premise selection task, effective while requiring little domain-specifht knowledge. Magmushammer is trained contrastively to perform premise retrieval in two stages: in the SELECT stage, retrieves the most relevant 1024 premises (measured by the cosine similarity of their embeddings to that of the current proof state) from tens of thousands (the database contains 433K premises in total and typically 30K-50K are available in each proof state); in the RERANK stage, the retrieved premises state-aware scores: tokens of the proof state directly attend to tokens of the premise, giving a more contextualized relevance score. An overview of Magnushammer's architecture is shown in Figure 2b
(Vaswani et al. 2017) premise
re-ranked with proof-
Magnushammer can prove 59.5% of the theorems on the PISA benchmark (Jiang et al. 2021).
substantial improvement over Sledgehammer's 38.3%. We demonstrate that this dominance is consistent with varying controlled compute budgets, shown in Figure Furthermore, we replace the premise selection component (Sledgehammer) in neural-symbolic model Thor (Jiang et al.) 2022a) with Magnushammer and improve the state-of-the-art proof success rate on PISA from 57% to 71%.
To train Magnushammer, we extracted a premise selection dataset from the Isabelle theorem prover and its human proof libraries. The dataset consists of 4.4M premise selection instances, with 433K unique premises. To the best of our knowledge. this is the largest open-sourced premise selection dataset, and the first one of this kind for Isabelle. We find Magnushammer to be data efficient, outperforming Sledgehammer with only 4K training examples (0.1% of the training data available). The main contributions of this work are the following:
We propose the use of transformers trained contrastively as novel way of addressing the premise selection problem. Our method, Magnushammer, achieves a 39.5% proof rate on the PISA benchmark, significantly improving the 38.3% proof rate of Sledgehammer, the most powerful general-purpose automation tool for Isabelle.
We extract and open source the largest, to the best of our knowledge, premise selection dataset. It consists of 4.4M premise selection examples and 433K unique premises.
We analyze how Magnushammer's 's performance depends the model size, dataset size, and the inference-time compute budget. We show its superiority with moderate resources.
2 BACKGROUND: PROOF ASSISTANTS, ISABELLE, AND SLEDGEHAMMER
Proof assistants (aka interactive theorem provers, or ITPs) such as Isabelle (Paulson 1993). Lean (de Moura al. 2015), Coq (Bertot, 2008), HOL Light (Harrison) 1996), Mizar (Grabowski
jet 20.10, are software tools designed to assist the development of formal proofs. They provide expressive language for the formalization of mathematical statements and proofs while verifying them formally. In Isabelle, theorems are proved sequentially: an initial proof state is obtained after the theorem is stated, and the proof state changes when the user provides a valid proof step (see Appendix A. for an example). Proof states contain information about the already established facts and the remaining goals to prove. Proof steps consist of tactics, which are optionally parametrized by premises. Tactics are theorem-proving procedures and can complete some proofs in one step provided with relevant premises. However, finding these premises is difficult: one needs to select a handful of relevant facts from the current proof context, which typically contains tens of thousands of them.
Sledgehammer (Paulson and Blanchette, 2012 Blanchette et al., 2013) is a powerful automated reasoning tool for Isabelle. It belongs a broader class of tools known as "hammers," which integrate automated theorem provers (ATPs) into proof assistants. The goal of these tools is to support the process of finding and applying proof methods. Sledgehammer has become indispensable tool for Isabelle practitioners (Paulson and Blanchette| (2012). )). It allows for closing low-level gaps between subsequent high-level steps of proof without the need memorize entire lemma libraries.
2

---

Published as a conference paper at ICLR 2024
Ordered (SELECT)
Ordered [RERANK]
Sledgehammer
Textual representation top promises
Relevance filter
Cosine Similarity
Sigmoid
Proof State Embedding
Translation to appropriate logics
Embodding
ECT Premise
SELECT Projection
RERANK Projection
SPASS
Vamppre
Z3
CVC4
Oteer ATPs
Projectoon
Transformer Backbone
Traneformer Backbone
Tranaformer Backbone
proof
proof
proof
proof
proof
proof
Reconstruction in Isabelle (only for successful proofs)
Proof State Premise
(a) A call to Sledgchammer triggers the following sequence of steps: First, available facts are filtered based on their similarity to the conjecture. Then, the conjecture together with the selected facts (usually a few hundred number) are translated to simpler logic used by the external provers (E, SPASS, etc.). Then, such problems are fed into each ATP sepa- rately. Finally, the premises used in the successful ATP proofs are used reconstruct proof inside Isabelle using its native methods.
Available Promises
Proof State
(b) Given proof state, we first retrieve the relevant premises according to cosine similar- ity of their embeddings with the proof state embed- ding (SELECT). We then re-rank these with a model that encodes each proof state and premise pair, out- putting a relevance score (RERANK). The bulk of the architecture a shared transformer model, in orange.
Figure 2: Overview of Sledgehammer (a) and Magnushammer (b).
Sledgehammer is designed to first pre-select a number of relevant facts heuristically, translate them together with conjecture to simpler logic, and try to prove the conjecture using strong, external ATPs like E (Schulz) 2004), SPASS (Weidenbach) 2001). Vampire (Kovács and Voronkov] 2013). Z3 (de Moura and B Borner 2008), evc5 (Barbosa al. 2022). If successful, these provers generate complete proofs. They are, however, not trusted by Isabelle. Instead, the facts used in the external proofs are extracted and used to produce proof inside Isabelle using its native methods. Up to this last step, known as proof reconstruction, Sledgehammer is essentially used as a precise premise selection tool. See Figure 2a depicting the whole process.
While immensely useful, Sledgehammer comes with several limitations. First, increasing compu- tational power for Sledgehammer brings quickly diminishing returns (Böhme and Nipkow 2010). Second, the logic projection and proof reconstruction in hammer are not straightforward for type systems other than higher-order logic (Czajka and Kaliszyk 2018). Finally, Sledgehammer performance hinges on the relevance filtering scheme, a suite of methods based on handcrafted heuristies (Meng and Paulson 2009) or classical machine learning (Kühlwein et al., 2013). Such approaches are unlikely to efficienlly utilize the constantly growing body of proof data.
We argue that all these limitations can be overcome with deep-learning- beased approaches. Neural networks have shown remarkable effectiveness in end-to-end problem solving with little no feature engineering (Krizhevsky et al. 2012 Brown al. 2020). Adopting textual representations with generic neural solutions removes the need for logic projection, ATP solving, and proof reconstruction. Moreover, large language models have recently displayed impressive scaling properties with respect to both model size (Kaplan et al. 2020 and data (Hoffmann et al. 2022)
3 MAGNUSHAMMER
The goal of premise selection is to find relevant mathematical facts for given proof state. We focus on selecting premises with a neural model informed by their textual representations instead of relying on fact structures like Sledgehammer (see Section 2. The core idea of Magnushammer is to combine fast retrieval based on representational similarity (SELECT) with a more accurate re-ranking (RERank), outlined in Algorithm[] Our method closely follows those Nogueira and Cho (2019) and Izacard et al. (202I). This hierarchical approach is scalable to large formal libraries containing hundreds of thousands of facts. Below describe the two-stage Magnushammer approach.
3

---

Published as a conference paper at ICLR 2024
SELECT leverages representation similarity and is based on Datch-contrastive learning similar to the methods Alemi et al. (2016). Bansal et al. (2019). Han et al. (202I). or Radford et al. (2021). SELECT embeds premises and proof states into common latent space and uses cosine similarity to determine their relevance. During inference, it requires only one pass of a neural network to compute the proof state embedding and dot product with cached premise embeddings. SELECT is hence fast and scalable to large sets of premises. In our experiments, there are between 30K and 50K premises in typical proof state context, from which we select Kg 1024 most relevant ones.
RERANK scores the relevance of the Ks selected premises for the current proof state by analyzing the (proof_state, _state, premise) pairs. RERANK trained output the probability of the premise se being relevant to the proof state. The Ks premises retrieved by SELECT are re-ranked with respect to these probabilities, and the final list comprises of the top K R premises (we set KR = K)). Having both the premise and the proof state in a single input allows RERANK to be more accurate. However, at the same time, it is much slower, as each pair must be scored individually.
Algorithm 1 Premise selection with Magnushammer.
Require:
proof state, premises
proof state to retrieve premises for and database of available premises number of premises to retrieve with SELECT and RERANK, respectively SELECT stage starts
Ks, KR
I: state embedding + eeteeddeeddgn (proof state)
2: comissesembeddingg
4- wrt.eebbddinggeppreieee
3: Cache Cache(premi ses (premnisss.mmmmediggg
4: sim_scores = sttate.embeddin premises .ew.eddiiees
5: selected
Ks]]
6: batch-1
RERANK stage starts
7: for premise in selected do
8: batch.append (prooofsstatttteeoeeeeoeeeeeeeee )
9: rerank ssoress <- get www.ere....oreeeaae...eee.eeeeee
10: top- op--prensse selected (argsort rerank KR]] return top pop.premises
Training We train Magnushammer using two alternating tasks: SELECT is trained with modified InfoNCE loss (van den Oord et al. 2018), and RERANK is trained with the standard binary cross- entropy loss. The architecture of Magnushammer shares a transformer backbone with specialized linear projections on top (see Figure 26). The backbone is pre-trained with a language modeling task on the GitHub and arXiv subsets of the Pile dataset (Gao al. (02T). For training, consisting of (proof (proof_state, .state,,tttttt premise) pairs extracted with a procedure described in Section 4
datasets
During SELECT'S training, each batch consists of N proof states, N positive premises (one for each proof state), and additional M negative premises sampled from available facts that are not ground truth premises for any of the selected proof states. This gives N
M negatives per proof state in one batch. We typically use M = 3N, which differs from standard batch-contrastive learning (Radford al. 202T), in which Md and negatives are only the other N premises in the batch RERANK is trained using binary classification objective. For each positive -troof-state, premise) pair in the dataset, we construct 15 negatives from the most likely false positives returned by SELECT. Specifically, all the premises M that are facts that were never used as premise for proof state, are first chosen. Then, the top 1024 of M according to SELECT are selected, and 15 are sampled from them to construct negative training pairs. See Appendix B for complete training details.
Evaluation in Isabelle We outline how premises chosen by Magnushammer are used to prove theorems in Isabelle. Given a proof state, a list of the k most relevant premises P is retrieved. We construct proof steps consisting of a tactic t and subset of premises S C P. Such proof steps are executed in parallel, with timeout of 2 seconds. The evaluation is successful if any of these proof steps completes the proof. For S. we pick the top of P, where i's are consecutive powers of up to 2', or 0 for tactics that do not accept premises. More details, including the set of tactics used, are presented in Appendix D An example a proof with tactics and premises is given in Appendix A..]
Note that the procedure of trying multiple different subsets of premises is commonly applied in the context of automated theorem proving (Urban al., 2008 Kühlwein et al., (2022) and similar to the technique implemented in Sledgehammer (Paulson and Blanchette. 2012). The rationale behind this is that the proof procedures implemented ATPs and high-level ITPs' tactics perform combinatorial search, and providing them with fewer premises to restrict their search space is beneficial.
4

---

Published as a conference paper at ICLR 2024
4 DATASETS
We created and released a comprchensive dataset of textual representations for Isabelle's proof states and premises. To the best of our knowledge, this is the first high-quality dataset of this kind for Isabelle, and also the largest premise selection dataset overall. We used the two largest collections of Isabelle theories to create the dataset: the Archive of Formal Proofs and the Isabelle Standard library
For every proof step in every proof from these collections, we extracted the preceding proof state and the set of premises used in the proof step; this was turned into (proof state, premise) pairs constituting training data points. We call this the HUMAN PROOFS LIBRARY (HPL) dataset. In addition, we used Sledgehammer generate proofs that are different from the human ones by using potentially alternative premises. We refer to this as the SH partition, and its union with HPL constitutes the datasets are given in Table] | Note that MAPL grosses over 4M data points.
PROOFS LIBRARY (MAPL) dataset. Statistics for all these
Below we describe in more detail how data points are extracted from a proof step. An Isabelle's proof aaroof_sttee, _state, proof _step) pairs: proof_statt has the state information, and proof_step is a tactic application that advances the proof. A proof step may use premi ses: the- orems, lemmas, or definitions established previ- ously. Suppose a proof_step contains premises: P1.P2.....PPr We then extract n data points: (proof _sttte p1) pi),..., (proof _state,,t,,.. p.). Ex- ecuting Sledgehammer on the proof proof_state _state may result multiple different synthetic proof _steps, and data points can be extracted from each in the same way (see Appendix A.2 for details).
Table 1: Statistics of MAPL and both its partitions: HPL (coming from proofs) and SH (coming from Sledgehammer generated proofs). The data points are of the form of (proof (proof_state, premise) pairs.
sequence of (proof
Dataset
HPL
SH
MAPL
Data points
1.1M
3.3M
4.4M
Unique proof states
570K
500K
570K
Unique premises
300K
306K
433K
Mining the HPL partition took 10K CPU hours, and mining the SH partition took 150K CPU hours (17 CPU years) on a distributed system.
Our datasets have 2 distinguishing features:
1. The human- originating dataset is augmented by alternatives generated with Sledgehammer, which results in a significantly larger and more diverse dataset. This also decreases the probability of sampling false negatives while training contrastively: a negative example (proof_stated premise) may in fact be positive, but we just have not seen alternative proof using premise. Generating multiple alternative proofs partially remedies this problem.
2. Both proof_states and premi ses represented "high-level" Isabelle's 's text instead of "low-level" logical formalism like, e.g., TPTP (Sutcliffe (201)) used by AAlama et al. (2014). This makes the dataset more suitable for language models, decreases the need for feature engineering, and facilitates cross-proof-assistee pre-training (Conneau and Lample 2019).
5 EXPERIMENTS
We evaluate Magnushammer on the PISA and mini theorem proving benchmarks using proof success rate metric. Our main result is that Magnushammer outperforms Sledgehammer by large margin and, combined with Thor (Jiang et al. 2022a), sets new state of the art on the PISA A benchmark (71.0% from 57.0%). Through ablations, study the effectiveness of Magnushammer and the contribution its components. Additional results and details can be found in Appendix
5.1 EXPERIMENTAL DETAILS
Benchmarks For evaluation, we use PISA JTang et al. 2021) and miniF2F (Zheng et al. 2022 benchmarks. PISA contains problems randomly selected from the Archive Formal Proofs we use the same 1000 problems Jiang et al. (2022a) for our evaluations. miniF2F consists of 488 high-school competition-level problems, split into validation and test set, each with 244 problems.
attps:/ //twgggngggacccccccco co/ asett /wwmimiiiiiieeeeeeeeeeeeeie wwwp:/eeeeeeeeeeeeeeeeeeeeeeeeee selecctioninn.iiiiii.ieee When training on data from the Archive of Formal Proofs, remove the subset of appearing in PISA
5

---

Published as a conference paper at ICLR 2024
Table Proof rates on the PISA benchmark. On the single-step task, Magnushammer outperforms both Sledgehammer and BM25 by wide margin. On the multi-step task, Magnushammer combined with Thor achieves the state-of-the-an proof rate of 71.0%.
Task
Method
Proof (%)
BM25
30.6
TF-IDF
31.8
Single-step
OpenAl embed. NNcllkantan al. 2022 Sledgehammer
36.1
38.3
Magnushammer (ours)
59,5
LISA
Jiang et al.
2021
33.2
Multi-step
Thor Jiang al.
2022a
57.0
Thor Magnushammer (ours)
71.0
Table 3: Proof rates on the miniF2F benchmark. the single-step task, Magnushammer outperforms
Sledgehammer and its variant with additional heuristics (Jiang et al. (002b)). On the multi-step task, Thoor-Manushammerr obtains competitive results, significantly outperforming Slodeeeedgee.mmrr
Task
Method
Valid (%)
Test
Sledgehammer
9.9
10.4
Single-step
Sledgehammer + hcuristics
18.0
20.9
Magnushammer (ours)
33.6
34.0
Thor Sledgchammer (Jiang et al. 2022a)
28.3
29.9
Multi-step
Thor + Sledgchammer + auto (Wu ct al. 2022a
37.3
35.2
Thor Magnushammer (ours)
36.9
37.3
DSP (Jang et al. 2022b
43.9
39.3
Metric and evaluation setups To evaluate the performance, we measure proof success rate: the percentage of successful proof'. A proof is successful if it is formally verified by Isabelle. We distinguish single-step and multi-step settings. In the single-step setting, we check if the theorem can be proven in step by applying premises retrieved by the evaluated premise selection method (e.g.. Magnushammer). In the multi-step scenario, we perform proof search using a language model following Thor (Jiang al., 2022a). Thor Magnushammer uses Magnushammer instead of Sledgehammer as the premise selection component. A further explanation is given in Section 5.2
Evaluation protocol and computational budget Algorithm 3 (in Appendix D) details the evaluation of Magnushammer in the single-step setting. It generates 17 x | proof steps by combining each tactic E T with top & premises from ranking provided by Magnushammer, where 'I is prescribed set of tactics, A E K, and K a list of integers. Such constructed proof steps are then executed in Isabelle. We define the computational budget for such an evaluation as C T |K] T. where 7' is a timeout expressed in seconds (we use T' = 2 S as we observed little benefit from increasing it). Estimating the computational budget for Sledgehammer is difficult due its complex internal architecture. We approximate it by C = S x T, where S is the 'number of CPU cores' (corresponding to steps executed parallel) and T is the timeout. We use See Appendix A.4 for more details.
for our calculations.
Architecture and training details For our main experiments, we pre-train standard decoder- only transformer models with 38M and 86M non-embedding parameters and fine-tune them for downstream tasks of premise selection or proof step generation. Full details are given in Appendix C In our experiments, we use the Portal-to-ISAbllle API (Jiang et al. 2021) to interact with Isabelle.
5.2 RESULTS PISA AND MINIF2F BENCHMARKS
Our main empirical results, summarized in Table and Table 3 were obtained with the 86M parameter model. Figure and Section 5.2.1 deepen this study, showing that Magnushammer outperforms Sledgehammer across broad spectrum of computational budgets.
Performance the single-step task In the single-step setting, Magnushammer outperforms Sledgehammer by a wide margin on both PISA (59.5% vs. 38.3%) and miniF2F (34.0% vs. 20.9%). Additionally, PISA, Magnushammer outperforms TF-IDF and BM25: text-based, non-trainable

---

Published as a conference paper at ICLR 2024
retrieval methods (Robertson and Zaragoza 2009) which strong baselines in common retrieval benchmarks (Thakur et al. (021). This suggests that Magnushammer able to learn more than just superficial text similarity. In all these experiments used the same evaluation protocol (following
Algorithm 3 and computational budget of 1000 as detailed in Appendix D..
Interestingly, retrieval based on the generic OpenAl embeddings (Neelakantan al. 2022 (specifi- cally: -iw-eembbddiingdd---000 yields reasonable performance comparable to Sledgehammer. This confirms the potential of neural premise selection to replace traditional symbolic methods. There is, however, a large gap to match Magnushammer. This shows that contrastive fine-tuning on our dataset provides non-trive non-trivial gains and supports our hypothesis that Magnushammer learns more than just mere textual similarity exploited by the general purpose method.
Performance on the multi-step task Neural theorem provers utilize language models to generate proof steps, following the approach proposed by Polu and Sutskever (2020). This allows for the creation of more complex, multi-step proof'. The proof generation involves sampling proof step from the language model, verifying it, and repeating this process until the proof is closed or the computational budget is exceeded. The best-first search algorithm is often used to explore the most promising proof steps.
Thor (Jiang al., 2022a) augments neural theorem provers with premise-selection capabilities. To this end, Thor allows the model to generate proof steps using Sledgehammer, which we replace with Magnushammer (see Appendix D.2 for details). Thor + Magnushammer establishes new state of the art on the PISA benchmark (71.0% vs. 57.0%). On miniF2F, our method also significantly out- performs Thor and achieves results competitive with the current state of the art. In these experiments, we give Magnushammer computational budget of 200.
important to note that other theorem- proving approaches in the multi-step section of Table require much larger language models: for Thor it is 700M non-embedding parameters; DSP (Draft, Sketch, and Prove) by Jiang et al. (2022b) uses Minerva model ([eekowyez et al., 2022) with 62B parameters. Moreover, these other approaches rely on ideas orthogonal to premise selection. Specificallyy Thor + auto (Wu et al. 2022a) proposes a variation of Thor, involving expert iteration on auto- fottalfomalized data. DSP involves creating a high-level outline of a proof and uses Sledgehammer to solve the low-level subproblems. We hypothesize that both methods would perform even better when combined with Magnushammer.
5.2. SCALING COMPUTATIONAL BUDGET
In this section, we discuss how the quality of premise selection methods varies with the computational budget available during evaluation. Figure T shows the results, and the definition of the compute budget is provided Section 5.T Notably, Magnushammer outperforms Sledgehammer even with very limited computational resources, and it scales well, particularly within the medium budget range.
For Magnushammer and BM25, we use Algorithm 3 (Appendix DD in various configurations (i.e., settings of T and K). We start with one tactic, T {smt}, J. and K [27], which yields C' = 2 (recall that T = 2 s). We then gradually add more tactics to T and more values to K. The final setup uses T 36 and K containing all powers of 2, from 20 up to 2 which yields C' = 800. The details are provided in Appendix D For Sledgehammer, we scale the timeout parameter T up to 80 s.
5.3 IMPACT OF TRAINING DATA
We study how the amount and type of data impact the proof success rate by comparing HPL and MAPL datasets. For this comparison, we used models with 38M non-embedding parameters and computational budget of 800.
Dataset size Our method is data-efficient: see Figure 3a We observe that Magnushammer fine-tuned on only 0.1% of MAPL- equivalent to approximately 4K samples - is already able to outperform Sledgehammer. This indicates that when starting from pre-trained model, Magnushammer is promising approach for addressing premise selection in theorem- theorem-proving environments with limited training data. The effect of pre- trainiiinng diminishes as the amount of training data increases.
Dataset type Fine-tuning on MAPL or HPL leads to subtle differences (56.3% vs. 54.0% when the whole datasets are used). This outcome may be attributed to the impact of model pre-training and the fact that the HPL dataset is rich enough to obtain good performance on the PISA benchmark (as observed in the previous paragraph). We speculate that the bigger MAPL dataset might be essential for future harder benchmarks and scaling up the model size.
7

---

Published as a conference paper at ICLR 2024
57.5
X
55.0
50
Proof Rate (%)
52.5
40
50.0
47.5
30
Progf
MH MAFL trainzd HPL
20
MH-APP
42.5
Pre trained pre-raaned
Skidgehammrr
40.0
Siddgehammer
10
37.5
0.1%
1%
10%
100%
10f
10 #Parameters
10a
Training Dataset Fraction
(a) We randomly sample fractions of MAPL or HPL datasets and them for training Magnushammer.
(b) We train Magnushammer of different sizes. Even with one-layer transformer, Magnushammer outper- forms Sledgehammer. We observe consistent perfor- mance gains with increasing model sizes. Pre-trained models perform better. See Table for numerical data.
Even 0.1% of the MAPL dataset allows pre-trained
Magnushammer to outperform Sledgehammer and BM25 baselines. See Table for numerical data.
Figure 3: Impacts of the training data quantity and the model parameters on the proof rate. The vertical axis is the proof rate in percentage. In Subfigure [3a the horizontal axis is the fraction of training dataset used and Subfigure 3blit the number of parameters in the model.
5.4 ABLATIONS
We use models trained on the MAPL dataset and evaluate them with a computational budget of 800. To study how the performance our method depends on the model size, we vary the number of layers L and embedding dimension D. A positive correlation between the model size and the proof rate is shown in Figure 3b We observe that even tiny model with 920K parameters (L = D 256) outperforms Sledgehammer (40.7% vs. 38.3%). We also note the benefit of pre-training and that scaling number layers is more beneficial than scaling the embedding dimension. The details The impact of re-ranking is studied in Appendix C.5
can be found in Appendix C.I
RELATED WORK
Premise selection becomes crucial task whenever proving theorems automatically within large formal library. Moreover, this task has several unique aspects that are challenging from the perspective of learning- baasid approaches. Therefore, there exist multiple works that tackle learning premise selection (either explicitly or implicitly) applying various methods focusing on different aspects.
Many works employ classical machine learning like Bayesian and kernel methods (Kühlwein et al.
2012
Alama et al. 2014), J--N (Blanchette et al. 2016), or decision trees (Piotrowski and Urban
Nagashima and He 2018 Piotrowski al. (023). The common weakness of these approaches is the necessity of using hand-engineered features, whereas faster, simpler training is an advantage.
2018
Alemi et al. (2016) were the first apply deep learning premise selection, thus dispensing with the hand-designed features completely. Their approach was evaluated in an automated theorem proving setting and not proof assistant, is Magnushammer. They also implicitly learn embeddings of conjectures and premises, which are concatenated and passed through shallow network, whereas the training signal comes from the logistic loss. In contrast, Magnushammer demonstrated the strength of training with the contrastive loss, where the obtained embeddings just need to be passed through simple cosine similarity measure to provide high-quality rankings.
Most of the methods explicitly targeting the premise selection problem (including this work) retrieve a ranking of independently treated premises. contrast, Piotrowski and Urban (2020) aimed at modelling the implicit dependencies between the premises and used LSTM- -Ssed language models to produce structured sequences of premises. However, the premises were treated there as opaque tokens, not giving the neural model the ability inspect the statements of the premises.
Effective deep learning approaches often leverage the explicit structure of mathematical expressions using graph neural networks (Wang et al. 2017; 7 Paliwal et al. 2020 Goertzel et al. 2022). Our work uses the transformer architecture VVaswani et al. 2017). which is highly scalable and capable of producing powerful representations of raw text data.
8

---

Published as a conference paper at ICLR 2024
Pre-trained transformer language models have been applied to various aspects of theorem proving
including autoformalization [Wu et al. 2022a Jiang et al., 2022b), conjecturing (Urban and Jakubuv 2020), and tactic prediction / proof step search Yang and Deng 2019 Polu and Sutskever [0200] Han
et al.) 2022: Lample et al. 2022 Polu et al. 2023). The works from the last category often implicitly deal with premise selection by treating premises names / tokens he generated and not inspecting their statements. The application of generative language models to statement-aware premise selection has been limited, as the length of the possible premises often greatly exceeds the context of several thousand tokens that the models are designed to handle. Thor (Jiang et al.) (022aa) circumvents the difficulty of premise selection by invoking Sledgehammer. In contrast, Magnushammer retrieves rather than generates to overcome the context length limitation. Therefore it can be used in tandem with other models (its combination with Thor is demonstrated in Section 5
Batch-contrastive learning is widely used in speech (van den Oord et al. 2018), text (Izacard et al. 202T), image (Chen et al,, 2020) and image-text (Radford et al. 2021 representation learning. These methods have proven effective despite the possibility of false negatives occurring in contrastive batches (Robinson et al. 202T). The SELECT phase of our premise selection model relies on in-batch negative examples tram the retriever, similar to HOList (Bansal et al. 2019) and Contriever (Izacard eet al. (021]. Like HOList, we mine additional negatives, which we found crucial for performance. The RERANK stage closely resembles (Nogueira and Cho (019)) but instead of using BM25, we jointly train retrieval and re-ranking, utilizing premises retrieved by SELECT as hard negatives for RERANK training. Han al. (202T) use contrastive learning in informal premise selection. Concurrently to our work, Yang et al. (2023) develop a premise selection method for Lean also using contrastive learning in a way similar to our SELECT method, but without the RERANK stage.
There are multiple lines of work considering datasets based on formal theorem proving. These include benchmarks like ProofNet (Azerbayev et al. 2022) for Lean, and miniF2F (Zhngg al., 2022) that supports multiple ITPs. These datasets only focus on evaluation, not providing data for training the models. Another line of research focuses on benchmarking machine learning models' reasoning
capabilities while also providing training data (Bansal et al., 2019 Li et al.
[021 Han et al. 2022).
Existing public datasets for premise selection include the ones introduced in (Alama et al. 2014
Piotrowski and Urban 2020). In comparison to these works, we publish the data in high-level, textual format, as seen in Isabelle, instead of low-level, structured languages such as TPTP SStcliffee 2017).
There exists rich body of work developing complex hammers systems for different proof assistants (Paulson and Blanchette| [012] Kaliszyk and Urban, 2015a; Gauthier and Kaliszyk, [205)] Czajka and Kaliszyk| 2018). Unlike the traditional hammers, method does not depend on external ATPs and requires little domain-specific knowledge.
7 LIMITATIONS AND FUTURE WORK
Other proof assistants Magnushammer treats proof states and premises as text and makes no assumptions about their structure. As such, no feature engineering is needed to apply it to other proof assistants. We conjecture that Magnushammer can prove effective in other environments because it is agnostic to the logic or type system used. We plan to evaluate Magnushammer in Lean proof assistant on ProofNet (Azerbayev et al. (2022) and miniF2F (Zheng et al. (022) benchmarks, using the recently published LeanDojo toolkit (Yang et al. 2023) that also provides baselines for comparison.
Richer proof and premise representations Magnushammer utilizes the textual representation of the proof state given by Isabelle. This representation, however, does not provide complete semantic information about the referenced objects. Including function definitions and object types in the proof state representation might further improve performance.
Modelling full proof steps Combining language models with external premise selection tools significantly improves their secorrem-pooving performance, as demonstrated by Jiang et al. (2022a) and our work. A natural step would be to further integrate premise selection with language models into a single model capable of generating proof steps containing relevant retrieved premises. A proof of concept of this idea was explored by Tworkowski et al. (2022). This would also allow to model existing implicit dependencies between returned premises, which was shown beneficial by Piotrowski language models (Wu et al. 2022bb Borgeaud al. 2022 could facilitate progress in this direction.
and Urban (2020). We believe that recent ad advances in eetrieval-augment

---

Published as a conference paper at ICLR 2024
ACKNOWLEDGEMENTS
We gratefully acknowledge that our research was supported with Cloud TPUs from Google's TPU Research Cloud (TRC). Moreover, Piotr Miloš was supported by the Polish National Science Centre grant 2019/5/00/S66004444.
REPRODUCIBILIIT STATEMENT
The data that were used for pre-training of the backbone transformer model Magnushammer are freely available under this link:
The Isabelle data used in training for the down-stream tasks are available under this link:
http:////pppprieisssseseettteote selection in
isabe 11e
The benchmarks used for evaluation of Magnushammer are freely available on GitHub:
miniF2F:
PISA also implements the interface for interacting with Isabelle that we used our experiments.
specifies the setup of Sledgehammer that we used in comparisons. Appendices Band detail the shape of the transformer architecture used, define the loss functions applied in the SELECT and RERANK stages, specify the hyperparameters used in pre-training and training for our down-stream tasks, and disclose the hardware used for training. Appendix details the setup for evaluation of Magnushammer in Isabelle, in particular the list of tactics applied on top of the Magnushammer's premise selection.
Appendix A.4
REFERENCES
Jesse Alama, Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Premise selection for mathematics by corpus analysis and kernel methods. CoRR, abs/1 108.3446, 2011.
Utt.httt:::/axxivvooom
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. Autom. Reason,, 52(2): URL /http::///o// http://oo.org/1.110000
191-213, 2014. doi: 10. 101107/s00117-013-99888 s10817-013- 9286--
Alexander A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, and Josef Urban. Deep- Math - deep sequence models for premise selection. CoRR, Abs/1600.04442, 2016. URL
:ttp:///axiv.orgg/abs..
04442
Zhangir Azerbayev, Bartosz Piotrowski, and Jeremy Avigad. ProofNet: A benchmark for auto- formalizing and formally proving undergraduate-leve mathematics problems. In Advances in Neural Information Processing Systems 35, 2nd MATH-AI Workshop at NeurIPS'22, 2022. URL qithub. io httpp/ppprrs//// pdf
httts::/mathai2000
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. 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 Proceedings of Machine Learning Research, pages
PMLR, 2019. URL
mlr. wttps///.//aaaaalla... hmmm
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, AbdaIrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng. Cesare Tinelli, and Yoni Zohar. cve5: versatile and industrial-strenge 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 Part of the European Joint Conferences Theory and Practice of Software, ETAPS
10

---

Published as a conference paper at ICLR 2024
2022, Mumich, Germany, April 2-7, 2022, Proceedings. Part I, volume 13243 of Lecture Notes in Computer Science, pages 415 442. Springer. 2022. doi: 10. httpss:/doii org.i.org/ii 100110007//90 1007000800077783000 -11777998833-----0 99524-9 24
URL
Yves Bertot. A short presentation of coq. In Otmane Ait Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logies, 2 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: 0001007/978-3-550-700777---
URL
https://dof orr. / 1007 978 3 540 00000-71067- 71067-7_3
Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. J. Autom. Reason, (0(1):10911101011)0 128, 2013. doi:
URL DTt_AA/pp////a....c//0000000///0
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-basse baandd fact selector for Isabellc/HOL.. Autom. Reason., 57())211-244, 2016. doi: 10.
0007//10817-016-9362222 URL https://doi.. http://di..ogr//// www.ooggg/..... 101.1110001010111111111111111111 --6 9362
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 11883--642-12003-1
Sebastian Borgeaud, Arthur Mensch, Jordan Hoffmann, Trevor Cai, Eliza Rutherford, Katie Mil- lican, George van den Driessche, tean-Bapting 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. Im- proving language models by retrieving from trillions fanie 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, vol- ume 162 of Proceedings of Machine Learning Research, pages 2206 PMLR, 2022. URL https:// https:///ppcceedinng. ml prwss/essvvv.. vl 62/ 52/borgeaud22a.hhrg html
tokens. In Kamalika Chaudhuri, Ste-
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-Vone 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, hiss/2005.14165. 2020. URL / arxii..iivv...... org/ abs /20/220055.00 14165
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::t:/proceeeiiiii wwr..pres/aee v chen20j. html
Alexis Conneau and Guillaume Lample. Cross-lingual language model pretraining, In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Bue, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32. Curran Asso- ciates, Inc., 2019. URL https:t/proceeedinnnnn .ewriiiseessppp cctppapeee//11//11eeeeee 30cc99c2c22274b355577aaaaa.
pdf
Lukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for dependent type theory. Autom. Reason,, 61(1-4):423-453, 2018. doi: 10.10077110817--188945554- URL https
Nicolaas Govert De Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. Symposium on automatic demonstration, pages 29-61. Springer, 1970.
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 Heidelherg. ISBN 978-3-540-7880033
11

---

Published as a conference paper at ICLR 2024
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 Middel- dorp, editors, Automated Deduction CADE-25 25th International Conference
Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378 388. Springer, 2015. doi: 10. 00.1077978-3-339-214400 httpss:/doi..on org/ www.///gg/........ 1007/ 3- 319 21401-6 26
URL
Gabriel Ebner. Integration of general-purpose automated theorem provers in Lean, 2020. /tttps://ww.. /wwww andrew. www..cm..... wtt.rrewwc...uuuuueeeeee httm.//e////ee///iig////o/////// htwp:///ggo///mmeeooo////////2/0 Fomm20207
https:
slices/ form Sioner.pdE
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 800G dataset of diverse text for language modeling. CoRR, abs/2101.00027, 2021. URL
https://arxiv.. org/ abs http://.////20000000 00027
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. 10.144526777742269317.. URLttttss: /tw.//o....o///////// wwt.o//g//0.. 45/ 6724. 2693173
Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsá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 LIPles, pages 16:1-16:21. Schloss Dagstuhl Seibniz-Zentrun für Informatik, 2022. doi: 10230//LPlcc..TP.202222
Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in nutshell. Formaliz. Reason,, 3(2): 245, 2010. doi: 10. ww.6092/isse 1972 11w.::n171922-777199999999
URL https::/dda org/
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.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for thcorem proving with language models. In The Tenth International Conference on Learning Representationss ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022.
URL httpttttss//ppeeeeeeeeeeeeee htt.://eeeeeeeeeeeeeeeee/oarrraa 1ttp:/ormm2dddrpxe999494
John Harrison. HOL light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, Formal Methods in Cemputer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1166 of Springer, 1996. doi: 10.1007//F6003188
Lecture Notes in Computer Science, pages wttp://///1111110///00///00
URL
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.488550/axXi.2228.5555 URL https: / /tt:::/dooi.oooo 10. (088550/axxxoo 220..22233322 15556
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 htw.s: //aclaaathoooooc ogy. oot.oorgll... 8 1031/
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/21 12.09118 18, 2021. URL /tl..httss://axxwv....
09118
12

---

Published as a conference paper at ICLR 2024
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.
Albert Q. Jiang. Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóádć, Piotr Mitos, Yuhuai Wu, and Mateja Jammik. 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 formm? id fue0yttt-
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/rxX..2220...55
Cezary Kaliszyk and Josef Urban.
Online ATP service for HOL Light. Math. Comput. Sci., 9(1): 22, 2015a. doi: 10. 10.1007/511786--14401133
Utthttps::/doi..rgg
10.1007/s11786-1111
Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. Journal of Automated Reasoning. 55(3): 245-256, 2015b.
Cezary Kaliszyk, François Chollet, and Christian Szegedy, HolStep: A machine learning dataset for higher-order logic theorem proving. CoRR, abs/l703.00426. 2017. URL http::
orq erq/abs/110 1703. 00426
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 2020. URL
abs/ 2001. 08361
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- 1007
URL
httpps://oi..oo
Alex Krizhevsky, Ilya Sutskever, and Geoffrey E. Hinton. ImageNet classification with deep convolutional neural networks. Peter I.. 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 meeting held December 3-6, 2012, Lake Tahoe, Nevada, United States, pages cctpaper//01////aaeeee.rerer
1106-1114, 2012. URL c399862d3b9dess
hwwpriinnnnnnuuuureerrremm html
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 3928-99--60 Springer. 2012. doi: 10. 00.10079988-3-444
_300 URL
luttps://do/ org 10 1007
642 31365-16--
Daniel Kühhlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. MaSh: Machine learning for Sledgehammer. Sandrine Blazy, Christine Paulin-Mohrinn 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. 978 3- 642-642320 306339-64-2-
6.
Guillaume Lample, Timothee Lacroix, Marie Anne Lachaux, Aurelien 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 fattps://operreiiie net/forum?id=d33e http:/ormmm21ddd4xx888ccaca
13

---

Published as a conference paper at ICLR 2024
Aitor Lewkowycz, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag. Theo Gutman-Son -oloo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative rea- soning problems with language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances in Neural Information Processing Systems, 2022. URL
net -tte//ooooddd---TE--------2 IFXTZERXcM?
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:://ppnreett
net www.fforrriiorreoorroo of
Jia Meng and Lawrence C. Paulson. Lightweight relevance filtering for machine- machine-generated resolution problems. Appl. Log., 7(1):41-57, 2009, doi: 10.1016/j.jo jal .0.0044
Yutaka Nagashima and Yilun He. PaMpeR: Proof Method Recommendation system for Isabelle/HOL, 2018. URttttpss: / arxiv www.orr//aaae abs/ 806.006600 07239
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.
Tobias Nipkow. Fun with functions. Archive of Formal Proofs, August 2008. ISSN 2150-914x. ment.
wtw.:iiithfunniiiinno hhttsttmlmmmm Formal proof develop-
Rodrigo Frassetto Nogueira and Kyunghyun Cho. Passage re-ranking with BERT. CoRR, 11001100115.1..11
0e///901000885 2019. URL http::::/wwxww.rr//..////
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph repre- sentations for higher-order logic and theorem proving. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The
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- 2020, pages 2967- 2974. AAAI Press, 2020. URL htttt::ttp/osat aaai org/ win/x.iddxxx///// whppppppppaaaap /A..:AAAI//AA http/AAAA/rrtiilee. view/5689
Lawrence C. Paulson. Isabelle: The next 700 theorem provers. CoRR, cs.L0/9301106, 1993. URL https://arxiv. org/ abs///////////// cs/ 9301106
Lawrence Charles Paulson and Jasmin Christian Blanchette. Three years of experience with Sledge- hammer, practical link between automatic and interactive theorem provers. In IWIL @LPAR. 2012.
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 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 576. Springer, 2018 doi: 11110079978-3331994400555 9- 22226-536337
33..
:/op:::///o.... org 10.000000000 00t....1100000000
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, vol- ume 73 of EPIC Series in Computing, pages 409-422. EasyChair, 2020. doi: 10.29007//5hd. URL
https://dol 0ttp://....01110..0000000000000. 29007 5hd
Bartosz Piotrowski, Ramon Fernández Mir, and Edward W. Ayers. Machine-learned premise se-
lection 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- 18-21, 2023, Proceedings, volume 14278 of Lecture Notes in Computer Science pages 175-186. Springer. 2023, doi: 10. 10.10009978-3-03--435335
10. URL
https: //do: .rgg 1007 0-1088833331--1------33
14

---

Published as a conference paper at ICLR 2024
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03333 2020. URL http::/tss////.... /ttp//axivvv...////v//..///..av. ozg/ abs/2009, 03393
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. OpenRe- view.net, 2023. URL htt.::tpss:. httppss://ppeeeeiieeeeeee/
net /pdff 7id P 7G 8dmSh4
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, llya Sutskever, et al. Language models are unsupervised multitask learners. OpenAl blog, 1(8):9, 2019.
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, 0///2103.00020/
2021. URLbttpps httths////aziiii //axiiv.aa//i/////aa ozg abs /2103.2113..m 00020
Stephen E. Robertson and Hugo Zaragoza. The probabilistic relevance framework: BM25 and beyond. Found. Trends Inf. Retr., 3(4):333-38, 2009, doi: 10. (0.155//150000001
Joshua David Robinson, Ching- Yao Chuang, Suvrit Sra, and Stefanie Jegelka. Contrastive learn- ing with hard negative samples. 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https:
h //openreview www.:nnttttfodneeooooooo. wiop:nidddddtooooutttt XOQOUTh-
Stephan Schulz. System description: E 0.81. David Basin and Michaël Rusinowitch, editors, Automated Reasoning, pages 223-228, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.
ISBN 978-3-540-22984-88
Jianlin Su, Yu Lu, Shengfeng Pan, Bo Wen, and Yunfeng Liu. Roformer: Enhanced transformer with rotary position embedding. CoRR, abs/2104.09864, 2021. URL ptttpa://arxiv..ot
2104.09861
G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to THO, TPTP v6.4.0. Journal of Automated Reasoning, 5944):483-502 2017.
Terence Tao. Solving mathematical problems: A personal perspective. Oxford University Press, 2010.
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 /
08663
Szymon Tworkowski, Maciej Mikuła, Tomasz Odrzygóžżž, Konrad Czechowski, Szymon Antoniak, Albert Jiang, Christian Szegedy, Lukasz Kuciński, Piotr Milos, and Yuhuai Wu. Formal premise selection with language models. AITP 2022, 2022. hhtt:::/aatp--coffeeeeec.. org/
2022/abst AAITP 202e_paperrr_ppppppppppppappaer2
paper _2cerr___2000 32.pdf
Josef Urban and Jan Jakubuv. 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.1 978-3-030-53518-6, URL httph: /tatts:://oi..oo http:///ooooog/0///// 1007/978 53508-3518--00 6
24
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jifí 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 441-456, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-71070-77
Aäron van den Oord, Yazhe Li, and Oriol Vinyals. Representation learning with contrastive predictive coding. CoRR, abs/1807. 003748, 2018. URL
15

---

Published as a conference paper at ICLR 2024
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/ 2017. URL
http:://rxivv org/ httpg//ab//17..... 03762
Ben Wang and Aran Komatsuzaki. GFT-J-6B: A 6 Billion Parameter Autoregressive Language Model. https://githube com www.coooooiioooo www.nooooooooooooooooooooooooooe mesh Cransformes Jax May 2021.
Mingzhe Wang. Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. CoRR, htss/1009009944 2017. URL http://arxx...xxx//bb/////
09994
Christoph Weidenbach. Combining superposition, sorts and splitting. In John Alan Robinson and Andrei Voronkov, editors, Handbook Automated Reasoning, pages 1965-2013, Elsevier and MIT Press, 2001. doi: 10. 00019/97788004455511335530000000 1016/b978 04445044848 3/50029
URL htttpa://doi.rrre
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 /
Yuhuai Wu, Markus Norman Rabe, DeLesley Hutchins, and Christian Szegedy. Memorizing transformers. In The Tenth International Conference Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022b. URL /
Kaiyu Yang and Jia Deng. Learning 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 1984-6994. PMLR, 2019. URL html
ngs ml wttppppr//////////gg//3339 /
Kaiyu Yang. Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with aetieeel-augmmented language models. CoRR, abs/2306. 15626, 2023. doi: 10.48550/anXiw.2336.5566 URL https
//doi. 48550/ 2306 2306.15626
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: A cross-system benchmark for formal olympiad- mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL httts::/openreviier net httt:/orommood---220g
16

---

Published as a conference paper at ICLR 2024
APPENDIX
A ISABELLE ENVIRONMENT
This section contains visual examples of proofs in Isabelle and provides some configuration details of the environment.
A.1 VISUALIZATION THE ISABELLE ENVIRONMENT
Figure A.1 shows example theorem and its proof, as seen in Isabelle's most popular IDE, jEdit. The theorem comes from an entry to the Archive of Formal Proofs Fun With Functions (Nipkow 2008). It states that any mapping from the set of natural numbers to itself that satisfies [[(()) n 1)
must be the identity function. The proof starts with a simple induction and then refines the result to arrive the thesis. This problem was included in Terence Tao's booklet Solving Mathematical Problems Tao 2010
theorem identityl: fixes "nat = nat" assumes fff: "An. f(f(n)) f(Suc(n))*
shows "f(n) n
proof
fix n have key: "n & m = S f(m)"
(induct n arbitrary: m)
show ?case by simp
next
case (Suc n)
hence "m ş 0" by simp
then obtain
where [simp]: "m Suc k" by (metis noto implies Suc)
have "n < f(k) using Suc by simp
hence *n f(f(k)) using Suc by simp
also have .... < f(m)* using fff by simp
finally show 7case by simp
qed
hence
*An. n S f(n)" " by simp
hence *An. f(n) < f(Suc n)" by(metis fff order less trans)
hence *f(n) n+1" by (metis fff lift suc_mone mono less_ iff[ot f] suc_eq Suc_eq_plusi)
with <n f(n)> show "f n" by arith
qed
Figure A.1: :: An example theorem in Isabelle. The statement is highlighted in the orange frame and the body of the proof is in the green frame. this proof, most of the lines contain two consecutive steps: the first formulates new proposition, and the second proves it. See detailed analysis of the line 8 of the proof in Figure A.2 below.
proot (state)
this:
Suc k
goal (1 subgoal):
1. An m. (Am. n S m = S f m)
Suc
Suc
then obtain where [simp]
"m
Suc k* by (metis
note
implies Suc)
note implies Suc:"n
m
Suc m"
Figure A.2: The line broken down into two steps: the first one (green frame) includes the proposition (since m is natural and positive, it must have predecessor k) and the second (blue frame) proves it using the tactic metis a with premise mp es__uc, that states that a nonnegative natural number is successor of some other natural number. The used premise is fact which is already defined in the lemma library. The proof state resulting from the first step is in the yellow frame. The full premise statement is highlighted in pink.
17

---

Published as a conference paper at ICLR 2024
A.2 ALTERNATIVE PROOF STEP GENERATION WITH SLEDGEHAMMER
This section describes how to generate alternative proof steps using Sledgehammer which we do to obtain datasets described in Section First, we find all intermediate propositions within the proof (they can be nested) and try to replace the proof of the proposition with Sledgehammer step. If successful, we record such step the dataset and proceed with both the original and the alternative proof. Figure A.3 provides visual example of the aforementioned propositions.
proof
have key: "n = S f(m)"
prodf(induct n arbitrary: m)
case show 7case by simp
next
case (Suc n)
hence "m / 0" by simp
then obtain k where [simp]: "m Suc k" by (metis notê Sep__pllle_____ Suc)
have "n S f(K)" using Suc simp
f(f(k))" using Suc by simp also have "... f(m) using fff by simp
hence
finally show 7case by simp
qed }
hence *An. n S f(n)" by simp
hence -An. f(n) fSuc n)" bymmtsis fff order le less trans)
hence [f(n) < n+1" by (metis fff lift Suc mono less iff[of f] Suc eq eq_sllss)
with <n S f(n)s show "f n = n* by arith
Figure A.3: Example intermediate propositions highlighted in red. Note: not all propositions were highlighted.
A.3 EXAMPLE OF A PROOF WITH TACTICS REQUIRING PREMISES
Figure A.4 contains a multi-step proof of the irrationality of v2 written in Isabelle. The proof contains multiple usages of tactics that require premises.
1emma "sqrt Q" proof
"sqrt 2 E Q" then obtain bitint where "sgrt a/b" "coprime b" 0"
by (metis Rats sass_ccses' less irreff)
then have c: "2
b²2""
by (smt (23) of si_iit_ppower power power_divide heal_sqrt_powa
then have "b"2 0" by fastforce
then have *; "2*b"2 a"2"
by (smt (verit, cefv_SIG) eq divide eq numeral(1) mult cancel Barlll_rihhh111 numeral numeral_Bit0 numeral_plus numeralumelllll of int of of_ int power of int L__int_power___ power_oweeepee eq of int cancel iff one plus jameraaum))) then have "even a"
comm comm_ class.distrii
by (amt (z3) even pven_power oddE) then obtain disint where "a-2*e" by blast
with have "b"2 2*a"2" by auto
then have "even b"
by (amt (23) even_power oddB)
with .coprime a b, ceven a reven bi show Palse by fastforce
qed
Figure A.4: proof of /2 & Q (Jiang et al. 2022a Figure 1). The steps containing met i amt, fastforce, blast, auto, fast force examples of steps using premises. For instance, one such proof step is by (metis Rats cases' messiireefl This step invokes metis and provides two premises arguments, namely Rats.cases' and l irrefl.
18

---

Published as a conference paper at ICLR 2024
A.4 SLEDGEHAMMER SETUP
We set up Sledgehammer in Isabelle 2021-1, following the configuration used by Jiang et al. (202a)). We Sledgehammer using different sets of settings and calculate the total proof by taking the union of problems solved by each run. The Sledgehammer timeout is set to default 30 seconds. We use only on-machine automated theorem provers (same as Isabelle environment), so external provers used by Sledgehammer are the following: Z3, SPASS, Vampire, CVC4, and E.
In our calculation of the Sledgehammer computation budget, see Section 5.1 cores." We run our experiments on machines with 96 CPU cores, making the assumption realistic. Moreover, we emphasize that the performance gap between Magnushammer and Sledgehammer large enough that altering the value of S, e.g. to an unrealistic level S = 1, would not qualitatively change conclusions.
assume S 10 'CPU
B DETAILS OF MAGNUSHAMMER
B. SELECT STAGE
SELECT stage is trained using the InfoNCE loss van den Oord et al. (2018) defined as:
exp (s (g, k /T)
C (q, ((, exp (4) /r) + Σ exp (s (g, /T)
where q is a query (a proof state), k4 a positive premise (a ground truth from the dataset), k; are negative premises. We define cosine similarity between proof state and premise embeddings: T 0 is non-trainable temperature parameter. We list our hyperparameter choices in section C.2
B.2 RERANK STAGE
Premise retrieval task can be cast as binary classification, trying determine if given pair (proof state, premise) is relevant. Applying classification to each pair is computationally in- feasible, however, could used to re-rank a small set of premises retrieved by SELECT. Namely, we use the following cross-entropy loss:
-=
Σ log score(p) - Σ log((1 - score(p)))
pEP
P&N
where spore(p) is the output of the RERANK part of the model (see "Sigmoid" in Figure 2b for given p = (proof state, premise) pair. Typically, we sample a batch of 16 positive pairs P from the dataset. For each such pair (proof state, premise) 15 negatives are constructed from the most likely false positives returned by SELECT. Specifically, negative premises M, which are facts that were never used as premise for to SELECT are selected, and 15 are sampled from them to construct negative pairs, which are included in N.
are first chosen. Then, the top 1024 of M according
B.3 MAGNUSHAMMER
We train Magnushammer as two separate tasks alternating update steps as presented in Algorithm Note that the backbone of the architecture is shared between SELECT and RERANK, thus such multi- task training is potentially more effective than having two separate models. Calculation of the negative premises for SELECT is costly, thus for efficiency reasons we recalculate the top 1024 premises, Section B.2, every T = 1000 steps in the recompute sewateeee..aaaaieeeeeaeee rerank function, as outlined in the Algorithm
C TRAINING DETAILS
C.I MODEL ARCHITECTURE
We use a decoder-only transformer architecture, following the setup from Wang and Komatsuzaki (202T) and using rotary position embedding by Su al. (2021), variation of relative positional
19

---

Published as a conference paper at ICLR 2024
Algorithm 2 Magnushammer training.
Require:
initial trainable parameters
D
premise dataset
T
> interval for updating rerank dataset
1: Dersak recompute negatives for rerank(0, D)
2: step =
3: while step < num_ num_train_stereeeeeeeeeeeemeeeep do
4: batch.select <- D.sample()
5: 0 train_step(() batch.select)
6:
batch.rerank <- D rerank sample()
7:
f- train_step( ( rerank)
8:
step < step +
9:
if step mod T then
10:
Drarank +- recompptteeaaggtivvvss.orror...t D)
encoding. The feedforward dimension in the transformer block is set to 4 x D where D denotes embedding dimension, and the number attention heads H D/64. Our 38M model has L, = 12 layers and an embedding dimension of D 512. The larger 86M model consists of L 12 layers and has 768. For all the models, we use the original GPT-2 tokenizer (Radford et al. 2019).
In SELECT, append specialized token at the end of the sequence compute the embedding for a proof state and linearly project its embedding. Premises are embedded analogously. Similarly to Radford et al. (202T) that train separate projections for images and captions, we train separate proof state and premise projections and share the transformer backbone (see Figure 2bb.. Analogously for RERANK, we compute the relevance score by taking the embedding of the last token and then projecting it to a scalar value.
C.2 HYPERPARAMETER SETUP
We performed the following hyperparameter sweeps. We note that have not observed significant differences between obtained results.
Learning rate: (1c-4, 2c-4, 30 4, 5c-4), 4), chosen: 20-4
Dropout: {0.0, 0.05, 0.1, 0.2). chosen: 0.1
Weight decay: (0.02, 0.05, 0.1}, chosen: 0.02
Batch size N in SELECT: {128, 256, 512), chosen: 256
Number of negatives in SELECT: {0, 256, 768, 1536), chosen: 768
Temperature for InfoNCE loss in SELECT: (0.05, 0.07, 1), chosen: 0.07
Batch size for RERANK: {16, 32, 64), chosen 64
Number of negatives per proof state M in RERANK: 17, chosen: 15.
C.3 PRE-TRAINING ON LANGUAGE MODELING
Pre-training has been shown to dramatically increase the capabilities and performance of decoder-only models on tasks other than language modeling (Howard and Ruder] 2018). Motivated by that, we pre-train our models on GitHub and arXiv subsets of the Pile (Gao et al. 2021). The models are trained for 1M steps, with a context length of 2048. Global batch size is set to 32 sequences giving a total number of 65536 tokens per batch. Dropout is disabled, and weight decay is set to 0.02. The learning rate increases linearly from 0 to 0.0003 for the first 10000 steps, and then the cosine schedule is applied to decrease its value gradually.
C.4 FINE-TUNING FOR DOWNSTREAM TASKS
We train Magnushammer by taking a pre-trained language model, removing its language modeling head, and attaching three linear projections heads one projection for proof state embedding. another
20

---

Published as a conference paper at ICLR 2024
one for premise embedding, and the last one for producing relevance score for RERANK, depicted in Figure 2b and described in Section [.I] For the proof step generation task, we fine-tune our language models by applying the algorithm used to train Thor (Jaag et al. 2022a).
C.5 IMPACT OF RE- RE-RANKING
We find that the SELECT-only method, i.e., Magnushammer without the RERANK phase, already significantly outperforms Sledgehammer, Tested the 38M model, it achieves 54.2% proof rate comparable to 56.3% obtained by Magnushammer. SELECT-only mode is computationally appealing alternative, as it only needs a single forward pass embed the current proof state (the setting used recently by Yang et al. (203).) Premise embeddings can be pre-computed and cached, allowing inference on the CPU without the need for GPU TPU accelerators.
C.6 HARDWARE
We gratefully acknowledge that our research was supported with Cloud TPUs from Google's TPU Research Cloud (TRC). We use TPU virtual machines from the Google Cloud Platform (GCP) for all stages: pre-training. fine-tuning, and evaluation. Each TPU virtual machine has TPU v3 cores, 96 CPU cores, and over 300GB of RAM. TPU v3 cores have around 16GB of memory each. The Isabelle environment is set to have access to 32 CPU cores.
D MAGNUSHAMMER EVALUATION
In Algorithm 3 we outline our evaluation method described in Section 5.1 To generate proof steps, we use the following tactics: smt, metis, auto, simp, blast, meson, force, eval, presburger. 1 linarith. Algorithm is also used to evaluate BM25, where we select top.premises with this retrieval method instead of Magnushammer.
D.1 COMPUTATIONAL BUDGET
For our main result (Section 5.2 allocate the computational budget of 1000 follows: apart from the powers of two from 2 to 200 we also try the following values: [48, 96, 192]. which in total gives 14 values. With each of these values, 36 tactics are used with timeout T = 2, yielding C' a 1000.
For the ablation studies, only powers of two from 2 to 210 and the same of 36 tactics, which gives C' x 800.
Algorithm 3 Magnushammer evaluation in ITP environment.
Require:
> theorem to prove Magnushammer's premise selection model > number of premises to retrieve with SELECT number of premises retrieve with RERANK D> available premises list with the number of top premises generate steps with list of tactics to generate steps with ITP environment (e.g.. Isabelle) initialize problem 2: top-premises + prensel.modeel _attte,,tteeeeee premises, Ks, Kn) get top premises generate proof steps combining of tactics and top k premises
theorem
premsel model
Ks
KR
premises
top k. top.k.prentt
www.ppemmessttt..mmm to.trr tactics.to.try
env
1: proof troof_state- state init ietiiinniiniiiieec problem(eny. theorem)
3: steps=
4: for in top.k..rreisse..oo.trr do
5: top k premises +- top premises(: k]
6: new new.steps +- generate steps steps(tactics to try, top k premises)
7: steps.extenddnew.stee
8: solved +- pry-steps(env, steps) & evaluate generated proof steps in the ITP's environment
9: return solved
21

---

Published as a conference paper at ICLR 2024
D.2 THOR MAGNUSHAMMER
To generate more complex proofs we combine Thor (Jiang et al. 2022a) with Magnushammer as introduced in multi-step setting in Section 5.2
Firsdly, we follow the procedure described in Jiang et al. (022a)) to pre-process training data and fine- tune our pre pre-traie ree-trained language model for the proof generation task (pre-training details can be found in Appendix C.3). During the evaluation, when the language model generates the <hammer> token, call method instead of Sledgehammer. More specifically, we use augmented Algorithm| that returns the proof states resulting from applying the steps (instead of returning binary information on whether any of the steps closed the proof). We then pick at most states among these and add them to the BFS queue.
We assign the same computational budget as proposed in Thor, with the only difference being that each proof_ster f-step has timeout limit of 2 s (instead of 10 s), which we found to perform better in our setup. The search is terminated if and only if one of the following scenarios happens: (1) valid proof has been found for the theorem; (2) the language model is queried 300 times; (3) wall- timeout of 500 has been reached (assuming parallel execution of Magnushammer steps); (4) the queue is empty but the theorem is not proved. We keep the same maximum length of the queue equal to 32.
E ADDITIONAL EXPERIMENTAL RESULTS
E.1 SUPPLEMENTAL DETAILS
We provide additional details for our main experiments and ablations.
Table 4: Relation between the training data and the proof rate discussed in Section 5.3 and Figure 3a
Dataset
Fraction
Pre-trained
Proof rate (%)
MAPL 0.1%
Yes
39.2
HPL
0.1%
Yes
34.9
MAPL
0.1%
No
16.8
MAPL
1%
Yes
47.7
HPL
1%
Yes
42.7
MAPL
1%
No
29.0
MAPL
10%
Yes
53.2
HPL
10%
Yes
49.4
MAPL
10%
No
48.5
MAPL
100%
Yes
56.3
HPL
100%
Yes
54.0
MAPL
100%
No
53.0
E.2 STEP TACTIC PROMPT
We observed that different tactics use different subsets of premises. This motivated us to extend the context given to our model with tactic prompt. Namely, provide the tactic name as an additional argument to the premise selection model, similarly to Bansal et al. (2019). Prompting model with the tactic name does not yield significant improvements. However, it allows the model for a more accurate premise selection. Namely, as presented in Figure and and Table observe that premises necessary to close the proof are ranked higher. This motivates an alternative performance metric presented in the next section.
22

---

Published as a conference paper at ICLR 2024
Table Proof rate PISA for different models discussed in Section 5.4 and Figure 3b
We vary the
number of layers L and the embedding dimension D of the Transformer model.
Transformer (L, D)
#Parameters
Pre-trained
Proof rate (%)
(1, 256)
920K
No
40.7
(1,
3.7M
No
43.9
(2, 256)
1.7M
No
47.0
(22
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,
38.3M
No
52.6
(12, 512)
38.3M
Yes
56.3
(12, 768)
86.2M
Yes
57.0
60
55
50
Proof Rate (%)
45
40
35
30
25
Tactic Dependent
20
Tactic
15
16 32
64
128
256
Number of premises tried
Figure A.5: We calculate accumulated proof rate in the following way: try premise, count problems solved, then try 2 premises, count problems solved using or 2 premises, then try 4 premises, count problems solved using 1, 2, or premises etc. Following this, on the x-axis we have the number of premises used to generate steps in Algorithm 3 The y-axis presents the accumulative proof rate as we try more and more premises. The higher the proof rate for the smaller number premises used the better. We observe that prompting the model with the tactic is not necessary to achieve the final high proof. However, allows the model for more accurate premise selection all premises necessary to close the proof are ranked higher.
Table 6: Effect of the number of premises used for generating tactic steps the proof rate. We fix set of tactics and accumulate problems solved as we increase the number of premises used to generate steps in Algorithm 3 Namely, for each kt we count the number of problems solved using most k premises. The "Tactic" column indicates whether the model was given a tactic prompt.
Model
Tactic Dataset
<
4
<
<
<
<
128
<
256
BM25
N/A
9.63
13.56
15.62
16.70
18.47
20.73
23.38
25.44
28.00
30.55
MH-86M
No
HPL
9.63
19.25
22.99
28.68
34.58
39.88
44.50
47.84
51.47
52.95
MH-86M
Yes
HPL
9.63
20.24
25.44
31.53
36.15
40.67
44.70
48.53
51.87
54.22
MH186M
No
MAPL
9.63
18.27
22.00
27.70
35.07
39.78
44.99
49.31
52.65
55.60
MH-86M
Yes
MAPI.
9.63
19.94
25.93
33.79
39.29
43.71
47.94
52.06
54.32
56.19
23

---

Published as a conference paper at ICLR 2024
E.3 NUMBER OF PREMISES USED AS A PERFORMANCE METRIC FOR PREMISE SELECTION.
Consider the number of premises used to generate steps in Algorithm 3 (arameterr k in the for-loop). Intuitively, the fewer premises needed the better, since it means that all the premises necessary to close the proof are ranked higher (high recall), thus the model does a more accurate premise selection. In other words, a better retrieval model should be able score all the necessary facts higher and push unnecessary facts down the list.
To compare different models we fix a of tacties and accumulate problems solved as we increase the number of premises used to generate steps in Algorithm 3 This is presented in Table 6 and Figure A.5] Namely, for each k we count the number of problems solved using at most & premises. Effectively, each new value of l adds one new step per tactic to try.
E.4 SINGLE-STER PROOF RATE BOUND
non-trivial to estimate the lower bound on how many problems can be closed directly from the root state in a single proof step. To answer this question, we use different models in Algorithm 3 and take the union of problems solved by them. Namely, we ensemble the results of the Mag- Magnushammer-3888
nushammer variations introduced in previous sections: Magnushammer-800 Magnushammer- Setthhhammm----LEE.... Sledgchammer, BM25, and the models presented in Section 3.4 Such a combination successfully closes 65.5% of the proofs.
F EXAMPLES OF PROOFS FOUND BY MAGNUSHAMMER
In Sledgehammer, once one of the external provers found a proof, it is likely that it can be reproduced inside Isabelle (but not always, as reported by Paulson and Blanchette (2012). (01))) The external provers significantly reduce the number of premises passed to the reproduction step, therefore the Isabelle's proof will be short. The major bottleneck of Sledgehammer, however, is the pre-selection step: the external provers often cannot find a proof because they are provided too few or too many premises.
In Magnushammer, on the other hand, we skip the external provers completely and input premises directly into the native Isabelle's 's tactics to produce a proof. This means that the prediction must be of high quality in order to obtain good results. The number of the premises will be typically larger therefore the proofs will be longer, and of form of a combination of strong tactic and a long list of premises as its arguments.
As example demonstrating the difference between Magnushammer and Sledgehammer from the perspective of produced proofs, let's see two proofs of the algebraic theorem set_r_at co.kksoree from the Archive of Formal Proofs
Sledgehammer's proof:
by (smt (z3) Ri king.oo set_r_ar__co_eeeeeeeeeee ker_ideal]
Magnushammer's proof:
by (clarsimp simp add: set_ar_cos def Ring.Ring Ring.siinne set_r_ar_co_ eq_prop Ring. __i____tt_____c_ Set. bexE Ring.ring_is_ag ker_ideal)
Both Sledgehammer and Magnushammer were able to solve it, however, the latter used more premises. This is expected: whenever both methods find proof, the Magnushammer's proof is often longer in the sense of the number of premises used. Yet, Sledgehammer's weaker pre-selection scheme causes it find fewer proofs in comparison.
An example of a theorem that Sledgehammer was unable to prove (with a generous time limit of 60% s), but Magnushammer has proven, lemma iit.aaadss...fi..mmossss.....mu. The proof
from the Groop--nnngMMottteellggggree..t accesible wwtpa//lllalllttgpe///eee...ooaa tum.
'fomm the theory Cragae/eaaaaaaaooooooooooooooonn accessiilel
24

---

Published as a conference paper at ICLR 2024
produced by Magnushammer consists of the smt tactic and a list of premises. Thus, Magnushammer was able to retrieve the necessary premises in contrast to Sledgehammer:
by (smt (23) unst_disc fix unit circle fix
Oriented Ciciteie_irrrceeeseooo unit disp_ddsc____eeeeeeee def mnit_circlee fix moebiuss_minee uminus
unit_ddsc_fik_mmeebuuu..oo Set. set.imageiiff unit_disc_fixxiff
Moebius. uubbuuus_ummiuu___muuuu____ddd mataayyleettloos.ulaaayllaaaaaat
unit_dise_fix.abs_..g unit_disc_fix untt_diss__ixx_ooobssu...
beebiuss.plus.moebiuu_oo
_ait_iisc_ixx_id_mebiuu
Set.imaget Set. imagel
brijented_iiccllnss.eer.._
www.vertt_iinusssipplll
mii__dircle__ixxxmeebuss...
25


Reviews:
[{"review_id": "NGfwjt6fFm", "reviewer": "Reviewer_t7yc", "summary": "The paper introduces a language-model-based premise selection tool, Magnushammer, for the Proof assistant Isabelle. Given the current textual proof state, Magnushammer, is able to select a set of relevant premises based on trained transformer models. This selection is two-staged: (1) SELECT: an efficient step that selects premises with the highest representation similarity to the given proof state; (2) RERANK: re-rank the selected premises based on a score outputted by a binary classifier predicting whether the proof state and the premise are relevant. The models in both stages are trained contrastively, upon the data collected from human-proof libraries and alternative proofs from Sledgehammer. During experiments, Magnushammer shows significant improvement over Sledgehammer. The authors also open-sourced the collected premise-selection dataset.", "questions": "•\tThe author mentioned that the MAPL dataset “decreases the probability of sampling false negatives while training contrastively”. Could the author provide further details on the likelihood of a premise being positive if it is not found by human-proof collections and Sledgehammer? Additionally, are there other methods to validate or enhance the confidence that it is a true negative? Also, the influence of false negatives on batch-contrastive learning can be elaborated.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "The paper proposes a novel approach to premise selection, which was previously considered a difficult task for LLMs since the length of relevant premises is usually much larger than what LLMs can handle. With batch-contrastive learning and careful data design and collection, Magnushammer retrieves premises instead of generating them using Transformers, showing impressive performance on theorem-proving benchmarks.\n\n•\tThe experiment design is generally sound and compelling. The experiment separates the training and test data and evaluates the quality of premise selection in both single-step (direct evaluation) and multi-step (integration with Thor) tasks. The authors also present the impact of the number of selected premises on the proof rate, as an alternative measurement of the premise selection quality.\n\n•\tThe ablation study is comprehensive, covering the pre-trained model, model size, dataset size, and compute budget.", "weaknesses": "The presentation of why the premise selection was considered difficult for LLMs, and how the proposed method tackles these difficulties is somehow weak. Some more examples and explanations/discussion on LLM/contrastive learning would help.\n\n•\tSection 6 mentions GPT-f, PACT, Thor, and other LLM-based theorem-proving efforts, highlighting their diverse focuses. It would be nice if the authors provided a more insightful and coherent discussion on how different aspects are connected (e.g., premise selection, tactic prediction, proof step search), how the previous works explicitly or implicitly tackled the premise selection problem, and how the proposed method is advancing the area.\n\n•\tSection 3 Training part mentions that “This gives N-1+M negatives per proof state in one batch”. Is it possible that a positive premise for one state is also positive for another state in the same batch? Did you select positive examples intentionally avoiding this possibility, or, in this case, the negative examples are less than N-1+M?\n\n•\tDuring the evaluation, for each proof state, Magnushammer parallelly checks whether a proof can be completed from premise subsets of different sizes. The author claims that similar techniques are also implemented in Sledgehammer. The author can explain more on this point to ensure the experimental comparison between Magnushammer and Sledgehammer is fair, e.g., in terms of parallelism, number of selected subsets, and their sizes.\n\n•\tMinor formatting issue: the reference of Thor in Section D.2 on Pg21.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "LGCvkoxnNB", "reviewer": "Reviewer_uz6C", "summary": "In the field of automated theorem proving, premise selection is the process of selecting a subset of mathematical statements that are already known to be true as a set of premises to build new knowledge. In this work, the authors introduce MAGNUSHAMMER, a premise selection technique based on transformers.", "questions": "What are other suitable datasets for the evaluation of tools for premise selection?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The idea of using transformers in for premise selection is quite interesting. In my opinion, the main strength of this paper the fact that this approach was able to outperform an automated theorem prover based on similar paradigm by a good margin. More specifically, the new approach obtained a proof rate of 59.5%, while sledgehammer, which is one of the most well known premise selection tools for Isabelle, obtained a proof rate of 38.3%. \n\nThe authors also contribute with a large dataset for benchmark of premise selection paradigms. \n\nFinally, the authors provide a careful analysis of their approach by analysing the dependence on quantities such as model size, dataset size. According to their results, when resources are moderate, their approach outperforms existing techniques.", "weaknesses": "The main drawback seems to be the fact that the tools were evaluated only on two datasets (PISA and miniF2F).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "NpUNLwaTsN", "reviewer": "Reviewer_7Qsu", "summary": "This paper Magnushammer, a transformer model trained for premise selection on Isabelle. They first build a training set of premise selection from human-written proofs and machine-generated proofs produced by Sledgehammer. Magnushammer select relevant premises in two steps, first select a larger set of premises from all candidate based on cosine similarity of embeddings from a transformer model, then rerank these the selected premises by concating them with the proof state and feeding the new sequences into the transformer for binary classification. Experiments validate that, compared to Sledgehammer, better premise selection using Magnushammer leads to significant improvement for theorem proving with Thor on the PISA (57% -> 71%) and miniF2F (29.9% -> 37.3%) dataset.", "questions": "1 It is great to know we could advance theorem proving by developing better premise selection approaches. My question is what the upper bound is given our current recipe. Is it possible to obtain the results of Thor with ground truth premise selection?\n2 Did you retrain Thor with Magnushammer or just apply the original Thor trained with Sledgehammer to Magnushammer?\n3 Could you quantitatively evaluate the contribution of Magnushammer for theorem proving with Thor, such as how many proof steps call Magnushammer in your test.", "limitations": "", "rating": 8, "confidence": 5, "soundness": 4, "presentation": 4, "contribution": 2, "strengths": "1 Similar to LeanDojo, this paper demonstrates that better premise selection is crucial for the success of theorem proving. \n2 The proposed approach is technically sound, with properly designed select and rerank steps, InfoNEC and BCE losses and data collection steps.\n3 Experiments demonstrate significant improvement resulting from Magnushammer. \n4 The proposed dataset for premise selection could facilitate the future progress for automated theorem proving.", "weaknesses": "Still, the main story of this paper is almost the same as LeanDojo. The proposed two-step pipeline and training method are also commonly used.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "qsQdt7Gbgy", "reviewer": "Reviewer_XHfH", "summary": "This paper proposes a new method for premise selection in automated theorem proving. The proposed method is based on training a transformer model on the text of the lemmas that are available in a library. The proposed method improves the testing accuracy of AI assistants on some benchmarks.", "questions": "Would it be possible for the authors to expand on their improvement on the miniF2F benchmark? Specifically, I would be interested to know what are the specific unsolved theorems that Magnushammer was able to solve, and how complex are those proofs. When one tries to solve those theorems with Sledgehammer or other assistants, what exactly goes wrong, and what is the gap that Magnushammer can bridge while sledgehammer cannot? Are the premises that Magnushammer can find, and Sledgehammer fails to find, related to the premises that were chosen by the authors for their contrastive learning? I think giving maybe two or three examples (theorems from miniF2F that were solved by Magnushammer) would improve the presentation of this paper’s contribution.\n\nAuthors mention that one benefit of Magnushammer is that it can be trained on various languages, and it is not limited to Isabelle, etc. Have authors experimented with lean? I did not see any results on lean, but I might have missed it.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The open source premise selection dataset appears to me as a useful contribution for the community.\n\nI found the approach and the proposed method interesting. \n\nPaper is well structured and its writing is clear.", "weaknesses": "The main shortcoming that appears to me is the lack of comparison with recent methods such as LeanDojo. Perhaps authors can address this during the rebuttal, clarifying the advantage of their proposed method.\n\nSpecifically, in the list of novel contributions of the paper, the first item is stated to be the use of contrastive learning for premise selection. However, contrastive learning was previously used in LeanDojo. It would be helpful if authors clarify the specifics of their contribution compared to previous methods.\n\n-----\n\nMoreover, authors have not cited the reference below which also trains a GPT model on mathematical statements. It seems that the authors' use of the GPT-2 model has some similarities with the approach taken by the paper below. So, it is not clear to me whether authors' approach is as novel as it is claimed to be. I ask that authors clarify their contributions in relation to this reference as well.\n\n[1] Polu, S., Han, J.M., Zheng, K., Baksys, M., Babuschkin, I. and Sutskever, I., 2022, September. Formal Mathematics Statement Curriculum Learning. In The Eleventh International Conference on Learning Representations.\n\n\n------------\nAs a limitation of Sledgehammer, this paper mentions the need for handcrafted design. In contrast to Sledgehammer, it is mentioned that Magnushammer does not need handcrafted design and feature engineering. However, the choice of negative premises appeared to me as a handcrafted approach in Magnushammer. I do not think this is necessarily a shortcoming of the Magnushammer, but I think the benefits and contributions of the Magnushammer might have been magnified a bit.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (poster)