Venue: ICLR 2022 Conference

Reviews:

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: This paper is about a method that mines the library of existing proofs for frequently occurring patterns of proof steps that constitute separate proofs of theorems (lemmas) used in the original proof. The method uses graph neural networks. It extracts correct unseen theorems modestly frequently (19.6% of the time). These newly found theorems are then added separately to the library and used as lemmas to prove existing theorems. The result is that they are used frequently in many proofs, lead to shorter proofs, and can improve the baseline theorem prover's performance.
main_review: The paper is well written and presents an interesting methods for mining library of proofs for re-usable new lemmas. My main concerns regard:

* Clarity of the syntax of the theorem prover's language: it is hard to understand what the proofs are about and hence it is hard to understand how precisely the refactoring works through the examples presented (e.g., Figure 1).

* Not sufficient comparison with related work is presented in the paper: 
  * the authors claim that Metamath library of proofs is one of the largest but don't mention and compare this with the Isabelle's AFP library, or Mizar's library.
  * no qualitative comparison with the author's work is given with other machine learning for theorem proving, the related works are only listed.
  * how is this work related to other formal systems that extract lemmas, so example Isaplanner?

* A lot of comparisons and results are given in absolute numbers without percentage comparison, so it is difficult to judge if the improvement is significant, for example: 
  * is 19.6% a good result? Based on what? In comparison to what?
  *  is 733.5 times usage of a new theorem frequent? The absolute figure does not place this result in context: for example, one could list the number of times that the top 10 most frequently used theorems are used.
  * the improvement is table 4 is from 14.3 to 17.1%: this seems marginal for a completely new and complex method

* Scalability: while the neural network can deal with large datasets of proofs, if the author's method is already working on one of the largest libraries that exist, how is this going to scale up for improvement (as the authors hope) with larger libraries, if these do not exist? Has the method therefore reached its ceiling in practice? It would be better to improve the method without relying on larger proof libraries. Sure synthetic libraries could be created, but the authors do not explore this avenue. 


summary_of_the_review: Interesting method with but modest results.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: The paper describes a neural method for identifying useful lemmas in large proof graphs.

The method is evaluated on the MetaMath library and gives a good improvement.
main_review: Strengths:

- This is the first use of GNNs for this problem.

- The proposed method for generating synthetic training data for the GNN by expansion makes sense. While quite straightforward, it seems novel in this context. I have not checked if a similar approach was used in related graph-learning tasks (code graphs, etc.).

- The experimental evaluation seems appropriate and the results are good.

- The paper is written quite clearly and wrt the ML community, it is on a relatively new and interesting topic.

Weaknesses:

- The method is a relatively straightforward modification of the lemma
extraction methods proposed previously (cited in the paper) and
evaluated on the HOL/Flyspeck and Mizar libraries. The novelty is in
using GNNs for training some of the graph classification tasks instead
of using methods such as PageRank.

- Despite using possibly "more advanced technology", the improvement
measured in this work seems quite comparable to the previous simpler
methods. The data reported in previous work are 5-20%, while here it
is 15%. However, this is not done on the same benchmarks.

- The numbers reported in Table 4 are generally low compared to today's performance of ML-guided and hammer systems on the theorems in the Mizar, Isabelle, HOL and Coq libraries. The Metamath theorems are not harder than those, so the baseline system used here is quite weak. But this obviously does not invalidate the relative improvement obtained here.

summary_of_the_review: Generating relevant synthetic theorems is a nice and nontrivial
research direction. It is related to tasks such as lemma introduction
and theory exploration. The performance of the systems is good. 
The authors have done a decent amount of work.
review_title: null

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: This paper proposes a deep learning-based approach for extracting theorems from existing human proofs. The problem is formulated by classifying the nodes of the proof trees in/out of the extracted theorem. Graph neural networks are applied to this problem of node classification. This approach is applied to the Metamath dataset and extracts 1923 new theorems. These new theorems could compress the original human proofs and new test theorems are proved by the prover trained on the compressed set of proofs.
main_review: Strength: (1) Propose a novel problem to extract useful theorems from human proofs. (2) The proposed approach is technically sound. The formulation of binary node classification and the generation training data are clearly demonstrated. (3) Experiments verify that the proposed approach could extract useful new theorems that advance the theorem proving on Metamath.

Weakness: The proposed problem (extracting theorems from proofs) seems to be irrelevant to the practice of formal mathematics. From the appendix, the extracted new theorems are quite simple and not very interesting mathematically. From what I can see, the only way to apply this method for formal reasoning is to compress the human-written database by discovering reusable sub-proof trees. The improvement of the theorem prover via training on compressed proofs is descent. So maybe the main story of this work should be improving theorem proving by learning to compress the human proofs.

Question: in Sec. 5.6, do you construct the compressed set of training proofs by using the 16 theorems extract from set.mm only or the 1923 new theorems?
summary_of_the_review: Due to the concern mentioned above, I don't recommend accepting this paper.

