IsarStep: a Benchmark for High-level Mathematical Reasoning
Authors: Wenda Li
Lei Yu
Yuhuai Wu
Lawrence C. Paulson
Venue: ICLR 2021 Poster (2021)
Keywords: mathematical reasoning
dataset
benchmark
reasoning
transformer

Abstract: A well-defined benchmark is essential for measuring and accelerating research progress of machine learning models. In this paper, we present a benchmark for high-level mathematical reasoning and study the reasoning capabilities of neural sequence-to-sequence models. We build a non-synthetic dataset from the largest repository of proofs written by human experts in a theorem prover. The dataset has a broad coverage of undergraduate and research-level mathematical and computer science theorems. In our defined task, a model is required to fill in a missing intermediate proposition given surrounding proofs. This task provides a starting point for the long-term goal of having machines generate human-readable proofs automatically. Our experiments and analysis reveal that while the task is challenging, neural models can capture non-trivial mathematical reasoning. We further design a hierarchical transformer that outperforms the transformer baseline. 

Published as a conference paper at ICLR 2021
ISARSTEP: A BENCHMARK FOR HIGH-LEVEL MATHEMATICAL REASONING
Wenda Li University of Cambridge w1 w13020cam ac..uk
Lei Yu DeepMind l yei com
Yuhuai Wu
University of Toronto, Vector Institute ywuêcs toronto.edu
Lawrence C. Paulson University of Cambridge 1p158cam. ac.
ABSTRACT
A well-defined benchmark is essential for measuring and accelerating research progress of machine learning models. In this paper, we present a benchmark for high-level mathematical reasoning and study the reasoning capabilities of neural aequence-to-sequenee models. We build non-synthetic dataset from the largest repository of proofs written by human experts in a theorem prover. The dataset has a broad coverage of undergraduate and research-level mathematical and computer science theorems. In our defined task, a model is required to fill in a missing intermediate proposition given surrounding proofs. This task provides a starting point for the long-term goal of having machines generate readable proofs automatically. Our experiments and analysis reveal that while the task is challenging, neural models can capture non-trivial mathematical reasoning. We further design a hierarchical transformer that outperforms the transformer baseline. The dataset and models are available from: https: ///github. com/
INTRODUCTION
Neural networks have achieved outstanding performance on wide range of problems in natural language processing, computer vision, and speech recognition. However, research investigating their capacity of doing mathematical reasoning is still limited, with earlier attempts focusing on
simple arithmetic tasks like integer addition and multiplication (Zaremba & Sutskever [014] Kaiser & Sutskever 2016 Trask al.) (2018). More recently, there has been work solving school-level mathematical problems (Saxton et al. 2019), logical reasoning (Evans et al.) 2018), and problems of function integration, ordinary differential equations (Lample & Charton 2020), and properties of differential systems (Charton et al.) (020). While these are valuable contributions to the machine learning community, they focused generating answers questions from specific domain and were carried out on synthetic datasets with small vocabulary (e.g. up to 100 unique tokens).
In this paper, we consider general undergraduate and research-level mathematical proofs target for neural networks. When humans prove theorem, a crucial step is to propose an intermediate proposition bridge the gap between the goal and the currently known facts. This step requires complicated reasoning capabilities such as creative thinking, inference, understanding existing conditions, and symbolic manipulation of rules. For example, consider the following proof of the irrationality of /2:
Proof of irrationality of V2. Assume v2 is rational. Then there exists pair of coprime integers and b such that v2 = a/b, and it follows that a² /B² and then 2b a². Hence is even. Thus there exists an integer such that a = 2c, which combined with 26 = a² yields 2c² = b2: hence b is also even. So and b are both even although they are coprime, contradiction.

---

