REFACTOR: Learning to Extract Theorems from Proofs

Thank you for your constructive feedback and we address individual points below.

The necessity of training a neural network to extract sub-proof is not validated and explained. One can easily traverse the proof tree and obtain multiple sub-proof as theorems. This simple method can also surpass the proposed method in lots of aspects. For example, if it extracts all sub-proof, it might obtain all human-defined rules instead of 19.6% of them and more valid theorems than 1923. The experiments do not have a comparison with such baselines and cannot validate the effectiveness of the proposed method.

Thank you for your comment and we would like to provide some clarifications.

If we traverse the proof trees and extract all possible sub-proof as theorems, the amount of theorems will be combinatorial to the number of nodes in the proof tree, which is not practical and useful for downstream tasks. Instead, we compared our method against a symbolic extraction method [1] where we keep the number of extracted theorems being the same (1923 in this case). This makes a fair comparison and the results are discussed in the last paragraph of page 7. The symbolic baseline only achieves a 1.7% accuracy compared to 19.6% by REFACTOR.

Furthermore, our goal is not only extracting new theorems but also demonstrating their usefulness on downstream tasks. In Table 4, we show that with our newly extracted theorems (REFACTOR), the Holophrasm theorem prover can prove 75 more test theorems whereas the symbolic baseline improves Holophrasm only by 9 theorems.

These results demonstrate that training a neural network to extract new theorems is more effective than symbolic baselines.

The paper does not give a detailed description in the main text of how to extract a theorem given the binary prediction results within a proof.

Sorry for the confusion and missing it in the main text. We simply extract all the nodes whose output probability is greater than 0.5. We provided more details on theorem extraction in Appendix A.1. We will update our main text based on the Appendix in the final version of the paper.

Why not fill some nodes with pre-defined rules to connect the positive nodes and obtain more valid theorems?

Thank you for the great suggestion! More valid theorems can indeed be obtained with the introduction of pre-defined rules. In this work, our goal is to show the possibility of just training a neural network to extract useful theorems. A hybrid approach that combines with rule-based methods is complementary to REFACTOR and we leave this as future work.

How does the theorem extracted from the validation set occur/support the proofs from the test set?

Thank you for raising this point. To test the generalization ability of the neural network, we performed a target-wise split on the dataset. That is, the theorems to be extracted are non-overlapping for the training, validation and test set. We provide more detailed discussion on dataset creation in Section 5.1.

Do the positive and negative nodes balance in the training data?

Thank you for the comment. Because of the presence of many large proof trees, the positive and negative nodes are not balanced. We did not explicitly balance the number of positive and negative nodes in the training data. The proof-level test accuracy of 19.6% attained by our best model suggests the model can still learn under unbalanced data.

Can simple rule-based extraction methods, such as byte-pair encoding(BPE), improve the performance of ATP?

Thank you for the suggestion. In Table 4 and Section 5.6, we use a simple rule-based extraction method [1] optimized for compression objective to extract new theorems and investigate whether it can improve the theorem prover performance. Compared to the symbolic baseline, REFACTOR leads to proving 66 more test theorems, demonstrating the usefulness of the extracted theorems.

[1] Vyskočil, Jiří, David Stanovský, and Josef Urban. "Automated proof compression by invention of new definitions." In Logic for Programming, Artificial Intelligence, and Reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, Revised Selected Papers 16, pp. 447-462. Springer Berlin Heidelberg, 2010.

Thank you for your valuable and detailed review on our paper. We address individual points below.

It is claimed a few times that proof refactoring "mimics what human mathematicians do" or the like, but this is not backed up. Is it your intuition or do you have evidence? I am not convinced that compression of proofs is similar to human conjecture-making and definition-building behaviour. It certainly makes sense as a procedure for defining new abstractions, but it does not account for intrinsically motivated conjecture-making (guessing a theorem is true and then trying to prove it).

Thank you for the question. The intuition comes from scenarios where we notice there is some part of the proof that is self-contained and does not relate closely to the rest of the proof. It seems clearer to separate it out into a lemma both better presentation, future use and compositional generalization.

Our focus of the paper is not to fully capture what human mathematicians would do which involves iterative processes and refinement. We fully acknowledge human mathematicians perform a variety of actions such as conjecture making, definition building besides theorem abstraction from existing knowledge base. As a first attempt to capture partially what a human mathematician would do, we perform theorem expansion on human written corpus for imitation learning targets. We then learn to extract a modular component from the existing corpora. The extracted new theorems are shown to be useful in improving an off-the-shelf theorem prover performance as seen in Table 4.

Section 3 misses essential mathematical background to theorem proving. The equivalence of proofs and programs / computation trees is stated and assumed without further comment, but it is not a trivial concept. The Curry-Howard correspondence and how it applies to Metamath deserves more discussion. See or cite, e.g., [P. Wadler, "Propositions as types"] for historical overview.

