MLFMF: Data Sets for Machine Learning for Mathematical Formalization
Venue: NeurIPS 2023 Datasets and Benchmarks Poster (2023)
Keywords: recommendation system
formalized mathematics
proof assistant
Lean
Agda
link prediction
graph learning
TL;DR: Recommender systems for large libraries of formalized mathematics in Agda and Lean

Abstract: We introduce MLFMF, a collection of data sets for benchmarking recommendation systems used to support formalization of mathematics with proof assistants. These systems help humans identify which previous entries (theorems, constructions, datatypes, and postulates) are relevant in proving a new theorem or carrying out a new construction. Each data set is derived from a library of formalized mathematics written in proof assistants Agda or Lean. The collection includes the largest Lean 4 library Mathlib, and some of the largest Agda libraries: the standard library, the library of univalent mathematics Agda-unimath, and the TypeTopology library. Each data set represents the corresponding library in two ways: as a heterogeneous network, and as a list of s-expressions representing the syntax trees of all the entries in the library. The network contains the (modular) structure of the library and the references between entries, while the s-expressions give complete and easily parsed information about every entry.
We report baseline results using standard graph and word embeddings, tree ensembles, and instance-based learning algorithms. The MLFMF data sets provide solid benchmarking support for further investigation of the numerous machine learning approaches to formalized mathematics. The methodology used to extract the networks and the s-expressions readily applies to other libraries, and is applicable to other proof assistants. With more than $250\,000$ entries in total, this is currently the largest collection of formalized mathematical knowledge in machine learnable format.

MLFMF: Data Sets for Machine Learning for Mathematical Formalization
Andrej Bauer
Matej Petković
Faculty of Mathematics and Physics
Faculty of Mathematics and Physics
University of Ljubljana
University of Ljubljana
Institute for Mathematics, Physics and Mechanics Ljubljana, Slovenia
Department of Knowledge Technologies
Jožef Stefan Institute
andrej bauer@fmf uni-lj.ss
Ljubljana, Slovenia
matej - wwt.oviiitffftt uni-lj.as si
Ljupčo Todorovski
Faculty of Mathematics and Physics
University of Ljubljana
Department of Knowledge Technologies
Jožef Stefan Institute
Ljubljana, Slovenia
1 touooo.tooorovsak uni-lj. si
Abstract
We introduce MLFMF, collection of data sets for benchmarking recommendation systems used to support formalization mathematics with proof assistants. These systems help humans identify which previous entries (theorems, constructions, datatypes, and postulates) are relevant in proving new theorem or carrying out a construction. Each data set is derived from library of formalized mathematics written in proof assistants Agda or Lean. The collection includes the largest Lean 4 library Mathlib, and some of the largest Agda libraries: the standard library, the library of univalent mathematics Agda-un unimath, and the Type Typelooy library. Each data set represents the corresponding library in ways: network, and as a list s-expressions representing the syntax trees of all the entries in the library. The network contains the (modular) structure of the library and the references between entries, while the s-expressions give complete and easily parsed information about every entry. We report baseline results using standard graph and word embeddings, tree ensembles, and instance-based learning algorithms. The MLFMF data sets provide solid benchmarking support for further investigation of the numerous machine learning approaches to formalized mathematics. The methodology used extract the networks and the s-expressions readily applies other libraries, and is applicable to other proof assistants. With more than 250 000 entries in total, this is currently the largest collection of formalized mathematical knowledge in machine learnable format.
heterogeneous
Introduction
Applications of artificial intelligence to automation mathematics have long history, starting from carly approaches based on a collection of cand-crafted heuristics for formalizing new mathematical concepts and conjectures related to them [Lenat] 1977]. In the last decade, there has been growing interest in formalization of mathematics with proof assistants, which verify the formal correctness of
37th Conference on Neural Information Processing Systems (NeurIPS 2023) Track on Datasets and Benchmarks.

---

