Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 4: Ok but not good enough - rejection
review_content: Summary:

The authors apply reinforcement learning to automated theorem proving to eliminate the need for human-written proofs as training data. During training, the prover is improved incrementally by using the current version to prove theorems and add proved theorems to the training data. The authors propose to use TF-IDF for premise selection. They show that it enables the prover to outperform a supervised learning baseline without using human proofs.


Strengths:

The paper addresses an interesting and important problem—learning theorem provers without explicit supervision from human proofs.

The evaluation is sound. The authors are able to show some benefits from their IF-IDF premise selection. The proposed method outperforms the baseline on the HOList benchmark. 

The paper is well-written overall, though some sentences are difficult to parse, e.g.,  "comparison OF the effect OF availability OF human proofs" in the intro. 

Weaknesses:

The method is not new. There exists a body of work leveraging reinforcement learning to learn theorem provers [A, B, C, etc.]. Many of them also do not rely on human proofs, e.g., [B]. Although the authors may be the first to apply reinforcement learning to prove theorems in interactive theorem proving environments, this is not a sufficiently novel contribution.

[A] Kaliszyk, Cezary, et al. "Reinforcement learning of theorem proving." Advances in Neural Information Processing Systems. 2018.
[B] Piotrowski, Bartosz, and Josef Urban. "ATPboost: Learning premise selection in binary setting with ATP feedback." International Joint Conference on Automated Reasoning. Springer, Cham, 2018.
[C] Zombori, Zsolt, Josef Urban, and Chad E. Brown. "Prolog technology reinforcement learning prover." arXiv preprint arXiv:2004.06997 (2020). 


Besides, using TF-IDF for premise selection is not new. In the related work section, the authors say, "Gauthier et al. (2017) uses a tf-idf based premise selection model, but does not learn a model." I do not understand what the authors mean by "does not learn a model." It would be great if the authors can further clarify the difference with Gauthier et al.

review_title: Review for "Learning to Reason in Large Theories without Imitation"

final_score: rating: 6: Marginally above acceptance threshold
review_content: This paper presents how to train a theorem prover without access to human proofs using deep reinforcement learning. The paper views premise selection as an information retrieval problem where the goal to prove is the query and the knowledge base of previously proven theorems is the document set. The proposed method achieves better theorem proving performance than systems purely trained on human proofs, and approaches the performance of a prover trained by a combination of imitation and reinforcement learning. Overall, the paper is well organized and easy to follow.

Reasons to accept the paper:
1. The paper demonstrates that training the theorem prover without human data can succeed when using deep reinforcement learning.
2. The paper provides a side-by-side comparison of the effect of the availability of human proofs on the final theorem proving performance.
3. Experimental results show that the theorem prover trained without human proofs outperforms provers that are trained only on human proofs. Also, multiple ablation studies are provided to understand the underlying properties of the proof assistant and reinforcement learning setup.

Reasons to reject the paper:
1. The computational complexity and cost of the proposed method is not discussed in detail. Since the method is proposed to reason in large theories, the training efficiency should be important.
2. The proposed method relies on tf-idf based premises selection, which may limit the application scenario of the proposed method.
review_title: Official Blind Review #2

final_score: rating: 6: Marginally above acceptance threshold
review_content: In this paper, they tackle the challenge of learning to automated theorem (ATM) proving without any human imitation. Specifically the problem they focus on is premise selection. They find that while a vanilla RL scheme for ATM without any imitation learning of existing proofs frequently gets stuck and is not able to prove very many theorems, when a portion of the premises are selected via a simple term frequency-inverse document frequency (tf-idf) rule,  it dramatically increases the fraction of theorems proved — approaching the fraction of theorems proved with imitation learning of existing proofs.

In general I like this idea. While the approach is simple, the authors convincingly demonstrate that it is effective and it’s certainly interesting to learn that it is effective in this novel and highly important context. The authors also do several ablation experiments to thoroughly evaluate the components of the system.

