Mathematical Reasoning via Self-supervised Skip-tree Training
Authors: Markus Norman Rabe
Dennis Lee
Kshitij Bansal
Christian Szegedy
Venue: ICLR 2021 Spotlight (2021)
Keywords: self-supervised learning
mathematics
reasoning
theorem proving
language modeling

Abstract: We demonstrate that self-supervised language modeling applied to mathematical formulas enables logical reasoning. To measure the logical reasoning abilities of language models, we formulate several evaluation (downstream) tasks, such as inferring types, suggesting missing assumptions and completing equalities. For training language models for formal mathematics, we propose a novel skip-tree task. We find that models trained on the skip-tree task show surprisingly strong mathematical reasoning abilities, and outperform models trained on standard skip-sequence tasks. We also analyze the models' ability to formulate new conjectures by measuring how often the predictions are provable and useful in other proofs.

Published as a conference paper at ICLR 2021
MATHEMATICAL REASONING VIA SELF-SUPERVISED SKIP-TREE TRAINING
Markus N. Rabe
Dennis Lee
Kshitij Bansal Google Research
Google Research
Google Research Idenn setrris@@oogle.com
mrabe@gcogle.com com
kbk@googl e
Christian Szegedy
Google Research
szegedyy@goolle.com
ABSTRACT
We demonstrate that self-supervised language modeling applied mathematical formulas enables logical reasoning. To measure the logical reasoning abilities of language models, we formulate several evaluation (downstream) tasks, such as inferring types, suggesting missing assumptions, and completing equalities. For training language models for formal mathematics, we propose novel skip-tree task. We find that models trained on the skip-tree task show surprisingly strong mathematical reasoning abilities, and outperform models trained on standard skip- sequence tasks. We also analyze the models' ability to formulate new conjectures by measuring how often the predictions are provable and useful in other proofs.
INTRODUCTION
Language modeling using Transformers (Vaswani et al. 2017) has been hugely successful for applications like translation and text generation. Models like GPT are able to generate news articles and stories given just an abstract (Radford et al., 2018). These models are usually (pre-)trained proxy task, such as predicting missing words in the case of BERT (Devlin al., 2019). before fine tuning the models more specific (downstream) tasks such machine translation and question- answering. These proxy tasks are not reliant on labels, and thus can be trained on large corpora of unlabeled data. Recently, however, have successful demonstrations of language modeling using only self-supervised training without any fine tuning (Brown et al.) 2020).
In this work, extend this line of thought and demonstrate that purely self sule-super training can even lead to mathematical reasoning abilities. This represents major departure from prior work in deep learning for mathematics, which has focused on learning directly logical reasoning tasks, such as predicting the proof steps or premises or assignments. These approaches require labeled data, which is hard come by and typically very limited in size. In contrast, our language modeling approach to mathematics allows us to train on unlabeled mathematical expressions. We start with the HOList dataset (Bansal et al. 2019), which spans wide range of mathematical topics, including topology, multivariate calculus, real and complex analysis, geometric algebra, and measure theory, formalized the HOL Light proof assistant (Harrison) 1996).
We find that training a language model on all mathematical expressions in this dataset leads to surprisingly strong mathematical reasoning capabilities. We believe that this opens the door to different kinds of neural theorem provers, which do not only search through well-defined search space of tactics and premises, but which are capable to generating their own lemmas and could even come up with
Ansatz requiring creative substitution.
For self-supervised training on mathematical expressions, we propose a novel skip-tree task, which is specialization of the skip-sequence task that respects the tree structure of expressions. We show that models trained on the skip-tte tree task significantly outperform those trained on the skip-sequence task, which is the state of the art for sequence sequence models for natural language.

---

Published as a conference paper at ICLR 2021
Reasoning refer to wide range of abilities, and thus measure the mathematical reasoning abilities of language models on a variety of tasks, including mechanical derivations, such as type inference, and also creative tasks, such predicting under which assumptions a statement is true. As we want to study what reasoning capabilities can be acquired just through self-supervised training, we do not employ fine-tuning on these tasks. Instead, we designed the tasks to be syntactically similar to the training task, such that the language model may produce correct answers.
An advantage of formal language compared to natural language that can attempt automatically evaluate statements. That is, we can let our language models produce conjectures, which we then try to prove using the DeepHOL theorem prover (Bansal et al. 2019 2020). Besides evaluating the provability of the produced statements, we go one step further and evaluate their usefulless, by measuring how many times they are used as premises in proofs of other theorems.
Our contributions are as follows:
1. We show that self-supervised training on mathematical formulas alone leads to logical reasoning capabilities.
2. We introduce a new skip-tree training task that outperforms the tfae-of-the--a art Skip-sequence training. We also introduce several evaluation tasks that are subsumed by skip-tree training (i.e. predict missing subexpression), but test specific logical reasoning abilities to make the performance of the models interpretable.
3. We suggest a way to create and evaluate mathematical conjectures using existing neural theorem provers.
The remainder of this paper is structured as follows: First, we review related work on language modeling and deep learning for mathematics in Section [ Then, in Section 3 we discuss the source corpus of formal mathematical statements from which we generate our training data. In Section 4 we present the skip-tree training task, well several variations that we used in our ablation studies. We present the evaluation tasks in Section 5], discuss our experimental findings in Section [ and conclude in Section 7
2 RELATED WORK
Recently, we have seen a series of rapid improvements in language modeling stemming from better pretraining tasks (Devlin et al.] 2019; /Zhang et al.) 2019 [Song et al.] 2019; [Dong et al. 2019 Raffel et al. 2019 Conneau and Lample 2019). BERT (Devlin et al. 2019) is a pretraining task for Transtormers Vaswani et al.) 2017). which masks out certain fraction of the input tokens that the model then has to predict. UniLM uses multiple pretraining tasks (Dong et al. 2019). One of them is sequence-to-seyee to-seueence task; to predict the next sentence from the previous sentence. MASS and BpanBERT consider a generalized sequence-to-sequene
pretraining task, which is to predict a masked out subsequence of the input (Song al., 2019 Joshi et al., (020). However, both MASS and SpanBERT reveal the length of the sequence to predict as they replace it by a number of mask tokens equal the length of the sequence.
T5 introduced a generalization of work (Raffel et al. 2019). They replace the subsequence (or multiple subsequences) be predicted by a single token (not number of mask tokens equal to the length of the subsequence, as in MASS). Zhang al. 2019) additionally exploit the sentence structure of natural language. They suggest the pretraining task Pegasus, which masks out entire sentences of given text, and additionally masks out randomly selected tokens in the remaining text (or alternatively replace them by other tokens). In similar way Pegasus' exploitation of the sentence structure of natural language, our skip-tree task exploits the tree structure of formal expressions. Zhang et al. (2019) also suggest sampling the sentences to be masked with the help of ROUGEI-FI [in 2004).
pretraining tasks that is crucial to our
We work with the HOList dataset by Bansal et al. (019), which is closely related to the Flyspeck dataset by Kaliszyk and Urban (2014). There are other datasets which might be suitable for our approach as well, including proofs extracted from HOL4 (Gauthier et al. 2017), and from Coq (Huang
et al. 2019 Yang and Deng. 2019 Sanchez-Stern al. 2019)
2

---