mathematical proofs and constructions, and help automate the tedious parts. The trend is correlated with the interest of machine learning community in aiding formalization efforts with its expertise.
Machine learning methods are often used to address premise selection, i.e., recommendation of theorems that are useful for proving given statement. DeepMath [Irving et al. (016) proposes using convolutional and recurrent neural networks to predict the relevance of a premise for proving the given statement. While many other approaches [Polu and Sutskever, 2020, Welleck et al.) 2022 use transformers and general language models, Paliwal et al.) [2020] have shown that taking into account the higher-order structure of logical expressions used in formalizing mathematics can greaty improve the performance of premise selection and automated proving. Indeed, many approaches use graph neural networks learn from the higher-order structures, e.g.. [Wang al., [017]. More recently, graph neural networks have also been proven useful for explorative, unsupervised approaches to automated theorem proving with reinforcement learning [Bansal et al., 2020 [ample et al. 2022]. Some of these approaches address alternative tasks, such as recommending or automatically selecting suitable proof tactics, i.e., routines for performing series of proof steps, applying decision procedure, or for carrying out proof search.
Data sets of different origins have been used to evaluate the proposed approaches. Welleck al. [2022] evaluate their approach on a selection of three hundred proof' included in the ProolWiki proofwiki] library of mathematical proofs written in a combination of natural language and LKTEX. Polu and Sutskever (2020) use a standard library of the Metamath proof assistant. [ample et al.
[2022] combine proots from the Metamath library with proofs from the Mathlib library [Mathlib] of the Lean proof assistant. The latter has also been used for evaluating the approaches in |Han et al.
2022]. Wang et al. [2017]. Paliwal et al. 2020), [Bansal et al. [2020) evaluate their models within the HOL Light proof assistant based on higher-orden logic |arrissn 2009]. The formalized proofs in standard HOL libraries have been transformed into a HOLStep data set for machine learning, where examples correspond to more than 2 million steps from 11 400 proofs (Kaliszyk et al. 2017]. The training set includes proof steps in context (local hypotheses and the current statement being proved) and the library entry used in the step. Descriptions of the library entries are included in human- readable and machine- readaale, tokenized versions. The data set has been recently upgraded to the interactive benchmark environment HoList for training automated proof systems with reinforcement learning [Bansal et al. 2019].
We present a collection of data sets, MLFMF, based on libraries of formalized mathematics encoded in two proof assistants, Agda and Lean. It supports evaluation and benchmarking of machine learning approaches for recommendation systems in the context of formalized mathematics.
ID
entry N:
zero: N
suc (n): N +
0+ n, for all n E N suc(m) + n suc(m + n). for all m, n N
Lemma I (LI)
m m00 m for all m E N.
This proved by induction
Lemma 2 (L2)
+ suc(n) = suc(m + n), for all m, n E N.
This is proved by induction
m.
Theorem (T)
m m n==== n + m, for all m, n E N. This is proved by induction on m. In the base case (m = 0), we need L.1. In the induction step (m suc(f)), we need L2.
Table 1: An example formalization of proof that the addition of natural numbers is commutative.
We transform each library into a directed multi-graph whose nodes represent library entries (theorems, lemmas, axioms, and definitions), while edges represent the references between them. Consider the example in Table [ starts with a definition of the set of natural numbers with two simple constructors that define the first natural number 0 and constructs all the others inductively by asserting that a successor suc (n) of a natural number n is also a natural number. The definition the addition of natural numbers follows their definition by asserting two simple rules for the left addition of O and the left addition of successor. Note that the definition of + references the definition of N. Next, the first lemma establishes the rule for the right addition of zero the first simple commutativity case.

---

The second lemma establishes the right addition of a successor the second case. The theorem at the end references the two lemmas show (and prove) the commutativity of adding natural numbers.
The entries from Table ! are transformed into a multi-graph depicted in Figure Ta It contains five nodes, each corresponding to a table row. The multi-graph includes an edge from the node to the node N. indicating the reference to the set of natural numbers in the definition of addition. It also contains the self-reference of +. since the second case of this definition is recursive. Similarly, there are four edges from the theorem node to the two lemma nodes and the two nodes defining natural numbers and addition thereof. The obtained data allows us to approach premise selection as a standard edge prediction machine learning task.
Furthermore, we transform each formalized entry into directed acyclic graph that retains complete information about the entry, see Figure Tb. By including the entire entry structures in the data sets, make them suitable for further exploration of the utility of the state-of-the-art approaches to graph-based machine learning. A detailed description of the format is given in Sections 3.3 and 3.4
(:entry
LI
(:name N)
(:type (..))
(:data
(...)
T
(:name N. zero)
(:name suc)
L2
(a) The multi-ge multi-graph graph representation of the example proof from Table
(b) An s-expression from which we obtained the DAG for the entry N in Table
Figure 1: The two-part representation of a library. Library as a whole is represented as a network of references (a). Additionally, every entry is represented DAG which is shown here in its textual s-expression format (b). Note that some nodes of DAG were replaced by (...) for better readability.
Our approach is general and can be applied to other proof assistants based on type theory. Moreover, even though Agda and Lean have quite different internal representations, the corresponding data sets a common format that requires little or knowledge about the inner workings of proof assistants. Thus our collection provides the machine learning community with easy access to a large amount of formalized mathematics in familiar formats that allow immediate application of machine learning algorithms. To our knowledge, MLFMF is the first and most extensive collection of data sets featuring more than proof assistant and providing access to the higher-order structured representation of more than 250 000 mathematical formalization entries.
Formalized Mathematics
Formalized mathematics is mathematics written in format that allows algorithmic checking of correctness of mathematical proofs and constructions. The programs that perform such checking are called proof assistants proof checkers. An early proof checker was AUTOMATH [Bruijn 1970).
while today the most prominent assistants are Isabellc/HOL [Isabelle| HOL Harrison], Coq [Cgg].
Agda [Agda] and Lean (d Moura al. 2015). They all interactive: As the user develops piece of formalized mathematics the assistant keeps track of unfinished proof goals, displays information about the current goal, checks the input the fly, and provides search and automation facilities.
The level of automation varies between different proof assistants. In Agda, which supports little automation, the user directly writes down proofs and constructions in abridged type-theoretic syntax that Agda checks and algorithmically elaborates to fully formal constructions. On the other end the spectrum are IsabelleHHOL. and Lean, where the user relies heavily on lactics, which are routines that automatically perform various tasks, such as running a domain-specific decision procedure, applying heuristic, or carrying out proof search.
3

---

The mathematical formalism most commonly used as the underpinning of proof assistant is type theory, of which there are many variants [Church 1940 Martin-Lör 1975| Coquand and Huet 1988]. The proof assistant processes the user input by disambiguating mathematical notations, applying tactics and other meta-level processing commands, and internally stores the resulting proofs, theorems, constructions, definitions, and types as expressions, or syntax trees, of the chosen type theory. These are typically quite verbose, so that checking their correctness is straightforward, but contain many more details than a user may wish to look at.
Libraries of formalized mathematics comprise units, organized hierarchically with module system or namespaces, each of which contains number of entries: definitions of types, constructions of elements of types. statements and proofs of theorems, unproved postulates (axioms), as well as meta-level content, such as embedded documentation, definitions of tactics, hints for heuristics, and other automation mechanisms.
In the last decade the libraries of formalized mathematics have grown considerably, most recently with the rise of the popularity of the Lean proof assistant and the Mathlib library [Mathlib community 2019), around which mathematical community of several thousand mathematicians has formed. Such growth presents its own challenges, many of which of the software engineering kind and can be so addressed. In our work we addressed the specific problem of recommendation: given a large body of formalized mathematical knowledge, how can the proof assistant competently recommend theorems or constructions that are likely useful in solving the current goal? There are two typical scenarios: the user knows which theorem they would like to use but have a hard time finding it in the library, or the user is not aware of the existence of a potentially useful theorem that is already available. Both are obvious targets for machine-learning methods.
3 MLFMF Data Sets
In this section we describe our data sets in detail. We first explain the semantic content of the data extracted from libraries of formalized mathematics, describe the format and information content of the data sets, continue by reviewing the machine learning tasks for which the data sets were built, and finish with overview of the technical aspects of the tibrary-to-datar transformation process.
3.1 The Extracted Data
Formalized mathematics is written by the user in domain-specific language, often called the vernacular or the meta-language. The proof assistant evaluates the source code, which involves executing tactics, decision procedures, etc., verifies that the proofs and constructions so generated are mathematically valid, and stores the results using an internal type-theoretic format. One may apply machine learning techniques directly the vemacular, written by the user, on the formal representation of mathematics. The former approach roughly corresponds to learning how to do formalized mathematics, and the latter what formalized mathematics is.
We took the latter approach, namely learning on the formalized mathematics itself, for two reasons. First, because we aimed at a uniform approach that is applicable to most popular proof assistants, it made sense to use the internal type-theoretic representations, which are much more uniform across proof assistants than the vernaculars. Second, the vernacular contains meta-level information, such as what tacties to use, from which one cannot discern directly which theorems are actually used in a given proof. Without this information, one can hardly expect a recommendation system to work well.
Every data set that we prepared is generated from a library of formalized mathematics. Most librarics. and all that we incorporated, are organized hierarchically into modules and sub-modules, each of which is unit of vernacular code that, once evaluated by the proof assistant, results in a list of entries: definitions of types, constructions of elements of types, theorems and their proofs, and unproved postulates. The entries refer to each other and across modules, possibly cyclically case of mutually recursive definitions.
The internal representations of entries vary across assistants, but all have certain common features:
1. Each entry has qualified name M,.M2... ... Mr by which it is referred to, where My.M2 M₁ is a reference to a module in the module hierarchy and N the local name of the entry, for example Algebra.Gron Group. Firssroooroooooooeaaaoooeeee

---

For example, the (name1 declarationi body1) (name2 declaration2 body2)
lib2sexp
sexp2graph
LIBRARY
Figure 2: The two stages of the data transformation. First, a language-dependens (i.e., Agda or Lean) command line tool used transform the library entries into s-expressions. In the second stage, Python scripts are used to explicitly construct the directed multi-graph, which contains library modules, entries, and references among them.
2.
Each entry has an associated type T, which specifies the information content of the body of the entry. For example, the type List(N) specifies that the entry is a list of natural numbers. Importantly, logical statements are just special sort of types, so that the type of a proof the logical statement that it proves. (This is to be contrasted with first-order logic, where logical statements are strictly separated from types.)
3. An entry has a body, which an expression of the given entry type. In some cases the body may be missing, for instance if the user declares an axiom.
4. Depending on the proof assistant, various meta-level information is included, such which arguments to functions are implicit (need not be provided by the user).
3.2 Data Description
In this section, we describe the data set. We start with brief description of data transformation process, continue with the detailed description of the resulting pair of computational graphs for the entries in the library, and the directed, multi graph of references in the library (see and 3.4).
Every data set consists of two parts. The first part is set T of abstract syntax trees (AST) that correspond to the entries in the library, while the second is directed multi-graph G(V, F), where V is of library entries, and E includes the references among them. ASTs are actually trees in the case of Agda libraries. However, in Lean, they are directed acyclic graphs (DAGs) due to memory optimization and node-sharing: all the parents that would potentially reference their own copy of a node (or a subtree), rather reference the same node. For this reason, we refer to them as computational graphs. They provide the full information about every entry in the library and are given in the s-expression format that is much easier to parse, as compared to the typically very flexible syntax of proof assistants that allows for implicit arguments, mix-fix notation, function if of_then___ thee_else x z in Agda can be called as if then else z. Learning from the source code would put an additional burden on the machine learning algorithm. Learning directly from computational graphs, on the other hand, is much easier.
Entry
name
doclaration
body
Figure 3: The DAG representing an entry has single root node with three children: a node containing the entry name, a DAG containing the entry declaration, and DAG representing the entry body.
3.3 The Computational Graphs
During compile time, the full type of every entry in the library is computed and the source code of the entry is converted (directed acyclic) computational graph. We intercept this procedure and export every entry as Lisp s-expression, which is defined recursively as:
5

---

1. A literal is an s-expression, and
2. A list of s-expressions is an s-expression.
For example, the literals 12 and "foo" are s-expressions, and the ("foo" ("bar" 12) "baz") also s-expression with three elements: "foo", ("bar" 12) (which contains two s-expressions) and "baz". Every s-expression that obtained from the entries in a library is three-part, part, as shown in Fig. 3 In consists of the name of the entry, the s-expression that describes the declaration, and the s-expression that describes the body of the entry.
Even though the entries were manually encoded and mostly take at most a few kilobytes of space, their computational graphs can much larger (more than a gigabyte), mostly due to the type checking and the expansion of the declared type of the entry.
3.4 The Multi-Graph
For simplicity reasons, we will refer to the directed multi-graph G(V, E) simply as a graph. Its meta-structure is shown in Fig. 4a In the description below, we follow this structure (in the bottom-up manner) and the concrete example of a subgraph for Agda's standard library Fig. 4b
Entry nodes. Every module in a library defines least one entry (shown green circles), e.g.. Bijection DEF DEFINES id, Bijection DEFINES Bijection (these are two different nodes), and Injection on DEFINES injective. We further differentiate between different kinds of entries, as Most of the nodes in the graph are entries (and most of them are functions), and most of the edges are of type REFERENCE FROM DECLARATION/BODY,
shown in Tab. 2
Library and module nodes. The only nodes with no incoming edges (root nodes) the library nodes (shown as blue squares). Every graph contains at least one library node-th the one that corresponds to the library itself. In Fig. 4b this is the node stdlib. However, the graph might contain
FROM DEC- LARATION
CONTAINS
Library
CONTAINS
Module
DEFINES
Entry
REFERENCE FROM BODY
(a) The meta-structure the graph.
Bijection
Bijection
stlib
Function
id
Injection
injective
(b) An excerpt from Agda's standard library. The entry id (indentity function) is defined in the module Bijection, which submodule of module Function, which one the top modules the library. the declaration of id, the entry Bijection is referenced. In the body of id, the entry injective is referenced. The two referenced entries are defined in the submodules Bi Bijection and Injection, respectively.
meta- graph of libraries (a) and subgraph the graph that was created from Agda's standard library (b) that follows the prescribed meta-structure.
Figure 4:

---

Table Tags of the nodes in s-expressions.
kind
description
:atta
inductive data type (natural numbers, lists and trees)
constructor
data-type constructor (successor, cons)
:function
function (including constants as nullary functions) record type structure with named fields attributes)
:record
:axiom
postulated type or statement (no inhabitant or proof given) built-in (primitive) function
:primitive
:sort
the sort of a type (proposition, universe at a given level) the inductionn/recurionn principle associated with inductive data-type entry whose body is hidden
recursor
rabstract
an additional node outer library if any of the library entries reference some external entries that are not part of the library (for example, built-in types). The library nodes are directly connected to the nodes representing modules (shown as blue diamonds) via the edges of the type CONTAINS, e.g., stdlib CONTAINS Function. Every module can contain zero or more (sub)modules, e.g.. Function CONTAINS Bijection.
In the case of Agda libraries, the module nodes correspond to the modules that are actually present in the library and resemble the file system of the library. Lean, however, supports the use of namespaces. If the file a/b/c.lean defines an entry foo. bar F, and the file d/e.lean llla defines an entry foo. war.bar..........o.............. G. those two entries are part of the same namespace foo. bar and the exact location in the file system where these two entries were defined, is irrelevant. Therefore, module nodes for Lean's ' library Mathlib4 correspond to namespaces in the library. Following the previous example, we create module nodes foo and bar, together with the edge foo CONTAINS bar.
3.5 Machine Learning Tasks
The main motivation for the creation of the data set was the development of machine learning algorithms that would enhance current proof assistants and help mathematicians using them. This translates to the following two machine learning tasks.
Link prediction. Given the current state of the multi-graph of references among the entries, learn model that predicts the future, novel links (references) among the library entries. Formally, we learn model M (u, v) M(u, v) E [0, 1] that given nodes and outputs the model confidence in the presence of the edge (u, v). The (current) computational graphs of the entries can be used as additional information for learning such a model. If learning from the multi-graph only, one can use standard node- or edge-embedding approaches as well as graph neural networks.
Recommendation. The problem of predicting the future references among the entries could be understood as a recommendation task as well. Given a specific unfinished entry (possibly with some additional context, such as the list of lemmas/ claims that were used last), the task is to recommend the candidates that could be referenced in the current computational graph of the entry to complete
Note that the two tasks are equivalent, i.c., solving one solves the other. A link prediction model M (see above) can be converted into a recommendation system by fixing the entry and recommending the entries
V with the highest confidence levels M Mu, v). Vice versa, given a recommendation model M' : u + M'u S V. we can define corresponding link link- areeeeediition model M as M v) = 1 if E (M)), and M (u, v) = 0 otherwise.
Since the essential part of the MLFMF data set is directed multi-graph (which represents heterogeneous network), other standard learning tasks for graphs/ networks might also be interesting. Here, mention example instances of the common node classification task.
Entry class detection. A traight-foowardd instance of node classification task would be classifying the entries into their types from Table e.g., function or axiom. This does not require additional manual labeling and should not be too hard, especially when computational graphs are taken into account, since the structure of function is quite different from the structure of, e.g., record.
7

