LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
Authors: Yuhuai Wu
Markus Norman Rabe
Wenda Li
Jimmy Ba
Roger Baker Grosse
Christian Szegedy
Venue:  (2021)
Keywords: Theorem proving
Pre-training
Inductive bias
Reasoning.

Abstract: While designing inductive bias in neural architectures has been widely studied, we hypothesize that transformer networks are flexible enough to learn inductive bias from suitable generic tasks. Here, we replace architecture engineering by encoding inductive bias in the form of datasets. Inspired by Peirce's view that deduction, induction, and abduction form an irreducible set of reasoning primitives, we design three synthetic tasks that are intended to require the model to have these three abilities. We specifically design these synthetic tasks in a way that they are devoid of mathematical knowledge to ensure that only the fundamental reasoning biases can be learned from these tasks. This defines a new pre-training methodology called ``"LIME" (Learning Inductive bias for Mathematical rEasoning). Models trained with LIME significantly outperform vanilla transformers on three very different large mathematical reasoning benchmarks. Unlike dominating the computation cost as traditional pre-training approaches, LIME requires only a small fraction of the computation cost of the typical downstream task.

Under review as a conference paper at ICLR 2021
LIME: LEARNING INDUCTIVE BIAS FOR PRIMITIVES OF MATHEMATICAL REASONING
Anonymous authors Paper under double-blind review
ABSTRACT
While designing inductive bias in neural architectures has been widely studied, we hypothesize that transformer networks are flexible enough to learn inductive bias from suitable generic tasks. Here, we replace architecture engineering by encoding inductive bias in the form of datasets. Inspired by Peirce's 's view that deduction, induction, and abduction form an irreducible set of reasoning primitives, we design three synthetic tasks that are intended to require the model to have these three abilitics. We specifically design these synthetic tasks in a way that they are devoid of mathematical knowledge to ensure that only the fundamental reasoning biases can be learned from these tasks. This defines a new pre-training methodology called "LIME" (Learning Inductive bias for Mathematical rEasoning). Models trained with LIME significantly outperform vanilla transformers on three very different large mathematical reasoning benchmarks. Unlike dominating the computation cost as traditional pre-training approaches, LIME requires only a small fraction of the computation cost of the typical downstream task.
INTRODUCTION
Inductive bias is essential for successful neural network learning. Many of the breakthroughs in machine learning are accompanied by new neural architectures with better inductive biases, such locality bias in convolutional neural networks (LeCun al., 1999), recurrence and memory in LSTMs (Hochreiter and Schmidhuber 1997), and structural bias in graph neural networks (Scarselli) al. 2008). However, existing designs of inductive biases need to be explicitly encoded in neural architecture. This is sometimes difficult as one may not know the exact mechanism for an abstract ability, in order to describe the architectural bias explicitly. In particular, designing proper inductive bias for abstract concepts such mathematical reasoning becomes an extremely challenging task. Moreover, attempts to design elaborate architectures for reasoning often fall short of the performance of more generic transformer architecture. In this work, we aim to avoid the search for new architec- tures and investigate whether one can learn useful inductive bias for mathematical reasoning through pretraining.
Large-scale unsupervised pretraining of language models revolutionized the field of natural language processing (NLP), improving the state-of-the-art in question answering, name entity recognition. text classification, and other domains, e.g. (Radford et al. 2018 Devlin et al. 2019 Yang et al. 2019 Liu et al.) 2019: Raffel al. 2020 Brown et al. (020). D. As result, pretraining has become common practice for modern neural network based NLP. One plausible explanation for the benefit of pretraining is that the model can learn world knowledge by memorizing the contents of the natural language corpus. This can be useful in various natural language downstream tasks, such as question answering and text classification. However, there is another potential advantage of pre-training may distill inductive biases into the model that are helpful for training on downstream tasks (Brown) jet al. 2020, Warstadt and Bowman 2020). We focus on the latter and design pre-training tasks that are intentionally devoid of knowledge and only allow the model to learn inductive bias for reasoning.
Inspired by the logician Charles Peirce (Peirce 1992). we believe that the following three primitives are the most crucial for reasoning:
1. Deduction: the ability to deduce new truths from given facts and inference rules.
2. Induction: the ability to induce general inference rules from a set of known facts.
3. Abduction: the ability to explain the relationship between the evidences and inference rules.

---

Under review as a conference paper at ICLR 2021
To endow the models with an inductive bias for mathematical reasoning, we design synthetic task for each of the three inductive biases. We hypothesize that the transformer networks are flexible enough to learn strong inductive bias from the three synthetic reasoning tasks and consequently improving the downstream tasks. Although such inductive bias may be useful in general reasoning tasks (e.g., NLP tasks), in this work, we focus mathematical reasoning benchmarks, for which we expect to observe the largest gains. We call training on these tasks LIME an acronym for "Learning Inductive Bias for Mathematical rEasoning". Note that there is only limited amount of pretraining data available for formal mathematical benchmarks, therefore the study of generic pre pre-training techniques is particularly important for the success of machine learning in mathematical reasoning.
We demonstrate that LIME pretrained models provide significant gains across three large math- ematical reasoning benchmarks: IsarStep (Li et al., 2020), HOList Skip-tree (Rabe et al., (020) and MetaMathStep (Polu and Sutskever 2020). Notably, on the IsarStep benchmark, pre-training improved the top-1 accuracy from 20.4% to 26.9% and top- 10 accuracy from 33.1% to 41.0%. Compared to the traditional pre-training tasks, there are two major differences. First, we do not load the input embeddings or the weights in the output layer for finetuning on downstream tasks. This allows us to use the same pre-trained model for a variety of downstream tasks, which can have vastly different vocabularies due language tokenization differences. Also, it prevents the transfer of content knowledge from the pretraining to downstream tasks, supporting the evidence of learning inductive biases. Furthermore, pretraining on synthetic tasks require only fraction of the computational cost of downstream tasks. With only about two hours of training on single modern GPU, one already obtains all the benefits, in contrast days of training on large natural language corpus with hundreds of GPUs/TPUs.
Our method can also be regarded as a form of curriculum learning. in which the model is taught basic. extremely generic but general skills before being trained on the specific problem domain.
To summarize, the contributions of the paper are:
1. Providing the first method design inductive biases in the form of datasets for mathematical reasoning.
2. Demonstrating significant improvements in the reasoning performance of transformer models on three large mathematical reasoning benchmarks with negligible extra computation cost.
3. By showing how pretraining brings benefits other than learning content knowledge, disentangling the study of its working mechanism.
2 RELATED WORK
Learning Models Applied to Mathematics There has been increasing interest in applying deep
learning methods to Interactive Theorem Provers (ITP) (Bansal et al.) 2019 Gauthier al. 2020
Huang et al. 2019: Yang and Deng 2019 Wu et al. 2020 Li et al., 2020; Polu and Sutskever
2020). The work that is most related to ours is GPT-3" (Polu and Sutskever 2020). The authors performed pretraining on several natural language corpora and showed significant improvements for an ITP system MetaMath. Different from ours, they used GPT-style large-scale language modeling pretraining, which dominates the computation cost compared to the downstream task. We, on the other hand, propose pretraining on a few lightweight synthetic tasks costing only a minor fraction of the computation spent on the downstream task.
Lample and Charton (2020) have demonstrated that transformer models can be used for symbolic mathematics by successfully predicting the integrals of formulas from randomly generated dataset. Similar observations are made for logical problems relevant to verification: that transformer networks can learn the semantics of logics (Hahn et al. (020). Rabe et al.) (2020) have shown that mathematical reasoning can emerge from self-supervised training alone. Li et al. (2020) show that language models can learn to synthesize missing high-level intermediate propositions given local context. Piotrowski and Urban (2020) used RNNs in automated theorem provers for first-order logic. |Wang et al. (2020) explored the use of machine translation to translate between synthetically generated natural language descriptions of proofs and formally represented proofs. Urban and Jakubúy (2020) present initial experiments generating mathematical conjectures with Transformer model.
2

---

