Venue: ICLR 2017 conference

Reviews:

final_score: rating: 6: Marginally above acceptance threshold
review_content: Use of ML in ITP is an interesting direction of research. Authors consider the problem of predicting whether a given statement would be useful in a proof of a conjecture or not. This is posed as a binary classification task and authors propose a dataset and some deep learning based baselines. 

I am not an expert on ITP or theorem proving, so I will present a review from more of a ML perspective. I feel one of the goals of the paper should be to present the problem to a ML audience in a way that is easy for them to grasp. While most of the paper is well written, there are some sections that are not clear (especially section 2):
-	Terms such as LCF, OCaml-top level, deBruijn indices have been used without explaining or any references. These terms might be trivial in ITP literature, but were hard for me to follow.  
-	Section 2 describes how the data was splits into train and test set. One thing which is unclear is – can the examples in the train and test set be statements about the same conjecture or are they always statements about different conjectures? 


It also unclear how the deep learning models are applied. Let’s consider the leftmost architecture in Figure 1. Each character is embedded into 256-D vector – and processed until the global max-pooling layer. Does this layer take a max along each feature and across all characters in the input? 

My another concern is only deep learning methods are presented as baselines. It would be great to compare with standard NLP techniques such as Bag of Words followed by SVM. I am sure these would be outperformed by neural networks, but the numbers would give a sense of how easy/hard the current problem setup is. 

Did the authors look at the success and failure cases of the algorithm? Are there any insights that can be drawn from such analysis that can inform design of future models? 

Overall I think the research direction of using ML for theorem proving is an interesting one. However, I also feel the paper is quite opaque. Many parts of how the data is constructed is unclear (atleast to someone with little knowledge in ITPs). If authors can revise the text to make it clearer – it would be great. The baseline models seem to perform quite well, however there are no insights into what kind of ability the models are lacking. Authors mention that they are unable to perform logical reasoning – but that’s a very vague statement. Some examples of mistakes might help make the message clearer. Further, since I am not well versed with the ITP literature it’s not possible for me to judge how valuable is this dataset. From the references, it seems like it’s drawn from a set of benchmark conjectures/proofs used in the ITP community – so its possibly a good dataset. 

My current rating is a weak reject, but if the authors address my concerns I would change to an accept.



review_title: Interesting dataset, reasonable first steps

final_score: rating: 8: Top 50% of accepted papers, clear accept
review_content: The authors present a dataset extraction method, dataset and first interesting results for machine-learning supported higher order logic theorem proving. The experimental results are impressively good for a first baseline and with an accuracy higher than 0.83 in relevance classification a lot better than chance, and encourage future research in this direction. The paper is well-written in terms of presentation and argumentation and leaves little room for criticism. The related work seems to be well-covered, though I have to note that I am not an expert for automated theorem proving.
review_title: null

final_score: rating: null
review_content: In Section 2, you describe the extraction process for the dataset. It becomes clear that it was not a trivial undertaking and probably even more subtleties had to be taken into account to generate the final dataset. Could the same strategy/code be applied directly to other proofs?

In the conclusion, you state that other ITPs or ATPs could be targeted in future work, whereas it could be interesting to integrate even more proofs into the existing dataset. Are you planning to disclose your code for dataset generation?
review_title: The dataset extraction method

final_score: rating: null
review_content: Thanks for the interesting paper. In your results you report proof step classification accuracy. As in AlphaGo this reflects the ability of your models in mimicking the bias in proof structure of proofs that humans discovered. Can you comment whether this bias will affect an automated theorem prover if these models are used as subroutines? Moreover, it's possible that the class of proofs which we find difficult are exactly the proofs for which this method won't help. Thanks!
review_title: When is this applicable?

final_score: rating: 7: Good paper, accept
review_content: The authors describe a dataset of proof steps in higher order logic derived from a set of proven theorems. The success of methods like AlphaGo suggests that for hard combinatorial style problems, having a curated set of expert data (in this case the sequence of subproofs) is a good launching point for possibly super-human performance. Super-human ATPs are clearly extremely valuable. Although relatively smaller than the original Go datasets, this dataset seems to be a great first step. Unfortunately, the ATP and HOL aspect of this work is not my area of expertise. I can't comment on the quality of this aspect.

It would be great to see future work scale up the baselines and integrate the networks into state of the art ATPs. The capacity of deep learning methods to scale and take advantage of larger datasets means there's a possibility of an iterative approach to improving ATPs: as the ATPs get stronger they may generate more data in the form of new theorems. This may be a long way off, but the possibility is exciting.
review_title: Great start, interested in future work

Meta-review: The paper presents a new dataset and initial machine-learning results for an interesting problem, namely, higher-order logic theorem proving. This dataset is of great potential value in the development of deep-learning approaches for (mathematical) reasoning.
 
 As a personal side note: It would be great if the camera-ready version of the paper would provide somewhat more context on how the state-of-the-art approaches in automatic theorem proving perform on the conjectures in HolStep. Also, it would be good to clarify how the dataset makes sure there is no "overlap" between the training and test set: for instance, a typical proof of the Cauchy-Schwarz inequality employs the Pythagorean theorem: how can we be sure that we don't have Cauchy-Schwarz in the training set and Pythagoras in the test set?
Decision: Accept (Poster)