---

Claim detection. A more challenging instance of node classification is predicting whether function entry is a claim (e.g.. lemma, corollary, theorem, etc.) or not, since some of the entries are simply definitions of, for example, the addition of natural numbers. Approaching this task, however, would require additional (manual) labeling of the entries.
3.6 License
We make MLFMF publicly available under the Creative Commons Attribution 4.0 International ! (CC BY 4.0) license at httts:///githu.. com/ul htlffulffff////////////////////l ffff/mm/e mmlfffff-mff data
4 Experiments and Results
In this section, we first introduce the experimental setup for the baseline experiments (how to prepare the train and test part of the data set, and which standard metrics can be used), and then, after briefly introducing the baseline methods, report the experimental results.
4.1 Train-test split
When splitting the graph into train and test data sets, we should split the multi-graph G(V, E) and the set of computational graphs the entries. In the case the link prediction and recommendation tasks, we should focus function nodes, since these are the only nodes that correspond to computational graph whose body contains a proof of a claim formalized in the declaration part of the computational graph.
In our baseline experiments from Sec. 4.4| we follow a generic approach to creating a train-test split. The approach takes two parameters: Prest E (0. 1), Pouly E [0, 1). First, we randomly choose the proportion Piea of function nodes. We assume that those correspond to partially written entries whose computational graphs have completely specified type, i.e., the user knew how to formalize a claim, and partially known body, i.e., the proof of the claim is not finished yet. Note that, often, proofs are not written linearly and might contain so-called holes at problematic parts where the right lemmas are yet to be applied (possibly with already known arguments). Thus, we need to modify the computational graphs of the test nodes to reflect the changes in the multi-graph.
We simulate the applications of the missing lemmas by keeping only the proportion of Pbody of the references in the body. Since our graph contains a weighted edge u REFERENCE FROM BODY which we either remove or keep intact, we remove all references them. Then, the unfinished proofs are simulated by keeping the proportion of Pbody of the body of u, which is done by iterative pruning of the leaves of the body. At each iteration, a leaf is chosen uniformly at random. If the chosen leaf is reference that we have to keep, the leaf is not pruned and we continue with the next iteration.
from the body of or none of
The removed edges represent positive test examples, and the negative test examples for learning predictive models need be sampled. In the baseline experiments, the negative test examples were sampled uniformly at random.
4.2 Evaluation metrics
For link prediction, one can use standard classification metrics, such as accuracy, precision, recall, and F.-sc If the model returns its confidence M(,,, v) [0. 1] instead of the class value (M (u, v) E {0, 1)), one could additionally consider area under the receiver-operating -arrrrr-pperattinnccaaatttttttt -haracctrristicc curve. Similarly goes for the recommendation models: one can use precision and recall.
the recommendation model returns the relevance score of a candidate entry to the current context, we can rank candidates according to the score values, with the top recommendation having rank of one (1). We can then compute the minimal (and the mean) rank of the actual references and average them over the testing examples. This is important metric, since it counts the number of false recommendations with better ranks than any of the actual references. Ideally, the minimal rank is close to one, i.e, the top-ranked recommendation mostly matches the missing entry to be referenced.
8