Under review as a conference paper at ICLR 2021
Saxton et al. (2019) suggest dataset for the analysis of mathematical reasoning skills. In contrast to the datasets considered here, their dataset is synthetic, focuses on calculation with concrete numbers, and only contains relatively few symbolic tasks.
Language Model Pretraining The advent of the transformer architecture (Vaswani et al., 2017) and the BERT style pretraining (Devlin et al., 2019) represented a huge improvement in the quality of language modeling. Since then, explosion of research activity in the area pushed the quality of
language models through better pretraining tasks. Where BERT (Devlin et al.) (2019) masks out frac- tion of the input tokens, later works demonstrated the advantages of masking out subsequences (Song
et al. 2019, Dong et al., 2019 Joshi et al. 2020: Raffel et al. 2020: Conneau and Lample (019) and whole sentences (Zhang al. 2020).
Besides the choice of pretraining tasks, the scale of language models is also an important factor. Language models improve in quality and develop new abilities they grow larger while trained on the same data (Radford et al. 2018 Raffel et al. 2020 Brown et al. 2020)..
Inductive Biases in General There have been works studying learning inductive biases other contexts. In particular, [MCCoy et al. (2020) studied whether one learn linguistic inductive biases on synthetic datasets via meta-learmin. [Papadimitriou and Jurafsky (2020) shows inductive biases learned in music data can be useful for natural language. They further designed several synthetic tasks and showed similar kind of improvements for natural language tasks. From a more theoretical point of view, Xu al. (2020) formalize an aspect of inductive (architectural) bias under the context of GNNs, with a notation called architectural aligument. The architecture is aligned when the architecture can perfectly simulates the ground truth solution. But their work is limited to showing alignment in combinatorial problems, whose ground truth solutions are known. In contrast, our work tries to learn architectural bias by relying on the flexible Transformer architecture and training on synthetic datasets.
Inductive Biases for Mathematics Previous work studying inductive biases for logical reasoning has focused on encoding bias in the neural architecture. Initial works focused on encoding the tree structure of expressions using TreeRNNs (Evans et al.) (0118). Graph neural networks are shown to provide a much stronger performance than tree models in premise selection (Wang et al.. (017)) and theorem proving (Paliwal et al.) 2020 GNNs also scale to larger formulas in SAT (Selsam et al. 2019 Selsam and Björner 2019 Han 2020), QBF (Lederman et al. 2020), and #SAT (Vaezipoor et al. 2020). Crouse et al. 2019 have shown that pooling mechanisms can have impact on the performance of GNNs on logical formulas as well. Closely related. Hellendoor et al. (2020) have shown that it can be helpful to hard-code the tree structure of programs in the attention mask of transformers. [Schlag et al.] (2019) developed an architecture for encoding relational information using tensor product representation for mathematical reasoning.
3
METHODS
In this section, first discuss the primitives of reasoning, inspired by Peirce's views, and design one synthetic task for each reasoning primitive.
3.1 REASONING PRIMITIVES
In Peirce's view, there are exactly three kinds of reasoning: deduction, abduction, and induction. Deduction is known as the workhorse for mathematics. It is the process of deriving new facts by applying logical inference rules to known facts or premises. On the other hand, abduction and induction can be thought of as the inverses of deduction. If we call the premise used in deduction as Case, its logical rule as Rule, and its conclusion as Result, then abduction is equivalently the inference of Case from a Rule and Result, while induction may be said to be the inference of a Rule from Case and a Result. We summarize the three reasoning primitives in the following table:
Reasoning Primitives Inference Map
Deduction
Rule, Case - Result
Abduction
Rule, Result - Case
Induction
Case, Result - Rule
3

---

Under review as a conference paper at ICLR 2021
To give example, we let Rule be "All the beans in this bag are white", Case be "These beans from this bag", and Result be "These beans are white". Deduction is to derive the fact that these beans white (Re) from knowing all the beans from this bag are white (R) and these beans from this bag (C). Abduction explains why the beans are white (Re) from knowing that all the beans in the bag are white (R)- because these beans must be from the bag (C). Lastly, induction aims provide a general principle to observing the fact that the beans are white (Re) and they come from this bag (C), which is that all the beans in the bag must be white (R). We refer to Peirce (1992) and Bellucci
and Pietarinen (015) for more elaborate discussions on the primitives of reasoning.
Mathematical reasoning exhibits nontrivial uses of these reasoning primitives. Deduction happens when one needs to derive new valid statements from the given premise (Case) and theorems in the library (Rule). Abduction is used to postulate conjectures from the known facts and theorems, allowing one to decompose the challenging theorem into subgoals for proof. Induction, the ability to extract general principles from known facts and theorems is also one of the major activities of mathematical reasoning. It is used when one derives theorems from special cases and proposes new definitions and general frameworks to encapsulate existing knowledge.
3.2 LIME SYNTHETIC TASKS FOR REASONING PRIMITIVES
We design three synthetic tasks inspired by the three reasoning primitives. As discussed in the previous section, all of the reasoning primitives consist of three essential elements: Rule, Case, and Result. Inspired by this, we first design a method to generate those elements. Once they are generated, can construct tasks that predict one element from the other two. In the following, we describe one simple way to generate those three elements, though we acknowledge that there are many other possible approaches.
We require two types of symbols: 1. math symbols, 2. rule symbols. In general, these symbols can take any forms (e.g., integer representations). But for the ease of discussion, we will think of math symbols as the union of those operators used in mathematics (e.g.. "+ * ()&") and lower case letters (e.g., a, c...). ). and rule symbols as upper case letters (e.g.. A, B. C ...). We now construct Rule, Case, and Result in order:
1. Rule is randomly sampled string that consists of i) rule symbols and ii) math symbols. The length of the string is randomly sampled from a range. For instance, a randomly sampled rule can be: A A B C with rule symbols A, B, and C.,
2. Case is dictionary that represents substitutions. For each rule symbol used in the Rule string, we sample a random string of random length that consists of math symbols. This forms dictionary, whose keys are all rule symbols, and the values are the corresponding sampled string. To illustrate, following the previous example, for each A, B and C, we sample random string to form a dictionary as: (A a, B b, C: ::d+ e).
Result is the outcome of the substitution. For each rule symbol in the Rule string, we replace with the corresponding value stored in the Case dictionary. This gives rise to the Result string. As per the previous example, we now substitute A with a, B with b and C' with d + e into the Rule string, generating the Result string: * + b d +
After Rule, Case, and Result are generated, we can construct three tasks for deduction, abduction, and induction respectively. We define the three synthetic tasks as follows:
Deduct: Source: Rule string and Case dictionary. Target: Result string.
Abduct: Source: Rule string and Result string. Target: Case dictionary.
Induct: Source: Case dictionary and Result string. Target: Rule string.
We also consider a task called Mix, which is a uniform mix of three tasks. Namely, during generation,
we randomly select a task and sample an example from that task. To formulate them as sequence to sequence tasks, we represent the Case dictionary also as string, e.g., "(A a, B b, C: d e)". An example of Abduct using the examples of Rule, Case, and Result above is to predict the target {A a, B b, C: d + e} from the source A A + B C 
 a d +c. c.
Pre- training on our synthetic tasks can be seen as a form of ckip-component learning. There are three essential components: Rule, Case and Result, and we skip one of them and use the remaining
4

---

Under review as a conference paper at ICLR 2021
two elements to reconstruct the missing one. Past work has shown that learning to predict missing words (Devlin et al. 2019), subsequences (Song et al. 2019 Raffel et al. 2020), or subtrees (Rabe) et al. 2020) strong pre-training tasks.
3.3 SYMBOL-AGNOSTIC REPRESENTATION
In order to solve the synthetic tasks, the model needs to distinguish which set of symbols can be substituted (rule symbols). As result, the model may memorize information about the symbols that irrelevant the inductive biases encoded in the task. To prevent such memorization, propose way to make the synthetic tasks agnostic to the choice of symbols.
We first note that the choice of symbols is irrelevant to our synthetic tasks. To avoid symbol-specine memorization, for each training and evaluation example, we randomly sample two sets of symbols to be used in Rules and in the rest of the example. But for the Abduct task, the model needs to know which symbols are replaced by the Rule part of the example and which symbols are in the Result language. We simply list the split of the symbols used in the example the beginning of the input string, marked by two special symbols, <Rule> and <Math>, They are followed by the original source string. The target string remains unchanged. For example, the previous example in the Abduct task becomes,
Source: <Rule> A B <Math> * abdde 
 A A+ B C 
 
