Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 7: Good paper, accept
review_content: This paper extends the idea of language-model style self-supervised learning approach to training logical reasoning models from unlabeled mathematical expressions. The main idea is to develop a skip-tree proxy task (self-supervision) for training the encoder-decoder architecture.  The skip-tree method masks out a complete sub-tree in the input and linearizes it into a sequence in the form of S-expression. The model is required to predict the masked subtree at the decoder end. The paper also proposes several new reasoning tasks for evaluating the model performance. Experimental results show that models learned from this task significantly outperform those trained on the skip-sequence task. Furthermore, the model also exhibits good conjecturing ability in generating quite reasonable amount of new theorems that are provable and useful, which is quite encouraging and impressive.

I’m curious about why the method only masks out one sub-tree for prediction while treating other masked sub-trees as auxiliary part (by increasing the difficulty of the task). This seems to be a waste of self-supervision signals. It might be more (sample) efficient to predict all the masked part in one sample just as what BERT did. It would be helpful to provide experimental justification for this specific design choice if deemed so.

The current pretrained model is used on the newly created tasks without any finetuning because these tasks are similar to the mask prediction problem. This is interesting, but I’m wondering if the proposed method be used in various other downstream reasoning tasks? For example, even with certain finetuning, could the pretrained reasoning model be used in other downstream tasks that are less similar to the pretraining objective? Since it is claimed earlier that ``In contrast, we train language models on an unsupervised proxy task that does not require labeled data and can thus be applied to almost any source of mathematical expressions” (Section 2), it would be necessary to further evaluate the pretrained models on other popular logic reasoning tasks. This would show how generalizable the skip-tree pretrained model is on various other downstream reasoning tasks, which would greatly enhance the strength of the work.

review_title: Interesting work

final_score: rating: 7: Good paper, accept
review_content: --------------------------------------------------------------------------------------------------------------------------------
Summary:

This paper proposes a skip-tree training task. The authors show that self-supervised language models (the Transformer architecture to be exact) trained on the proposed skip-tree training task for mathematic theorem proving enable mathematical reasoning capabilities. Moreover, no fine-tuning is required to achieve the reported reasoning capabilities. They compare the mathematical reasoning abilities of the skip-tree training task with skip-sequence and show an impressive performance improvement. Another interesting result is studying whether any useful (novel) conjectures can be generated by the model.

--------------------------------------------------------------------------------------------------------------------------------
Overall assessment:

I really enjoyed reading this paper. The authors work on an interesting problem that has been gaining popularity in the last few years. I believe that this problem domain is a suitable test bed to investigate the reasoning capabilities of language models. The authors propose a skip-tree training task and show that it significantly improves the performance of skip-sequence training. The idea is simple and nice: instead of masking out arbitrary sub-sequences (which is the case for skip-sequence), the authors propose to mask out sub-trees. The authors provide extensive ablation studies and evaluations to justify several design choices and to show the reasoning abilities of their model. I do have some comments about presentation clarity (look below), that I hope the authors can address during the rebuttal. Moreover, I am a bit skeptical about the almost 0 performance of the skip-sequence task under some scenarios. I will clarify this as well in the cons section below.

--------------------------------------------------------------------------------------------------------------------------------
Pros:

 (1) I like the idea of skip-tree training for structured problems. It seems to improve the performance of the model dramatically (from almost not being able to predict AT ALL to near perfect prediction — in the Hard inference problem for example). I do have a comment about this in the cons section. 

 (2) The authors design a set of mathematical reasoning evaluations that are used as down-stream tasks (without fine-tuning) to evaluate the self-supervised trained models. They show good performance on all the tasks compared to their baselines.

 (3) The authors provide a set of ablation studies to justify their design choices.

 (4) I liked the conjecture experiment that evaluated whether the model can generate novel provable conjectures.