---

4.3 Baseline Methods
Dummy recommender. This recommender ignores the current context and always recommends the k nodes of the multi-graph with the highest in-degree.
Bag of Words/TFIDF recommenders. Bag of Words (BoW) recommender converts every compu- tational graph g(u) of an entry in a library into bag of words (o) We compute the relevance M(u, 2) of the candidate entry e for the current context using the Jaccard similarity between the corresponding bag-of-words:
((Bo((u), (v) = (w) n (o)(
Bo)(u) U BoW(u))
Similarly, FFIDDFrreoommender embeds g(u) into a feen vectors (obtained from the corresponding bags-of-words) as implemented in Scikit-Leamn 1.2.2 [Pedregosa et al., 2011]. The relevance of the candidate entry is computed as Manhattan cosine distance between the TFIDF-vectors u and v.
FastText embedding recommender. It embeds every computational graph gu)) into vector ((g(u)) = Ewedee(u) wo wwword, g())) FFc (oo (word), where (ee(word) is the vector word obtained from the fastText model trained of Common Crawl [Mikolov et al. 2018). and w(word, g(u)) is the TFIDF weight of the word the entry u.
Recommendations via analogies. We design a recommender that is based on fastText analogies property, i.e., the fact that x = queen one of the approximate solutions of Pee (king) (x) Pe (manman) Pcel (woman). We design the analogy recommender that for a given entry recommends the nodes u, for which a good analogy u' > v of the edge - v can be found. The relevance of the candidate entry in given context u is defined in terms of the Manhattan distance as
min r(u, v) = V'E'EEIC
[1( - PPo (e)] (p)) PPo (1))ll)
Node2vec-basee link prediction. We train node2vec [Grover and Leskovec 2016) model (as implemented in Gensim 4.3.1 [Rehurek and Sojka 2011] on the multi-graph to obtain node embed- dings. We obtain the embedding of the edge (u, v) by concatenation of the node embeddings for u and v. A tree-bagging classifier M sp(u v) M (ffu
v)) E [0, 1] is trained on the tabular data obtained with using the edge embeddings as inputs and the edge presence as the target to be predicted. We selected bag of trees ensemble since it is robust classifier, working well on tabular data, when using the recommended settings of 100 fully grown (not pruned) classification trees.
We selected baseline methods that are not computationally expensive and are robust to hyper- parameter settings: if not mentioned otherwise, the methods use the default parameter settings. We can combine multiple embeddings (e.g., those from node2vec together with those from fastText) as the input to the similarity measure of the recommender or classifier for the link prediction task. However, as noted in the next section, this did not improve the best results. In all the experiments, we generated the train-test split with the parameters Prest = 0.2 and pbady = 0.1. The results here are reported for k 5 recommended items and the threshold e = 0.5 for classification.
4.4 Results
The experiments on Lean were run on a computer with 4 Intel Core i7-6700K CPU cores and 64 GB of RAM. The experiments Agda were run smaller machine (2 Intel Core i7-5600U CPU cores, 12 GB of RAM). Experiments that would last more than a week were not carried out (analogies on the Type Topology and Mathlib4 libraries, and fastText on the Mathlib4 library).
Tab. reports the results of the experiments: for extended report including other evaluation metrics (accuracy@k, @k, area under the ROC curve, etc.), and ablation study of node2vec on Agda stidib, check the supplementary material. For the algorithms that were run with more than one parameter setting, the best results are reported (for example, TFIDF was run with cosine- and Manhattan- similarity measures). The best-performing baseline method is node2vec.
the only one that ranks on average at least one actual reference among the ten most relevant candidate references for the three