aaabb=d
Target: {A:a, a, b, dd
In our implementation, we use integers represent symbols. Specifically, for each example, we sample two disjoint sets of integers from the set [S} to represent the math symbols and the rule symbols, where S is the size of the vocabulary. In our experiments, we sample 44 math symbols and 24 rule symbols for each problem. The complete pseudo-code of generating the symbols, Rule, Case, and Result for one task example provided in Appendix Algorithm
4 EXPERIMENTS
In this section, we present results on three large mathematical reasoning tasks that are especially useful the context of automated theorem proving. Our results show significant gains learning inductive biases from synthetic tasks. We have selected three tasks to cover three different styles of interactive theorem provers: The HOL-Light (skip-tree) corpus was created from very high-level tactic-based proofs, but it is less interpretable than IsarStep's declarative style corpus. We also evaluate the next proof-step prediction task on the set. mm library of MetaMath, which consists of very granular, basic proof steps. Namely, the proof steps more predicable and average proof lengths have significantly increased.
4.1 EXPERIMENT DETAILS
LIME Pretraining We generate datasets of our synthetic tasks for pretraining: Deduct, Abduct, Induct, Mix. For pretraining of IsarStep, used a vocabulary size S of 1000. For the other two downstream tasks, we used a vocabulary size of 100. The reason we used different vocabulary sizes was that we found (cf. appendix) the discrepancy in vocabulary size affects the performance of a downstream task if it has a very large vocabulary size (IsarStep has 28K). We use 44 math symbols and 24 rule symbols. The length of the Rule string sampled from 5 to 20, the length of the string for each substitution (the values of Case dictionary) is sampled from 2 to 8. We used word-level tokenization for all the tasks. We pretrained the model for 20K updates. For tasks with larger vocabulary size (i.e., 1000), we found the learning became more difficult. Hence we used a curriculum learning scheme: we first trained the model for 10K steps on the same task with vocabulary size of 100, then continue training for another 10K step vocabulary size of 1000. The pretraining was done on a single Nvidia Tesla T4 GPU with CPU cores for hours. We set the maximum number of tokens in batch to 4096, and accumulate four batches of gradients for one parameter update. We used the Adam optimizer (Kingma and Bal 2015) with learning rate - We used dropout rate of 0.1 and label smoothing (Szegedy et al. 2016) with coefficient 0.1.
5

---

Under review as a conference paper at ICLR 2021
Table I: Test top-1, top-10 (%) accuracy on the IsarStep task.
Model
Top-1 Acc.
Top- Acc.
No pretrain (Li et al. 2020
20.4
33.1
HAT (Li et al. 2020
22.8
35.2
LIME Deduct
24.7
37.7
LIME Abduct
26.7
41.0
LIME Induct
23.9
38.8
LIME Mix
26.9
40.4
Table 2: Test top-8 Accuracy Skip-Tres Tree HOList (%).
Model
Equation completion
Hard type inference
Missing assumptions
Easy type inference
pretrain (Rabe al. 2020
46.3
95.0
41.8
95.9
LIME Deduct
50.3
94.8
47.9
97.0
LIME Abduct
48.4
94.8
46.1
96.3
LIME Induct
44.8
94.9
42.6
96.4
LIME Mix
51.7
95.6
46.1
97.6
Fine-tuning For all the downstream tasks in this section, when loading the pretrained models for fine-tuning, we do not load in the vocabulary embeddings nor the output layer weights. For the downstream task IsarStep and MetaMathStep, cores for training. We set the maximum number tokens in a batch to 4096, and accumulated four batches of gradients for one parameter update. We trained the model for 200K updates. We used the Adam optimizer, and we searched over the learning rates {3 10 7 10 10-4) (4000, 8000}. We used a dropout rate of and label smoothing with a coefficient 0.1. For the HOList skip-tree task, we used TPUs for running the experiments. We used batch size of 256 sequences and trained the model for million updates.
used four Nvidia Tesla T4 GPU with 16 CPU
JJ and warmup steps
Architecture All experiments used the transformer base model from Vaswani et al. 2017) 7) i.c. 512 hidden size, 2048 filter size, attention heads. For the IsarStep and MetaMathStep task, used layers for both the encoder and decoder, implemented using fairseq (On et al. 2019). For the HOList skip-tree experiment, we used a somewhat modified transformer architecture with encoder and decoder layers of the same size as above in which the self self-ateention and attention over the encoder output were merged.
Evaluation During training, we kept track of the best validation tokenized BLEU score I and we used the model with validation BLEU for evaluation the test We report top-1 and top-10 10 accuracies. We consider an output sequence as correct if it matches the target sequence exactly. We performed beam search with width 10. The top-1 accuracy is then defined as the percentage of the best output sequences that are correct. The top-n accuracy is defined as the percentage of target sequences appearing in the top n generated sequences.
4.2 ISARSTEP
The lsarStep task is taken from Li et al. 2020). IsarStep is a task of predicting the missing intermediate propositions given surrounding propositions to bridge the gap between the goal and the current state of the proof. The dataset was mined from the public repository of formal proofs of the Isabelle proof assistant (Paulson, 1994). Unlike HOList and MetaMath, IsarStep contains mostly declarative proofs, proof style close to humans' prose proofs. The dataset has broad coverage of undergraduate and research-lewe mathematics and computer science theorems. There are 820K, 5000, 5000 sequence pairs for the training, validation, and test sets with a maximum of 800 tokens in source sequences and 200 tokens in the target sequences. Following Li et al. 2020), during training, we use 512 as the
trans inl.latiinnnooia 1y1199

---

Under review as a conference paper at ICLR 2021
Table 3: Test top-1, top-10 (%) accuracy on the Meta task.
Model
Top-1 Acc.
Top-10 Ace.
No pretrain
67.7
76.5
LIME Deduct
68.8
77.4
LIME Abduct
68.8
76.1
LIME Induct 69.9
78.0
LIME Mix
69.1
77.9
maximum length for both the source and target, and truncated those that exceed the length to 512. For reporting, we evaluate all 5000 test examples regardless of their lengths.
The results on the IsarStep task for four pretrained models and the baseline transformer model without pretraining is shown in Table | We also include an- other baseline, HAT transformer introduced in Li et al. (2020), which is a specially designed hierar- chical transformer architecture tailored to this task. We see the pretrained model achieved substantial improvement over the model trained from scratch as well as HAT. Notably, the model that was pre- trained on Abduct improved the top-10 accuracy from 33.1% to 41.0%, for almost 8% absolute im- provement. The model pretrained on Mix performed the best top-1 accuracy, improving the baseline by 6.5% accuracy. We also showed the validation BLEU scores along training in Figure We that the pretrained models learned much faster than the model trained from scratch. With around 50K steps of updates, the pretrained model already obtained better BLEU scores than the best score achieved by the un-pretrained model. Moreover, since the downstream task requires 200K steps of training with 4 GPUs, the amount of computation spent on pretraining is only 2.5% of the downstream task, strongly demonstrating the efficiency of the proposed pretraining method.
Validation BLEU: IsarStep
65
60
LIME Deduct
LIME Inductt
50
LIME Abduct
LIME Mix
pretrain
45
50K
100K
150K
200K
Training steps
Figure 1: Validation BLEU along training on the IsarStep task.
4.3 HOLIST SKIP-TREE
As the second mathematical reasoning benchmark we consider the HOList skip-tree evaluation tasks by Rabe et al. (2020). These tasks include two variants of type inference, predicting under which assumptions theorems hold, and completing equalities. All source expressions for these tasks taken from the validation set of the theorem database of the HOList proof logs (Bansal et a..). The evaluations are done on a random sample of 1000 instances from the full evaluation sets. We initialized the model parameters with the pretrained weights and then repeated the experiments by Rabe et al. (2020). That is, we trained the models for up to IM parameter updates on the training set with batch size 256 and repeat the evaluation every 100K steps. In Table 2 we present the best result from these 10 evaluation runs. We see a significant improvement in these reasoning tasks when the models are initialized with the pretrained weights. Notably, on equation completion and missing assumptions task, we improved the beam search (with width 8) exact match rate performance from 46.3% to 51.7% and 41.8% to 47.9%. Note that this is despite the amount of pretraining compute cost being negligible: it takes less than 1 percent of the cost of the downstream task training. Pretraining used 1/20 number the update steps (50K vs 1M) with (and 4) times smaller batches (pretraining has much shorter sequence lengths, 128 vs. 1024 and 512, respectively).
4.4 METAMATHSTEP
Compared to other ITPs, MetaMath is low-level proving system: each proof step makes only small step towards the goal. As such, each proof contains many more proof steps than other ITPs: with 37, 000 theorems in the human-written theorem library, there around 3 million proof steps.
7

---

Under review as a conference paper at ICLR 2021
Table 4: Comparisons to other pretraining tasks on IsarStep task.
Model
Top-1 1 Acc.
Top- 10 Acc
No pretrain (Li et al. 2020)
20.4
33.1
LIME Mix
26.9
40.4
Pretrain on MetaMathStep
23.1
35.7
Pretrain WMT En-De
17.2
30.3
We extract the proof steps and use them to construct a sequence-to-sequence task following Polu and Sutskever (2020) (their proof step training objective).
In this task, the model is asked to generate PROOFSTEPS given GOAL, namely, the GOAL string is the source input, and PROOFSTEPS the target output. We follow PPolu and Sutskever (2020) and use their string representation for the GOAL and the PROOFSTEPS. Instead of using subword tokenization in (Polu and Sutskever (2020), we use a character- task. Following Polu and Sutskever (020)) we split theorems into train/valid/ttes theorems of size 35K, IK, 1K, and associate all proof steps of a theorem with that split. For each dataset, we filter examples with lengths longer than 1024. This reduced the total number of proof steps to 1.4 million. For validation and test set, we randomly sample 3000 examples out of 40K (after filtering) and perform validation and test evaluations on them. In Table 3 we present the impact of pretraining on our synthetic reasoning tasks on MetaMathStep. We also observe gains from pretraining on this dataset, with the model trained on Induct task achieving 2.2% top-1 and 1.5% top- 10 test accuracy improvement. Similarly, as for the IsarStep task, the computation spent on pretraining is only 2.5% of the downstream task.
representation for our
5 ABLATION STUDIES
In this section, we perform ablation studies. Additional ablation studies can be found in Appendix C
5.1 PRETRAINING ON FORMAL REASONING AND NATURAL LANGUAGE TASKS
Here we investigate how LIME compares to pretraining on natural language or existing formal reasoning datasets. this set of experiments, we pretrained three models on Mix, MetaMathStep. and on the WMT 2016 Anglish-to-German (WMT En-De) translation task, and then we fine-tuned and evaluated these models on the IsarStep task. We pretrained the model on MetaMathStep and WMT EN-DE for 200K steps with GPUs, which is 40 times more computation spent than on LIME. Due to the mismatch between vocabularies of the pretraining task and the downstream task, we do not load the vocabulary embeddings nor output layer weights. The results in Table show that pretraining on MetaMathStep did provide gains, though significantly smaller than gains provided by LIME Mi x, despite their 40 times higher computational cost. Moreover, pre-training WMT translation had even a negative effect on the performance. We also conducted an analogous experiment with an evaluation on the MetaMathStep, which we present Appendix C
5.2 DO WE NEED VOCABULARY EMBEDDINGS FOR FINE-TUNING?
As mentioned earlier, we did not load in the vocabulary embeddings from the pretrained models when we switched to fine-tuning on downstream tasks. Even without loading the vocab embeddings. the pretrained models still improved the performance. In this ablation study, we investigate how much this decision has affected the results and whether vocabulary embeddings can help improve the performance even further. We performed the comparisons on IsarStep. The task contains token vocabulary of size 28336. We generated new synthetic tasks for the same vocabulary size, such that we can load the vocabulary embeddings and output layers when initializing the model for IsarStep. Table shows that this led to similar performance. This aligns with our expectation that the model should not learn content specific knowledge that is potentially stored in the vocabulary. These weights turn out to be non- non-essential for the final performance, supporting the evidence that the transformer learns inductive biases from the pretraining task.
8

---

Under review as a conference paper at ICLR 2021
Table 5: Whether one needs load vocabulary embeddings and output layer weights on IsarStep tasks.
Model
Top-1 Acc.
Top-10 10 Acc
No pretrain (Li et al. 2020)
20.4
33.1
LIME Mix
26.9
40.4
LIME Mix Loading All Weights
26.7
40.6
DOES LIME ENCODE INDUCTION, DEDUCTION AND ABDUCTION?
Although LIME has shown achieve substantial improvements across various benchmarks, it is entirely clear that the specific synthetic tasks necessarily enforce the reasoning ability of induction, deduction and abduction. We would like note that deduction, induction, and abduction are high- level and philosophical concepts, and serve only as an inspiration for us to design the synthetic tasks. We do not expect the model will necessarily learn exactly these three capabilities. After all, we have chosen a particular implementation of "Case", "Rule" and "Result". Furthermore, we also design tasks mimic proof steps in formal theorem proving (see the rewrite task in Appendix B.I), which also achieved excellent results. Nevertheless, we believe LIME is a first step towards building reasoning inductive biases, and provides many inspirations and directions for future work.
CONCLUSION
In this work, encoded inductive biases for mathematical reasoning in the form of datasets. We created three synthetic tasks inspired by three reasoning primitives of deduction, induction, and abduction. We demonstrated that pretraining these tasks (LIME) significantly improved the performances across three mathematical reasoning benchmarks. Notably, LIME requires negligible computation compared the downstream task, unlike being the dominating factor in previous pretraining methods. Our work naturally poses many future research questions. Could the primitive tasks provide similar gains for NLP tasks? Are there similar primitive tasks for natural language reasoning? We also look forward to disentangling the effects of pretraining between learning content knowledge and inductive bias for downstream tasks to better understand pre-training.

---

Under review as a conference paper at ICLR 2021
REFERENCES
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An Environment for Machine Learning Higher Order Logic Theorem Proving, In 36th International Conference on Machine Learning, ICML 2019, Long Beach, Califormia, USA, June 9-15, 20/9. .html
URL httpt::pppproocciigggg. m wtt.s/ppees/eee/eeseeseeee
Kshitij Bansal, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Viktor Toman. Learning to Reason in Large Theories without Imitation. arXiv preprint arXiv: 10501, 2019.
Francesco Bellueci and Ahti-Veikke Pietarinen. Charles Sanders Peirce: Logic. In The Internet Encyclopedia of Philosophy, 2015, URL
utm. http://iwp..tt.eccd//eee-------0
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert- Voss. Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. CoRR, 1tt/22055.11665 2020. URLbtttps /ttp:v//aaxivvvai org abs abt.aabb//00... 200./200511111 14165
Alexis Conneau and Guillaume Lample. Cross-lingual Language Model Pretraining. In Ad- vances in Neural Information Processing Systems, NeurIPS 20/9, Vancouver, BC, Canada, De- cember 8-14, 2019, pages 7057-7067, 2019. URL hattp://papers: wwweeersnniii.. wwws. wwtpcc/ppppp...eeeeeeeeeeeeeee.e lingualnnl--nn Sanguull-aanuugeer language mode 1 pretraining
Maxwell Crouse, Ibrahim Abdelaziz, Cristina Cornelio, Veronika Thost, Lingfei Wu, Kenneth Forbus, and Achille Fokoue. Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling, arXiv preprint arXiv: 1.06904, 2019.
Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: pre-training of deep bidirectional transformers for language understanding. In Jill Burstein, Christy Doran, and Thamar Solorio, editors, Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HILT 2019, Minneapolis, MN, USA, June 2-7, 2019, Volume (Long and Short Papers), pages 4171- 4186. Association for Computational Linguistics, 2019. doi: 10.18653/v1/n19-. 1/2333119111 URL https://doli wtt.:/..//.............
Li Dong, Nan Yang, Wenhui Wang, Furu Wei, Xiaodong Liu, Yu Wang, Jianfeng Gao, Ming Zhou, and Hsiao-Wuen Hon. Unified Language Model Pre-training for Natural Language Understanding and Generation. In Advances in Neural Information Processing Systems, NeurlPS 2019, Vancouver, BC, Canada, December 8414, 2019, pages 14063-13075,0 2019.
Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can Neural Networks Understand Logical Entailment? In International Conference Learning Representa- tions, 2018 URL
net wtte://ooommmmmdkeeeeee
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. TacticToe: Learning to Prove with Tactics. Journal of Automated Reasoning, pages 1-30, 2020.
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner. Transformers Generalize to the Semantics of Logics. arXiv preprint arXiv:2003.04218 2020.
Jesse Michael Han. Enhaneing SAT solvers with glue variable predictions. arXiv preprint arXiv:2007.02559, 2020.
Vincent J. Hellendoom, Charles Sutton, Rishabh Singh, Petros Maniatis, and David Bieber. Global relational models of source code. 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL. https
//openreview.o www.:/oruturmmm... -ereedddBBiinbbi B11nbRNEww
Sepp Hochreiter and Jürgen Schmidhuber. Long Short-Term Memory. Neural computation, 9()) 1735-1780, 1997.
10