============
Post-rebuttal: My main concern is still the problem setup. I don't think it is a useful task to extract reusable patterns from existing proofs as stand-alone theorems and I can not see how a tool that can solve this problem could help the AI/TP community. So I decided to maintain my original rating of this paper.
review_title: null

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: The idea of the paper is based on the view of a theorem + proof as a tree, wherein sub-trees are also theorem + proofs. The goal is to extract useful lemmas from existing proof trees. This is then cast as the problem of predicting whether each node should be extracted as a new theorem (or lemma). The main idea of the paper is to construct a training set for this prediction problem by replacing calls to lemmas with their proof tree, and labelling the nodes which root these newly inserted trees as positive examples, i.e. those to be extracted as useful lemmas.

main_review: 
The main idea of the paper is simple, clear and interesting.

The assumption that the loss function decomposes as (3) is in line with the authors' explanation "Our approach inspects one proof at a time and this intuition comes from the fact that human mathematicians do not need to look at multiple proofs and can instead determine whether a proof segment is broadly applicable just from the current proof." This seems like a strong assumption and it's not clear where this intuition comes from. On the contrary it feels like merely attempting to compress the library of proof trees by identifying repeated sub-trees (across proofs) could also work and violates the assumption above. Moreover, identifying repeated sub-trees has been done as cited, i.e. "Automated Proof Compression by Invention of New Definitions". 

Given the previous paragraph it seems that the proposed method is hard to evaluate without a more thorough comparison. Is this main (and I repeat, interesting) idea of forming a node labelling problem effective ? To answer it needs a comparison with the work "Automated Proof Compression by Invention of New Definitions" and possibly others.

Using T for proof and s for theorem seems strange since theorem starts with t.

In figure 1, are the captions switched for ali and mp1i ?

summary_of_the_review: This is an interesting and simple (in a good way, i.e. clear) idea for turning the problem of lemma extraction into one of supervised learning on the nodes of a graph. The underlying assumptions are not entirely intuitive however (despite the claims in the submission). Moreover there are more direct ways of achieving the same result, but these older methods are not compared to.
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: The authors propose to consider proof graphs from the Metamath library and train a network to extract isolated proofs from the proof steps.The extracted theorems are able to then be used to compress a large percentage of the metamath proofs.
main_review: 
### Strengths:
The paper overall introduces a novel task in automated theorem proving, performs the necessary ablations to understand the behavior of graph neural networks on this tasks, and demonstrate the utility of their trained model and extracted dataset in a novel downstream application of theorem compression.

- introduces a novel task for automated theorem proving
- Able to compress a large percentage of the metamath library
- Ablation of features, bidirectionally in Table 1 is helpful to understand better the tradeoff between node vs. proof-level accuracy, and the impact of the different components.
- paper is well written, and the accompanying figures are well designed (though the labels could be clarified)


### Weaknesses:
Automated theorem proving using neural networks is still nascent, and thus many novel downstream applications are still being discovered as presented in this paper. However the utility and difficulty of these applications is harder to assess. One significant weakness of the paper is the inability to compare to past approaches or provide natural benchmarks for the approach (e.g. how well could a human compress metamath, or how well could a random theorem extractor with rejection filtering do vs. a neural network extracted approach). Without these baselines, I fear that the impact of the work will be hard to estimate.

- Figure 1: while having a motivating example is great for improving readability, the labels of the nodes in the graph are harder to understand without additional background. Is there a way to rewrite this figure with either/both (a) a simpler example, (b) introduction/descriptions of what the abbreviations mean, and what how affect the overall proof. This could mean moving the text of 4.1. into the figure, or somehow aligning the text of 4.1 and the figure so that one an be understood independently from the other.
- Table 2: given the gains with larger models, a natural experiment would be to keep growing the model until diminishing returns are observed. This experiment is missing from the work, and calls into question the peak performance of REFACTOR.

- Section 5 introduces 3 questions, however to an external leader Q1, Q2 are secondary to Q3: to an external audience the impact of the work is scoped to whether the proposed approach is able to impact automatic theorem proving. Reorganizing the paper, and/or removing the question/answer format could help align the reader’s expectations with the content of the experiments.
summary_of_the_review: Using a neural network on existing proofs, the authors show that sub-theorems can be extracted an reused to compress a proof library. This novel contribution is well documented and the authors provide strong motivation. However, aspects of the approach lack baselines or natural comparison points, making the work feel too isolated from current automated theorem proving literature and putting into question its value to the research community.
review_title: null

Meta-review: The paper proposes a deep learning pipeline to extract lemmas from proofs and how to (re)use them to compress a proof library. The The topic is highly relevant, the motivation behind the work is clear but the current state of the manuscript is yet not ready for publication.

In fact, while all reviewers somehow recognized the potential impact of this work, they also highlighted some critical aspects that should be addressed before full acceptance. Namely:

  - the role of GNNs in achieving the achieved performance shall be discussed more in detail (what if they are replaced in the pipeline? an ablation study would help)
  - the broader literature of automated theorem proving should be addressed more precisely in the related works
  - comparisons against other ML methods for theorem proving should be extended (the comparison with MetaGen added in the discussion is a good starting point that can turn into a full experiment)
Decision: Reject