---

Agda libraries. However, it fails to do so for Lean Mathlib4 and this can be only partially explained by the size of the Mathlib4, Note that node2vec is also the only one that explicitly learns from the multi-graph and, apparently, humans writing proofs in Agda, structured the references better than the computers in Lean, where built-in search heuristics (tactics) are used. The multi-graph partially used by the analogies recommender as well, since the candidate recommendations are evaluated by considering the existing references u' + e' in the library. This might be the reason for its good performance on the Agda stdlib data set.
Table The accuracy (acc) and minimal rank of the true reference for the MLFMF data sets. The
best results (bold) are obtained with a combination of a node2vec and tree- tree- vre-bagging classifier.
Agda stdlib
Agda unimath
Agda TypeTTopology
Lean Mathlib4
method
acc
minRank
acc
minRank
acc
minRank
acc
minRank
Dummy 0.51
218
0.53
2134
0.50
4556
0.51
26065
BoW
0.50
1608
0.50
1571
0.50
4496
0.50
15458
TFIDF
0.51
144
0.52
112
0.51
552
0,51
443
fastText
0.51
132
0.52
394
0.50
1292
NA
NA
analogies
0.52
37
0.51
158
NA
NA
NA
NA
node2vee 0.96
4.37
0.96
3.24
0.98
5,81
0.95
195
Surprisingly, TFID embeddings perform no worse (or even better) than FastText embeddings. The reason for this might be that many words, such as group, ring, etc. have different meanings in mathematics than in general texts. Note that we tried to run additional experiments with the combination of node2vec and TFIDF/fastText embeddings, but accuracy and minRank were both worse, as compared to the node2vec results.
In sum, the baseline results show that the information on the structure the multi-graph crucial for obtaining classifiers with performance beyond the default performance of the dummy baseline. The recommendation performance, measured as mean minimal rank, is valuable enough (less than five recommendations to be checked to find the right one) for two Agda libraries. Developing sound recommendation systems for the other two libraries remains challenge to be addressed by machine learning methods beyond the baselines considered here.
5 Conclusion
We introduced MLFMF, a suite of four data sets corresponding to three libraries in Agda and one library in Lean proof assistants. It includes almost 250 000 entries, i.e., definitions, axioms, and theorems with accompanying proofs. References between entries are included in a multi-graph, where nodes are entries, edges represent references among the entries, and each entry is represented with a direct acyclic graph reflecting the structure of the entry source code encoding. Such a structure provides machine learning researchers with opportunity to address the task of recommending relevant entries for the goal at hand as a standard edge prediction task. Such a representation of the entries allows for of graph-based methods that exploit the structural and semantic information stored in the multi-graphs. The report on the results of the baseline methods establishes a benchmark for comparative evaluation of future developments of machine learning for mathematical formalization that goes beyond a single proof assistant.
A notable limitation of our data sets is the lack of information on the developmental evaluation of the libraries. If the latter could be followed, the more realistic test nodes Vist could be defined as the latest Vessi nodes encoded in the library. However, even with version control information (available since the libraries are stored in GitHub repositories but currently not included), determining the entries' chronological order might be computationally expensive. An approximation of the chronological order might be obtained by computing a topological ordering on the function nodes and selecting nodes from the tail of the ordered list. However, existing definitions in a library might be rewritten, so the accuracy of such an approximation is questionable.
Finally, we plan to include other, more recent libraries in our data set collection. The newly incorpo- rated libraries might include references to earlier, standard libraries, providing further opportunities for real-world testing scenarios.
10