--------------------------------------------------------------------------------------------------------------------------------
Cons:

  (1) The performance of skip-sequence training on three out of the four evaluation tasks in Table 2 (Hard type inference, Assumptions, Equalities) are extremely poor. It is my understanding that the only difference between these models and the proposed skip-tree model is in the held-out sub-expression (I am not sure if the skip-sequence models have the <MASK> tokens in addition to <PREDICT> or not). If that understanding is correct, then this might indicate that almost all of the masked <PREDICT> sub-sequences are not “proper” trees. Is that correct? If so, does enforcing a variable portion (say from 0% to 100%) of the held-out sub-sequences to be sub-trees smoothly move the success rates reported in Table 2 towards the skip-tree’s performance? 

  (1-1) Another possibility for the poor performance could be that the skip-sequence models were not trained with <MASK> tokens (I am just judging this based on the large difference between the skip-tree and the skip-tree (no mask) model). If this is the case, a fair comparison would also include the skip-sequence training with the additional <MASK> tokens. This allows the reader to understand which parts of the model result in the reported gains.

  (2) In figure 1 the authors illustrate the portion of the data that they use in their experiments for train and validation. It seems like the gray areas (specifically the test set) are not considered in the paper. What is confusing is that in Section 3 they do mention a train/validation/test split. But all the evaluation tasks defined in Section 5 in the paper seem to only refer to the validation data. There seems to be no indication of the use of a test dataset for the reported results (in Tables 2 and 3), which I find troubling. Especially because the authors do mention that they hyper-parameter optimized their models in Appendix A (not mentioned using which part of the data). Can you please clarify this (both in the rebuttal response and in the paper)?

  (3) How is a correct prediction assessed? It is mentioned that the model’s performance is evaluated for “exact match”. However, as mentioned in the Assumptions task, predicting y=x for the ground truth x=y should be counted as a “correct prediction”. If such predictions are not being counted as “correct”, I highly encourage the authors to add an evaluation metric that considers mathematical equivalence of the generated predictions and the ground-truth. A symbolic solver like Sympy or Mathematica might be able to at least verify the equivalence of simpler expressions (I am not sure how complex these expressions are). 

  (3-1) To follow up on point (3) above, the authors mention that “to make a correct prediction our language models thus have to understand which statements are more general and also know about naming conventions”. I strongly disagree that this is a good way of measuring mathematical reasoning abilities. On the contrary, I think a model that has truly learned to mathematically reason, is one that ignores irrelevant details such as naming conventions or “generality” of the statement (generality is subjectively used by the authors and I think references to it should be removed from the paper).
 
  (4) It is not clearly stated what the authors mean by “new” in section 6.1. Are variations of already seen statements considered new? (e.g. if x=y is in the training set, would y=x be a new statement?). I recommend the authors clearly define this in the paper. 

  (5) It is not clear to me what the takeaway is for the sampling strategy. In the main text it was implied that the weighted sampling will be better because it allows one to choose non-leafs more often. However, the results shown in Tables 2 and 3 show that some scenarios seem to be better with the uniform sampling and some with the weighted sampling. Do the authors have any comments/discussion on that?

--------------------------------------------------------------------------------------------------------------------------------
Smaller details:

  (1) Please use the correct citation command for references that are at the beginning of the sentence (e.g. section 2, Paragraph 2, line 4: Zhang et al. (2019)).

  (2) The authors mention that Lample and Charton (2020) “requires that the inverse of the prediction task can be computed”. Can you explain what this means?

  (3) The explanation of the s-expression given in Section 3 lacks enough details. I wasn’t able to fully understand the representation. Perhaps an illustration with step by step labels can make it easier to understand.

  (4) Section 3, Last paragraph: What does “the split is defined on the theorems” mean? In general this paragraph was somewhat hard to follow.

  (5) What portion of the training data is omitted as a result of what is described in Section 4, Paragraph 2.

  (6) I find the first argument about the reason for adding <MASK> tokens somewhat subjective. Why does making the task harder result in better performance?

  (7) I did not understand the multiple sample per dataset generation at all. Do the authors mean that for each math statement they generate n=100 samples with the <PREDICT> and <MASK> tokens? If so, this implies that there will be 360k*100 examples in the larger training set. But this is not consistent with the data stats provided in Table 1. 

  (8) I think it would be very useful if the authors add human-readable equivalents of the s-expressions presented in Appendix D to that Appendix.

  (9) Section 6: What does 1M “steps” refer to? Is that the number of model updates?

  (10) It would be great to add a few sentences about what the reinforcement learning experiments in the DeepHOL prover are to make the paper more self-contained. 