---

Under review as a conference paper at ICLR 2021
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 httpattp////ppeeeeeiee net i d= XWKoR9Y?]
Mandar Joshi, Danqi Chen, Yinhan Liu, Daniel S. 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/tacI, a) 00300. URL https
/ //doi. adoi.ooo wtw.z//..1161////.
a 00300
Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. In Yoshua Bengio and Yann LeCun, editors, 3rd International Conference on Learning Representations, ICLR 2015, San Diego CA, USA, May 7-9, 2015, Conference Track Proceedings, 2015. URL http:://rxiii wwg/absgg/...ooooo 141114112222 1412.6980
Guillaume Lample and François Charton, Deep learning for symbolic mathematics. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia. April 26-30, 2020. OpenReview.net, 2020. URL httpt::://ppeeeeiiieeeeee net forum?id Ske31kBtPr
Yann LeCun, Patrick Haffner, Léon Bottou, and Yoshua Bengio. Object recognition with gradient- based learning. In Shape, Contour and Grouping in Computer Vision, page 319, Berlin, Heidelherg. 1999. Springer-Verlag ISBN 3540667229.
Gil Lederman, Markus Rabe, Sanjit Seshia, and Edward A Lee. Learning heuristics for quantified boolean formulas through reinforcement learning. In International Conference on Learning Representations, 2020.
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. arXiv preprint arXiv:2006.0922 09265, 2020.
Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zettlemoyer. and Veselin Stoyanov. Roberta: A robustly optimized BERT pretraining abs / 1 907 11692
approach. CoRR, abs/1907.1 1692, 2019. http:hhtt////x.ti
Thang Luong, Hieu Pham, and Christopher D. Manning. Effective approaches to attention-baser neural machine translation. In Lluís Mårquez, Chris Callison-Burch, Jian Su, Daniele Pighin, and Yuval Marton, editors, Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, EMNLP 2015, Lisbon, Portugal, September 17-21, 2015, pages 1412- 1421. The Association for Computational Linguistics, 2015. doi: 10. 10.18653/v 1/815-1166 URL https: /tt::///ooii//
R. Thomas McCoy, F. Grant, P. Smolensky, T. Griffiths, and Tal Linzen. Universal linguistic inductive biases via meta-learning Proceedings of CogSci, abs/2006. 16324, 2020.
Myle Ott, Sergey Edunov, Alexei Baevski, Angela Fan, Sam Gross, Nathan Ng, David Grangier, and Michael Auli. fairseq: A fast, extensible toolkit for sequence modeling. In Waleed Ammar, Annie Louis, and Nasrin Mostafazadeh, editors, Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT 2019, Minneapolis, MN, USA, June 2-7, 2019, Demonstrations, pages 48 53. Association for Computational Linguistics, 2019. doi: 10. 101518653/vll 1/139/11111100999 URL https://doo . wwwoorgg111
4009
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In The Thirty-Fourt AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intel- ligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 2967-2974 AAAI Press, 2020. URL httpp:// /eattps:/aaai.... org wwwee//////......... js index. php/ http:/AAAaaaateeeeeeaaaa
Isabel Papadimitriou and Dan Jurafsky. Learning Music Helps You Read: Using transfer to study lin- guistic structure in language models. In Proceedings of the 2020 Conference on Empirical Methods
11