Published as a conference paper at ICLR 2021
Most previous works that apply sequence-to-sequence models to logics have focused specific logical tasks in supervised training settings (e.g. Piotrowski and Urban (2000a)). In contrast, we train language models
self-supervised proxy task that does not requie labeled data and can thus be applied to almost any source of mathematical expressions. [aample and Charton (2020) Transformer model for symbolic integration. They train their model directly on the the task to produce the integral of a given expression. To generate training data, their approach needs classical algorithm compute the derivative of the expressions. [Finbbeiner et al. (2020) explore the generalization properties of the Transformer architecture predicting the solutions to SAT formulas and temporal logic, but require data generator that can solve formulas, which is currently not feasible for higher-order logic. Piotrowski et al. (2019) train RNNs on individual logical reasoning steps, such as substitutions, using a dataset rewrites on polynomials extracted from Prover9. Waan et al.) (2018) translate between synthetic descriptions in natural language and formal mathematics on
dataset generated with Mizar.
Self-supervised training techniques for formal mathematics have received much less attention. Wang ct al. (020) apply recent self-supervised translation techniques by Lample et al. (2018) to align formal and informal statements. Very recently, [i et al. (2020) and Polu and Sutskever (2020)
applied language modeling to proofs of formal mathematics. contrast, this work focuses on measuring reasoning abilities mathematical statements (not necessarily proofs) achieved through self-supervised training only.
Independently from our work, Urban and Jakubáy (2020) presented initial experiments applying self-supervised language modeling to formal mathematics in order to produce conjectures. However, they only evaluate the learned models through the truth of the produced conjectures, while also consider several reasoning tasks and measure the usefulness of conjectures. Earlier methods to produce conjectures were limited in scope. For example, Piotrowski and Urban (2020b) propose method to predict the next literal in an automated theorem prover using recurrent neural networks after supervised training. Prior to that Gauthier et al. (2016) relied only on statistical approaches to produce conjectures. Applying natural language techniques to formal mathematics has long history. Already in 2004, [Carns (2004) applied information retrieval based on latent semantics to improve over search for keywords, and Urban (2004) formulated the intention to learn from large amounts of data in formalized mathematics.
Transformer models for program understanding have focused providing inductive biases in the architecture (Shiv and Quirk] [2019] |Hellendoom et al. (2020,, whereas this work suggests to use a modified language modeling proxy task.
DATASET
We start from the HOList dataset introduced by Bansal et al. (2019). The complete dataset includes 29465 theorems and their proofs. We here consider only the "core" and "complex" datasets which comprise 18943 theorems, 637 definitions and 603,950 proof steps. The theorems and proofs were written (by humans) using the HOL Light proof assistant, and span various areas of mathematics such set theory, arithmetic, linear algebra, topology, and multivariate complex analysis. Each proof starts with the theorem statement as proof goal. For each goal, the dataset contains a tactic that a human applied it, which then produces a list of subgoals. Most tactics have arguments, such as previously proven theorems (also called premises). which are invoked by that tactic. From this dataset we extract all theorem statements as well as all intermediate proof goals.
We use S- S-expressions to represent statements. For example, consider y. which in s-expression syntax is represented follows:
(a (c (fun (A) (fun (A) (bool))) =) (v A))
(v
)
Each subexpression here is either leaf or a triple. The first element of these triples indicates their kind: a indicates function applications, c indicates constants (i.e. symbols that have been defined in the formal system), indicates a variable, and finally fun indicates a function type. The equality operator "=" is represented by (c (fun (A) (fun (A) (bool)) ) =), which indicates that it is constant that has type (Fun (A) (fun (A) (bool))) ). This type indicate it is a curried function with two arguments of arbitrary type, indicated by the generic type variable A, and returns a
bool. The variables and y represented (v x) and (v A y). The indicates that this
3

---

Published as a conference paper at ICLR 2021
Training
Validation
Testing
Theorem datahase
Proofs
Figure 1: We use the theorems and proofs of the training split, marked in green, for training. For measuring the final performance our evaluation tasks, we only used the theorems of the test set, marked in blue. This ensures that the models have never seen the statements from which the evaluation tasks are derived.
Fun
boot
bool
Encoder
Decoder
Original formula:
fun
bcol
) Fun bool
bool
Figure 2: The skip-tree training task for the example of the equality operator on boolean constants (original formula). In this example assume that a part of the type sampled to be the subexpression to be predicted, and that subexpression с was sampled to be masked out additionally. Note the input the decoder is shifted the right, such that the token prediction task yields the target sequence.
subexpression is variable, and A is type variable, which indicates that and could have any type. Since both x and y use the same type variable A, they must have the same type.
In our dataset, we wrap each S-expression derived from theorem in <theorem> node, and all other expression in a <goal> node. That is, an expression (c (fun ...) ...) is represented now as (<goal> (c (fun ...) )..)).
We use the same split as used in HOList (Bansal et al. 2019). They first split the theorems into training, validation, and test, and then assign all statements entire proof of each theorem the same split as the theorem. This means that we have used the proof of 11,655 theorems in the training split of the core and complex libraries. This avoids partially revealing the proofs of theorems in the validation and test sets during training. We derive all training data from the theorems and proofs in training set, and use only the theorems (not the proofs) for the evaluation tasks. This addresses possibility that some proof steps for training theorems and for validation theorems might be shared. In Figure [ we depict our choice training and evaluation data.
4 SKIP-TREE TRAINING
In this section we define the skip-tree training task. We parse given mathematical statement into tree of subexpressions, and replace one of the subexpressions by <PREDICT> token. The task is to predict the subexpression replaced by <PREDICT>. See Figure for an example.
For training, the trees converted back sequence of tokens; the target sequence is extended by a <START> token in the front and an <END> token in the back. We filter out training examples that
are derived from an input sequence that is longer than 10k characters as our models would only small prefix of the input sequence (encoder length is 1024 tokens), and
4

---

Published as a conference paper at ICLR 2021
exceed the length of the decoder (512 tokens).
While the second criterion drops only a negligible 0. 1 of the training examples, the first criterion drops around 32% of the training examples. We confirmed that not dropping those training examples does not significantly change the results (see the ablation study titled "unfiltered").
The evaluation sets were also filtered, but only 0.16% of the evaluation examples were dropped.
Additional masked subexpressions. In addition to the subexpression be masked out by <PREDICT>, we select & = 2 subexpressions to be masked out by a different mask token <MASK>, In contrast to the <PREDICT> token, we replace all occurrences of these subexpressions by the <MASK> token. Note that it can happen that the subexpressions we want to replace by the <MASK> tokens overlap with each other or with the subexpression replaced by the <PREDICT> token. this case, give the highest preference to the <PREDICT> token, and then in decreasing order of size for the expression be replaced by the <MASK> tokens.
The subexpressions masked by <MASK> do not have to be predicted, they only hidden. They make the model tolerant to having only partial information. As a side-effect masking out additional terms makes the tasks harder and shorter.
Distributions of subexpressions. Sampling subexpressions uniformly at random results in very short sequences to be predicted: since our trees are mostly ternary, two thirds of the subexpressions are leaves. Besides picking subexpressions uniformly at random, we thus experiment with weighting the subexpressions by the number of tokens they contain. We refer these variants as "uniform" and "weighted". This results in a much more diverse set of expressions to be sampled. The experiments show that this helps on some, but not all, tasks.
Multiple samples per statement. We generate up to 100 training examples from each statement the source data set by sampling different subexpressions to predict (and different <MASK> tokens). To avoid duplicates, sample the subexpressions to predict without replacement. For small formulas with less than 100 subexpressions, this reduced the number of training examples generate from them.
Our initial data, the core and complex corpus of HOList, consists of 604K mathematical statements, from which 376K statements in the training split. After sampling and filtering out training examples that do not fit the requirements listed in the beginning of this section, we are left with around 25.8M training examples. Table lists the statistics of the datasets and various ablations.
4.1 ABLATIONS
To verify the design choices of the skip-tree training task generated multiple variants of the training task and trained a model on each of them.
No mask tokens. To answer the question of whether it helps to mask out subexpressions besides the one to predict, generated a dataset with & O, called "skip-tree (no <MASK>)".
Fewer samples per statement. Instead of sampling many training examples from each formula, we could train on fewer training examples for more epochs. We generated smaller version with n 20 of the skip-tree training data, which we call "skip-tree (small)""
Skip-sequence. For natural language the state-of-the-art self-supervised training task for sequence- to-sequence models is the skip-sequence task (see MASS (Song et al. 2019). SpanBERT (Joshi et al.) 2020), and T5 (Raffel et al., 2019)). The skip-tree task is similar to the skip-sequence task. But instead of predicting arbitrary subsequences in the skip-sequence task, the skip-tree task makes sure that the subsequence to predict is a subexpression. For example, for the statement a + b= c + d, the skip-sequence task may select the subsequence "= c+", but the skip-tree task would only allow to pick valid subexpressions, such as "a + b". Our experiments will show that this subtle difference has a dramatic impact on the ability of our language models predict correct answers reasoning tasks. We generated three datasets for the skip-sequence task, where we sample subsequences of different lengths (shor//mediun/long) with lengths up to 50, 100, and 512 tokens.
5

---

Published as a conference paper at ICLR 2021
Dataset
examples
# tokens (input/output)
avg length (input/output)
Skip-tree (weighted)
25.8M
17.4B/1.6B
675/61
Skip-tree (uniform)
25.7M
18.8B/316N
732/12
Skip-tree (small)
5.2M
3.5B/521M
673/100
Skip-tree (unfiltered)
37.4M
30.6B/3. 1B
817/83
Skip-tree (no <MASK>)
25.8M
19.4B/1.6 6BB.6666
750/61
Skip-sequence (long)
19.2M
11.9B/2.8B
620/ 146
Skip-sequence (medium)
26.0M
19.4B/884M
744/34
Skip-sequence (short)
26.0M
19.6B/479M
752/18
Table I:
Basic statistics of the training splits of the data sets. Number of tokens in the training set measured before padding.
Unfiltered. While generating the training data, we filtered out mathematical statements that exceed 10k characters. This removed some 32% of the statements from the HOList corpus. In this ablation study we removed this filter and train on the full corpus.
EVALUATION TASKS
In this section suggest several logical reasoning tasks which language models be evaluated. These tasks require different levels of logical reasoning, ranging from mostly mechanical tasks, such type inference, more creative tasks, such as predicting missing assumptions. We intentionally define them to have the same format as the training task, i.e. predict a missing part of a larger expression, as this allows us to test models without fine-tuning.
However, the evaluation tasks are out-of-distribution in two ways: First, we generate them from the theorems (excluding proofs) from the validation/test sets. This ensures that the model has never seen the theorems from which we generated these evaluation tasks, nor has it seen the proofs of these theorems. This makes the tasks more challenging, and forces the models go beyond memorization. Second, we mask out very specific elements, such as types and assumptions. This makes the results on the evaluation tasks easier to interpret. To give the interested reader better impression of the evaluation tasks, we provide list of randomly selected examples in Appendix E
Type Inference. We generate type inference problems by omitting the typing annotation of vari- ables, constants, and babbrrdtiassstaaiinnnn... We generated two variants: In the task we call "Type Inference," we replace only the selected type by the <PREDICT> token and do not mask out anything else. In the second variant we name "Hard Type Inference." " additionally replace all other types by the <MASK> token. The two tasks loosely correspond to the deriving the first and the last type during type inference.
Consider the following example of "Type Inference" evaluation task:
(a (a (c <PREDICT> =) A x)) (v y))
The type of the equality operator is uniquely defined, given the types of the two subterms of the equation. this example the type could have been computed by a classical type inference algorithm.
For the "Hard Type Inference" evaluation task, the input could look as follows:
(a (a (c <PREDICT> Now, the type inference task is highly ambiguous. In fact, variable x could have any type, and the equality operator would have to adapt to the type of its arguments accordingly.
(v <MASK>
(v <MASK> y)
Assumptions. This evaluation task is to predict missing assumptions for theorems in the validation set. We extract these tasks by searching for "top-level implications" and replacing their left operand by the <PREDICT> token. We define implication operator "=" in expression to be top-level implication it is either the top-most operator the expression, or occurs only under quantifiers, conjunctions, disjunctions,
the right side of other top-level implications. This definition helps us to avoid picking assumptions in negated parts of formulas.
Note that have multiple top-level implications per validation theorem. Consider the abstracted example (a + b) A (c + (d + e)). In this case, a, c, and are considered to be assumptions of top-level implications.

---

Published as a conference paper at ICLR 2021
An example from the theorem database is z =
y. for which the task is to predict I = y given <PREDICT> > + I = a + y. (We omit the presentation of this example as an s-expression for the sake of readability.) At first, the expression to predict in this case may seem unique, but there are actually many ways to complete the task into a true statement; e.g. = x or 0 A y 0. Still, most humans would likely guess x = y as it is simple and general, and because occurs before y in the alphabet. To make a correct prediction, our language models thus have to not only reason which which statements are likely correct answer, but also needs to find reasonably general statement and also know about naming conventions.
Below we give some examples of this reasoning task that we selected for their simplicity. (For a representative selection, see Appendix E While it is often easy to "see" that a given solution to such a task is correct, it can non-trivial to come up with solution in the first place. We encourage the reader to make their own predictions before looking up the ground truth in Appendix C
<PREDICT> = (x){ = 9
<PREDICT> = (x1/y1 = x2/y2 + x1 * y2 x2 x22xy1
<PREDICT>> = (s + (bv x1) A (bV z0))
Equalities. Similar to the task of predicting missing assumptions, we ask to predict one side of top-level equality in this task. Again, we define top-level equalíties to be any equality that occurs as the top-level operator of the formula or occurs inside quantifiers, conjunctions. disjunctions, or on the right side of implications. For example, from the theorem Vx.I = (x = True) we extract two evaluation examples: Vz. <PREDICT> (r True) and Vz. x <PREDICT>.
Again, we present some simple example tasks (in human-readable notation) and provide the ground truth as well as the model predictions in Appendix C
Vx,n N: (x" 1) = <PREDICT>
Vm, m
m = m + <PREDICT>
W;m: <PREDICT>> = APPEND (REVERSEE)))))( REVERSE(()
RESULTS AND DISCUSSION
In language modeling for natural language of the key metries is how often the next token in the ground truth is correctly predicted. This is not an ideal measurement for formal mathematics as even single incorrect token can invalidate the entire statement. Also, the S-expression representation is relatively lengthy and barely human-readable, so a token-level measurement does not allow us to compare our models the natural language models in any case. In the first part of our evaluation we therefore focus on exact (i.e. syntactic) matches of the entire predicted statement.
We trained Transformer architecture on the skip-tree dataset and each of the ablations for up to 1M steps (=parameter updates) with a batch size of 256. This means our models are trained for about 10 epochs (depending on dataset size). Our models have 39M trainable parameters; the hyperparameters are specified in the appendix. We trained them on an 8x8 TPU configuration, which equates to 128 cores. The training runs took between and 15 hours, depending on the average length of the output sequences, which translates to up to 1.4 and 4.2 PetaFL.OPs days per training run.
We measured each evaluation task on 1000 samples. The evaluation was performed on CPUs in a cloud computing framework on recent CPU architectures. Depending on the average length of the output sequences this required a different amounts of resources: (regular and hard) type inference took 4 CPU hours, equality completion took 24 CPU hours, missing assumption took 43 CPU hours. The average prediction time per token on CPU is around 60 milliseconds. Each evaluation task was repeated every 50k training steps on 1000 freshly sampled examples of the validation set. We then picked the best checkpoint (based on the results on the validation data) and evaluated it on the test set. In Table we present the results of this experiment.
Skip-tree vs skip-sequence. The skip-tree task and its ablations clearly dominate the skip-sequene task. One major difference between skip-tree and skip-sequence tasks is the lack of <MASK> tokens in the skip-sequence task. We therefore have to compare its performance to the "Skip-tree (no
7

---

Published as a conference paper at ICLR 2021
Dataset
Type Inference
Hard Type Inference
Assumptions
Equalities
Skip-tree (weighted)
96.7%
94.0%
43.9%
47.4%
Skip-tree (uniform)
96.3% %
94.2%
31.3%
37.7%
Skip-tree (small)
96.2%
90.6%
39.3%
36.6%
Skip-tree (unfiltered)
95.8%
94.3%
42.9%
47.9%
Skip-tree (no <MASK>)
95.8%
20.8%
42.5%
45.9%
Skip-sequence (long)
12.6%
0.0%
1.5%
1.0%
Skip-sequence (medium)
66.7%
6.6%
8.0%
9.9%
Skip-sequence (short)
87.3%
12.6%
3.1%
9.0%
Table Success rate of predicting the ground truth in beam search of width after training a model on various datasets. Bold numbers indicate results that are within 0.5% of the best result. Grayed out values indicate experiments where the training data did not include the <MASK> token but the evaluation did.
<MASK>)" ablation study get a fair picture. The length of the skipped sequences appears to play a substantial role, with the Skip-sequence (medium), masking out sequences of up to length 100, performing best. A manual inspection of the predictions of the skip-sequence models showed they rarely parse or typecheck. seems that the skip-sequent models consistently add surplus tokens at the end, or stop expressions too early; they appear be unable correctly identify the end of the expression.
Impact of <MASK> tokens. Hard Type Inference is the only evaluation task that contains the <MASK> token. Models trained on datasets without the <MASK> token perform poorly here (see grayed-out numbers T The presence or absence of <MASK> tokens has only a minor impact the other, <MASK>"".
observe through the comparison of "Skip-tree (weighted)" and "Skip-tree (no
Multiple samples per statement. For each source statement in the HOList corpus we sampled 100 subexpressions be masked out. Lowering n to 20 significantly decreased the performance, as we can see in the comparison between "Skip-tree (small)" and "Skip-tree (weighted)", Sampling many subexpressions per source statement appears be a good way to increase the number of training examples from limited source data.
Uniform vs weighted sampling, Sampling subexpressions weighted by their size in the skip-tree task significantly improves the performance on the harder tasks, missing assumptions and equality completion. On the Type Inference tasks, the performance is very similar. We conjecture this is because of the average size of the terms predict is smaller for the uniform sampling strategy, which is more similar to the average size of the types to predict.
6.1 CONJECTURING
In the experiments above, we measured how often the models predicted the ground truth in the evaluation tasks. We now change our point of view, and examine whether the models can be used to generate new and useful conjectures. In the following, Assumptions and Equalities tasks in Table and we introduce a new task, which we call free-form conjecturing.
analyze all statements produced in the
For free-form conjecturing we simply ask the model produce theorems by presenting the input sequence (the "prompt")) (<theorem> <PREDICT>). The subexpression the models has to fill in is thus an entire theorem. We use beam search with beam width 1024 to produce enough outputs for meaningful evaluation.
How often are predictions true and new? For this measurement, we attempt to prove the conjec- tured statements with the DeepHOL theorem prover (Bansal et al. 2019). This gives us a lower bound to the number of true statements, as the version of the DeepHOL theorem prover used here can prove around 58% of the validation theorems. So we expect the estimates here to be considerably below the number of actually true statements, In Table we report two numbers for each conjecturing task: The first number the percentage of generated statements known to be provable, including exact matches, statements from the training set, and statements provable with DeepHOL.. The second number is the
8

---

Published as a conference paper at ICLR 2021
Dataset
Assumptions
Equalities
Free-form Conjecturing
Skip-tree (uniform)
30.30%
16.73%/13.72%%
60.16% 44.73%
Skip-tree (weighted)
29.49%/25.60%
17.38%/13.64%%
Table 3: Percentage of "provable statements"""provablee new statements". The type inference tasks are not included as we are only interested in the predictions that do not match the ground truth. For the type inference tasks, these statements are either semantically equivalent existing statements or statements that do not type check.
percentage of generated statements that are provable and new - excluding exact (syntactic) matches with the ground truth and statements from the training set.
We believe that these measurements show a significant bias towards true statements. While some tasks, less than half of the statements were provable, there many more ways write false statement than a true statement.
Are the conjectures useful? For some evaluation tasks, the models could "cheat" on the truth metric by making the statements trivially true. For example, the models can predict False as an assumption, or complete the missing part of an equation by making it an identity (e.g. complete <PREDICT> by predicting x). In fact, manual inspection revealed several such cases.
To make this measurable, we added the provable statements to the theorem database, and ran the reinforcement learning experiments of the DeepHOL theorem prover (Bansal al. 2019) and then measured how many of the statements were used as premises. In this experiment we also make sure that the new theorems cannot be used in the proofs of their premises. In a "pruning" step DeepHOL minimizes proofs by removing each individual premise in proof and checking if the proof still holds. This filters out statements that have no effect on the proof. Only the premises that survive this step are classified as uveful.
We ran three reinforcement learning experiments, one for each set conjectures produced by one the evaluation tasks. We then measured how many of the theorems generated by each task are used as premise in one of the over 200,000 proofs found for each of the experiments. For the assumptions task, 505 of the 813 theorems were used at least once. For the equalities task and the free-form conjectures it was 831 out of 1811 I and 54 out 172, respectively. We provide usage histograms in Appendix B While some of the most frequently used conjectures turned out to be alpha-equivalent to existing theorems in the database, we found some interesting examples among the most used conjectures produced:
b =
COUNTABLE((S(N) Ine
Vf.s: (Vz: (VI: =(z)= = integrabll__nn
In fact, humans have used the first conjectured theorem over vector arithmetic in many proofs. However, this theorem has always been defined as a local lemma and thus did not make it into the theorem database. For theorems two and three in the list above, thorough manual search has revealed no closely related statement in the theorem database.
This suggest that self- supervised language models show some ability to produce new, useful conjec- tures, even without fine tuning or specialized training.
7 CONCLUSION
In this work, we applied the paradigms of self-supervised language modeling to formal mathematics and show that, surprisingly, this leads to mathematical reasoning capabilities. For training, we introduced a novel self-supervised skip-tree task for formal mathematics that outperforms existing training tasks used for natural language. We also suggested several evaluation tasks for measuring mathematical reasoning capabilities of language models for formal mathematics without the need of fine tuning. Finally, we explored the ability of language models to produce new conjectures by measuring how many of the new predictions are provable and useful for proving other theorems.

---

Published as a conference paper at ICLR 2021
REFERENCES
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulike 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, 4-9 December 2017, Long Beach, CA, USA, pages 5998-6000 2017. nips wwwpppppppp..ccccccc..ppp..p...a 7181 - Contentioonin is-a you need
URL
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and llya Sutskever. Language models are unsupervised multitask learners. In OpenAl Blog, 2018. URL
http://www..lllooooooooeeeeeeeee Language_modes models are wttee_sssueeriise_meeeeeeee cacrrd_multttaa wew.aasssseaaraeep.ppco
Jacob Devlin, Ming- Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: Pre-training of deep bidirectional transformers for language understanding. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguisties: Human Language Technologies, Volume 1 (Long and Short Papers), pages 4171-4186, 2019.
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert- Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners, 2020. URL https 7/arxiv. org/ abs / 2005. 14165
Kshitij Bansal, Sarah M Loos, Markus N Rabe. Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher-order theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICMI. 2019, 9-15 June 2019, Long Beach, California, USA, volume of Proceedings of Machine Learning Research, pages 454 463. PMLR, 2019. URL pdf
mlr.
John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Pulo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1166 of Lecture Notes in Computer Science, pages 265-269 Springer, 1996. URL https:://ti...... org.
10.1007/BFb003179
Kshitij Bansal, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Viktor Toman. Learning to reason in large theories without imitation, 2020.
Jingqing Zhang, Yao Zhao, Mohammad Saleh, and Peter J. Liu. PEGASUS: pre-training with extracted gap-sentences for abstractive summarization. CoRR, abs/1912.08777, 2019. URL
08777
Kaitao Song, Xu Tan, Tao Qin, Jianfeng Lu, and Tie- Yan Liu. MASS: masked sequence to sequence pre-training for language generation. In Kamalika Chaudhuri and Ruslan Salakhutdinov, edi- tors, Proceedings of the 36th International Conference on Machine Learning, ICMI 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Re- search, pages 5926-5936 PMLR, 2019. URL httt:://pocceedinnngee .mr..ngssmmmrrr...mmmm. www.mmm.....m..... preas/v97/ song19d. html
Li Dong, Nan Yang, Wenhui Wang, Furu Wei, Xiaodong Liu, Yu Wang, Jianfeng Gao, Ming Zhou, and Hsiao- Hon. Unified language model pre-training for natural language understanding and generation. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d' Alché Buc, Emily B. Fox, and Roman Gamett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, 8-14 December 2019, Vancouver, BC, Canada, pages 13042-13054, 2019.
10

---

Published as a conference paper at ICLR 2021
Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J. Liu. Exploring the limits of transfer learning with a unified ext-to-text transformer. CoRR, abs/1910..00000 2019. URL htattt://axxiiii org.///iiirrr.ooooooo abs/ 1910. 10683
Alexis Conneau and Guillaume Lample. Cross-lingual language model pretraining. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence Alché-Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NewrIPS 2019, 8-14 December 2019, Van-
www.:iipppppp..eeeeeeee cc/paper/ couver. BC, Canada, pages 7057-7067, 2019. URL httt:::/pppppoo/ httpp/ppppsppppa.pa.ppppppppapap
8928 11228-rross--ingge Laagguaaaaa-agggag----a- mode -ww.oddepppeetttannn
Mandar Joshi, Danqi Chen, Yinhan Liu, Daniel Weld, Luke Zettlemoyer, and Omer Levy. Spanbert: Improving pre- training by representing and predicting spans. Transactions of the Association
for Computational Linguistics, 8:64-77, 2020. doi: 10.1162/aa11 URL https
7/doi. oro.orrg//o.. 1ttooooo//...11//////11
00300
Chin- Yew Lin. ROUGE: A package for automatic evaluation of summaries. In Text Summariza- tion Branches Out, pages 74 81, Barcelona, Spain, July 2004. Association for Computational Linguistics. URL https::////. www. wwwp://wwww.....///tt..ooooooo/.
Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with flyspeck. Journal of Automated Reasoning, 53(2):173-213 2014.
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Toe: Learning to reason with HOL4 tactics. Thomas Eiter and David Sands, editors, LPAR-21, 21st International Conference Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7- 12, 2017, volume 46 of EPiC Series in Computing, pages 125-143 EasyChair, 2017. URL https: /tss:///asyccaaaa T. www.oorgpppu icat ions/ centtiinssolllon vml LPAR-21
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL htttps::/oppnrreeett
n iddz 1xWKKYYY
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 6984-6994, PMLR, 2019. URL htttp::/prrcceeding ngs mlr. ptwss/ waaaaglla//a hal.laaaaygggga...a...
Alex Sanchez-Ster,, Yousef Alhessi, Lawrence Saul, and Sorin Lerner Generating correctness proofs 1907
with neural networks. CoRR, abs/1907.07794, 2019. URL
07794
Bartosz Piotrowski and Josef Urban. Stateful premise selection by recurrent neural networks. In Elvira Albert and Laura Kováes, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 409-422, EasyChair, 2020a.
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. 8th International Conference Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 30,30, 2020. OpenReview.net, 2020. URL
net/ net/forummid:
Bernd Finkbeiner, Christopher Hahn, Markus N. Rabe, and Frederik Schmitt. Teaching temporal logics to neural networks. CoRR, abs/2003.0422 042118, 2020. UtL/pttpa///axxxv.orr
2003.00 04218
Bartosz Piotrowski, Josef Urban, Chad E Brown, and Cezary Kaliszyk. Can neural networks learn symbolic rewriting? In Conference on Artificial Intelligence and Theorem Proving, 2019.
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In International Conference on Intelligent Computer Mathematics, pages 255-270, 2018.
11

---

Published as a conference paper at ICLR 2021
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in Mizar. In Proceedings of the 9th ACM SIGPLAN International Conference Certified Programs and Proofs, pages 85-98, 2020.
Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc' Aurelio Ranzato. Unsupervised machine translation using monolingual corpora only. In International Conference on Learning Representations, 2018.
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Modelling high-level mathematical reasoning in mechanised declarative proofs. In arXiv 2006.09265, 2020.
Stanislas Polu and Iya Sutskever. Generative language modeling for automated theorem proving, 2020.
Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In Conference on Intelligent Computer Mathematics, 2020.
Bartosz Piotrowski and Josef Urban. Guiding inferences in connection tableau by recurrent neural networks. In Christoph Benzmüller and Bruce Miller, editors, Intelligent Computer Muthematics, pages 309-314, Cham, 2020b. Springer International Publishing. ISBN 978-3-030-53518--
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Initial experiments with statistical conjecturing over large formal corpora. In CICM 2016 Work in Progress Proceedings 1785, pages 219-222 2016.
Paul Cairns. Informalising formal mathematics: Searching the mizar library with latent semantics. In International Conference on Mathematical Knowledge Management, pages 58-72. Springer, 2004.
Josef Urban. motiiviniv,,,,, implementation, first experiments. Journal of Automated Reasoning, 33(3-4):319-339, 2004.
Vighnesh Leonardo Shiv and Chris Quirk. Novel positional encodings to enable tree- based transformers. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d' d'Alché-But Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Informa- tion Processing Systems 2019, NeurIPS 2019, 8-14 December 2019, Vancouver, BC, Canada. pages 10088-20068,
URL http://papers: nips. wttpsccccc..ccre 9376-novel-pose 23gg:paeeppoLLaaaaaaooooooooooo-
2019.
Vincent J. Hellendoorn, Charles Sutton, Rishabh Singh, Petros Maniatis, and David Bieber. Global relational models of source code. In 8th International Conference on Learning Representations,
ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL https
//openreview net/ ftrumfid-ippppeee InbbRNWw
12

---

Published as a conference paper at ICLR 2021
A HYPERPARAMETERS
We trained the Transformer models for the skip-tree tasks with these hyperparameters:
vocabulary size: 1200
embedding size: 128
attention dropout: 0.1
nonlinearity: gelu
hidden layer dropout: 0.1
hidden layer size: 512
initializer range: 0.02
intermediate size: 2048
number of attention heads: 8
number of hidden layers encoder:
number of hidden layers in decoder: 4
learning rate: le-4
We settled with these hyperparameters after trying various alternatives. We explored encoders and decoders with up 12 layers and various learning rates and intermediate sizes.
B USAGE STATISTICS OF CONJECTURES
10
19
Figure 3: Histograms of premise usage of the conjectures generated through the assumptions task (left), the equality task (middle), and through free-form conjecturing (right). X-axes are the new theorems, sorted by number of usages. Y-axes indicate the number of usages log scale.
C A CLOSE LOOK AT SIMPLE EXAMPLE TASKS
Assumptions. In Section presented the following three examples of the task to predict missing assumptions. For the sake of readability here discuss only the pretty printed versions. For examples in s-expression syntax, please visit Appendix
<PREDICT> = (g) {8))
<REDDIC>> = (xl/yl= = x2/y2 + xl x1 = x2 yl)
<PREDICT>> (a (bVxl) A (bV z0))
The ground truth answers follows:
((s E g)
0 <l A < y2. note that 0 * yl A + y2 would be more general assumption.
((b e Fa ralss) = (x + .0)) (b True) (x: + x1)
We prompted one of our skip-tree models with these tasks. For the second and the third task, the model "skip-tree (weighted)" makes correct prediction in the top candidates in beam search of width 8. For the first task, the model mostly produces incorrectly typed expressions: it appears to think that is set of the same type as g.
13

---

Published as a conference paper at ICLR 2021
Equalities.
We presented these examples for the equality evaluation task:
Vx, n E N: (x" = 1) - <PREDICT>
Vm, n: : n E m + m n = <PREDICT>
ll, m: <PREDICT> APPEND (REVERSE(M), REVERSE(I)
The ground truth for the tasks is:
T = =
m
REVERSE(APPEND((. m))
Examples two and three are predicted correctly in beam search with beam width 8. For the first example, the model almost gets it correct in two of the 8 attempts: x = -vn-= 1, and x 0V 1. We find it surprising that the model apparently understands that there two cases to consider, but that the exact combination of constants (1 and 0) is challenge.
D MODEL PERFORMANCE BY TRAINING STEP
In Figure we can see the performance of the model throughout training. We can see that the performance validation and test is very similar, but that there is some variance. We also observe that even after 1M steps, the model has apparently not quite converged.
0.5
0.5
0.3
0.3
0.2
0.1
0.1
200K
400K
600K
800K
1V
200K
4C0K
600k
80Ck
1M
Figure 4: Performance on the Missing Assumptions task a model trained on the Skip-tree (weighted) task. Y-axis is the training steps and X-axis is the model performance the ratio of correctly predicted examples. Left: validation data. Right: test data.
E RANDOMLY SELECTED EXAMPLE TASKS
In the following, we provide list of examples for each of the evaluation tasks, sampled uniformly at random.
Type Inference.
(<theorem> (c <PREDICT> !) (1 (v (fun (cart (real) ?1)
(bool)) t) (a (c (fun (fun (fun (cart (real) ?1) (bool))
(bool)) (bool)) !) (1 (fun (cart (real) ?1) (bool)) u)
(a (a (c (fun (bool) (fun (bool) (bool))) ==>) (a (a (c (fun (bool) (fun (bool) (bool))) A) (a (c (fun (fun (cart (real) ?1) (bool)) (bool)) !) (1 (v (cart (real) ?1) b) (a (a (a (fun (bool) (fun (bool) (bool))) V) (a (c (fun (fun (cart (real) ?1) (bool)) (bool)) ?) (1 (v (cart (real) ?1) w) (a (a (c (fun (bool) (fun (bool) (bool))) A) (a (a (c (fun (cart (real) ?1) (fun (fun (cart (real) ?1) (bool))
(bool))) IN). (v (cart (real) ?1) w)) (v (fun (cart (real) 21) (bool)) t))) (a (a (c (fun (cart (real) ?1) (fun (fun
14

---

Published as a conference paper at ICLR 2021
(cart (real) 21) (bool)) (bool))) IN) (v (cart (real) ?1)
W)) (a (c (fun (prod (cart (real) ?1) (real)) (fun (cart
(real) ?1) (bool))) ball) (a (a (c (fun (cart (real) ?1)
(fun (real) (prod (cart (real) ?1) (real)))) ,) (v (cart
(real) ?1) b)) (a (c (fun (num) (real)) real_of_
(a (c
(fun (num) (num)) ) NUMERAL) (a (c (fun (num) (num) BIT1)
(c (num) _))))))))))>>> (a (c (fun (fun (cart (real) ?1)
(bool)) (bool)) ?) (1 (V (cart (real) ?1) w) (a (a (c (fun (bool) (fun (bool) (bool))) A) (a (a (c (fun (cart (real)
21) (fun (fun (cart (real) ?1) (bool)) (bool))) IN) (v (cart (real) ?1) w) (v (fun (cart (real) ?1), (bool)) u))) (a (a (c (fun (cart (real) ?1) (fun (fum (cart (real) 31) (bool)) (bool))) IN) (v (cart (real) ?1) w)) (a (c (fun (prod (cart (real) ?1) (real)) (fun (cart (real) ?1) (bool))) ball) (a (a (c (fun (cart (real) ?1) (fun (real) (prod (cart (real) 21) (real)))) ,) (v (cart (real) ?1) b)) (a (c (fun (num) (real)) real_of_num) (a (c (fun (num) (num) NUMERAL) (a (c (fun (num) (num)) BITI) (c (num) <01)))))>>>>>> (a (c (fun (fun ?0 (bool)) (bool)) !) (1 (v ?0 x) (a (a (c (fun (bool) (fun (bool) (bool))) ==>) (a (a (c (fun 70 (fun (fun 20 (bool)) (bool))) IN) (v ?0 x)) (v (fun ?0 (bool)) d))) (a (c (fun (bool) (bool)) ~) (a (a (c (fun (cart (real)
?1) (fun (fun (cart (real) ?1) (bool)) (bool))) IN) (a (v (fun 20 (cart (real) ?1)) g) (v ?0 x))) (a (a (c (fun (fun (cart (real) ?1) (bool)) (fun (fun (cart (real) ?1) (bool)) (fun (cart (real) ?1) (bool)))) UNION) (v (fun (cart (real) 21) (bool)) t)) (v (fun (cart (real) 21) (bool)) 1))1))
(a (c (fun (bool) (bool)) ~) (a (c (fun (fun (cart (real)
21) (bool)) (bool)) ?) (1 (v (cart (real) ?1) b) (a (a (c
(fun (fun (cart (real) 21) (bool)) (fun (fun (cart (real)
211 (bool)) (bool))) SUBSET) (a (c (fun (prod (cart (real)
?1) (real)) (fun (cart (real) ?1) (bool))) ball) (a (a
(c (fun (cart (real) ?1) (fun (real) (prod (cart (real)
21) (real)))) ,) (v (cart (real) ?1) b)) (a (c (fun (num) (real)) real_of_num) (a (c (fun (num) (num)) NUMERAL) (a (c (fun (num) (num) ) BITI) (c (num) _0))))))} (a (a (c (fun (fun ?0 (cart (real) ?1)) (fun (fun 70 (bool)) (fun (cart (real) ?1) (bool)))) IMAGE) (v (fun ?0 (cart (real) 21)) g))
(v (fun 20 (bool)) d))))))))))))
Ground truth: <START> (Eun (fun (fun (cart (real) ?1) (bool))
(bool)) (bool)) <END>
w IN ball Source theorem pretty printed: !t u. (lb. (?w. W IN t A
(b, (1)) V (?w. w IN A IN ball (b, (0))) A (!x. x IN d ==> ~ (g x IN t UNION ) ==> (?b. ball (b, &1) SUBSET IMAGE g d)
(<theorem> (bool)) 5) (a (a (c (fun (bool) (fun (bool) (bool))) =) (a (c (fun (fun (cart (real) N) (bool)) (bool)) is intervvall (a (a (c (fun (fun (cart (real) N) (cart (real) N)) (fun (fun (cart (real) N) (bool)) (fun (cart (real) N) (bool))))
(c <PREDICT> !) (1 (v (fun (cart (real) N)
ImAGE) (c (fun (cart (real) N) (cart (real) N)) vector_neg) (v (fun (cart (real) N) (bool)) s))) (a (c (fun (fun (cart (real) N) (bool)) (bool)) is_interval) (v (fun (cart (real)
N) (bool)) })))))}
Ground truth: <START> (fun (fun (fun (cart (real) N) (bool))
(bool)) (bool)) <END>
Source theorem pretty printed: !s. is_interval (IMAGE (-) s) <=>
is ssinterrall 8
15

---

Published as a conference paper at ICLR 2021
(<theorem> (a (c (fun (fun (real) (bool)) (bool)) !) (1 (v (real) x) (a (a (a (c (fun (fun (real) (real)) (fun (real) (fun (net (real)) (bool)))) mas_real_dee derivatieee (c (fun (real) (real)) atn)) (a (c (fun (real) (real)) real_inv) (a (a (a (fun (real) (fun (real) (real))) real_add) (a (c (fun (num) (real)) real_of_nuue
(a (c (fun (num) (num) NUMERAL)
(a (c (fun (num) (num) ) BIT1) (c (num) _0)))) (a (a (c (fun (real) (fun (num) (zeal))) real_pow) (V <FREDICT>>>> x) (a (c (fun (num) (num) NUMERAL) (a (c (fun (num) (num) BITO) (a (c (fun (num) (num) BIT1) (c (num) _01))))) (a (c (fun (real) (net (real))) atreal) (v (real) x))))
Ground truth: <START> (real) <END>
Source theorem pretty printed: !x. (atn has real_ derivative inv (&l + x pow 2)) (atreal x)
(<theorem> (a (a (c (fun (fun ?0 (bool)) (fun (fun 20
(bool)) (bool))) -) (a (c (fun (fun ?0 (bool)) (fun (fun ?0 (bool)) (fun ?0 (bool)))) INTER) (v (fun ?0 (bool)) s)} (a (a (c (fun (fun 20 (bool)) (fun (fun ?0 (bool)) (fun ?0 (bool)))) UNION) (v (fun ?0 (bool)) t)) (v (fun ?0 (bool)) ()))) (a (a (c (fun (fun 20 (bool)) (fun (fun ?0 (bool)) (fun ?0 (bool)))) UnIoN) (a (a (a <PREDICT> INTER) (v (fun 20 (bool)) s)) (v (fun 20 (bool)) t))) (a (a (c (fun (fun 20 (bool)) (fun (fun 20 (bool)) (fun ?0 (bool)))) INTER) (v
(fun 20 (bool)) s)) (v (fun ?0 (bool)) ))))))
Ground truth: <START> (fun (fun ?0 (bool)) (fun (fun ?0 (bool))
(fun 20 (bool)))) <END>
Source theorem pretty printed: s INTER (t UNION u) = INTER t UNION INTER
(<theorem> (a (a (c (fun (real) (fun (real) (bool))) =) (a (c (fun (cart (real) ?0) (real)) infnorm) (a (c (fun (num) (cart (real) )0)) vec) (a (c (fun (num) (num) NUMERAL) (c (num) _0))) (a (c (fun (num) (real)) real_of_nenl (a (c (fun (num) (num) NUMERAL) (c <PREDICT> _())))>
Ground truth: <START> (num) <END>
Source theorem pretty printed: infnorm (vec 0) &0
Hard Type Inference.
(<theorem> (a (C <MASK> !) (1 (v <MASK> 8) (a (a (c <MASK>
=) (a (a <MASK> INTERS) (v <MASK> 8) (a (a (c <PREDICT>
DIFF) (C <MASK> UNIV)) (a (c <MASK> UNIONS) (a (c <MASK>
GSPEC) (1 (v <MASK> GENSPVARSO) (a (c <MASK> ?) (1 (v
<MASK> t) (a (a (a (c <MASK> SETSPEC) (v <MASK> GENSPVAREC))
(a (a (c <MASK> IN) (v <MASK> t)) (v <MASK> s))) (a (a (c
<MASK> DIFF) (c <MASK> UNIV) (v <MASK> t))))11)))))))
Ground truth: <START> (fun (fun ?0 (bool)) (fun (fun ?0 (bool))
(fun ?0 (bool)))) <END>
Source theorem pretty printed: !s. INTERS DIFF t t IN s)
(:20) DIFF UNIONS ((:20)
(<theorem> (a (c <MASK> !) (1 (v <MASK> f) (a (c <MASK>
!) (1 (v <MASK> s) (a (a (C <MASK> =) (a (a (c <MASK> mniformly_continuuue
(v <MASK> f)) (v <MASK> s)l) (a
(c <MASK> !) (1 (v <MASK> e) (a (a (c <MASK> ==>) (a (a
(c <MASK> real it) (a (C <MASK> real of num) (a (c <MASK>
NUMERAL) (c <MASK> _0)))) (v <MASK> e))) (a (c <MASK> ?) (1
(v <MASK> d) (a (a (c <MASK> A) (a (a (c <MASK> real [a]]]t)
16

---

Published as a conference paper at ICLR 2021
(a (c <MASK> real of num) (a (c <MASK> NUMERAL) (C <MASK>
_))) (v <MASK> d) (a (c <MASK> !) (1 (V <MASK> t) (a
(c <MASK> !) (1 (v <MASK> t') (a (a (c <MASK> ==>) (a (a
(c <MASK> A) (a (a (c <MASX> SUBSET) (v <MASK> t)) (v <MASK>
8))) (a (a (c <MASK> A) (a (a (c <MASK> SUBSET) (v <PREDICT>
t()) (v <MASK> s))) (a (a (c <MASK> A) (a (c <MASK> bounded)
(v <MASK> t))) (a (a (c <MASK> A) (a (c <MASK> bounded) (v
<MASK> t())) (a (a (c <MASK> real_it) (a (c <MASK> hausdist)
(a (a (c <MASK> ,) (v <MASK> t()) (v <MASK> t))) (v <MASK>
d))))))) (a (a (c <MASK> real_lt) (a (c <MASK> hausdist)
(a (a (c <MASK> ,) (a (a (c <MASK> IMAGE) (v <MASK> f)) (v
<MASK> t())) (a (a (c <MASK> IMAGE) (v <MASK> f)) (v <MASK>
))))) (V <MASK> (
Ground truth: <START> (fun (cart (real) M) (bool)) <END> Source theorem pretty printed: s. f infformlyccontinuuussuoo
s
<-> (!e. &0 < --> (?d. &
(!t t'. t SUBSET s A t'
SUBSET A bounded t A bounded t' A hausdist (t',t) < d -=>
hausdist (IMAGE f t', IMAGE f t) < ))))
(<theorem> (a (a (c <MASK> -->) (a (a (c <PREDICT> IN) (v <MASK> a)) (v <MASK> 8))) (a (a (c <MASK> -) (a (a (c <MASK> DIFF) (a (a (c <MASK> INSERT) (v <MASK> a)) (a (a (c <MASK> DELETE) (V <MASK> t)) (v <MASK> b))) (v <MASK> s))) (a (a
(c <MASK> DELETE) (a (a (c <MASK> DIFF) (v <MASK> t)) (v
<MASK> )) (v <MASK> b))))
Ground truth: <START> (fun ?0 (fun (fun ?0 (bool)) (bool)))
<END>
Source theorem pretty printed: a IN S ==> a INSERT (t DELETE b) DIFF s
= (t DIFF s) DELETE b
(<theorem> (a (c <MASK> !) (1 (v <PREDICT> b) (a (c <MASK>
convex) (a (c <MASK> GSPEC) (1 (v <MASK> GENSPVARSO) (a (c
<MASK> ?) (1 (v <MASK> z) (a (a (a (c <MASK> SETSPEC) (v
<MASK> GENSPVARSC)) (a (a (c <MASK> real_gti (a (c <MASK> Im) (v <MASK> 2))) (v <MASK> b))) (v <MASK> 2)1)))1))))
Ground truth: <START> (real) <END>
Source theorem pretty printed: !b. convex {2 Im 2 > b)
(<theorem> (a (c <MASK> !)
(1 (v <MASK> x) (a (a (c <MASK>
==>) (a (c <MASK> ~) (a (a (c <MASK> nadd_eg _eq) (v <MASK> x))
(a (c <MASK> nadd of num) (a (c <MASK> NUMERAL) (c <MASK>
_o)))))) (a (c <MASK> ?) (1 (V <MASK> B) (a (c <MASK> ?)
(1 (v <MASK> N) (a (c <MASK> !) (1 (v <MASK> m) (a (c
<MASK> !) (1 (v <MASK> n) (a (a (c <MASK> ==>) (a (a (c
<MASK> A) (a (a (c <MASK> <=) (v <MASK> N)) (v <MASK> ))
(a (a (c <MASK> <=) (v <MASK> N)) (v <MASK> n))) (a (a
(c <MASK> <=) (a (a (c <MASK> x) (a (a (c <MASK> *) (a (a
(c <MASK> dest (add] (v <MASK> x)) (V <MASK> m))) (a (a (c
<MASK> dest_nadd) (v <MASK> x)) (V <MASK> n)))) (a (o <MASK>
dist) (a (a (c <MASK> ,) (a (a (c <MASK> *) (v <MASK> m) (a
(a (c <MASK> rinv) (v <MASK> x)) (v <PREDICT> n))) (a
(a (c <MASK> *) (v <MASK> n)) (a (a (c <MASK> nadd_rinv) (v
<MASK> x)) (v <MASK> m))))) (a (a (c <MASK> *) (v <MASK>
B)) (a (a (c <MASK> *) (a (a (c <MASK> *) (v <MASK> m)
(v <MASK> n))) (a (a (c <MASK> +) (v <MASK> m)) (v <MASK>
a
Ground truth: <START> (num) <END>
Source theorem pretty printed: !x. ~ (x === 60) ==> (?B N. Im N <=
m A N <= n ==> (fn x m * fn x n) * dist (m- x madd_riny x n, n Sadd_rins x m) <= B (m n) (m + n) )
17

---

Published as a conference paper at ICLR 2021
Assumptions.
Prompt: (<theorem> (a (a (c (fun (bool) (fun (bool) (bool)))
==>) (a (a (c (fun (fun ?1 (bool)) (fun (fun ?1 (bool))
(bool))) =) (a (c (fun (fun ?1 (bool)) (fun ?1 (bool)))
GSPEC) (1 (v ?1 GENSPVARSO) (a (c (fun (fun ?1 (bool))
(bool)) ?) (1 (v ?1 x) (a (a (a (c (fun ? (fun (bool) (fun ?1 (bool)))) SETSPEC) (v ?1 GENSPVARSO)) (a (a (c (fun (bool) (fun (bool) (bool))) A) (a (a (c (fun ?1 (fun (fun 21 (bool)) (bool))) IN) (v ?1 x)) (v (fun ?1 (bool)) s))) (a (a (c (fun ?0 (fun 20 (bool))) =) (a (v (fun ?1 70) f) (v ?1 x))) (v 20 a)))) (v 21 x)11)))) (v (fun ?1 (bool)) t))) (a (a (c (fun (bool) (fun (bool) (bool))) ==>) <PREDICT>) (a (c (fun (Eun ?1 (bool)) (bool)) !) (1 (v ?1 x) (a (a (c (fun
(bool) (fun (bool) (bool))) ==>) (a (a (a (fun (bool) (fun (bool) (bool))) A) (a (v (fun 21 (bool)) B) (v ?1 x))) (a (v (fun ?1 (bool)) Q) (v ?1 x)))) (a (c (fun (bool) (bool)) ) ~)
(a (a (c (fun ?0 (fun ?0 (bool))) =) (a (v (fun 71 ?0) f) (v ?1 x))) (v 20 a)))))))))
Ground truth: <START> (a (a (c (fun (bool) (fun (bool) (bool))) A) (a (c (fun (fun ?1 (bool)) (bool)) !) (1 (v ?1 x) (a (a (c (fun (bool) (fun (bool) (bool))) ==>) (a (v (fun ?1
(bool)) P) (v ?1 x)) (a (a (c (fun ?1 (fun (fun 21 (bool)) (bool))) IN). (v 71 x)) (v (fun ?1 (bool)) a)))))) (a (c (fun (fun ?1 (bool)) (bool)) !) (1 (v ?1 x) (a (a (c (fun (bool)
(fun (bool) (bool))) -=>) (a (a (c (fun (bool) (fun (bool)
(bool))) A) (a (v (fun ?1 (bool)) P) (v 21 x))) (a (v (fun
21 (bool)) Q) (v ?1 ))) (a (c (fun (bool) (bool)) ~) (a
(a (c (fun ?1 (fun (fun ?1 (bool)) (bool))) IN) (v ?1 x)) (v
(fun ?1 (bool)) )))))))) <END>
Source theorem pretty printed: {x 1 x NNNss =a) = t ==> (!x.
x ==> IN 5) A (!x. FxAQx=> (x IN t)) ==> (Ix. P
x
A 0 x ==> ~f x x
Prompt:
(<theorem> (a (c (fun (fun (fun (cart (real) N)
(bool)) (bool)) (bool)) !) (1 (v (fun (cart (real) N) (bool)) s) (a (a (a (fun (bool) (fun (bool) (bool))) ==>)
<PREDICT>) (a (a (c (fun (fun (cart (real) N) (bool)) (fun (fun (cart (real) N) (bool)) (bool))) =) (a (c (fun (fun
(cart (real) N) (bool)) (fun (cart (real) N) (bool))) inside) (v (fun (cart (real) N) (bool)) s)) (c (fun (cart (real) N) (bool)) EMPTЧ))))))
<START> (a (a (c (fun (bool) (fun (bool) (bool))) A) (a (c (fun (fun (cart (real) N) (bool)) (bool)) connected) (a (a (c (fun (fun (cart (real) N) (bool)) (fun (fun (cart (real) N) (bool)) (fun (cart (real) N) (bool)))) DIFF) (c (fun (cart (real) N) (bool)) UNIV) (v (fun (cart (real) N) (bool)) s)))) (a (c (fun (bool) (bool)) ~) (a (c (fun (fun (cart (real) N) (bool)) (bool)) bounded) (a (a (c (fun (fun (cart (real) N) (bcol)) (fun (fun (cart (real) N) (bool)) (fun (cart (real) N) (bool)))) DIFF) (c (fun (cart (real) N) (bool)) UNIV) (v (fun (cart (real) N) (bool))
Ground truth:
)))))} <END>
Source theorem pretty printed: !s. connected ((:reaIN) DIFF s) A bbounded ((:reaIN) DIFF s) ==> inside s = ()
Prompt: (<theorem> (a (a (c (fun (bool) (fun (bool) (bool)))
==>) (a (a (c (fun (bool) (fun (bool) (bool))) A) (v (bool) q) (a (c (fun (bool) (bool)) ~) (v (bool) p))) (a (a (c
18

---

Published as a conference paper at ICLR 2021
(fun (bool) (fun (bool) (bool))) ==>) <PREDICT>) (v (bool) x) )
Ground truth: <START> (a (a (c (fun (bool) (fun (bool) (bool)))
=) (v (bool) p)) (v (bool) a)) <END>
Source theorem pretty printed: A up ==> (p <=> q) ==>
Prompt:
(<theorem> (a (c (fun (fun (fun (cart (real) N) (real)) (bool)) (bool)) !) (1 (v (fun (cart (real) N)
(real)) f) (a (c (fun (fun (fun (real) (real)) (bool))
(bool)) !) (1 (v (fun (real) (real)) g) (a (c (fun (fun
(cart (real) N) (bool)) (bool)) !) (1 (v (cart (real) N) x) (a (a (c (fun (bool) (fun (bool) (bool))) ==>) <PREDICTS) (a (a (c (fun (fun (cart (real) N) (real)) (fun (net (cart (real) N)) (bool))) real_continuoua,
(a (a (c (fun (fun
(real) (real)) (fun (fun (cart (real) N) (real)) (fun (cart (real) N) (real)))) o) (v (fun (real) (real)) g)) (v (fun
(cart (real) N) (real)) f))) (a (c (fun (cart (real) N) (net (cart (real) N)) at) (v (cart (real) N) x)))))))))>>
Ground truth: <START> (a (a (c (fun (bool) (fun (bool) (bool))) A) (a (a (c (fun (fun (cart (real) N) (real)) (fun (net (cart (real) N)) (bool))) real seal_continuous)
(V (fun (cart
(real) N) (real)) f)) (a (c (fun (cart (real) N) (net (cart (real) N))) at) (v (cart (real) N) x)))) (a (a (c (fun (fun (real) (real)) (fun (net (real)) (bool))) real_continuous) (v (fun (real) (real)) g)) (a (a (c (fun (net (real)) (fun (fun (real) (bool)) (net (real)))) within) (a (c (fun (real) (net (real))) atreal) (a (v (fun (cart (real) N) (real)) f) (v (cart (real) N) x))) (a (a (c (fun (fun (cart (real) N) (real)) (fun (fun (cart (real) N) (bool)) (fun (real)
(bool)))) IMAGE) (v (fun (cart (real) N) (real)) f)) (c (fun (cart (real) N) (bool)) UNIV) <END>
Source theorem pretty printed: !f g.
x. f poll_continuors at x A real_ innnttnuuee nuous atreal (f x) within IMAGE f (:realN) ==> g o f leal_coontiuoue nuous at
Prompt: (<theorem> (a (c (fun (fun (fun (cart (real) M) (cart
(real) N)) (bool)) (bool)) !) (1 (v (fun (cart (real) M)
(cart (real) N)) f) (a (c (fun (fun (fun (cart (real) M)
(cart. (real) P)) (bool)) (bool)) !) (1 (v (fun (cart (real)
M) (cart (real) P)) g) (a (c (fun (fun (fun (cart (real)
M) (bool)) (bool)) (bool)) !) (1 (v (fun (cart (real) M)
(bool)) s) (a (c (fun (fun (num) (bool)) (bool)) !) (1
(v (num) n) (a (a (c (fun (bool) (fun (bool) (bool))) ==>)
<PREDICTS) (a (a (a (c (fun (num) (fun (fun (cart (real) M) (bool)) (fun (fun (cart (real) M) (cart (real) (finite_si) sum N P))) (bool)))) baire) (v (num) n)) (v (fun (cart (real)
M) (bool)) s)) (1 (v (cart (real) M) x) (a (a (a (fun (cart (real) N) (fun (cart (real) P) (cart (real) (finite sum N 2)))) pastecart) (a (v (fun (cart (real) M) (cart (zeal) N)
f) (v (cart (real) M) x))) (a (v (fun (cart (real) M) (cart (real) P)) g) (v (cart (real) M) (()11()1111)))))
Ground truth: <START> (a (a (c (fun (bool) (fun (bool) (bool)))
A) (a (a (a (c (fun (num) (fun (fun (cart (real) M) (bool))
(fun (Eun (cart (real) M) (cart (real) N)) (bool)))) baire)
(v (num) n)) (v (fun (cart (real) M) (bool)) a)) (v (fun
(cart (real) M) (cart (real) N)) f))) (a (a (a (c (fun (num)
(fun (fun (cart (real) M) (bool)) (fun (fun (cart (real) M)
(cart (real) P)) (bool)))) baire) (v (num) n) (v (fun (cart
19

---

Published as a conference paper at ICLR 2021
(real) M) (bool)) ))) (v (fun (cart (real) M) (cart (real)
))) ) <END>
Source theorem pretty printed: !f g a baire n s f A baire g ==> baire n (lambda x. pastecart (f x) (g x))
Equalities.
Prompt: (<theorem> (a (c (fun (fun (fun 70 (cart (real) (2)))
(bool)) (bool)) !) (1 (v (fun ?0 (cart (real) (2))) f) (a
(c (fun (fun (fun ?0 (cart (real) (2))) (bool)) (bool)) !)
(1 (v (fun ?0 (cart (real) (2))) g) (a (c (fun (fun (fun 20 (bool)) (bool)) (bool)) !) (1 (v (fun ?0 (bool)) s) (a (a (c (fun (bool) (fun (bool) (bool))) ==>) (a (c (fun (fun
?0 (bool)) (bool)) FINITE) (v (fun ?0 (bool)) s))) (a (a (c (fun (cart (real) (2)) (fun (cart (real) (2)) (bool))) =) (a
(a (c (fun (fun ?0 (bool)) (fun (fun 20 (cart (real) (2)))
(cart (real) )2)))) cproduct) (v (fun ?0 (bool)) s)) (1 (V
20 x) (a (a (c (fun (cart (real) (2)) (fun (cart (real) (2))
(cart (real) (2)))) camplex_mul) (a (v (fun ?0 (cart (real)
(2))) E) (v 20 x))) (a (v (fun ?0 (cart (real) (2))) g) (v
?0 ))))) <PREDICT>)))))
Ground truth: <START> (a (a (c (fun (cart (real) (2)) (fun (cart (real) (2)) (cart (real) (2)))) complex_mul) (a (a (c (fun (fun ?0 (bool)) (fun (fun ?0 (cart (real) (2))) (cart (real)
(2)))) eproduct) (v (fun ?0 (bool)) s)) (v (fun 70 (cart
(real) (2))) f))) (a (a (c (fun (fun 20 (bool)) (fun (fun ?0 (cart (real) (2))) (cart (real) (2)))) eproduct) (v (fun ?0
(bool)) s)) (v (fun ?0 (cart (real) (2))) g)) <END>
Source theorem pretty printed: !f g s. FINITE ==> eproduct s (xx. f cproduct s x sproduct s g
x g x)
Prompt:
(<theorem> (a (c (fun (fun (fun (cart (real) N)
(bool)) (bool)) (bool)) !) (1 (v (fun (cart (real) N)
(bool)) s) (a (c (fun (fun (fun (cart (real) N) (bool))
(bool)) (bool)) !) (1 (v (fun (cart (real) N) (bool)) t) (a (a (c (fun (bool) (fun (bcol) (bool))) ==>) (a (a (c (fun (bool) (fun (bool) (bool))) A) (a (c (fun (fun (cart (real) N) (bool)) (bool)) convex) (v (fun (cart (real) N) (bool))
s))) (a (a (c (fun (bool) (fun (bool) (bool)) A) (a (c (fun (fun (cart (real) N) (bool)) (bool)) affine) (v (fun (cart (real) N) (bool)) t))) (a (c (fun (bool) (bool)) ~) (a (a (c (fun (fun (cart (real) N) (bool)) (fun (fun (cart (real) N) (bool)) (bool))) =) (a (a ic (fun (fun (cart (real) N) (bocl)) (fun (fun (cart (real) N) (bool)) (Eun (cart (real) N) (bool)))) INTER) (a (c (fun (fun (cart (real) N) (bool)) (fun (cart (real) N) (bool))) relative_interion
(v (fun
(cart (real) N) (bool)) 8))) (v (fun (cart (real) N) (bool)) t))) (c (fun (cart (real) N) (bool)) EMPTY)))))) (a (a (c (fun (fun (cart (real) N) (bool)) (fun (fun (cart (real) N) (bool)) (bool))) =) <PREDICT>) (a (a (c (fun (fun (cart (real) N) (bool)) (fun (fun (cart (real) N) (bool)) (fun (cart (real) N) (bool)))) INTER) (a (c (fun (fun (eart (real) N). (bool)) (fun (cart (real) N). (bool))) closure) (v (fun (cart (real) N) (bool)) s))) (v (fun (cart (real) N) (bool)) t))))))))>>
Ground truth: <START> (a (c (fun (fun (cart (real) N) (bool))
(fun (cart (zeal) N) (bool))) closure) (a (a (c (fun (fun (cart (real) N) (bool)) (fun (fun (cart (real) N) (bool))
20

---

Published as a conference paper at ICLR 2021
(fun (cart (real) N) (bool)))) INTER) (v (fun (cart (real)
N) (bool)) 8)) (v (fun (cart (real) N) (bool)) t))) <END>
Source theorem pretty printed:
!s t. convex s A affine t A (}) ==> closure INTER
(relative_interion s INTER t) =
closure s INTER
Prompt: (<theorem> (a (a (c (fun (bool) (fun (bool) (bool)))
==>) (a (a (fun (fun ?0 (bool)) (fun (fun ?0 (bool))
(bool))) SUBSET) (v (fun ?0 (bool)) t)) (a (a (c (fun (fun 20 (bool)) (fun (fun (bool)) (fun ?0 (bool)))) DIFF) (c (fun 20 (bool)) ) (v (fun ?0 (bool)) s))) (a (a (c (fun (fun 20 (bool)) (fun (fun (bool)) (bool))) =) <PREDICT>> (a (fun 20 (bool)) EMPTY))))
Ground truth: <START> (a (a (c (fun (fun 20 (bool)) (fun (fun 20 (bocl)) (fun ?0 (bool)))) INTER) (v (fun 20 (bool)) 8)) (V (fun ?0 (bool)) ))) <END>
Source theorem pretty printed: t SUBSET (:?0) DIFF ==> s INTER
(
Prompt: (<theorem> (a (c (fun (fun (real) (bool)) (bool)) !) (1 (v (real) x) (a (a (c (fun (real) (fun (real) (bool)))
=) <PREDICT>) (a (c (fun (real) (real)) real_abs) (v (real)
x))))>
Ground truth: <START> (a (a (c (fun (real) (fun (num) (real))) seal_pow) (a (a (fun (real) (real)) sqrt) (v (real) x))) (a (c (fun (num) (num) ) NUMERAL) (a (c (fun (num) (num) BITO)
(a (c (fun (num) (num) ) BIT1) (c (num) ) <END>
Source theorem pretty printed: !x. sqrt x pow 2 = abs x
Prompt: (<theorem> (a (a (c (fun (fun A (bool)) (fun (fun & (bool)) (bool))) =) <PREDICT>) (a (c (fun (fun (bool))
(fun A (bool))) GSPEC) (1 (v A GENSPVARS0) (a (c (fun (fun A (bool)) (bool)) ?) (1 (v A y) (bool) (fun A (bool)))) SETSPEC) (v A GENSPVARSO)) (a (a (c (fun (bool) (fun (bool) (bool))) V) (a (a (c (fun (fun (fun A (bool)) (bool))) IN) (v A y)) (v (fun A (bool)) s)) (a (a (c (fun A (fun A (bool))) =) (v y)) (v A x))) (v A )))))))))
(a (a (c (fun (fun
Ground truth: <START> (a (c (fun (fun (fun (bool)) (fun ) INSERT) (v A x)) (v (fun A (bool)) 8)) <END> Source theorem pretty printed: INSERT s = (y 1 IN S V xl
21


Reviews:
[{"review_id": "pgYfXqaHOE0", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The authors propose a self-supervised learning task to enhance the reasoning capabilities of machine learning models on mathematical formulas and to perform conjecturing in higher order logic. The task consists in masking out specific portions of mathematical statements and predict them from the surrounding parts. The task can (i) be used during training, to provide supervisory signal to the machine learning model and to increase the effective size of the otherwise small training dataset, and (ii) be used during testing, to evaluate the reasoning capabilities of the learnt models by masking out the mathematical statements at different level of granularities. The authors perform an extensive experimental analysis and provide evidence on the utility of using self-supervised learning in the context of theorem proving.\n\nOverall, the paper is clearly written and the bibliography complete. Also, the experimental analysis is undoubtedly valuable for the machine learning community. In fact, it provides additional empirical evidence to the works of [1-2], in the sense that self-supervised learning can be used not only as a pre-training stage for the machine learning models, but also as a task to perform conjecturing.\n\nThere are major issues though. In particular, there are issues in terms of the originality of the proposed task and the reproducibility of the experiments, thus obscuring the positive aspects of the paper. Please, see below for more detailed comments.\n\nIn lieu of this, I consider the paper marginally below the acceptance threshold and therefore recommend for an initial rejection. Nevertheless, I'm willing to raise my score if the authors properly address the issues highlighted below.\n\nDETAILED COMMENTS\n\nOriginality: The proposed task seems to be identical to the task in [3], except for the fact that the task operates on mathematical statements rather than on natural language ones. Importantly, both kinds of sentences/statements share a tree-structured representation, which makes the task in [3] trivially applicable to the mathematical context. Can the authors highlight other differences or explain if this is not correct?\n\nReproducibility: First of all, it's extremely important to add in the section about results and discussion detailed information about the computational resources and the time required for training, as well as the size of the machine learning model used in the experiments. In fact, it is well-known from other domains, like vision and natural language processing, that the performance of self-supervised learning models increase proportionally with the size of the model, at the expense of the training computational resources.\nFurthermore, it's important to discuss about the methodology used to choose the hyperparameters. Appendix A only states that \"we explored encoders and decoders with up to 12 layers and various learning rates and intermediate sizes.\"\nFinally, do the authors plan to release the code?\n\nFURTHER IMPORTANT COMMENTS\n\nAnswering to this following comments could be helpful to clarify about the originality and the novelty of the proposed task.\n\nDistinguishing between training and evaluation tasks and saying that \"several tasks\" are proposed (i.e. in abstract, introduction, section 5 and conclusions) can be misleading for the reader, because he/she could think that they are different. Nevertheless, these tasks are all equivalent to the main skip-tree task, differing only in the way the terms are masked. Is that correct? If so, I would suggest to rephrase by saying that the main skip-tree task is quite flexible at masking statements. In fact, depending on which portion of statement is masked, the model can be induced to perform reasoning at different level of abstraction. Based on this, experiments are categorised according to the different ways of masking.\n\nFurthermore, it is not completely clear when the authors says that \"most previous works...have focused...in supervised training settings. In contrast, we train language models on an unsupervised proxy task\" (related work, but also introduction).\nIs the proposed training unsupervised? First of all, the data used in training contains only valid theorems. This can be already considered as a supervised information, because collecting valid theorems requires human effort. Secondly, the evaluation tasks are essentially similar to the training task and therefore I would consider this more as a supervised learning strategy. Could you please elaborate more on this, also in the text?\n\nMINOR COMMENTS\n\nIn the experiments about conjecturing (2nd paragraph), can you provide more details on how you generated the free-form conjectures?\n\nFurthermore, how is novelty of generated statements defined? Consider the following examples for conjecturing on assumptions and free-form conjecturing.\n\nConjecturing from assumptions\n\nImagine you have \n\na+b=0 implies a=-b\n\nand the task is given by\n\n<PREDICT> implies a=-b\n\nIs the statement 'a+b=c and c=0' considered new according to your definition?\n\nFree-form conjecturing\n\nImagine you have \n\n<THEOREM> for all x, x=x\n\nand the task is given by\n\n<THEOREM> <PREDICT>\n\nIs the theorem 'for all y, y=y' considered new according to your definition?\n\n\n[1] Li et al. Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. arXiv 2020\n\n[2] Polu and Sutskever. Generative Language Modelling for Automated Theorem Provers. arXiv 2020\n\n[3] Zhang et al. PEGASUS: Pre-training with Extracted Gap-sentences for Abstractive Summarization. ICML 2020\n\n########################################\n\nUPDATE\n\nThe paper provides important and novel empirical observations about the use of machine learning to perform mathematical reasoning. The authors have addressed and clarified some doubts about the originality of their idea and the reproducibility of their experiments in the discussion phase. I believe that the paper is now ready for publication and I'm happy to recommend for its acceptance.", "extra_scores": {}, "extra_text": {}}, {"review_id": "b8IP8v0G-ym", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Quality\n\nThe paper is quite well written and the experiments seem well thought out. Please see specific comments below.\n\nClarity\n\nThe S-expression needs more explanation for the paper to be self-contained. What is 'A' in (v A x)? \n\n\nFor those of us who might not be very familiar with the datasets, it might be helpful if the paper to demonstrate more examples as to what these proofs are translated to, in mathematical notation or textual explanations. There are a few snippets here and there but I don't think I get a good grasp of what kinds of proofs we deal with. For example, the theorem examples in Appendix section D seem quite lengthy. With effort it should be decoded into normal text by readers, but it would be more convenient to demonstrate it directly.\n\n\nIn addition, the free-form conjecturing evaluation can be more clear. In this section, it doesn't entirely explain in details what makes the generated statements 'new'. Is it only exact match with the training set? If that's the case, how robust is exact matching on measuring the novelty? \n\nOn the usefulness of the conjectures, there's not much explanation on the RL experiments + DeepHOL theorem prover. What is it supposed to do / how robust does it measure usability? \n\n\nQuestion: a beam search of 1024 seems rather large. How does the result look if no beam search is used?\n\nOriginality\n\n\tThe introduced method 'skip-tree' is not that different from the usual self-supervised training techniques used to train language models. This feature does not contribute to the novelty that much. However, this approach is a new take on learning mathematical reasoning with self-supervised learning, rather than supervised learning like in other previous work.\n\n\n\nSignificance\n\n\tDeep learning for mathematical proofs is an interesting direction and is relatively unexplored, compared to other application areas. \n\n\n\n\nHigh-Level Pros & Cons\n\nPros\n\t- The claim / conclusion for this work that self-supervised training can lead to mathematical reasoning is rather intriguing. \n\t- The proposed skip-tree technique seems to make a lot of difference for training.\n\t- Decent ablation study (not using <MASK> token, skip-sequence instead of skip-tree).\n\t- The evaluation tasks introduced seem interesting.\n\nCons\n\t- I am not 100% convinced that the ``mathematical reasoning'' demonstrated is beyond pattern recognition. I understand that the evaluation tasks are evaluated on validation set theorems which are not seen during training. However, how can we be sure that this is mathematical reasoning versus the model recognizing similar patterns (not necessarily exact match) \n\nMore explanations on this would be appreciated. \n\t- Low to moderate novelty for the skip-tree technique.\n\n\nOverall, I learned a lot from this paper and I believe others can benefit from it as well. ", "extra_scores": {}, "extra_text": {}}, {"review_id": "DCaGkex-CEj", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper extends the idea of language-model style self-supervised learning approach to training logical reasoning models from unlabeled mathematical expressions. The main idea is to develop a skip-tree proxy task (self-supervision) for training the encoder-decoder architecture.  The skip-tree method masks out a complete sub-tree in the input and linearizes it into a sequence in the form of S-expression. The model is required to predict the masked subtree at the decoder end. The paper also proposes several new reasoning tasks for evaluating the model performance. Experimental results show that models learned from this task significantly outperform those trained on the skip-sequence task. Furthermore, the model also exhibits good conjecturing ability in generating quite reasonable amount of new theorems that are provable and useful, which is quite encouraging and impressive.\n\nI’m curious about why the method only masks out one sub-tree for prediction while treating other masked sub-trees as auxiliary part (by increasing the difficulty of the task). This seems to be a waste of self-supervision signals. It might be more (sample) efficient to predict all the masked part in one sample just as what BERT did. It would be helpful to provide experimental justification for this specific design choice if deemed so.\n\nThe current pretrained model is used on the newly created tasks without any finetuning because these tasks are similar to the mask prediction problem. This is interesting, but I’m wondering if the proposed method be used in various other downstream reasoning tasks? For example, even with certain finetuning, could the pretrained reasoning model be used in other downstream tasks that are less similar to the pretraining objective? Since it is claimed earlier that ``In contrast, we train language models on an unsupervised proxy task that does not require labeled data and can thus be applied to almost any source of mathematical expressions” (Section 2), it would be necessary to further evaluate the pretrained models on other popular logic reasoning tasks. This would show how generalizable the skip-tree pretrained model is on various other downstream reasoning tasks, which would greatly enhance the strength of the work.\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "BdPzx0H6bLY", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 7, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "--------------------------------------------------------------------------------------------------------------------------------\nSummary:\n\nThis paper proposes a skip-tree training task. The authors show that self-supervised language models (the Transformer architecture to be exact) trained on the proposed skip-tree training task for mathematic theorem proving enable mathematical reasoning capabilities. Moreover, no fine-tuning is required to achieve the reported reasoning capabilities. They compare the mathematical reasoning abilities of the skip-tree training task with skip-sequence and show an impressive performance improvement. Another interesting result is studying whether any useful (novel) conjectures can be generated by the model.\n\n--------------------------------------------------------------------------------------------------------------------------------\nOverall assessment:\n\nI really enjoyed reading this paper. The authors work on an interesting problem that has been gaining popularity in the last few years. I believe that this problem domain is a suitable test bed to investigate the reasoning capabilities of language models. The authors propose a skip-tree training task and show that it significantly improves the performance of skip-sequence training. The idea is simple and nice: instead of masking out arbitrary sub-sequences (which is the case for skip-sequence), the authors propose to mask out sub-trees. The authors provide extensive ablation studies and evaluations to justify several design choices and to show the reasoning abilities of their model. I do have some comments about presentation clarity (look below), that I hope the authors can address during the rebuttal. Moreover, I am a bit skeptical about the almost 0 performance of the skip-sequence task under some scenarios. I will clarify this as well in the cons section below.\n\n--------------------------------------------------------------------------------------------------------------------------------\nPros:\n\n (1) I like the idea of skip-tree training for structured problems. It seems to improve the performance of the model dramatically (from almost not being able to predict AT ALL to near perfect prediction — in the Hard inference problem for example). I do have a comment about this in the cons section. \n\n (2) The authors design a set of mathematical reasoning evaluations that are used as down-stream tasks (without fine-tuning) to evaluate the self-supervised trained models. They show good performance on all the tasks compared to their baselines.\n\n (3) The authors provide a set of ablation studies to justify their design choices.\n\n (4) I liked the conjecture experiment that evaluated whether the model can generate novel provable conjectures.\n\n--------------------------------------------------------------------------------------------------------------------------------\nCons:\n\n  (1) The performance of skip-sequence training on three out of the four evaluation tasks in Table 2 (Hard type inference, Assumptions, Equalities) are extremely poor. It is my understanding that the only difference between these models and the proposed skip-tree model is in the held-out sub-expression (I am not sure if the skip-sequence models have the <MASK> tokens in addition to <PREDICT> or not). If that understanding is correct, then this might indicate that almost all of the masked <PREDICT> sub-sequences are not “proper” trees. Is that correct? If so, does enforcing a variable portion (say from 0% to 100%) of the held-out sub-sequences to be sub-trees smoothly move the success rates reported in Table 2 towards the skip-tree’s performance? \n\n  (1-1) Another possibility for the poor performance could be that the skip-sequence models were not trained with <MASK> tokens (I am just judging this based on the large difference between the skip-tree and the skip-tree (no mask) model). If this is the case, a fair comparison would also include the skip-sequence training with the additional <MASK> tokens. This allows the reader to understand which parts of the model result in the reported gains.\n\n  (2) In figure 1 the authors illustrate the portion of the data that they use in their experiments for train and validation. It seems like the gray areas (specifically the test set) are not considered in the paper. What is confusing is that in Section 3 they do mention a train/validation/test split. But all the evaluation tasks defined in Section 5 in the paper seem to only refer to the validation data. There seems to be no indication of the use of a test dataset for the reported results (in Tables 2 and 3), which I find troubling. Especially because the authors do mention that they hyper-parameter optimized their models in Appendix A (not mentioned using which part of the data). Can you please clarify this (both in the rebuttal response and in the paper)?\n\n  (3) How is a correct prediction assessed? It is mentioned that the model’s performance is evaluated for “exact match”. However, as mentioned in the Assumptions task, predicting y=x for the ground truth x=y should be counted as a “correct prediction”. If such predictions are not being counted as “correct”, I highly encourage the authors to add an evaluation metric that considers mathematical equivalence of the generated predictions and the ground-truth. A symbolic solver like Sympy or Mathematica might be able to at least verify the equivalence of simpler expressions (I am not sure how complex these expressions are). \n\n  (3-1) To follow up on point (3) above, the authors mention that “to make a correct prediction our language models thus have to understand which statements are more general and also know about naming conventions”. I strongly disagree that this is a good way of measuring mathematical reasoning abilities. On the contrary, I think a model that has truly learned to mathematically reason, is one that ignores irrelevant details such as naming conventions or “generality” of the statement (generality is subjectively used by the authors and I think references to it should be removed from the paper).\n \n  (4) It is not clearly stated what the authors mean by “new” in section 6.1. Are variations of already seen statements considered new? (e.g. if x=y is in the training set, would y=x be a new statement?). I recommend the authors clearly define this in the paper. \n\n  (5) It is not clear to me what the takeaway is for the sampling strategy. In the main text it was implied that the weighted sampling will be better because it allows one to choose non-leafs more often. However, the results shown in Tables 2 and 3 show that some scenarios seem to be better with the uniform sampling and some with the weighted sampling. Do the authors have any comments/discussion on that?\n\n--------------------------------------------------------------------------------------------------------------------------------\nSmaller details:\n\n  (1) Please use the correct citation command for references that are at the beginning of the sentence (e.g. section 2, Paragraph 2, line 4: Zhang et al. (2019)).\n\n  (2) The authors mention that Lample and Charton (2020) “requires that the inverse of the prediction task can be computed”. Can you explain what this means?\n\n  (3) The explanation of the s-expression given in Section 3 lacks enough details. I wasn’t able to fully understand the representation. Perhaps an illustration with step by step labels can make it easier to understand.\n\n  (4) Section 3, Last paragraph: What does “the split is defined on the theorems” mean? In general this paragraph was somewhat hard to follow.\n\n  (5) What portion of the training data is omitted as a result of what is described in Section 4, Paragraph 2.\n\n  (6) I find the first argument about the reason for adding <MASK> tokens somewhat subjective. Why does making the task harder result in better performance?\n\n  (7) I did not understand the multiple sample per dataset generation at all. Do the authors mean that for each math statement they generate n=100 samples with the <PREDICT> and <MASK> tokens? If so, this implies that there will be 360k*100 examples in the larger training set. But this is not consistent with the data stats provided in Table 1. \n\n  (8) I think it would be very useful if the authors add human-readable equivalents of the s-expressions presented in Appendix D to that Appendix.\n\n  (9) Section 6: What does 1M “steps” refer to? Is that the number of model updates?\n\n  (10) It would be great to add a few sentences about what the reinforcement learning experiments in the DeepHOL prover are to make the paper more self-contained. \n\n--------------------------------------------------------------------------------------------------------------------------------\nTypos: \n\nSec 1, Parag 3: which are capable (to) of generating …\nSec 2, Parag 4: models to logic(s)\n", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: All reviewers find the idea of self-supervised learning on mathematical reasoning with the proposed skip-tree training interesting and gave the firmly positive scores.  The paper is clearly written, and the experiments and the analysis are well-organized, particularly the ability of free-form conjecturing is quite thought-provoking.  Also, the reviewers' initial concerns have been properly addressed during the discussion phrase. 

I think this is a good paper from which people can learn a lot, and should be broadly presented at the conference either as an oral or a spotlight presentation.
Decision: Accept (Spotlight)