--------------------------------------------------------------------------------------------------------------------------------
Typos: 

Sec 1, Parag 3: which are capable (to) of generating …
Sec 2, Parag 4: models to logic(s)

review_title: Review of "Mathematical Reasoning via Self-supervised Skip-tree Training"

final_score: rating: 7: Good paper, accept
review_content: Quality

The paper is quite well written and the experiments seem well thought out. Please see specific comments below.

Clarity

The S-expression needs more explanation for the paper to be self-contained. What is 'A' in (v A x)? 


For those of us who might not be very familiar with the datasets, it might be helpful if the paper to demonstrate more examples as to what these proofs are translated to, in mathematical notation or textual explanations. There are a few snippets here and there but I don't think I get a good grasp of what kinds of proofs we deal with. For example, the theorem examples in Appendix section D seem quite lengthy. With effort it should be decoded into normal text by readers, but it would be more convenient to demonstrate it directly.


In addition, the free-form conjecturing evaluation can be more clear. In this section, it doesn't entirely explain in details what makes the generated statements 'new'. Is it only exact match with the training set? If that's the case, how robust is exact matching on measuring the novelty? 

On the usefulness of the conjectures, there's not much explanation on the RL experiments + DeepHOL theorem prover. What is it supposed to do / how robust does it measure usability? 


Question: a beam search of 1024 seems rather large. How does the result look if no beam search is used?

Originality

	The introduced method 'skip-tree' is not that different from the usual self-supervised training techniques used to train language models. This feature does not contribute to the novelty that much. However, this approach is a new take on learning mathematical reasoning with self-supervised learning, rather than supervised learning like in other previous work.



Significance

	Deep learning for mathematical proofs is an interesting direction and is relatively unexplored, compared to other application areas. 




High-Level Pros & Cons

Pros
	- The claim / conclusion for this work that self-supervised training can lead to mathematical reasoning is rather intriguing. 
	- The proposed skip-tree technique seems to make a lot of difference for training.
	- Decent ablation study (not using <MASK> token, skip-sequence instead of skip-tree).
	- The evaluation tasks introduced seem interesting.

Cons
	- I am not 100% convinced that the ``mathematical reasoning'' demonstrated is beyond pattern recognition. I understand that the evaluation tasks are evaluated on validation set theorems which are not seen during training. However, how can we be sure that this is mathematical reasoning versus the model recognizing similar patterns (not necessarily exact match) 

More explanations on this would be appreciated. 
	- Low to moderate novelty for the skip-tree technique.


Overall, I learned a lot from this paper and I believe others can benefit from it as well. 
review_title: Interesting direction/experiments. Could be more clear, however.

final_score: rating: 7: Good paper, accept
review_content: The authors propose a self-supervised learning task to enhance the reasoning capabilities of machine learning models on mathematical formulas and to perform conjecturing in higher order logic. The task consists in masking out specific portions of mathematical statements and predict them from the surrounding parts. The task can (i) be used during training, to provide supervisory signal to the machine learning model and to increase the effective size of the otherwise small training dataset, and (ii) be used during testing, to evaluate the reasoning capabilities of the learnt models by masking out the mathematical statements at different level of granularities. The authors perform an extensive experimental analysis and provide evidence on the utility of using self-supervised learning in the context of theorem proving.