A couple of questions — 
(1) Would taking into account the similarity of the newly generated sub-goals as per tf-idf (or some other metric) with respect to past sub-goals that had short proofs help?
(2) Is the allowed maximum runtime the same for the systems compared with and the new system?
review_title: Learning to Reason in Large Theories without Imitation

final_score: rating: 6: Marginally above acceptance threshold
review_content: The authors propose an RL approach to theorem proving focusing on improving the exploration aspect and demonstrates empirically that the proposed approach can perform well without requiring human proofs.

The paper is easy to read and the presentation is clear.

The authors address a very challenging issue of exploration in RL. Here, the proposed idea is to impose a preference on the action space being explored based on the tf-idf metric. The idea is itself not new but the way it is used in the RL setup, together with the presented empirical results, are relevant contributions.

With respect to the results in Figure 4, I wonder whether the authors can provide additional details in terms of the computational cost involved in each approach. In particular, what is the price to pay when going from pure-human to zero-explore? One would also imagine that with enough time resources, even zero-reference can eventually match zero-explore in validation score, but at what price?

It seems to me that the average proof length is a crucial parameter when it comes to scalability, since one would believe that the search complexity grows exponentially in the proof length. I assume that the use of tf-idf metric greatly reduced the "branching factor" in the initial search when the model is poor. Perhaps the author can comment on this so that the reader can judge whether a similar approach can be used in a different domain.
review_title: Simple idea, interesting empirical results.

final_score: rating: 6: Marginally above acceptance threshold
review_content: This paper aims at improving high-order theorem proving using deep reinforcement learning. The key idea of this study lies in the choice of premises for helping the prover. Here, the list of premises is formed by interleaving $k_1$ premises of highest score and $k_2$ premises to explore. The sublist of exploration premises is generated using a standard TF-IDF metric. The authors study how many extra premises can be added before the prover fails. They also propose a simple pruning technique for rapidly demoting irrelevant premises and promoting potentially relevant ones. Experiments using the HOLlist framework corroborate the interest of the approach.

Overall, this approach is conceptually simple and the experimental results look promising. Yet, I am not entirely convinced that this study provides a novel contribution since it is essentially using well-known techniques.

My main comment is that the hyper-parameters $k_1$ and $k_2$ have been carefully tuned, according to the table in Appendix A. It seems that the problem of choosing the top-k premises (included exploration premises) is intimately connected to online learning to rank with top-k feedback (e.g. Chaudhuri & Tewari, 2017). So, instead of choosing $k_1$ and $k_2$ at hand, could we use a bandit algorithm for selecting premises? Here, the “context/user” would be the theorem to prove, and the “items/documents” would be the candidate premises. 

As a minor comment, it would be nice to give more details about the (higher-order) language used to define expressions. It would help the reader in understanding more precisely the components of $r(G)$ and $r(P)$. 

----
Sougata Chaudhuri and Ambuj Tewari. Online learning to rank with top-k feedback. Journal of Machine Learning Research 18 (2017) 1-50

review_title: Review: Learning to Reason in Large Theories without Imitation

Meta-review: *Overview* This paper applies RL to automated theorem proving to eliminate the need for human-written proofs as training data. The method uses TF-IDF for premise selections. The experiments compared with supervised baseline demonstrate some good performance.

*Pro* The paper provides a side-by-side comparison of the effect of the availability of human proofs on the final theorem proving. 
The experiments compared with supervised baseline show that the proposed method has good performance even without human knowledge. The prosed TF-IDF selection algorithm addresses a challenging issue in exploration of RL. 

*Con* The reviewers primarily concern about  the novelty of the methods. It appears the method is not new since there exist a body of work leveraging RL to learn theorem provers. The tasks are also not novel.  After rebuttal, the reviewers are not convinced that the novelty is significant enough for ICLR. The reviewers are also concerned that the proposed method might not be easily generalized to other tasks. 

*Recommendation* Although the proposed method and experiment demonstrate some merits, there is a lack of novelty in terms of approaches. Since existing results already consider similar methods and similar tasks, it would make the paper stronger if thorough experimental comparisons are performed. 

Decision: Reject