---

Acknowledgments
This material based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-000 The authors also acknowledge the financial support of the Slovenian Research Agency via the research core funding No. P2-0103 and No. P1-0294.
References
Agda. The Agda proof assistant.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 454 463. PMLR, 2019. URL http
//proceedings. mlr pttpss/99/baasal19... 1attmmmaa19..am1lll1
Kshitij Bansal, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Viktor Toman. Learning to reason in large theories without imitation, 2020. URL https://doii.oo org/10..///o wwt.oo....////////...../..////
1905. 10501
de NG Bruijn. The mathematical language automath, its usage and some of its extensions. In Symposium on Automatic Demonstration, Versailles, 1968, volume 125 of Lecture Notes in Mathematics, pages 29-61, 1970.
Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5(2):56-68. 1940. doi: 10.2307/2266170.
The Mathlib community. The Lean mathematical library, 2019.
Coq. The Coq proof assistant. https://coq inrii.ir........ fr/
Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76, 1988.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob Raumer. The Lean theorem prover (system description). In 25th International Conference on Automated Deduction (CADE 25), August 2015. doi: 100000/977--3311-211000
Aditya Grover and Jure Leskovec. Node2vec: Scalable feature learning for networks. In Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, page 855-864 New York, NY, USA, 2016. Association for Computing Machinery. doi: 10.1145/ 2939672.2939754,
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022 URL
John Harrison. The HOL Light theorem prover. Available at hhttps://ww.cdd ac uk/ "jrhl3/hol-light/
John Harrison. Hol light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 60-66, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg.
HOL. HOL Interactive Theorem Prover. Available at
org
Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, and Josef Ur- ban. Deep sequence models for premise selection. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors, Advances in Neurul Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pages 2235 2235-2243, 2016.
www.sas---bttttttttaaaoaeeee html