Overall, the paper is clearly written and the bibliography complete. Also, the experimental analysis is undoubtedly valuable for the machine learning community. In fact, it provides additional empirical evidence to the works of [1-2], in the sense that self-supervised learning can be used not only as a pre-training stage for the machine learning models, but also as a task to perform conjecturing.

There are major issues though. In particular, there are issues in terms of the originality of the proposed task and the reproducibility of the experiments, thus obscuring the positive aspects of the paper. Please, see below for more detailed comments.

In lieu of this, I consider the paper marginally below the acceptance threshold and therefore recommend for an initial rejection. Nevertheless, I'm willing to raise my score if the authors properly address the issues highlighted below.

DETAILED COMMENTS

Originality: The proposed task seems to be identical to the task in [3], except for the fact that the task operates on mathematical statements rather than on natural language ones. Importantly, both kinds of sentences/statements share a tree-structured representation, which makes the task in [3] trivially applicable to the mathematical context. Can the authors highlight other differences or explain if this is not correct?

Reproducibility: First of all, it's extremely important to add in the section about results and discussion detailed information about the computational resources and the time required for training, as well as the size of the machine learning model used in the experiments. In fact, it is well-known from other domains, like vision and natural language processing, that the performance of self-supervised learning models increase proportionally with the size of the model, at the expense of the training computational resources.
Furthermore, it's important to discuss about the methodology used to choose the hyperparameters. Appendix A only states that "we explored encoders and decoders with up to 12 layers and various learning rates and intermediate sizes."
Finally, do the authors plan to release the code?

FURTHER IMPORTANT COMMENTS

Answering to this following comments could be helpful to clarify about the originality and the novelty of the proposed task.

Distinguishing between training and evaluation tasks and saying that "several tasks" are proposed (i.e. in abstract, introduction, section 5 and conclusions) can be misleading for the reader, because he/she could think that they are different. Nevertheless, these tasks are all equivalent to the main skip-tree task, differing only in the way the terms are masked. Is that correct? If so, I would suggest to rephrase by saying that the main skip-tree task is quite flexible at masking statements. In fact, depending on which portion of statement is masked, the model can be induced to perform reasoning at different level of abstraction. Based on this, experiments are categorised according to the different ways of masking.

Furthermore, it is not completely clear when the authors says that "most previous works...have focused...in supervised training settings. In contrast, we train language models on an unsupervised proxy task" (related work, but also introduction).
Is the proposed training unsupervised? First of all, the data used in training contains only valid theorems. This can be already considered as a supervised information, because collecting valid theorems requires human effort. Secondly, the evaluation tasks are essentially similar to the training task and therefore I would consider this more as a supervised learning strategy. Could you please elaborate more on this, also in the text?

MINOR COMMENTS

In the experiments about conjecturing (2nd paragraph), can you provide more details on how you generated the free-form conjectures?

Furthermore, how is novelty of generated statements defined? Consider the following examples for conjecturing on assumptions and free-form conjecturing.

Conjecturing from assumptions

Imagine you have 

a+b=0 implies a=-b

and the task is given by

<PREDICT> implies a=-b

Is the statement 'a+b=c and c=0' considered new according to your definition?

Free-form conjecturing

Imagine you have 

<THEOREM> for all x, x=x

and the task is given by

<THEOREM> <PREDICT>

Is the theorem 'for all y, y=y' considered new according to your definition?


[1] Li et al. Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. arXiv 2020

[2] Polu and Sutskever. Generative Language Modelling for Automated Theorem Provers. arXiv 2020

[3] Zhang et al. PEGASUS: Pre-training with Extracted Gap-sentences for Abstractive Summarization. ICML 2020

########################################

UPDATE

The paper provides important and novel empirical observations about the use of machine learning to perform mathematical reasoning. The authors have addressed and clarified some doubts about the originality of their idea and the reproducibility of their experiments in the discussion phase. I believe that the paper is now ready for publication and I'm happy to recommend for its acceptance.
review_title: Mathematical Reasoning via Self-supervised Skip-tree Training

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

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