Venue: ICLR 2020 Conference

Reviews:

final_score: rating: 3: Weak Reject
review_content: In the paper, the authors present a new algorithm for training neural networks used in an automated theorem prover using theorems with or without proofs as training data. The algorithm casts this training task as a reinforcement learning problem, and employs curriculum learning and the Proximal Policy Optimization algorithm to find appropriate neural network parameters, in particular, those that make the prover good at finding long proofs. The authors also propose a new dataset for theorems and proofs for a simple equational theory of arithmetic, which is again suitable for improving (via learning) and testing the ability of the prover for finding long proofs. The proposed prover is tested against existing theorem provers, and for the authors' dataset, it outperforms those provers.

I found it difficult to make up my mind on this paper. On the one hand, the paper tackles an interesting problem of improving an automated theorem prover via learning, in particular, its ability for finding long nontrivial proofs. Also, I liked a qualitative analysis of the failure of the curriculum learning for tackling hard tasks in the paper. On the other hand, I couldn't quite make me excited with the dataset used to test the prover in the paper. The dataset seems to consist of easy variable-free equational formulas about arithmetic that can be proved by evaluation. Of course, I may be completely wrong about the value of the dataset. Also, if the dataset includes variables and other propositional logic formulas, such as disjunction, negation and conjunction, so that the prover can be applied to any formulas from Peano arithmetic via Skolemization, I would be much more supportive for the paper. Another thing that demotivated me is that I couldn't find the discussion about the subtleties in using curriculum learning and PPO for the theorem-proving task in the paper. What are the possible design choices? Why does the authors' choice work better than others? 

I added a few minor comments below.

* abstract, p1: "significantly outperforms previous learning-based". When I read the experimental result section, I couldn't quite get this sense of huge improvement of the proposed approach over the existing provers. Specifically, from Table 4, I can see FLoP performs better than rlCoP, but I wasn't sure that the improvement was that significant (especially because rlCoP might not have given a chance to be tuned to the type of questions used to train FLoP -- I may be wrong here). I suggest you to add some further explanation so that a reader can share your sentiment and excitement on the improvement brought by your technique.

* p2: The related work section is great. I learned a lot by reading it. Thanks.

* p4: I think that you used the latex citation command incorrectly in "learning Resnick ... Chen (2018)"
and "features Kaliszyk ... Kaliszyk et al. (2015a; 2018)".

* p6: discount factor) parameters related ===> discount factor), parameters related 

* p8: a a well ==> a well 


review_title: Official Blind Review #3

final_score: rating: 3: Weak Reject
review_content: This paper uses reinforcement learning for automated theorem proving. The proposed method aims to generalize the short proofs to longer proofs with similar structure. Experiments were run to compare the performance of curriculum learning with the ones without curriculum.

Overall the paper attempts to explain clearly the original contribution of the proposed approach, which is using curriculum learning in RL based proof guidance. However,  I am not convinced about the how compelling the results are in support of the claim. The main arguments to bolster my decision are as follows.

I am familiar with RL and curriculum learning but not so much with connection tableau calculus. The description given in the paper seems to be insufficient and confusing for readers with limited knowledge in this area. A step-by-step explanation with a toy example might have done the job nicely. Without such a clear understanding of the calculus, it gets hard to appreciate the merits of the results.

Some claims of the paper are not clearly validated by the reported experimental results. For example:
- in Table 8, curriculum learning is worse in some cases and better in others. What to conclude from such a report?
- in experiment 3, curriculum learning tends to find shorter proofs. Isn't that contrary to the focus of the paper? 
- in Table 3, curriculum learning performs lot worse than the other method. What is to be inferred from such a report?

It would be nice if there was a clear explanation of the role of curriculum in the learning algorithm. For example, in Algorithm 1, how is Line 8 helping in overall objective of learning longer proofs? If one advances curriculum, one takes lesser number of proof steps according to stored proofs. How does that help in the learning? Does it imply 'less memorizing' with advancement of curriculum?
review_title: Official Blind Review #2

final_score: rating: 6: Weak Accept
review_content: OVERALL:

I don't work on ATP and am not particularly well suited to review this paper, but I am
slightly inclined to accept for the following reasons.

1. It's an important problem and not much work is done on it.
2. Creating new environments is hard, valuable work that is (IMO) insufficiently incentivized in our community,
and I think accepting papers that do this work is a good policy.
3. The experiments, to my super-inexperienced eye, seem well designed and like they address
obvious questions readers would have.

However, I have no idea if e.g. the baselines used in this paper are reasonable, so
I would appreciate someone with more experience on that topic weighing in.


Some limitations of the paper:

1. I'm not actually convinced there's much that's methodologically new here. 
It seems like mostly an application of existing RL techniques to an ATP environment.

2. The writing is not particularly clear, and could use substantial editing (but this
is something that could be fixed during the discussion period).

3. The focus on Robinson arithmetic seems kind of limiting.
Though I am sympathetic to the reasoning given in the paper, it's unclear to me (again, as a non-expert),
that the techniques that work in this context will actually work in the context considered by e.g. [1]

DETAILED COMMENTS:
> In the training set, all numbers are 0 and 1 and this approach works more often.
You have this sentence twice in different places.

> it is insightful to compare...
Not a very idiomatic use of insightful?


[1] Deep network guided proof search.

review_title: Official Blind Review #1

Meta-review: This paper proposes a curriculum-based reinforcement learning approach to improve theorem proving towards longer proofs. While the authors are tackling an important problem, and their method appears to work on the environment it was tested in, the reviewers found the experimental section too narrow and not convincing enough. In particular, the authors are encouraged to apply their methods to more complex domains beyond Robinson arithmetic. It would also be helpful to get a more in depth analysis of the role of the curriculum. The discussion period did not lead to improvements in the reviewers’ scores, hence I recommend that this paper is rejected at this time. 

Decision: Reject