---

Isabelle. Isabelle proof assistant. Available at https://isabbllle in. tum. de
Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A machine learning dataset for higher-order logic theorem proving. In The Fifth International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. net net/foorum'dddryyu//nee
OpenReview.net, 2017. URL pettps://openreeeee
Guillaume Lample, Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. HyperTree proof search for neural theorem proving. In Advances in Neural Information Process- ing Systems, 2022. URL http::/papper.aatt//////// wit.ss.miisccomm wwwp..cpppppp......eeeeepppepepe www.flllaaaaaeee hag.://ee7--bsstaaaa---ooooeree /tlea//apeer/2222/aaaa
html
Douglas B. Lenat. The ubiquity of discovery. Artificial Intelligene, ((): 1977. doi: 10. 1016/0004433722(77900222 p11/00044702779000448
com wwta//ciiinne/arrileee...// btttpp::/www.scieneddiie ort.aa/ceeectttttcoocceeeeeaaaaa
Per Märtin-Löf. An Intuitionistic Theory of Types: Predicative Part. In H.E. Rose and J.C. Shep- herdson, editors, Logic Colloquium '73, volume 80 Studies Logic and the Foundations of Mathematics, pages 73-118, Bristol, July 1975.
Mathlib. The Mathlib library. http:://lenppooverccommtttty github.ii
Tomas Mikolov, Edouard Grave, Piotr Bojanowski, Christian Puhrsch, and Armand Joulin. Advances in pre-training distributed word representations. In Proceedings of the International Conference on Language Resources and Evaluation (LREC 2018). 2018.
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In The Thirly-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Secont Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 2967-2974. AAAI Press, 2020. URL https://oja aaai org/ index phpp AAAI/ wwt.A//aatteeeeeeee////aaaaaa/// /168//689
F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion. O. Grisel. M. Blondel, P. Pretten- hofer, R. Weiss, V. Dubourg. J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. Scikit-leamn: Machine learning in Python. Journal of Machine Learning Research, 0122825-280, 2011.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020. URL URL /tttp:://///...ooo org.10. 48550/ arxiv. 2009. 03393
proofwiki. Proofwiki. https://proofwikt.c org/ Accessed: 2023-06-05.
Radim Rehurek and Petr Sojka. Gensom-python framework for vector space modelling. NLP Centre, Faculty of Informatics, Masaryk University, Brno, Czech Republic, 3(2), 2011.
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, De- cember 4-9, 2017, Long Beach, CA, USA, pages 2786-2796, 2017. URL /tpp:tttp/// 18d1
neurips. ctcccccppaee wwwpcccpppppppeeee /aneer/2111 2017 http://aaaaaaaeleeeeeeeeeeeeeee2 (eeaaaeeeeeaaeeee2255555ddddddee abst://aaeeabbddddddadtttttaaa.. html
Sean Welleck, Jiacheng Liu, Ximing Lu, Hannanch Hajishirzi, and Yejin Choi. Natural- prover: Grounded mathematical proof generation with language models. In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, editors, Advances in Neu- ral Information Processing Systems, volume 35, pages 4913 4927. Curran Associates, Inc., 2022. URL httpp:t//prccceediiiiie neurips.e.. wwtpcc/pppp.eeeeeeee filerrffilles http:/pprr..lleea/pp//////////// Paper- 1F5544a22223d066666eee//11111213 harp Conference.
12


Reviews:
[{"review_id": "ZGY6l45Q5r", "reviewer": "Reviewer_7Q4p", "summary": "", "questions": "", "limitations": "The authors briefly discuss some limitations in the form of directions for future development.", "rating": 8, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "S1: The context that the authors tackle is very relevant and it would be useful to have a public benchmark for this task.\n\nS2: The authors apply their domain-specific knowledge about theorem provers to nicely interpret the original problem into a graph edge prediction problem.\n\nS3: The paper is well-written and easy to follow, even for someone who does not possess a lot of knowledge of theorem provers.", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}, {"review_id": "sMHWovEXw8", "reviewer": "Reviewer_F1US", "summary": "", "questions": "", "limitations": "The authors have used the last paragraph of the conclusion section to identify future work. However, a more explicit discussion of the limitations may be more helpful. ", "rating": 8, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "1. The data set is quite substantial: 250,000 entries from two proof assistants. Further, each data set is represented as a heterogeneous network and a list of s-expressions. This will likely support a new wave of research into automated theorem proving.\n2. The baseline methods included in the paper are non-trivial: graph and word embeddings, tree ensembles, and instance-based approaches. Table 2 shows the relative efficacy of these methods.\n3. The idea of using a DAG representation of the internal type-theoretic format that is not too closely tied to the syntactic sugar of the two proof assistants gives me hope that others can contribute to this effort in the future and tools built using this library will apply to other proof assistants. It should be highlighted that this design decision comes with a penalty, often replacing kilobytes of source code in the vernacular of the proof assistant with gigabytes of internal representations. \n", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}, {"review_id": "YfCUhTTXJr", "reviewer": "Reviewer_zApR", "summary": "", "questions": "", "limitations": "I do not see expect any negative societal impact from this work. Refer to the prior section for the limitations within the current paper.", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "The authors contribute a relatively large data set suite of mathematical proof data and have made it publicly available to the research community. They appear to have meticulously unified the different library formats to be compatible with one another. They also go into considerable detail about how the data is constructed that would be of interest to subject matter experts.\n\nAssuming that this data set and benchmark is correlated with practical application from an evaluation metric standpoint, it can serve as an important testing bed for new methods to be developed.", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}, {"review_id": "l5rh33sZxd", "reviewer": "Reviewer_yGPU", "summary": "", "questions": "", "limitations": "1. I am not an expert in the field of mathematical formalization. I am not quite clear about the real-world usage of the proposed datasets. What's the real meaning if we conduct link prediction on the given DAG graphs.\n\n2. There are too many small DAG files in the proposed dataset. Are we supposed to merge them into one computational graph? If we want to train an ML model? How do we split the train and test sets (just by files)?\n\n3. The baseline results seem very strange to me. node2vec is almost doing perfect on this data while all other baselines are very close to the Dummy approach. Do we have better choices on these baselines?", "rating": 5, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "1. The paper is well motivated and the introduction is easy to follow. \n2. The authors spend lots of efforts to transform the datasets into different forms so that they can be easily used.", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}, {"review_id": "TB5lmVrjd0", "reviewer": "Reviewer_XBPs", "summary": "", "questions": "", "limitations": "\nThe text is challenging to comprehend, requiring substantial improvements before it can be considered for publication. For detailed information on the specific areas that require clarity enhancements, please refer to the Clarity section of my reviews.\n\nIn subsection 3.5, examples of machine learning tasks were presented, including link prediction, recommendation, and node classification. I find it challenging to grasp the relationship between solving these tasks and the relevance of recommending mathematical proofs. More specifically, each machine learning task corresponds to a specific step within a mathematical formalization language that is understood by machines. However, it remains unclear how this type of language can be translated into a format that is easily comprehensible to humans? \n\nThe documentation accompanying the paper is lacking, as it primarily emphasizes dataset collection while devoting minimal attention to constructing comprehensive documentation. Although some benchmark results are presented, reproducing these results proves to be exceedingly challenging. Furthermore, there is a dearth of specific details regarding the construction of the link prediction model, the hyperparameters employed, and the methodology for sampling negative links.\n \n", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "The motivation of the dataset was clearly explained in the paper, especially in section 2. \nThis is a challenging application of machine learning, the release of the dataset could help benchmarking machine learning methods in this research field.\n\n", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": ""}]

Author rebuttal:

Meta-review: This is a substantial dataset (250,000 entries) with the potential to accelerate development of proof assistants. It also includes 5 non-trivial baselines, along with code to replicate their results. There were some concerns about documentation, which the authors have worked to address. Overall, this is a well-done solution to an important problem. One reviewer wrote: "I'm not sure how I would improve the paper. The scope is well-defined and the authors provide a solid contribution within that scope." Another wrote: "Overall, the paper is well-written, and the dataset is likely to be very useful."
Decision: Accept (Poster)