Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 4: Ok but not good enough - rejection
review_content: This paper proposes a theorem prover based on Proximal Policy Optimization for the connection tableau calculus. This prover is applied on five domain-specific datasets, where theorems are relatively simple but their proofs are long and repetitive. The proposed theorem prover could achieve competitive performance with strong baseline provers, yet requires much few searches. 


I think the assumption of this paper is correct that we need more accurate heuristics but not more searches to find longer proofs. The main issue is that it is unclear what is the novelty of the proposed approach. The approach section of the main paper is quite short, just one paragraph (section 3) and one algorithm. It seems that the main approach is to train the theorem prover by reinforcement learning following a specific learning curriculum. It is not mentioned that why the proposed approach has advantages to finding longer proofs, and how the proposed approach is related to reasoning by analogy. Currently, the reasoning by analogy approach mentioned in section 2 seems irrelevant to the proposed approach, except that they may share the same effect and target to reduce the number of searches within the prover. 

I think the proposed approach shares the same form of heuristic as the prior work on neural theorem proving, that building a reactive policy to select the next action based on the current proof state. I can not see how this is related to reasoning by analogy, which is described as "Reasoning by analogy involves observing the proof of one problem, extracting the core idea, and
successfully applying it to another". All should we consider all neural-based provers as reasoning by analogy, since they are trained with existing proofs? 

=================================================
After reading the responses from the authors and other review comments, I maintain my previous rating of this paper. I am not convinced that the proposed approach is a simple form of analogy reasoning. Trying to build a relationship between the proposed approach and analogy reasoning is uninformative and misleading. 


review_title: How does FLoP relate to reasoning by analogy?

final_score: rating: 6: Marginally above acceptance threshold
review_content: Summary:
This work introduces a method for learning to prove theorems which can leverage prior proving experience in order to discover very long proofs. At its core it works by inputting a corpus of training problems (which can also be annotated with solutions i.e. proofs), training a policy to solve these training problems by curriculum learning. The curriculum works by first supervising on the trace of an entire solution, and then once the system can solve a particular problem, decreasing the amount of the trace that it supervises on. The authors claim that this is a kind of analogical reasoning, because the system's policy is implicitly learning to represent the state/action space on the basis of prior experience.

I'm not convinced that this looks very much like the analogical reasoning advertised in the introduction to the paper , which claims "Reasoning by analogy involves observing the proof of one problem, extracting the core idea, andsuccessfully applying it to another". The system does not work by fetching previous proofs and massaging them into a proof for a new problem, except implicitly through the prior knowledge represented in the weights of the policy. My only real objection to this work is that it doesn't function as advertised. In particular I'm not sure why the learned policy wouldn't be subject to the "the exponential blowup [which causes] the search... to fail beyond a certain depth," which afflicts prior methods.

IMO this paper should be accepted iff this approach is a new advance for automated theorem proving, but should not be accepted on the basis of it's connection to reasoning by analogy. However, it is possible that I have misunderstood how the algorithm works, and would like to be corrected by the authors if indeed the algorithm works as advertised. Because I am not well steeped in the automated theorem proving literature, I do not feel qualified to make the call on how big of an advance this is for that community. However, it does not seem like a large advance for deep learning or for combinatorial search.

Pros:
+ seems to scale to some extraordinarily long proofs! For example, their system can discover proofs with steps on the order of 10^3-10^4. Given the combinatorial explosion in the search space (scales exponentially with proof length) this is quite impressive.
+ reasoning by analogy is crucial yet underexplored. It should be especially important for few-shot learning of proof strategies, and I'm glad that the authors have taken up this line of research.

Cons/questions:
- How sensitive is the system to the training problems from which it forms analogies? For instance experiment 3 hinges on two particular seed expressions--how did you choose them?
- How much do you depend on the particular feature space? Appendix F lists what seem like a relatively impoverished feature representation for the state space. Is this intentional, whereby narrowing the feature space you improve transfer between the target (training) and source (test) proofs? In that case it would seem that the method would struggle absent careful feature engineering, which could limit its applicability beyond the simple theories considered here (nb: although the theories are simple the proofs are extraordinarily long)

Minor concerns:
typo page 3 - "allows for potential reusing" (potential to potentially)
missing citation page 3 - "Despite the unquestioned role of..." (include citation to "Mathematics and Plausible Reasoning")
make figure one larger
figures 2/3: surely you must be doing some kind of kernel density smoothing here?
experiment 1/table 2: describe E2--which is at ceiling--as exploiting hand-crafted domain-specific strategies for arithmetic, preferably in the caption. Otherwise it is confusing why it is at ceiling just by looking at the table
review_title: Impressively scalable search with fairly standard RL, possibly tenuous connection to analogy

final_score: rating: 8: Top 50% of accepted papers, clear accept
review_content: This work introduces a new algorithm FLoP for theorem proving using reinforcement learning, and tests it on a new evaluation dataset.  FLoP gives direction to a tableau based theorem prover by learning a state machine using curriculum learning applied to a prototype proof.  The authors state that this RL technique has not been previously applied to theorem proving.  I cannot judge this statement but if true it would seem enough novelty to justify publication.   They find that the technique works best on highly structured problems such as proving simple arithmetic statements in unary or binary arithmetic, and less well for problems which benefit from searching through databases of heterogeneous statements.

One could debate whether this deserves the name of "reasoning by analogy".   I suspect it should be called "reasoning by imitation".   To my mind, the term analogy suggests a reasoning process in which some features are extracted from the proof, and then the proof strategies which work for these feature values are selected out of a large set of possibilities including many with different feature values.  I quote from the authors' description at the beginning of section 6 of what they show: "In this highly structured dataset FLoP is capable of extracting a general proof pattern from one or two proofs and successfully generalizing to related proofs of arbitrary length."  This does not sound like analogy as I defined it, rather it sounds like imitating the prototype. 

Still, since the comparison with other techniques is encouraging, and since the paper is clearly written and gives a very extensive survey of comparable works, I found it enlightening and would recommend to accept it.
review_title: Does reinforcement learning include reasoning by analogy?

Meta-review: This paper describes an application of reinforcement learning to theorem proving in the connection tableau calculus.  The paper does a reasonable job in the application of RL techniques and the high level issues are important.  However, as the reviewers note, there is little connection to the notion of "analogy" outside of the very general idea that RL methods learn to generalize to novel situations.

I did not find the methods very original as it seems a somewhat mechanical application of RL methods.  That would be fine if the empirical results were convincing or surprising.  However, I found the Robinson arithmetic domains not very interesting as the problems were literally arithmetic, as in 2+5 = 7, rather than theorems such as the commutativity of addition.  The empirical results were not as convincing in the TPTP domains where MCTS seemed to dominate.

Also there are related papers in the area of deep learning applied to theorem proving that I believe dominate this paper ("learning to reason in large theories" and "an inequality benchmark".
Decision: Reject