Premise Selection for Theorem Proving by Deep Graph Embedding
We propose a deep learning-based approach to the problem of premise selection: selecting mathematical statements relevant for proving a given conjecture. We represent a higher-order logic formula as a graph that is invariant to variable renaming but still fully preserves syntactic and semantic information. We then embed the graph into a vector via a novel embedding method that preserves the information of edge ordering. Our approach achieves state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%.
The paper addresses the problem of premise selection for theorem proving. The objective in this line of work is to learn a vector representation for the formulas. This vector representation is then used as the input to a downstream machine learning model performing premise selection. 
The contributions of the paper are: (1) a representation of formulas as graph; (2) learning vector representations for the nodes and ultimately for the formula graphs; and (3) show empirically that this representation is superior to the state of the art on theorem proving data sets. 
Pros
* The paper is very well written. A pleasure to read and despite its technical content highly accessible. 
* The experimental results show a significant improvement over the state of the art. 
* The authors discuss all related work I'm aware of and do it in a fair and comprehensive way.
Cons
* There has been previous work on this topic. The novelty here is the graph representation and the way in which node embeddings are learned. The former is a nice idea. The latter is more interesting from a ML point of view but it would have made the paper much stronger if the authors had compared the averaging of neighboring node embeddings approach to other node embedding approaches such as DeepWalk.
This has been added after the rebuttal:
The main weakness of the paper is in my opinion the (lack of) novelty of the proposed approach. The difference to previous work is the graph representation of the formulas. To represent formulas as graphs is not new. Now, instead of learning a vector representation for the formulas directly, a vector representation of the graphs is learned. The downstream architectures are also more or less what has been done in previous work. It's a nice idea for premise selection that performs better than the SOTA by combining existing ideas (graph representation of formulas + graph vector representation learning). Since there's nothing really new here I would have liked more experimental results and a comparison of different graph embedding methods (many of these are cited by the authors). 
Minor comments:
Line 154: "To initialize the embedding for each node, we use the one-hot vector that represents the name of the node." You probably mean that you initialize the embeddings randomly?