---

Under review as a conference paper at ICLR 2021
in Natural Language Processing (EMNLP), pages 6829 6839, Online, November 2020. Associa- tion for Computational Linguistics. URL http://wwwwww...././///tttooooot monnp-mmin... 554
Charles Sanders Peirce. Reasoning and the logic of things: The Cambridge conferences lectures of 1898. Harvard University Press, 1992.
Bartosz Piotrowski and Josef Urban. Guiding Inferences in Connection Tableau by Recurrent Neural Networks. In Christoph Benzmüller and Bruce Miller, editors, Intelligent Computer Mathematics, pages 309-314, Cham, 2020. Springer International Publishing. ISBN 777-3-030-53518-41
Stanislas Polu and Πya Sutskever. Generative Language Modeling for Automated Theorem Proving. CoRR, abs/2009.03393, 2020. httpt:tttt/:.x...//eppt
2000 03393
Markus N. Rabe, Dennis Lec, Kshitij Bansal, and Christian Szegedy, Mathematical Reasoning via Self-supervised Skip-tree Training. arXiv preprint arXiv:2006.047577 2020.
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and 1lya Sutskever.
Language models are unsupervised multitask learners. In OpenAl Blog, 2018. URL
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 Unified Text-to- Text Transformer. J. Mach. Learn. Res., 21:140:1-140:00 2020. URL htthhttp://mmrr.
papers/v21/20-00 .tmll
David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In Proceedings of International Conference on Learning Representations (ICLR), 2019.
Franco Scarselli, Marco Gori, Ah Chung Tsoi, Markus Hagenbuchner, and Gabriele Monfardini. The graph neural network model. IEEE Transactions Neural Networks, 20(1):61-80 2008
Imanol Schlag, Paul Smolensky, Roland Fernandez, Nebojsa Jojic, Jürgen Schmidhuber, and Jianfeng Gao. Enhancing the transformer with explicit relational encoding for math problem solving. CoRR, abs/1910.06611 2019. URL htt.::://axii...rr.ttt.
06611
Daniel Selsam and Nikolaj Bjørner. Guiding High-Performance SAT solvers with Unsat-Core Predictions. In International Conference on Theory and Applications of Satisfibillty Testing, pages 336-353. Springer, 2019,
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL htttps://openzeveee
net/ www.moorriiooooom.... HJMC iA5tm.
Kaitao Song, Xu Tan, Tao Qin, Jianfeng Lu, and Tie- Tie-Yan Liu. MASS: masked sequence to sequence pre-training for language generation. In 36th International Conference on Machine Learning, ICML 2019, Long Beach, California, USA, June 9-15, 2019, 2019. URL http: httt:://proceeding
m1 mlr.press wwt.pppess/s/s/nnece 9d. ht.ml
Christian Szegedy, Vincent Vanhoucke, Sergey loffe, Jon Shlens, and Zbigniew Wojna. Rethinking the inception architecture for computer vision. In Proceedings of the IEEE conference computer vision and pattern recognition, pages 281 8-2826, 2016.
Josef Urban and Jan Jakubův. First Neural Conjecturing Datasets and Experiments. In Christoph Benzmüller and Bruce Miller, editors, Intelligent Computer Mathematics, pages 315-323, Cham, 2020. Springer International Publishing. ISBN 978-3-030-53518-42
Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris J. Maddison, Roger B. Grosse, Edward A. Lee, Sanjit A. Seshia, and Fahiem Bacchus. Learning Branching Heuristics for Propositional Model Counting. CoRR, abs/2007.0322 2020. U https: //a rxiii .rgg abs 2007. 03204
12

---

Under review as a conference paper at ICLR 2021
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is All you Need. In Proceedings of Advances in Neural Information Processing Systems (NeurIPS), 2017.
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems, pages 2786-2796, 2017.
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural ma- chine translation in autoformalization of mathematics in mizar. Proceedings of ACM SIGPLAN International Conference on Certified Prugrams and Proofs, 2020.
Alex Warstadt and Samuel R. Bowman. Can neural networks acquire a structural bias from raw linguistic data? Proceedings of CogSci, 2020.
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Grosse. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. arXiv preprint 2rxXiv:0007.29924. 2020.
Keyulu Xu, Jingling Li, Mozhi Zhang. Simon S Du, Ken-ichi Kawarabayashi, and Stefanie Jegelka. What can neural networks reason about? ICLR 2020, 2020.
Kaiyu Yang and Jia Deng. Learning to Prove Theorems via Interacting with Proof Assistants. In Proceedings of International Conference Machine Learning (ICML), 2019.
Zhilin Yang, Zihang Dai, Yiming Yang, Jaime Carbonell, Russ R Salakhutdinov, and Quoc Le. XInet: Generalized autoregressive pretraining for language understanding. In Advances in Neural Information Processing Systems, NeurlPS 2019, Vancouver, BC. Canada, December 8-14, 2019, 2019.
Jingqing Zhang, Yao Zhao, Mohammad Saleh, and Peter J. Liu. PEGASUS: pre-training with extracted gap-sentences for abstractive summarization. In 37th International Conference on Machine Learning, ICML 2020, Vienna, Austria, 2020, volume 119, PMLR, 2020.
13

---