Published as a conference paper at ICLR 2021
theorem "sqrt É Q" proof
assume "sqrt 2 Q"
then obtain b int where "sqrt 2 a/b* "coprime a b"
by (metis Rat_ cases Rats_def def imageE normalize stable of of_rat_divice
of_rat_ _ot_ooo____ int eq quotient ofriiooFrrrrr Fract quotient __ _ivv
then have "2
b2n by (smt of of_int_power power power_divide real_sqrt_powe then have *:'2*b² a²
by (cases "b=0", autoo simp:field simps, use of af_int__ ff_int_eq_it eq_iff in fastforce)
10
then have "even a"l by (metis dvd triv left even pot__mllt_ii iff power2_eg _ere2_e__suuaaa_ees_e___ee square)
obtain c:rint where "a=2*c" by blast
12
with have "b2 2*c2" by simp
13
then have "even b" by (metis dvd. trittiv__eee left even_ coon_mult_iri power2 eq square)
14
with ceven a> <coprime a by show False by auto
15 qed
Figure 1: Full declarative proof the irrationality of /2 in Isabelle/HOL.
To derive 3c Z. 2c from 21² a², the intermediate proposition "a is even" would reduce the gap and lead to a successful proof. We would like to simulate the way humans prove theorems by proposing an intermediate proposition synthesis task IsarStep. Instead of having primitive steps like 3 + 5 = 8, the proof steps in IsarStep are at higher-level, with much bigger steps as basic. Therefore it usually cannot be simply solved by pattern matching and rewriting. To succeed in this task, a model is required to learn the meaning of important mathematical concepts (e.g. determinant in linear algebra, residue in complex analysis), how they are related to each other through theorems, and how they are utilised in proof derivations. Solving the IsaStep task will be potentially helpful for improving the automation of theorem provers, because proposing a valid intermediate proposition will help reduce their search space significantly. It is also first step towards the long-term goal of sketching complete readaare proofs automatically.
We have built the IsarStep dataset by mining arguably the largest mublicly-hosted repository of mechanised proofs: the Achieve of Formal Proofs (AFP) The AFP is checked by the Isabelle proof assistant (Paulson 1994) and contains 143K lemmas. Combining the AFP with the standard library of Isabelle/HOL. yields dataset of 204K formally-proved lemmas. The dataset covers a broad spectrum of subjects, including foundational logic (e.g. Gödel's incompleteness theorems), advanced analysis (e.g. the Prime Number Theorem), computer algebra, cryptographic frameworks, and various data structures. A nice property of the mined formal proof's is that they are mostly declarative proofs, proof style very close to human prose proofs Fig. illustrates the proof of irrationality of v2 in Isabelle. We can see that the proof is actually legible (even to people who are not familiar with the system) and and it captures high-level structures like those in human proofs.
We further explore the reasoning capabilities of neural models. We frame the proposed task as (seq2xeq) prediction problem. Beyond evaluating the existing neural seq2seq model baselines the seq2seq with attention (Bahdanau et al. (015). the transformer (Vaswani et al. 2017) we also propose a new architecture, the hierarchical transformer ($4). The architecture is motivated by the way humans reason about propositions; it consists of a set of local transformer layers, modelling the representation of each proposition, and a set of global layers, modelling the correlation across propositions. Experiments ($5) show that these neural models can solve 15-25% of problems on the test set, and the hicrarchical transformer achieves the best result. Further analysis (66) on the output of these models shows that while the proposition synthesis task is hard, the neural models can indeed capture mathematical reasoning. We find that the embeddings of closely related mathematical concepts are close in cosine space; models can reason about the relation between set, subset, and member, and perform more complex multi-step reasoning that is even hard for humans.
Our contributions are summarised follows:
1. We mine large non-synthetic dataset of formal proofs and propose task for evaluating neu- ral models' mathematical reasoning abilities. The dataset contains 820K training examples with vocabulary size of 30K.
httpps:/wwet isa a f org
A comparison of proofs in different systems is available in Wiedijk 2006). The declarative style proof is also available in Mizar (Grabowski et al. 2010), where the style originates.
2

---

Published as a conference paper at ICLR 2021
2. We evaluate existing neural seq2seq models on this task.
3. We introduce hierarchical transformer model, which outperforms the baseline models.
4. We provide a comprehensive analysis of what has been learned by the neural models.
5. We provide test suite to check the correctness of types and the validity of the generated propositions using automatic theorem provers.
2 THE ISARSTEP TASK
In this section, we define the task of intermediate proposition generation more concretely, We again take the proof of irrationality of / as an example. We will have the following derivation:
26 26²= a is even
3c Z. a = 2c
(1)
(2)
In our proposed task, we would like to generate (2) given (1) and (3). When humans prove a theorem, they implicitly assume certain background knowledge, lemmas. For example, in this case we assume that we can trivially prove (1) > (2) based on the fact that the product of two numbers are even iff least one of them even. In Isabelle (Paulson 1994). these relevant lemmas (e.g. even @ven_mult__.
even (2a ?b) (even ?a even ?b) corresponding to line 10
in Fig. [ can be found automatically by its built-in automation Sledgehammer (Blanchette et 2011). In our task, we optionally provide these lemmas as extra information in addition to (1) and (3).
The derivation of (2) + (3) in the proof above is a simple step, because only (2) is needed to arrive (3). most cases, multiple propositions have to used logether order to infer proposition, for example P1 P2. P3 = P2. For these more general cases, we also include the additional propositions (e.g. P2 and P1) as part of the source propositions.
To summarize, each example in the IsarStep dataset is formed by five parts:
F1 a target proposition (c.g. is even).
F2 a set of used local propositions to derive F.1 (c.g. 26² = a²).
F.3 local proposition derived from the target proposition (3c Z. 2c),
F.4 other local propositions and (library) lemmas used to justify M3
F.5 set of used (library) lemmas to justify F. (e.g. crre__mult_ifee even (?a ?b)
(even Pa V even {b)).
We synthesise F.1 given R22 F4 with F.5 optional: the named lemmas in R. are common
knowledge and can be used as additional hints. The propositions are generated as a sequence of tokens and therefore the search space Σ": search over 30K actions ($3.3) vocabulary size for seq2seq models) at every timestep without predefined maximum output length.
IsarStep can considered as single step reasoning, which can repeated to sketch more complex proofs. Good performance on this task is crucial step for designing models that can automatically prove theorems with minimal human assistance.
DATASET PREPROCESSSING AND STATISTICS
The mined raw dataset has long propositions and large number of unique tokens. To alleviate the performance deterioration of machine learning models due to the aforementioned problems, we propose tricks to preprocess the raw dataset, including free variable normalisation and removing unnecessary parentheses. These tricks substantially reduce the sequence lengths and vocabulary size.
3.1 THE LOGIC AND TOKENS
The core logic of Isabelle/HOL is simply-typed X-calculus with de Bruijn indices for bound variables (Wenzel 2020 Chapter 2.2). A local proposition (library) lemma/theorem is essentially a term
3

---

Published as a conference paper at ICLR 2021
in the calculus. As types can be inferred automatically, drop types in terms (to reduce the size of the vocabulary) and encode a term as a sequence of tokens that include lambda term constructors: CONST, FREE, VAR, BOUND, ABS (function abstraction), and (function application). Additionally, parentheses have been used in the sequence to represent the tree structure. To give an example, we encode the proposition even as the following sequence of tokens separated by white space:
CONST HOI., Trueprop $ (CONST Parity. sem
even $ PRRE <x0>>
where CONST HOL Trueprop is a boilerplate function that converts from type bood to prop; CONST Parity serity..emiiill.
even is the even predicate; FREE <x0> en-
codes the Skolem constant a in even a. Since is a user-introduced local constant that can be arbitrary, we normalised vocabulary size (see $3.2).
the algorithmically generated name <x0> in order to reduce the
Overall, every local proposition and library lemma/theorem is encoded sequence of tokens, and can be mostly decoded to the original term with type inference.
3.2 FREE VARIABLE NORMALISATION
Due to Isabelle's s use of de Bruijn indices, bound variables have already been normalised: V x. P x is no different from V y. y, as both and y are encoded as BOUND However, arbitrary variable names can be introduced by the command fix in declarative proofs or unbounded variables in lemma statements (e.g. False = P and False = Q are semantically equivalent but with different free variables). To reduce the vocabulary size here, we normalised these free variables like the bound ones. For example, False = P would be normalised to False = <V0> as is the first free variable in the proposition. Such normalisation reduced the vocabulary size by one third. The normalisation preserves the semantics, and we can always parse a normalised term back under a proper context.
3.3 STATISTICS
We have mined a total of 1.2M data points for IsarStep. removed examples in which the length of the concatenation of the source propositions, i.c. F2 F4 in longer than 800 and the length of the target propositions, i... F1 in $ longer than 200, w which results in approximately 860K examples. From these examples data, we removed duplicates, the examples whose target propositions exist in the held-out set, and those that are from the same theorems as the propositions in the held-out set. The final dataset split is 820K, 5000, 5000 for the training, validation, and test sets, respectively. The vocabulary size is 29,759.
randomly sampled 10K examples for validation and test. In the training
4 MODEL
We define X = [x .......,'''
x'] as the sequence of / source propositions, and = (v1 V2. yN) the target proposition containing N tokens. Let xx' = (2......... xMM) represent the ith proposi- tion in the set, consisting of M tokens. Each source proposition æ belongs to category F2 F.4
defined in $2 We annotate the category corresponding to æ' as C, and therefore the sequence of categories corresponding X is C = [C1, C2........ ....... Cr). The generation of target proposition y is determined by finding the proposition y. where p(ù X,C) is optimal,
ÿ = arg max ply X,C).
We propose two approaches to parameterising the conditional probability p'y X,C), which differ in the way of modelling the sequence of source propositions. The first method is simply appending a label to each source proposition indicating their category and then concatenating the source propositions using a special token <SEP>, treating the resulting long sequence the input to seq2seq model.
Our second approach models the encoding of source propositions hierarchically. As shown in Fig. 22, the encoder has two types of layers. The local layers build the proposition representations by modelling the correlations of tokens within each proposition; the global layers take the proposition
4

---

Published as a conference paper at ICLR 2021
Category Position Taken
Local Layers
Global Leyers
Propostion Proposation
Figure 2: Architecture of the encoder of the hierarchical transformer (HAT). There are two types of layers, the local layers model the correlation between tokens within proposition, and the global layers model the correlation between propositions. The input to the network is the sum of the token embedding, the positional information, and the embedding of the corresponding category.
Table 1: Test set accurarcies (exact match) and BLEU scores of different models on the IsarStep task.
Top-1 I Acc.
Top- 10 Acc.
BLEU
Model
Base
F.5
Base
F.5
Base
+ F.5
RNNSearch
13.0
16.7
26.2
32.2
42.3
52.2
Transformer
20.4
22.1
33.1
34.6
59.6
62.9
HAT
22.8
24.3
35.2
37.2
61.8
65.7
representations as input and model the correlations across propositions. Both the local layers and global layers are transformer layers (Vaswani al., 2017). Positional information is encoded separately for different source propositions. That is, suppose x² has M tokens, then the position of the first token in x² is not M + 1 but The embedding of a token sm is obtained by adding the token embedding, the positional information, and the embedding of the category that the proposition x' belongs The category embedding is learnt together with the rest the network. We call this model the hierarchical transformer (HAT), Intuitively, HAT models the structure of the source propositions more explicitly compared the first approach and therefore should be better at capturing reasoning between source and target propositions. We will validate our hypothesis in $5)
EXPERIMENTS
benchmark three models on IsarStep ($2). namely the seq2seq model with attention (RNNSearch) (Bahdanau et al.] 2015) Wu et al.) 2016). transformer (Vaswani et al. (017), and hierarchical transformer (HAT). The input to the RNNSearch and the transformer is concatenation of source propositions (the first parameterisation approach described in $4). We train these models with the same training data and report their performance on test sets. See appendix for experimental setup.
5.1 EVALUATION
Widely used metrics for text generation are BLEU score (Papineni et al.) 2002) and ROUGE score [Lin 2004) that measure n-gram overlap between hypotheses and references. Both metrics are not ideal mathematical proofs since a proposition can be invalid due to one or two incorrect tokens. Therefore, in addition to BLEU score, also consider exact match between hypotheses and references as our evaluation metric. We report top-1 accuracy and top-10 10 accuracy. The top-1 accuracy is the percentage of the best output sequences that correct in the given dataset. The t0p-10 accuracy is the percentage of target sequences appearing in the top 10 generated sequences.
It is possible that models generate alternative valid propositions that not exactly the same as the references. We further implemented a test suite to bring the generated propositions back to the Isabelle environment and check their correctness using automatic theorem provers (ATPs).
5

---

Published as a conference paper at ICLR 2021
5.2 RESULTS
BLEU and Exact Match Table 1 presents the results of different models for the IsarStep task. Overall, the neural seq2seq models achieve around 13-25% top-1 accuracies and 26-38% top-10 10 accuracies, which indicates that this task is non- trivial and yet not too difficult for neural networks. Of the three models, the transformer (Vaswani et al.) 2017) outperforms the RNNSearch (Bahdanau ett al.
2013: Wu et al.] 6016) significantly and our HAT performs best. As mentioned in 2 adding F.5 is optional and is conjectured for better performance due to exploiting used lemmas explicitly. We experimented with both cases and found that adding this extra information indeed leads to further improvement. This is consistent with the scenario when humans prove theorems: if humans are told that certain lemmas are relevant the current proof, they will these lemmas and have better chance of success.
Alternative Valid Propositions We consider an output propo- sition P as an alternative valid intermediate proposition if 1) P well-formed proposition and does not match the ground truth at the surface form; 2) P does not match any substring of the source (to avoid being simple copy of F.3 or assumption in F:2;; 3) both F22 P and P
Table 2: Percentage of correct propositions.
Model
Base
F.5
can be automatically
proved by ATPs Note that this will only give us a lower bound to the number of alternative propositions, due to the limitation of ATPs' automation. Table T presents the percentage of correct propositions on the test set. Correct proposition is proposition that matches either the corresponding ground truth or one the alternative valid propositions. We can that alternative propositions contribute percentage point more correct propositions, compared to top-1 accuracy in Table
Transformer
25.2
26.8
HAT
27.6
29.4
Automation Improvement In lots of cases, ATPs cannot infer from one step to another automat- ically (i.e. F2 F3 without the crucial intermediate steps proposed by humans. We found that cannot be proved automatically by ATPs. And within these 3000 cases, 61 cases can be proved automatically given the generated intermediate propositions from our HAT model: F2 P and P ther progress is needed to improve seq2seq models' reasoning capability in order to improve the automation of theorem provers significantly.
there are about 3000 cases in our test set that F2
F3
F33 This is not big improvement. Fur-
Better Generalisation of НAT Since the transformer and HAT have different source sequence encoding, we explore how well these two models perform on examples with various source sequence lengths. We categorise the examples the IsarStep test set into 5 buckets based on their source lengths and calculate the top-1 accura- cies for different buckets, shown in Fig. 3 Interestingly, although we did not train the models with source sequences longer than 512, they can still achieve reasonable accuracies long sequences. In particular, HAT performs significantly better than the transformer on sequences longer than 480. Especially in the length bucket of 640-800, HAT doubles the accuracy of the transformer.
Tranformr
HAT
20.0%
15.0%
5.0%
0.0%
160-300
Figure 3: Accuracy of differ- ent source sequence lengths.
Importance of Category Information We subsequently investi- gate the effect of incorporating the category information for source propositions into the models by removing the category embedding for the input to the HAT encoder (Fig. 2) i.c. we are now modelling p(y X) instead of p(y X. X.C). We see dramatic drop in accuracy: 14.6 versus 22.8 obtained by the HAT with category embedding included, indicating the importance of category information. This is in line with human proofs: without knowing the logical relations between propositions, we do
F,3 is directly provable via ATPs, trivial proposition (e.g. 1 = 1) can be considered as an alternative. This is hard to detect automatically but could still serve fair comparison across seq2seq models long as they can propose well-formed trivial proposition in such scenario.
'Ir F2

---

Published as a conference paper at ICLR 2021
not know what proposition is missing. This indicates that the models not simply doing pattern matching but should have captured some reasoning information.
QUALITATIVE ANALYSIS
In this section, we present analysis of what has been learnt by the neural network models. To summarise our findings: 1) the seq2seq models can learn the syntax of propositions correctly; 2) the learned token embeddings are comprehensive in that related mathematical concepts are close in cosine space: 3) manual inspection of the generated propositions reveal that models can learn non-trivial mathematical reasoning and even more complicated multi-step reasoning.
Token Embeddings To investigate whether the seq2seq models have learnt mathematical reason- ing, we checked whether the learnt token embeddings were meaningful. We first projected the learnt embeddings for all the tokens in the vocabulary into a three-dimensional space via principal compo- nent analysis and chose random tokens and checked their 50 nearest neighbours in cosine distance. We found that the embeddings of related concepts in mathematics were close, indicating that the models have managed learn the relations between mathematical concepts the basic step towards reasoning mathematically. For example, in Fig. 4 the neighbours of 'Borel measurable' are mostly measure theory related including 'almost everywhere', 'integrable', and 'null set', while 'arrow' is close to 'isomorphism' (EpiMMonlsoocaate wtt.sso.catoooiiioooo 'identity' "Category.partin partiallmaaaaaaa...o mal__mmaaaaaeee and 'inverse arrow' arithmetic also seems to connect related mathematical definitions: for example, the three closest tokens next to 'bounded' + 'closed' are 'bounded', 'closed', and 'compact', where compactness can be alternatively defined boundedness and closedness (on a Euclidean space).
which are concepts in category theory. Additionally, vector
Attention Visulisations We next investigate how reasoning has been learnt by visualising attentions from transformer (Vaswani al., 2017). We find that important and related tokens are likely to attend to each other. For example, Fig. illustrates the visulisation of the last layer of the transformer encoder
for the source propositions [22
F33; 3770 E X:39 F.4 J55 T30- The target proposition generated from the model is I70 E C57. The interpretation of those source propositions is that combining with
(F4 I57 C 239 we would like to infer the intermediate step so that the goal 1770 E I39 can be proved. The transformer model gives the correct answer 270 E Ø57 which implicitly applied the lemma
x E A,A,A C B
B
that relates E and C. On the last self-attention layer of the transformer encoder (Fig. 5 E and C attend each other. Interestingly, the above reasoning seems robust. If we swap 257 and 339 in
Z39 S Æ37). the answer becomes I70 E Zzg. This totally makes sense since 2p no longer applies (despite that and C still attend to each other
E4 (i.e., the source is now F22 F.3 270 E 239
F4
similarly as in Fig. 5) and 270 E .:39 can only be discharged by proving itself.
Multi-Step Reasoning By further inspecting the generated propositions, we find that the model can implicitly invoke multiple theorems as humans normally do. While this property can be found in quite few examples, here we show one of them due the limited space. We refer the readers the appendix for more examples. Given the source F2: dli((spanzzo) S card(a22) F33 card(22) dim(zo) F.4 (22) S dim())). finite(r2), where dim, span and card refer to the dimensionality, the span, and the cardinality of set of vectors, respectively, and the model gives the correct answer dim(zo) < (22) Here, dim(zo) < card(22) is derived by dim(span I card(x2) only if the model has implicitly learned the following theorem + ddim(span(SS (S) dim() & ca2)( yields c22)( = dim(ao) (in conjunction of card (x2) I dim(xo)) only the model has implicitly invoked the antisymmetry lemma I S y. x H x = y-
dim(S), while
Failures We observe that incorrect propositions are well-formed and plausible propositions but they are usually copy of parts of the source propositions.
7 RELATED WORK
There have been a series of work that evaluates mathematical reasoning abilities of seq2seq models. The tasks that these works attempt to solve include school-level mathematical problems (Ling et al..
7

---

Published as a conference paper at ICLR 2021
Jagms Alaibr nesuubble
oftitaation adapt, stachann
Boooe_@ppaeebbfeLLeesuuee measurale
Madee Cre
Sembolkammde
Calegory.partial arr
Menuse Spacersl asts
CONST
.MRly, Cww.ll/eeeccaseeraccc.oo www.eeeenwweedeaee. wolliie AFREE
Aloroeaatie, jroepatiet
.Comerypennal prggrti
Sppce simont pvrrpite
Stapilogicall Spaces
canoperjarr
Congrrance portil ctaettcarter
aiiiic, Irit
Catepry-ennniee hergugge
Moneggetve
Figure 4: Nearest neighbours of the tokens 'Borel measurable' (left) and 'arrow' (right) in cosine space. The 512-dimensional embeddings are projected into 3-dimensional embeddings. Neighbours are found by picking the top 50 tokens whose embeddings are closest to the selected token.
commogaanee others
comumaance www.eeettteeeeeo.oooooooooo otheres
0OUST atreru
aereento
Sermerer 5e
172 <070>
DONST
D0N01
DOKST
betrembe
5
FREE
CONAT
CONEST
FREE
-0ET>
CONCT
3
FREE
TREE
CONeS
HOL TTUSSO
CONKS
FREE
Figure 5: Attention visualisation of the last layer of the transformer encoder for the source propositions
I'70 E T339
F4
337 S
Z39. The generated target proposition is 270 Ø57-
function integration and ordinary differential equations (Lample & Charton 2020), properties of differential systems (Charton et al. 2020), SAT formulas and temporal logic (Finkbeiner et al.) 2020). Our task is different from the previous ones in the sense that ours is non-synthetic, with realistic vocabulary size (i.e., 30K vs. less than 100) and has a broad coverage topics in research-level mathematics and computer science that have no general algorithmic solutions.
2017
Saxton et al. 2019
Our work is closely related to the most recent work on applying language modelling to theorem proving. Urban & Jakubuv (2020) present initial experiments generating conjectures using GPT-2 (Radford et al., 2019). Polu & Sutskever (2020) show that the GPT-3 language model (Brown al. (020b) additionally pretrained with mathematical equations mined from the web generate propositions that enable theorem provers to prove more theorems automatically. Rabe et al. (2020)
pretrain masked language models on proofs mined from the HOL ist dataset (Bansal et al.
2019)
and apply the pretrained models to the downstream tasks of type inference and predicting conjectures.
While both their work and ours find that transformer models have strong mathematical reasoning capabilities, they have different objectives from ours. Their objectives are to show the effectiveness of pretraining on downstream tasks; by contrast we building benchmarks to test models' ability of solving mathematical problems. In fact, we can pretrain seq2seq models following their proposed methods and verify their effectiveness on our dataset. We will leave this for future work.
There exists a few benchmarks for theorem proving. Kaliszyk et al. (2017) propose machine learning benchmark for higher order logic reasoning. Alemi et al. (2016) use convolutional networks for premise selection. Both of these tasks are classification problems, whereas our proposition generation task is generation problem with a countably infinite search space. In the benchmarks for tactic synthesis (Huang et al. 2019; Bansal et al. 2019 Yang & Deng 2019: Sanchez-Stern al. 2019 Paliwal et al.] 2019) Gauthier et al. 2017). an agent is asked to propose a sequence tactics to solve the current goal. Our task is complementarg the model is required to conjecture goal (intermediate proposition) that is likely to useful a derivation. |W et al. (2020) proposed a synthetic inequality theorem proving benchmark that studies the out-of-distribution generalization abilities of models.
8

---

Published as a conference paper at ICLR 2021
Conjecturing literals in tableau proofs using recurrent neural networks has been investigated by Piotrowski & Urban (2020).
Other related work includes analogy/syntax driven conjecturing (Gauthier et al., 2016 Nagashimal
& Parsert 2018: Wang & Deng 2020), goal classification//anking (Goertzel & Urban Brown
al. 2020a), proof method recommendations (Nagashima [2200] Nagashima & He 2018 and
autoformalisation of mathematics (Wang et al. 2020 Szegedy 2020
Hierarchical Models Hierarchical models have been proposed to solve natural language processing tasks such document representation (Yang et al., 2016) and document summarisation (Zhang et al. 2019; Liu & Lapata, 2019). Both our hierarchical transformer (HAT) and those models share the similar spirit of introducing local layers to encode local sentences (or propositions) and global layers to capture cross sentence (or proposition) information. However, our HAT is different from their hierarchical models in the way of representing sentences (or propositions): while their models encode sentences into fixed size vectors, the representation of proposition in our model is matrix of dynamic size. The model by Liu & Lapata (2019) has a more sophisticated architecture for capturing sentence representations compared those by Yang et al. (2016) and Zhang et al. (2019), where they introduce multi-head pooling to encode sentences with different attention weights. Compare to Liu & Lapata (2019)'s model, our model does not introduce additional parameters beyond the standard transformers. Another subtle difference between our model and the existing models is the way of doing positional encoding. Unlike documents where the order of sentences matters, propositions within each category of our ItarStep task do not require an order. Therefore, we do not encode the positional information of different propositions.
8 CONCLUSION
We mined a large corpus of formal proof's and defined proposition generation task as benchmark for testing machine learning models' mathematical reasoning capabilities. In our defined task, the gap between adjacent proof steps is big and therefore it cannot be simply solved by pattern matching and rewriting. We evaluated the RNN attention model and the transformer on this dataset and introduced hierarchical transformer that outperforms the existing seq2seq model baselines especially long source sequences. Our analysis shows that the neural seq2seq models can learn non-trivial logical relations and mathematical concepts. We hope that our work will drive the development of models that can learn to reason effectively and eventually build systems that can generate human-readable proofs automatically.
ACKNOWLEDGMENTS
Both Li and Paulson are supported by the ERC Advanced Grant ALEXANDRIA (Project 742178), funded by the European Research Council. We would like to thank Dani Yogatama, Adhiguna Kuncoro, Phil B Blunsom, and Christian Szegedy for helpful comments on an earlier draft of this paper. We also thank the anonymous reviewers for their insightful suggestions.
REFERENCES
Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban. DeepMath- - Deep Sequence Models for Premise Selection. In Proceedings of NeurIPS, 2016.
Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. Neural machine translation by jointly learning to align and translate. In Proceedings of ICLR, 2015.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving, In Proceedings of ICML, 2019.
Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C Paulson. Extending Sledgehammer with SMT solvers. In Proceedings of International Conference on Automated Deduction, 2011 1.

---

Published as a conference paper at ICLR 2021
Chad E Brown, Bartosz Piotrowski, and Josef Urban. Learning to advise equational prover. 2020a. 32. 32.pdf
URL httpp://ttt.ccnneeeeeeeee//////2
Tom B Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et Language models are few-shot learners. arXiv preprint arXiv:2005. /4165, 2020b.
François Charton, Amaury Hayat, and Guillaume Lample. Deep differential system stability learning advanced computations from examples. CoRR, 21s/20006.0646,, 2020.
Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? Proceedings of ICLR, 2018.
Bernd Finkheiner, Christopher Hahn, Markus N Rabe, and Frederik Schmitt. Teaching temporal logics neural networks. arXiv preprint arXiv:2003.04216 2020.
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Initial experiments with statistical conjecturing over large formal corpora. In Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, 2016.
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to Reason with HOL4 Tac- tics. In Proceedings of International Conference Logic for Programming, Artificial Intelligence and Reasoning, 2017.
Jonas Gehring, Michael Auli, David Grangier, Denis Yarats, and Yann N. Dauphin. Convolutional sequence sequence learning. In Proceedings of ICML., 2017.
Zarathustra Goertzel and Josef Urban. Usefulness of lemmas via graph neural networks. URL htt.://eeeeee..oooo/0oo///aaaaar 100AATPP_2111__ 2019_000000 $_paper 1aaper_3__p00 pdf
Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in nutshell. Journal of
Formalized Reasoning, 3(2):153-245, 2010.
Sepp Hochreiter and Jürgen Schmidhuber. Long short-term memory. Neural computation, 9(8):
1735-1780, 1997.
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A Learning Environ- ment for Theorem Proving. In Proceedings of ICLR, 2019.
Lukasz Kaiser and Ilya Sutskever. Neural gpus learn algorithms. In Proceedings of ICLR, 2016.
Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. In Proceedings of ICLR, 2017.
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In Proceedings of ICLR, 2020.
Shin-Yew, Lin. Rouge: A package for automatic evaluation of summaries. Text summarization branches out, pp. 74-81, 2004.
Wang Ling, Dani Yogatama, Chris Dyer, and Phil Blunsom. Program induction by rationale genera- tion: Learning to solve and explain algebraic word problems. In Proceedings of ACL, 2017.
Yang Liu and Mirella Lapata. Hierarchical transformers for multi multi-document summarization. In Proceedings of ACL, 2019.
Yutaka Nagashima. Simple dataset for proof method recommendation in isabelle/hol. In International
Conference Intelligent Computer Mathematics, 2020.
Yutaka Nagashima and Yilun He. Pamper: Proof method recommendation system for isabelle/hol. CoRR, 2018.
07239
Yutaka Nagashima and Julian Parsert. Goal-oriented conjecturing for isabelle/hol, 2018.
10

---

Published as a conference paper at ICLR 2021
Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph Representa- tions for Higher- Bigher--rrdr Logic and Theorem Proving, 2019. StLp:t/:://ae http:::/aaxxiv..oo www.iv..rgiio org /bs
1905.10000
Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of ACL, 2002.
Lawrence C Paulson. Isabelle: A generic theorem prover, volume 828. Springer Science & Business Media, 1994.
Bartosz Piotrowski and Josef Urban. Guiding inferences in connection tableau by recurrent neu- ral networks. In International Conference Intelligent Computer Mathematics, pp. 309-314. Springer, 2020.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03394 2020.
Markus Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757 2020.
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. OpenAl Blog, 1(8)99 2019.
Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner Generating Correctness Proofs with Neural Networks, 2019. URL
David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In Proceedings of ICLR, 2019.
Christian Szegedy. promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce Miller (eds.), Intelligent Computer Mathematics, 2020.
Andrew Trask, Felix Hill, Scott E. Reed, Jack W. Rae, Chris Dyer, and Phil Blunsom. Neural arithmetic logic units. In Proceedings of NeurIPS, 2018
Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics, 2020.
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 NeurlPS, 2017.
Mingzhe Wang and Jia Deng. Learning Prove Theorems by Learning to Generate Theorems, 2020.
URL httpps://axxxi.. www.eoorrrrooooe abs///02.22222////////// 07011
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural ma- chine translation in autoformalization of mathematics in mizar. Proceedings of ACM SIGPIAN International Conference on Certified Programs and Proofs, 2020.
Makarius Wenzel. The Isabelle/lsar Implementation. https: // sabe le. in. tum. de/ di st
s- f 2020. [Online; accessed M1-May-2020J.
Freek Wiedijk. The seventeen provers of the world: Foreword by Dana S. Scott, volume 3600.
Springer, 2006.
Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoc Le. Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, Jeff Klingner, Apurva Shah, Melvin Johnson, Xiaobing Liu, Lukasz Kaiser, Stephan Gouws, Yoshikiyo Kato, Taku Kudo, Hideto Kazawa, Keith Stevens, George Kurian, Nishant Patil, Wei Wang. Cliff Young, Jason Smith, Jason Riesa. Alex Rudnick, Oriol Vinyals, Greg Corrado, Macduff Hughes, and Jeffrey Dean. Google's 's neural machine translation system: Bridging the gap between human and machine translation. CoRR, 2016. URL httt::tt//aaattt
org/ abs 1609. C8144
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Grosse. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. arXiv preprint arXiv=2007.02924 2020.

---

Published as a conference paper at ICLR 2021
Table 3: Additional results.
Top-1
Acc.
Top- 10 Acc.
BLEU
Model
Base
F.5
Base
+
Base
F.5
Conv2Conv
8.7
8.3
21.7
20.8
48.66
46.54
Kaiyu Yang and Jia Deng. Learning Prove Theorems via Interacting with Proof Assistants. In Proceedings of ICML,, 2019.
Zichao Yang. Diyi Yang. Chris Dyer, Xiaodong He, Alexander J. Smola, and Eduard H. Hovy. Hierarchical attention networks for document classification. In Kevin Knight, Ani Nenkova, and Owen Rambow (eds.), Proceedings NAACL HLT, 2016.
Wojciech Zaremba and Ily Sutskever. Learning to execute. arXiv preprint arXiv:1410.4615. 2014.
Xingxing Zhang, Furu Wei, and Ming Zhou. HIBERT: document level pre-training of hierarchical bidirectional transformers for document summarization. Proceedings of ACI., 2019.
A EXPERIMENTAL SETUP
For RNNSearch Bahdanauu et al., 2015: Wu al. 2016), we use 2-layer LSTMs (Hochreiter Schmidhuber 1997) with 512 hidden units and 0.2 dropout rate. The hyperparameters for training the transformer are the same as transformer base (Vaswani et al., 2017). , i.e. 512 hidden size, 2048 filter size, 8 attention heads, and 6 layers for both the encoder and decoder. The hyperparameters for HAT are the same, except that the number of local context layers is and global context layers is 2. We share the source and target token embeddings for all the three models. We use beam search decoding with beam size 5 (for topl accuracies) and 10 (for top10 accuracies). The configurations for different models are the best steps and pick the checkpoint with the best BLEU on the validation set to evaluate on the test set. Training the transformer and HAT takes 72 hours on 4 Tesla-VI00 GPUs.
found based validation performance. We train these models for 100K
B ADDITIONAL EXPERIMENTAL RESULTS
We report additional experimental results from convolutional seq2seq models (Gehring et al. 2017 6 in Table 3
We use the setup of fconv_iwsit de en to train the model.
C TEST SUITE
We use the default Sledgehammer (Blanchette et al. (201T) method in Isabelle as our automatic theorem prover for checking deriva- tions. To ensure fair and efficient comparisons, we shut off three of its options: "isar proofs", "smt cont_proofs" and "learn". The timeout for Sledgehammer is 30s. We run the test suite on a platform with Intel 9700K CPU and 32G RAM, and it takes about 44 hours to evaluate on test set. Due to some technical issues (e.g.,
Table 4: Percentage of well- formed propositions
Model
Base
+ F.S
Transformer HAT
58.2
60.1
the sampled example appears before Sledgehammer is introduced when booting Isabellc/HOL), 92/5000 examples from the test set not supported by the current version of our test suite. We present the percentage of well-formed propositions (i.e., outputs that type checks Isabelle/HOL) of Transformer and HAT in Table
58.2
58.9
*Codehase:
CCddhaase: http:///aaa.a...ooo.///////////a
"Codebase:
conv
seq2.seq
12

---

Published as a conference paper at ICLR 2021
With such settings, Sledgehammer automatically prove the goal F.3 in 1984/4908 examples. By incorporating the ground truth F.1 the derivations (i.e., to prove both F.2
can be closed automatically in 2243 examples. Among the 1125 examples that HAT produces exact
F.1
and
match, 466 of them have a "small" gap: Sledgehammer discharges the goal F.3 directly; 61 of gaps
"just right': the introduced intermediate step F.T can help Sledgehammer bridge the gap; most of the remaining 598 examples have 'large' gaps (in either F.2
F.1 or F1
F.3 that are beyond the
capability of Sledgchammer. It appears that the insignificant amount of automation improvement can be attributed to the limited number of 'just right' gaps that are within the reach of Sledgehammer.
D ALTERNATIVE STEPS
Many alternative steps are trivially equivalent to the ground truth (e.g- A = B given the ground truth being = A, and P A = given the truth being P). However, we still manage to find few non-trivial oncs, and one of them (#954 in the test set) even identifies a redundant derivation in the Isabelle standard library:
M
z (29)2(27)) 29)
(3)
22
377 {w
w path_image(rs) A n(x3, w) = 0}
(4)
I9 E
(5)
dr
ng I 26g
14
& dr n(x3,2)
Vz & path pmaheiiag)(
x - 2Ti
37 {w w @ath_image(1r) A ni w) 0}
39 E 27
Here, i is the imaginary unit, path_imaged returns the image of the contour ig on the interval
0. 1]. and (1)) is the winding number of va around the point wg. F.2 F.1 combining 4 and
5 leads to n²23, (rg) that proves (3
F11 F.4
F33 joining
(8) and yields
Tg & path image(r3)
(10)
n(13, x9) =
(11)
By further joining (10) with (7) we have
dx
n( v9)
Fg
2
which leads to (6) considering ni .g) = (i.e., Note that our Fur is not used in the derivation above hence redundant. Instead of the redundant ground truth, HAT proposed (10) which is clearly much better intermediate step.
E EXAMPLES OF CORRECT SYNTHESISES
In this section, we present some correctly synthesised propositions which will be labelled as F1 in each case.
13

---

Published as a conference paper at ICLR 2021
#605 in the validation set:
additive(A2,, M2e)
(12)
subalgcbra(Ro,.21)
(13)
tarasure_spacee Kx Mzo)
(14)
(15)
positive(As: Hoo)
(16)
mcasure Sacturrr_ppaeerr__ (11, to, 02) (0(11, vo) A positive(to, U2) A additive(rag (vo, v2))
(17)
Here, 20 and measure spaces. For a measure space y. Xy. Ay. and Hyy are the three components
of y (i.e., y = (2y, Ay. My)), where X, is the carrier set, Ay is a collection of subsets on Xy. and Py
a measure defined on Ay. F2 F.1 Ij being a subalgebra of zo (i.c., (13) implies AsT Ama
so that μ4z, in additive(Az.: Mzz (i.c., [1x is countably addictive on A which is implied by æ being a measure space) can be substituted with Mx, which yields (12).
F3 deriving (14)
requires unfolding the definition of measure spaces (i.e., (17). which requires Up is a sigma algebra
on vi, the measure 1/2 is non-negative on tig and v2 countably additive on up- Two of the three
requirements have already been satisfied by (15) and (16) respectively, while (12) entails the last one and eventually leads to [14..
#2903 in the validation set:
M
322 & (nnh__maae((7))
(18)
P2
22 E proots((g) - prools box(x1,
(19)
path (ath_imag)(77) pro)ts(20) 0
(20)
22 & cbox(x1, 22)
(21)
cbox(=1, = box(xI, x2) U path path_image((r))
(22)
229 E proots(a - pelooossoohhineeeet within((o. x2))
(23)
Here, path image(27) is the image of the path function 27 the interval [o, 1]; proots and proots within (Zo, 5) are, respectively, the roots of a polynomial Øo and the roots (of zn) within set S: box(21, (bounded) boxes on an Fuclidean space. F2 E.
{ar . <
.22) and cbox((1,
(xr 21 < S 222)
X22 is a root of .i (by (19) that does not
intersect with the path of 27 (i.e., (20).
F.
combining with (22). 21 equivalent to
42 & box(x1, x2) A I29 & path image [7 which follows from joining 23 with 18
#1514 (4 in the validation set:
Iz (2x100
< 20g
(24)
x: (x
F2
x2()
39 Max
y S 28
(25)
x3(l))
F10 Dz
(26)
Zz (2x110) S (210)
(27)
0 x<x1(110)
(28)
14

---

Published as a conference paper at ICLR 2021
E.1
26 implies
x2((211) I4 (110)
3/ (2
E
y S xs
(V)
hence 24
by the definition of Max.
by arithmetic and the positivity of the denominator
(i.e., 28
# 1222 in the validation set:
lizro + V - zro1 1
(29)
iizo + V 1 - 1x01
(30)
((rrcsin(Fo) = 0
(31)
3(arcsin(vu)) - In( / 11--00 -g1))
(32)
= 1/(e"))
(33)
E.1 by arithmetic.
3 (arcsin(vo)) In(100 + /1 r/]l) In 0.
#35 in the validation set:
24 = x10
(34)
Vx. 13 = No [x] A < len(x6) - xa = 110 [x]
(35)
23 x x01212]
(36)
Ø12 < len (x6)
(37)
3
K4 = x7 [11]
(38)
27 = #0#
(39)
212 < lon[na
(40)
= 112 +
(41)
Here, Iin [112] refers the æ12 element in the list Zin; len is the length function list; #2
a list where the element Dg is concatenated to the front of the list F
F.2
F.
by instantiating
the quantified variable x in (35) 122 and combining with (36 37
F.
E.
F.3
24 21 [12]
(zy (212 1) x7 [x1).
15


Reviews:
[{"review_id": "ywrsWrcbTVb", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 9, "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\nSummary:\n\nThis paper proposes a benchmark for high-level mathematical reasoning and study the reasoning capabilities of neural sequence-to-sequence models. This is a non-synthetic dataset from the largest repository of proofs written by human experts in a theorem prover, which has a broad coverage of undergraduate and research-level mathematical and computer science theorems. Based on this dataset, the model need to fill in a missing intermediate proposition given surrounding proofs, named as IsarStep. It's a very interesting task. This task provides a starting point for the long-term goal of having machines generate human-readable proofs automatically. The experiments and analysis also reveal that neural models can capture non-trivial mathematical reasoning.\n\n\n##########################################################################\n\nReasons for score: \n\n \nOverall, I strongly vote for accepting. I think this is a very important work and this benchwork would benefit to other fresh ideas and new approaches for mathematical reasoning related research. My only concern is that as a benchmark, do authors need to conduct more experiments and baseline models on their data set to be more convincing?\n\n \n##########################################################################Pros: \n\nPros:\n\n+ 1. The paper mined a large corpus of formal proofs and defined a proposition generation task as a benchmark for testing machine learning models’ mathematical reasoning capabilities. Such beckmark is important and beneficial to the development of the artificial intelligence community.\n\n \n+ 2. The proposed HAT model is novel for better capturing reasoning between source and target propositions. The design of two types of layers is reasonable and interesting. The local layers model the correlation between tokens within a proposition, and the global layers model the correlation between propositions.\n\n \n+ 3. This paper provides comprehensive experiments, including both qualitative analysis and quantitative results, to show the effectiveness of the proposed model. Experiments and analysis reveal that while the IsarStep task is challenging, neural models can capture non-trivial mathematical reasoning.\n\n\n+ 4. The paper is well-written and the design decisions are clearly explained. The comparison of benchmark methods is also interesting to read. In general, I think this is a worthy publication. \n\n \n##########################################################################\n\nCons: \n\nMy only concern is that as a benchmark, do authors need to conduct more experiments and baseline models on their data set to be more convincing? The authors only use two baseline models: RNNSearch and transformer, it seems to be insufficient. At Bert era, do those improved models based on Generative Learning tasks could also be applied to IsarStep as baseline, like MASS(Masked Sequence to Sequence Pre-training for Language Generation)/UNILM(Uniﬁed Language Model Pre-training for Natural Language Understanding and Generation)?", "extra_scores": {}, "extra_text": {}}, {"review_id": "Rtp1tIz8K3N", "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": "The authors propose a new benchmark task to evaluate the high-level reasoning capabilities of machine learning models (specifically sequence-to-sequence models) in the context of proof assistants. The task consists of predicting the intermediate proposition from its surrounding ones, namely its previous and its subsequent propositions. The experimental analysis provides evidence on the difficulty of the task at hand. The authors propose also a solution based on a hierarchical transformer, which is able to better capture the mathematical relations of intra- and inter-propositions compared to existing sequence-to-sequence models, as demonstrated by quantitative as well as qualitative analyses.\n\nThe paper is clearly written and has a good balance between technicality and readability.\nProvided examples are pedagogical to better understand the introduced concepts. Also, it is positive the fact that the authors are prone to publish their data and code to foster the reproducibility of the experiments.\n\nThe major drawback with the paper is in the weak/not well supported motivations of the proposed benchmark task. Also, a discussion of the differences between the proposed model and existing hierarchical transformer architectures is missing. Please, refer below to more detailed comments.\n\nTaking into account that it's not clear to me why the proposed benchmark task is necessary to advance the research in the field of proof assistants, 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 can provide a better explanation on their motivations or provide more convincing arguments supporting the need of their proposed benchmark task. Furthermore, I suggest the authors to discuss some missing related work on hierarchical transformers.\n\nDETAILED COMMENTS\n\nThe authors argue that \"solving the IsarStep task will be potentially helpful for improving the automation of theorem provers, because proposing a valid intermediate proposition will help to reduce their search space significantly\". In general, I agree with the authors that developing benchmarks is an essential driving factor in research and that designing methods able to reduce the search space is essential to improve the automation of theorem provers. I'm not able to see why and how IsarStep can drive this advancement though.\nProofs, both procedural and declarative ones, are inherently sequential and IsarStep breaks this sequentiality by assuming that the proposition subsequent to the missing one is given. For instance, consider the same example used in Section 2 to prove the irrationality of the square root of 2. Why can statement (3) be considered given and in which practical situations does the task of predicting (2) given (1) and (3) occur? Does the IsarStep task occur in practice when proving new conjectures? Wouldn't it be more natural to predict (2) and subsequently (3) by having only (1)?\n\nFurthermore, in which sense is solving IsarStep \"a first step towards the long-term goal of sketching complete human-readable proofs automatically\"? Can you elaborate more on that?\n\nHierarchical transformers have been already proposed in natural language for the purposes of document summarization [1-2]. Can you relate with these existing works and particularly discuss what are the architectural novelties of your proposed transformer, as this is one of the contributions listed in the introduction?\n\nMINOR COMMENTS\n\nIn the experimental section regarding the visualisation of attention, can you specify what is F2 and what is F3?\n\n[1] Zhang et al. HIBERT: Document Level Pre-training of Hierarchical Bidirectional Transformers for Document Summarization. ACL 2019\n[2] Liu and Lapata. Hierarchical Transformers for Multi-Document Summarization. ACL 2019\n\n#########################\n\nUPDATE\n\nAuthors have clarified the doubts raised by my questions. I believe that the task proposed in the paper provides new insights on the weaknesses of deep learning models. Therefore, solving the task is important to advance the automation of proof assistants through machine learning. Based on this, I recommend for acceptance.", "extra_scores": {}, "extra_text": {}}, {"review_id": "Qj38VJ_-WNt", "reviewer": "AnonReviewer4", "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": "The paper introduces a dataset for proposing intermediate\nlemmas/conjectures based on a repository of Isabelle\nformalizations. It also does an evaluation of neural\nsequence-to-sequence methods on the dataset complemented to some\nextent by ATP evaluation. A hierarchical transformer is proposed that\noutperforms a transformer baseline.\n\nThis is a useful task and such datasets are useful. Apart from the\ndataset being based on Isabelle (which is indeed a major proof\nassistant with a nice library), there is however not much\nnovelty. Similar datasets have been extracted from other libraries and\nneural experiments have been done over them. To those cited, I would\nadd [1] based on the large E_conj dataset [2] created in 2017.\nCompared to the dataset presented here, [2] also provides an effective\ncomputational metric (based on hundreds of thousands of E prover runs)\nfor judging the usefulness of the intermediate lemmas. Such datasets\nare easy to produce and to scale up to orders of magnitude larger\nsizes.  \n\nSimilar works also include AIMLEAP [3] and the datasets created by\nPiotrowski using seq2seq for predicting the next tableau steps [4].\n\nOne big issue with the dataset compared to the related work is that it\nis not clear how to run the ATP evaluation. The interesting parts of\ncombining ML and TP typically occur when one can easily run tools on\nboth sides, do feedback loops, etc.\n\nOn the other hand, the ML study seems interesting, it is good that the\nIsabelle library is starting to be used this way, and the hierarchical\ntransformer seems to help. Hence my neutral to mildly positive score,\neven though the claims about the uniqueness of the benchmark should be\ncorrected.\n\n\nSome more detailed remarks:\n\np2: give a pointer to declarative vs procedural proofs - the sqrt 2 example has been largely developed by Wiedijk and the declarative proof style comes from Mizar\n\np4: Free variable normalization\n==> \ntreating of (eigen)variables has been a big topic in the ML-for-TP area. For the most recent feature-based encodings see e.g. the ENIGMA approach. For principled neural treatment, see e.g. the work of Olsak on invariant GNNs [3].\n\np6: how is the ATP evaluation done?\n\nReferences:\n\n[1] Zarathustra Goertzel and Josef Urban: Usefulness of Lemmas via Graph Neural Networks. \nhttp://aitp-conference.org/2019/abstract/AITP_2019_paper_32.pdf \n\n[2] https://github.com/JUrban/E_conj\n\n[3] Learning to Advise an Equational Prover\nChad E. Brown, Bartosz Piotrowski, and Josef Urban\nhttp://aitp-conference.org/2020/abstract/paper_32.pdf\n\n[4] Bartosz Piotrowski, Josef Urban:\nGuiding Inferences in Connection Tableau by Recurrent Neural Networks. CICM 2020: 309-314\n\n[5] Miroslav Olsák et al:\nProperty Invariant Embedding for Automated Reasoning. ECAI 2020: 1395-1402\n\n================\n\nUPDATE\n\nThanks to the authors for their replies and paper updates. My overall evaluation remains on the slightly positive side: I believe that conjecturing is an important task and Isabelle provides a nice corpus for that. Even if declarative proof corpora based on Mizar have been used for similar ML/TP tasks before and the work is not quite novel.\n\nFurther notes:\n\n- I would recommend exporting the corpus in the TPTP format. This typically makes the ATP evaluation and building of ML/ATP feedback loops (much) more accessible to ATP researchers, allows including the benchmark in the CASC LTB (large-theory batch) competition, etc. This has been done before [6] for the large corpus of declarative Jaskowski-style Mizar proofs that can be easily used in a similar way as the Isabelle data provided here.\n\n- I do not quite agree with the response claim that E_conj is synthetic and focused on ranking and classification. It is derived from a real-world (Mizar) problem set and the ATP-synthesized lemmas are equipped with a metric of their real-world usefulness. So the various tasks such as regression, ranking, classification and (indeed) synthesis (there is nothing hard about synthesis in the E_conj scenario) have a direct impact in terms of suitable splitting of the real-world ATP problems and their easier solution. It is the same cut introduction task as the authors consider here, just with much more data derived from ATP runs and their characteristics rather than from human proofs. This kind of ATP-based data augmentation is one of the most useful ones in the ML-for-TP domain - quite often more useful than working with human proofs [7] because the ultimate evaluation scenario typically involves ATPs. So it is certainly not the kind of artificial/synthetic task that has an unclear real-world value.\n\n[6] Josef Urban, Geoff Sutcliffe: ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments. Math. Comput. Sci. 2(2): 231-251 (2008)\n\n[7] Daniel Kühlwein, Josef Urban: Learning from Multiple Proofs: First Experiments. PAAR@IJCAR 2012: 82-94\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "Qh8bG0hmhl_", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 7, "confidence": 5, "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 presents a non-synthetic dataset generated from the Isabelle AFP, the largest mechanised proof repository for the task of filling in a missing intermediate proposition given surrounding proofs. Together with the dataset the paper presents a hierarchical transformer model (HAT). Top-10 accuracy, which is the percentage of target proposition appearing in the top 10 generated propositions, is 37.2 for their HAT model. The task this paper addresses is important for theorem proving practitioners, and synthesising propositions appears to be a more difficult challenge compared to other ML tasks in theorem proving (choosing useful lemmas or choosing tactics).\n\nStrengths:\n\n- The database is produced from a non-synthetic dataset called the Archive of Formal Proofs (AFP). AFP is a good source to produce a database that covers diverse topics.\n- The newly proposed hierarchical transformer model outperforms the baseline models.\n- The evaluation includes a comparison to models reported by other researchers.\n- The paper uses a simple motivating example, which helps readers understand the task.\n- The evaluation results reported in Table 1 and Table 2 are good for the difficult task of synthesising propositions for diverse problems from the AFP.\n\n# Weakness\n- The link to the dataset and model is missing as well as the link to their \"test suite to check the correctness of types and the validity of the generated propositions using automatic theorem provers\". This is a serious problem to evaluate the paper. The results presented in Tables 1 and 2 are good for the difficult task of proposition synthesis, and I want to test their model for some problems myself. Without the link this is not possible\n\n- The contribution to the proof automation is surprisingly small. They reported 70 cases out of about 3000 are newly proved given the generated intermediate propositions from their HAT model. From the numbers reported in Table 2, I would expect more improvements could be achieved. Without further investigation it is hard to understand this discrepancy.\n\n# Further comments:\n\n- Maybe, it is better to give short names to F1 ~ F5 instead of Fs and numbers?  For example, F1 can be \"target\" in bold or in teletype font.\n- In Section 3.1, the example token pops out of the column for the main text. Maybe removing spaces after the left parenthesis and before the right parenthesis helps?\n- In Section 4, the vector \"x\" is underlined. Is this aligned with the convention in the community? I saw that \"x\" with an over-line to denote vectors in the past.\n- \"as the sequence of source propositions with I propositions\" -> \"as the sequence of I source propositions\"?\n- In Section 5.2,  it seems reasonable to consider \"alternative valid propositions\". Can you formally introduce the definition of \"correct proposition\"? I guess a \"correct proposition\" is a proposition that matches either the corresponding ground truth or one of the alternative valid propositions. Am I right?\n- In the paragraph for Alternative  Valid Propositions in Section 5.2, \"5% more correct propositions\" -> \"5 percentage point more correct propositions\"?\n- In Section 5.2, the reported contribution to the automation is surprisingly small considering the numbers reported in Table 1 and Table 2. 70 out of 3000 is a 2.3 percentage point increment, even though the previous paragraph says \"alternative propositions contribute 5% more correct positions\".  Does this mean that some of propositions produced by HAT are valid intermediate lemmas that can be derived from local propositions (F2) and that can be used to prove the goal (F3), but the ATPs are so strong that they can prove F3 from F2 without the valid intermediate lemmas, i.e. IsarStep tends to include small steps that can be skipped by the state-of-the-art ATPs? It is natural if this happens since ATPs are continuously improved and sometimes Isabelle users intentionally write down small steps that are not necessary for the state-of-the-art ATPs.\n- In Table 3 in Appendix B, I guess you forgot to multiply numbers by 100 to compute percentage. If so, these numbers in Table 3 appear to be good to me, and it is interesting to know that Transformer slightly outperforms HAT in Table 3 even though HAT outperforms Transformer for producing \"correct propositions\".\n", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper introduces a clever new problem that may prove useful in the advancement of Automatic Theorem Proving -- finding intermediate steps in a proof. A non-synthetic benchmark is created based on a large human-created dataset of proofs. Neural models were shown to have non-trivial performance. Reviewers were convinced that this is ultimately a useful benchmark.
Decision: Accept (Poster)