Sorry for missing the important background in establishing equivalence between these two concepts. We have updated Section 3 of our paper pdf in blue. We provide a very high level explanation to establish the equivalence between proofs and computation citing the related work. We would highly appreciate your feedback on our revision.

The example in Fig. 1 was hard to make sense of. (Note that the reviewer is familiar with Lean but not Metamath.) Can the last paragraph of section 3 explain it in plain(er) language, explaining what types of objects ph, wffph, etc. are and what the theorem means?

We apologize for the confusion and below is a more detailed explanation for Figure 1 (a) theorem a1i. We will incorporate the explanation in the final version of the paper.

The theorem proved in Figure 1 (a) states if ph is true, then (ps->ph) is true. Although this is rather low-level and possibly trivial, it is proven with the axiom of simplification along with the rule of Modus Ponens. To begin with, we start from wffps and wffph. These are expressions that state variable ps and ph are well-formed. Next, a theorem wi is invoked, which leads to wff (ps->ph). This means (ps->ph) is also well-formed. With wffps and wffph shown on the top right corner of Figure 1 (a), an axiom called “the principle of simplification” can be invoked to arrive at |-(ph->(ps->ph)). The axiom essentially states the expression a->(b->a) is always true. In the last step, we use the rule of Modus Ponens. Specifically, it takes in 4 arguments: wffph, wff(ps->ph), |-ph and |-(ph->(ps->ph)). The third argument |-ph comes from the hypothesis of the theorem (if ph is true) and the rest of arguments have been shown to hold from above. By applying the rule of Modus Ponens, we arrive at the goal |-(ps->ph).

Incorrect use of "connected component" (several times on p.4). It is used to mean "connected subgraph", when in fact "connected component" has a different and very well-established meaning in graph theory.

Related, please also explain in a few words why connected subtree is not sufficient for validity. Note that issues related to bound variables would only be worse in more sophisticated proof systems -- this could be discussed as a limitation.

Sorry for the incorrect terminology and we have updated the paper pdf. Since both hypothesis statement and theorem application are represented as nodes in the proof tree, it is possible to have an incorrect number of hypotheses (arguments) for a theorem (function) invocation. We agree with the reviewer that the issue could be worse in more sophisticated proof systems. One possible remedy is to automatically fill in the missing hypotheses during extraction.

Thank you for the answers, clarifications, and corrections. In particular, I seem to have missed that Table 4 has results comparing the number of test theorems proved with your method compared to compression-based baselines like [Vyskočil et al.]. I updated the score. I see that this can be a useful method, but the simplistic and deterministic way of selecting a proof subtree (via the logit thresholding) seems like a major limitation, one that isn't present in compression-based schemes.

Thank you for your encouraging review and comments! We respond to your individual questions below.

However, I’m concerned whether extracting “new theorems” from existing proofs is helpful to the automated theorem proving community, or the maths community in general.

Thank you for the question. We believe our work is still meaningful for the automated theorem proving community. In this work, we propose a novel way to expand proof trees and then create targets for training a neural network. The method along with the generated data from Metamath could be helpful to researchers who are interested in improving automated theorem prover performance. Besides, we extracted 1923 new theorems and as shown in Table 4, these newly extracted theorems are also directly used to prove test set theorems. Therefore, we believe this is a meaningful contribution.

Even though 19.6% is a non-trivial result, it would be meaningful if we know whether the results can be improved by expanding the theorems even more and generating more training data.

Thank you for raising this point. We believe with a more sophisticated way of theorem expansion such as recursive expansion, we could create more diverse targets to further improve the performance.

The related work comparison can be improved.

Thank you for the great suggestion and we have updated the Related Work section of our paper pdf in blue.

Do you plan to apply it to other math libraries, e.g., LEAN? If so, can your technique be lifted to that setting without much effort. Please provide justification, if your answer is YES.

Yes. Our work can be lifted to other popular theorem proving environments such as Lean. As discussed in Section 1 and 3, our approach only makes the assumption of a simple substitution inference rule. Proof trees in other math libraries such as Lean and Isabelle can also be represented as trees and mathematically support the substitution of lemmas. Furthermore, thanks to the development of theorem proving playground in Lean (LeanDojo) [1], interacting with the proof trees has become more convenient. With the development of better language models, the features on each node can also be embedded with a better semantic meaning.

[1] Yang, Kaiyu, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. "Leandojo: Theorem proving with retrieval-augmented language models." arXiv preprint arXiv:2306.15626 (2023).

Thank you for your thoughtful review and suggestions. We address individual points below.

Metamath is a relatively simple formal mathematical language and less commonly used for advancing theorem proving compared to other formal provers like Isabelle and Lean. Although the proposed method may be applied to other provers, the implementation and the results of this paper doesn't contribute much to the advance of ATP directly.

Thank you for the comment. We fully acknowledge the fact that we implement REFACTOR on Metamath because of its simplicity and the inference rule (substitution). Our approach is also generally applicable to other formal systems such as Lean and Isabelle since proofs in these environments can also be represented as trees and mathematically support the substitution of lemmas.