Under review as a conference paper at ICLR 2021
APPENDIX A
SYNTHETIC TASK GENERATION PSEUDOCODE
Algorithm 1
1: function GENERATE T Vocabulary size S)
2:
Vocabulary V + ,.)
..).
Usc an integer representation of symbols.
SAMPLE(V, n=44, replacement-Falle), 4: Rule symbol set R + SAMPLE(V M, n=20, replacement=Falke)..
3: Math symbol
Sample distinet symbols.
Sample 20 distinct symbols.
5: Rule R SAMPLE(M UR ==RANDOM(5220), replacement-Falls))
Sample sequence of
symbols of length between 5 and 20.
6: Case dictionary C +- 0
7: for in R do
Case dictionary C[s] <- SAMPLE(M, r=RANDOM(228), replacement-Truu), b Sample sequence of symbols for each rule symbol, of length of length between and 8.
9: end for
Result R' Rule
P result string It' same as rule string R.
11: for s in R do
12: SUBSTITUTE(R', 8, C(s)).
Substitute every rule symbol in result string R' with previously
randomly sampled string C(s)).
13:
end for
14:
return Math symbol M,, Rule symbol set R, Rule R. Case C, Result R'. end function
APPENDIX B OTHER SYNTHETIC TASKS
In this section, we give descriptions of other variants of the synthetic tasks we considered than the ones introduced in the main paper.
APPENDIX B. REERITE AND REARITE_MULTIE
We propose rewrite task, inspired by the rewrite tactic used in interactive theorem provers. The Rewrite task requires the model to rewrite a string according to rule transformation. One example of the task is:
Source: + b <<S> A+ B B+
Target: b+a. -
"A+B= B i the rule transformation, which is applied to the LHS string "a + b- The model needs to predict the RHS string as the result of the rule application, i.c., b+ a - c. Besides rule symbols and math symbols, the ease of our discussion, we we will think math symbols as the union of those operators used in mathematies (e.g.. "+
also require the third set of symbols, named as "string symbols". For
()&"), rule symbols upper case letters (e.g., A, B, C ...). and string symbols as lower case letters (c.g., a, b, ....). We first sample a random string as the LHS string, consisting of math symbols and string symbols (e.g.. a + b c). We sample a sub-string of the LHS string, and replace the string symbols in the sub-string with rule symbols. For example, we sample and obtain the substring + from a x- c, and we replace a, with rule symbols A, B. This then forms the LHS of the rule transformation. A + B, with the substitution dictionary {A a, B b). We then sample the RHS of the rule transformation from the union of rule symbols and B, and all math symbols, e.g., B + A. This gives the rule transformation A B B + A. We substitute the value of the substitution dictionary for each rule symbol in the RHS rule, and then substitute back to the original LHS string to obtain + the rule transformation as the source input, and use the result the rule transformation as the target.
The task example is constructed by using the LHS string and
We further introduce multi-step version of the rewrite task: Rewrite muitistep. In this task, the source may contain more than one rewrite rule, and the target is the result of applying all the rewrite rules in sequence. This task is motivated from the need perform multi-step planning in
14

---

Under review as a conference paper at ICLR 2021
Table 6: Test top-1, top-10 (%) accuracy on the IsarStep task.
Model
Top-1 Acc.
Top- 10 Acc.
No pretrain (Li al.
2020
20.4
33.1
HAT (Li et al. 2020)
22.8
35.2
LIME Deduct
24.7
37.7
LIME Abduct
26.7
41.0
LIME Induct
23.9
38.8
LIME Mix
26.9
40.4
LIME Rewrite
26.0
38.6
LIME Rewrite_mte Rewrite_maltisst mmm_liitteeppppppe
28.6
43.9
LIME Induct_v2
25.6
39.8
LIME Induct_vi v3
25.0
38.8
LIME Induct_rewrin
25.8
39.5
mathematical reasoning tasks. During pre-training, for each training example, we uniformly sample the number of rewrite steps from to
APPENDIX B.2 OTHER VARIANTS OF INDUCT TASK
We introduce three other variants of the Induct task.
Induct_ v2: We move the Case dictionary from the source input to the target output. This makes the task significantly harder, which requires the agent to synthesize rule and possible explanation (Case) to explain the Result.
2. Induct_v3 v3: Instead of providing the Case dictionary, we provide two Result strings, coming from the same Rule. Namely, we sample two Case dictionaries, and applying each to the Rule string to obtain two Result strings. Both Result strings are used as source, and the target is the Rule string.
3. Induct_ anduct_rewriter We also create a "induction" version of the Rewrite task. In this task, the source the LHS string concatenated with the RHS string, that the result of the rewrite. The target is the rewrite rule that is used to do the rewrite.
APPENDIX B.3 A FULL COMPARISON OF ALL SYNTHETIC TASKS
In this section we present a full comparison for all synthetic tasks. We followed the training protocol in and evaluate the method IsarStep. The results reported in Table 6 We the Rewrite mul multister tistep achieved the best performance across all synthetic tasks, surpassing the baseline by 8.2% for Top-1 accuracy and 10.8% for Top- accuracy. This indicates the inductive bias for long horizon reasoning encoded in Rewrite_multistee is very useful for the reasoning task.
that
APPENDIX C
MORE ABLATION STUDIES
APPENDIX C.I DOES THE VOCABULARY SIZE MATTER?
In this section, we investigate whether the vocabulary size S in the synthetic task generation algorithm has an effect on the performance. We used the REWRITE task for the experiment in this section. We generated datasets of various vocabulary sizes, 100, 512, 1000, 5000, 25000. We used the same curriculum learning for pre-training as described 4. on larger vocabulary sizes: first training on the Rewrite te task of vocabulary size 100 for 10K steps, then training each individual dataset for another 10K steps. We compare the performance on the downstream task Isarstep. The results are presented in Table 7 We see that when the vocabulary size is equal or larger than 512, the performance were similar. The smallest vocabulary size 100 obtained the worst performance among all, and all the other four models achieved similar BLEU scores. The model trained the largest vocabulary achieved best performance on top-1 accuracy and top- 10 accuracy. The results show there is non-trivial effect of the vocabulary size of the synthetic task to the performance of the
15

---

Under review as a conference paper at ICLR 2021
downstream task. Hence vocabulary size of 1000 for all the experiments in the main paper. We leave investigations of the causes to future work.
Table 7: Vocabulary sizes' effects on the IsarStep task.
Model
Top-1 Acc.
Top-10 10 Acc
No pretrain
20.4
33.1
LIME on Rewrite, S 100
24.1
37.5
LIME on Rewrite, S 512
25.4
38.8
LIME on Rewrite, S 1000
26.0
38.6
LIME on Rewrite, S = 5000
25.8
38.5
LIME on Rewrite, 25000
27.4
40.9
APPENDIX C.2 PRE-TRAINING ON ISARSTEP FOR METAMATHSTEP
Following Section 5.1 performed pre-training IsarStep for MetaMathStep. The result is shown in Table In contrast to MetaMath helping IsarStep, we see that pretraining on lsarStep task did not help the downstream task MetaMathStep. We hypothesize that this could be due to MetaMathStep task is closer to the LIME tasks than IsarStep, and hence providing more gains than the opposite direction. We leave investigations to the future versions.
Table 8: Pretraining on IsarStep for the MetaMathStep task.
Model
Top-1 Acc.
Top-10 Acc.
No pretrain
67.7
76.5
LIME Mix
69.1
77.9
Pretrain on IsarStep
67.0
76.1
APPENDIX C.3 DOES LIME HELP LSTMs?
In this section, we investigate if LIME also helps other architectures than transformers. In particular, we applied LIME to two LSTM based architectures: 1. vanilla LSTM, 2. LSTM with attention mechanism. The vanilla LSTM a stacking LSTM with 4 layers, each with 1000 cells, and 1000- dimensional embeddings. The LSTM with attention architecture is taken from Luong et al. (2015), also with 4 layers, 1000 cells and 9000-dimensional embeddings. We evaluate on the IsarStep task. and compared model trained from scratch and a model pre-trained on LIME abduct task. We used the same training protocol as described 4.T The results are shown Table g along with the results on transformer. We observe that LIME improved LSTM as well LSTM with attention, but the improvements were small compared to transformer. Specifically, we compare Top-1 accuracy, that LIME improved LSTM from 5.5% to 6.9%. LSTM with attention from 12.3% to 13.4%. and transformer from 20.4% to 26.7%. This observation is aligned with our hypothesis that the transformer is malleable architecture and hence it is capable of learning architectural inductive biases from datasets. This is mainly attributed to the potential of learning dynamic attention graphs in self-attention layers. We note that this still warrants further investigation as the performance of these architectures are not at the same level, and that may also lead to different improvements.
Table 9: Comparing LIME's benefits on LSTMs on the IsarStep Task
Model
Top-1 Acc.
Top- Acc.
LSTM
5.5
11.3
LSTM LIME Abduct
6.9
14.3
LSTM attention
12.3
22.7
LSTM
attention + LIME Abduct
13.4
26.3
Transformer
20.4
33.1
Transformer + LIME Abduct
26.7
41.0
16


Reviews:
[{"review_id": "rYQY08q-AHG", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 2, "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": "With the aim of learning inductive biases for deep neural net architectures, this paper presents three synthetic experiments for learning primitive forms of mathematical reasoning in theorem provers. The overall idea is inspired by Pierce’s view that these primitives are deduction, abduction, and induction. The synthetic tasks are built upon a simple arithmetic language with a source and a target. Using those tasks for pretraining a transformer model, the authors show the merit of this methodology in several mathematical reasoning experiments.\n\nI am not an expert in transformer models and pre-training techniques, so it is possible that I did not understand some parts in Section 4 & 5. Overall, I think that the idea of training a learner with primitive forms of inference is interesting for improving its performance in mathematical reasoning. The experimental results corroborate the relevance of this approach. \n\nMy main comment lies in the specification of synthetic tasks (Section 3.2). Here, the authors are using an ad-hoc arithmetic language upon which deduction, induction, and abduction tasks are defined. But this ad-hoc language has no formal semantics, so we cannot formally capture the primitive forms of reasoning. \n\nContrastingly, in Section 3.1, the three reasoning primitives identified by Pierce are well-defined because they are captured by the semantics of first-order logic. For example, take the abductive mode of reasoning:\n\nRule: $\\forall x, Bag(x) \\rightarrow White(x)$ (All the beans from this bag are white)\n\nResult: $White(o)$ (These beans are white, where $o$ is an object in the Herbrand universe) \n\nCase: $Bag(o)$ (These beans are from this bag) \n\nFrom the rule and the result, we can indeed infer by abduction that the case is an explanation of the result since:\n\n(i) $Bag(o) \\wedge \\forall x, Bag(x) \\rightarrow White(x) \\not\\models \\bot$ (consistency), and\n\n(ii) $Bag(o) \\wedge \\forall x, Bag(x) \\rightarrow White(x) \\models White(o)$ (consequence). \n\nBut in Section 3.2, the arithmetic language is given without any semantics, and hence, we cannot define a clear, unambiguous form of logical consequence ($\\models$). Therefore, the notion of abduction is here very unclear. \n\nTo sum up, the synthetic tasks proposed by the authors might indeed help in learning an inductive bias capable of improving theorem provers, but there is a discrepancy between the logical notions of deduction, abduction, and induction defined by Pierce (and more generally in the Knowledge Representation literature), and the reasoning primitives (essentially some forms of pattern matching) presented in the synthetic tasks. \n", "extra_scores": {}, "extra_text": {}}, {"review_id": "aqaR02w_S2E", "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": "\n## Summary\n\nThe authors propose LIME: a pretraining strategy for learning inductive biases for mathematical reasoning. They construct 3 synthetic datasets corresponding to 3 basic reasoning patterns: deduction, induction, and abduction. Each dataset is designed to be devoid of concrete mathematical knowledge but encodes inductive biases of the reasoning pattern. In experiments, LIME pretraining improves the performance of a generic transformer model on 3 benchmarks for mathematical reasoning: IsarStep, HOList Skip-tree, and MetaMathStep. \n\n\n## Strengths\n\n+ I really like the idea of designing the synthetic datasets inspired by 3 basic patterns of mathematical reasoning: deduction, induction, and abduction. Though the basic reasoning patterns were discovered a while ago, it is novel to apply the idea to synthetic data for theorem proving. Traditional automated theorem proving focuses on deduction, but as the authors have explained in the paper, induction and abduction also play significant roles in conjecturing and framing new definitions. \n\n+ The proposed LIME pretraining lead to descent performance improvements on 3 benchmarks. It is surprising since the pretraining task is a very simple string rewriting task without any mathematical knowledge. It is interesting if it actually works.\n\n+ The paper is well-written and very easy to read.\n\n\n## Weaknesses\n\n- The authors acknowledged that there are numerous alternative designs for the pretraining datasets and presented a few alternatives in the appendix. Are there empirical comparisons between these alternatives? Why did the authors decide to use the current ones?\n\n- It would be great to have ablations that only include 2 of the 3 pretraining datasets. Then we can know if the 3 reasoning patterns are truly irreducible. \n\n- In Sec. 3.2, I'm confused about how the authors define \"Rule\" and \"Case\". To me, it looks like A * A + B = C is more like a \"Case\", whereas {A : a; B : b; C : d + e} is more like a \"Rule\"; since it describes how to map rule symbols to math symbols.\n\n- I'm confused about framing \"pretraining\" as \"learning inductive biases.\" Technically, I believe it's correct. Suppose \"inductive biases\" is defined as the learning algorithm's preferences when choosing one hypothesis among many equally valid ones. In that case, the initialization of model parameters is a kind of inductive bias.  Then, any pretraining is \"learning inductive bias.\" It would be great if the authors clarify more about \"pretraining\" and \"inductive biases\" in the next revision.\n\n\n## Conclusion\n\nI like the idea of constructing synthetic datasets inspired by basic reasoning patterns. And it is surprising that pretraining on these simple tasks can work. However, I have a few questions, and the paper lacks ablations. I could potentially raise my score if the authors are able to address these questions.\n\n## Minor Comments\n\nThese are minor points that did not account for my score. The authors do not have to address them in the rebuttal.\n\n1. There should be more margin between Table 1 and the caption of Table 2.\n\n2. Use \"K\" for thousand consistently, not \"k.\"\n\n3. \"We set the size of the math symbol set 44 and rule symbol set of size 24.\" This sentence is difficult to parse correctly. I thought there was a typo before reading it a few more times.\n\n\n\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "JSfNIp_7hv3", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 8, "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": "In this work, the authors introduce a method called LIME for imparting certain mathematical inductive biases into a model. The structure of the approach is to first pretrain the model on synthetic tasks that are designed around three principles of mathematical reasoning: deduction, induction, and abduction. Each of these pretraining tasks is a sequence-to-sequence mapping involving 3 basic components of reasoning (Rule, Case, and Result), where two of these three components are provided as input and the third component is the target output. After pretraining on these tasks, the authors fine-tune on 3 different proof datasets, and find that the pretraining almost always improves performance, sometimes by a large margin.\n\nStrengths:\n1. This approach is creative and thought-provoking; pretraining is an important topic in ML nowadays, and this paper gives several interesting insights about how to structure pretraining. Therefore, publishing this paper at ICLR could help inspire others to use and develop improved variations of pretraining.\n\n2. One aspect of the pretraining that I found particularly impressive was how the authors found such clear improvements from such small amounts of pretraining. This is in stark contrast to the usually massive pretraining datasets that are used, and stands as an especially strong piece of evidence for the model’s usefulness.\n\n3. The experimental setup is well-motivated, drawing on a principled analysis of the problem domain. \n\n4. The paper is overall clearly written and clearly structured.\n\n5. There were some interesting discussion points and ablation studies analyzing the approach in more detail. I particularly liked the discussion about how loading the vocabulary weights had little effect, showing that the inductive biases that were imparted were abstract in nature. It was also useful to see that LIME was more useful than other pretraining tasks, ruling out the possibility that you could get similar improvements from just any pretraining task.\n\nWeaknesses:\n\n1. Part of the paper’s motivation for imparting inductive bias through a dataset, rather than through an architecture, is that designing an architecture “strongly requires human insight.” This is true, but LIME also seems to strongly rely on human insight, so this point is not a benefit for LIME over architectural approaches. This is not a huge problem, but it does not seem like a great motivation for LIME. \n\n2. Related to the previous point, it would be good to discuss the fact that the usefulness of LIME may be limited by the need to design the right pretraining task(s). As Table 4 shows, the nature of the pretraining task is very important; and although the authors were able to create some successful pretraining tasks for mathematical reasoning, it might be harder to create similarly useful tasks for larger-scale tasks in, e.g., language or vision. Again, this is not a huge problem, but I think it at least deserves some discussion.\n\n3. Though the goal of the approach (if I am understanding correctly) is to give inductive biases for induction, deduction, and abduction, the paper gives no direct evidence that it has done so: The authors create an approach *intended* to impart certain inductive biases, and this approach improves performance on 3 tasks that plausibly would benefit from those biases. But this result does not necessarily mean that the model has the inductive biases that were intended to be imparted; it’s possible that LIME imparted some other inductive biases that are also useful for mathematical reasoning but that are not related to induction, deduction, and abduction. Thus, there is a bit of a gap between the motivation and the actual experiments.\n\n4. It’s not entirely clear to me that the specific tasks (Deduct, Induct, Abduct) will necessarily enforce the types of reasoning that they are intended to enforce. For instance, consider the following input/output example: {A : a, B: b, C: d+e} 
 A A + B = C -> a a + b = d + e. Such an example is intended to show deduction, but it could instead be viewed as induction (where A A + B = C is the Result, a a + b = d + e is the Rule, and the Case dictionary should be read in reverse, treating the values as keys and the keys as values). Thus, related to the previous point, I think there is some concern that the LIME tasks may not necessarily encode the intended primitives. The results show that the LIME tasks clearly encode something useful, but it’s not clear exactly what useful things they encode. \n\nRecommended citations: (you definitely don’t need to include all of these or even any of these, but I’m pointing to them just in case they’re useful):\n\n1. You already cite the GPT-3 paper (Brown et al.), But it might make sense to cite it in a second place as well, for the sentence where you say “However, there is another potential advantage of pre-training--it may distill inductive biases into the model that are helpful for training on downstream tasks.” Another paper you can cite for this point is this one: Can neural networks acquire a structural bias from raw linguistic data? https://arxiv.org/pdf/2007.06761.pdf\n\n2. Like your approach, the following paper also uses carefully-constructed synthetic datasets as a way to impart targeted inductive biases into a model. (However, they use these tasks for meta-training, not pre-training): Universal LInguistic Inductive Biases via Meta-Learning. https://arxiv.org/pdf/2006.16324.pdf. This paper might also be useful as an example of how you can address the last two points I listed under weaknesses, as this paper gives examples of how to test whether a model has some specific inductive biases; the paper I linked to in the previous bullet (Warstadt and Bowman) also does this. (However, adding such analyses might be more work than would be doable for a camera-ready).\n\n3. It might be good to cite Peirce when first mentioned in the intro; right now, the citation to Peirce is buried deep in the paper, after he has already been discussed at length.\n\n4. Some more potentially-relevant examples of architecturally encoding inductive biases for math: https://arxiv.org/pdf/1910.02339.pdf, https://arxiv.org/pdf/1910.06611.pdf \n\nOther comments (these are not things that have affected my assessment. Instead, they are just comments that I think might be helpful in revising):\n\n1. Note that there is another approach in ML called LIME, which could potentially cause confusion. It’s completely up to you, but I would consider renaming to avoid confusion. Here is the other LIME by Ribeiro, Singh, and Guestrin: https://dl.acm.org/doi/pdf/10.1145/2939672.2939778?casa_token=VrGSeKoqOnkAAAAA:tmzXq2uCWkUVyPdd9ytCNK4LSdRfIwsIeX4hd8EMkjnjevZ4d-rCeIIM7acIRWGtQlQemUqDlAJx-Q \n\n2. Abstract: “neural architecture” should be “neural architectures”\n\n3. Abstract: “on three large very different mathematical reasoning benchmarks” should be “on three very different large mathematical reasoning benchmarks”\n\n4. Abstract: I did not understand what “dominating the computation” meant until I read the rest of the paper.\nThe intro says “It is commonly believed that the benefit of pre-training is that the model can learn world knowledge by memorizing the contents of the natural language corpus.” This statement seems strong - I am more inclined to think that much of the benefit comes from learning linguistic structure, not world knowledge. So it might be safer to reword as saying “One plausible explanation for the benefit of pretraining is…”\n\n5. Page 3 says “the BERT pretraining objective,” which suggests that BERT is the objective. But BERT is a model, not an objective; the objectives are masked language modeling and next-sentence prediction.\n\n6. Table 1: The formatting of the table makes it look like the first two rows are numbers copied from Li et al. But from the prose of your paper, and from looking at Li et al, I’m pretty sure that these numbers are from your own re-implementation. Is that correct? If so, it might be best to format the table different - using the citation within the body of the table gives a strong suggestion that the numbers come from Li et al., in my opinion.\n\n7. Table 4 and Table 5: In the caption, say what task these results are for, so that the table can be understood on its own.\n\n8. Please double check the references: Several of them seem to only list authors, title, and year when there is at least an arXiv version that could be listed as well. E.g., “Mathematical reasoning via self-supervised skip-tree training”, “Enhancing sat solvers with glue variable predictions”, “transformers generalize to the semantics of logics”. Also, where possible, cite a paper’s actual publication venue instead of arXiv - e.g., the Raffel et al. T5 paper appeared in JMLR, not just arXiv. \n\nSummary: Overall, I am rating this an 8 because I find the strengths compelling but think that the weaknesses in framing hold the paper back from an even higher score. I would consider increasing the score if those weaknesses were addressed, though those weaknesses are deep enough that it would be hard to properly address them in time.\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "1UIYk_KdHqL", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "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": "Summary: \nThis paper proposes a pretraining method, LIME, to improve Transformer’s performance on mathematical reasoning benchmarks. Specifically, this paper design three synthetic tasks to teach the transformer model to first learn three primitive reasoning steps: deduction, abduction, and induction respectively. The three datasets are used in the pre-training step, and the paper shows empirical performance gains on large mathematical reasoning tasks in the context of automated theorem proving.\n\nReasons for the score: \nThis paper provides an interesting direction in the field of automated theorem proving. In particular, it proposes a novel way to teach the model to learn primitive reasoning steps via designs of datasets. The paper provides good motivations and intuitions for their proposed method, but it would be nice for the authors to also formalize these intuitions and provide rigorous definitions as an academic paper (e.g. what is inductive bias and so on; details see below). The proposed method provides some ablation studies in the experiment section, but it is still worthwhile to conduct the following studies to enhance the quality of the paper: 1) how the positive transfer from the proposed pretraining change as we increase the size of the model? 2) It seems unclear from the current text how the LIME pretraining compares with large-scale unsupervised pretraining (e.g. BERT) in terms of convergence rate and the number of samples needed on the downstream tasks. For example, would pretraining on BERT lead to faster convergence and a smaller number of samples compared to LIME pretraining?\n\nPros:\n1.The idea of designing pretraining datasets to help mathematical reasoning is novel. \n2.Good empirical performance gains on large mathematical reasoning tasks in the context of automated theorem proving\n\nCons:\n1.Though the proposed method provides some ablation studies in the experiment section, but it is still worthwhile to conduct the following studies to enhance the quality of the paper:\n\na. How the positive transfer from the proposed pretraining change as we increase the size of the model? \n\nb. It seems unclear from the current text how the LIME pretraining compares with large-scale unsupervised pretraining (e.g. BERT) in terms of convergence rate and the number of samples needed on the downstream tasks. For example, would pretraining on BERT lead to faster convergence and a smaller sample complexity comparing to LIME pretraining?\n\nc. Would the proposed method have similar improvements when using different architectures (e.g. LSTM, LSTM+attention, GPT2)?\n\n2.The writing provides good intuitions in general, but it would be nice for the authors to also formalize these intuitions and provide rigorous definitions as an academic paper:\n\na. The word “inductive bias” may have different connotations across different contexts and it would be nice for the authors to give a more formal definition of what they mean by “inductive bias” in the context of this work. For example, inductive bias may refer to the structural bias imposed by the architecture. It may also refer to the prior knowledge of the target tasks or to the preference of the training scheme (e.g. what kind of functions are learned first by an SGD optimizer). It seems to me that the usage of inductive bias in this work is close to the prior knowledge of the target tasks, but this is not clear from the current writing.\n\nb. Similarly, it would be nice for the authors to clearly state what they mean by ‘‘knowledge’’ in the context of this work. Is it referring to knowledge distillation, learned representations of the context, or something else? For example, in this sentence “we focus on the latter and design pre-training tasks that are intentionally devoid of knowledge and only allow the model to learn inductive bias for reasoning”, it is unclear why specific reasoning procedure cannot be treated as a form of knowledge.\n\n3.The design of the three pre-training tasks is based on the three primitive rules for logical reasoning, which requires nontrivial human insights to formalize. Thus, the proposed approach may not be easily transferrable to other fields.\n\n4.It would be nice for the authors to provide discussions with relevant works on the reasoning abilities of neural networks such as [1] and [2]. The proposed dataset in [1] could be of interest to this work as a pretraining dataset. [2] provides a theoretical framework to formalize the inductive bias in graph neural networks, which demonstrate the limitations of graph neural networks in terms of its reasoning capacity.\n\n[1] Saxton, David, et al. \"Analysing mathematical reasoning abilities of neural models.\" arXiv preprint arXiv:1904.01557 (2019).\n\n[2] Xu, Keyulu, et al. \"What Can Neural Networks Reason About?.\" arXiv preprint arXiv:1905.13211 (2019).", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: 
The authors propose a pretraining strategy learning inductive biases in transformers for deduction, induction, and abduction.  Further, the claims and results seem to indicate that such pretraining is more successful in transformers which provide a more malleable architecture for learning inductive (structural) biases.  There are open questions that remain, specifically surrounding disentangling high performance from structural bias learning (i.e. is pretraining doing what we think it is) and whether datasets are the "correct" mechanism for imparting such biases/knowledge.
Decision: Reject