Venue: ICLR 2020 Conference

Reviews:

final_score: rating: 3: Weak Reject
review_content: This paper focuses on the problem of developing deep learning systems that can prove theorems in a mathematical formalism -- in this case, MetaMath. This has been a rapidly growing topic in the past few years, as evidenced by the numerous cited works. What sets this work apart from others is its focus on the instrumental task of generating data to train a prover, rather than directly training the prover on human theorems (via reinforcement learning) or human proofs (via imitation learning).

The paper proposer two approaches to generating theorems imitation learning (IL) and reinforcement learning (RL). The IL approach trains a neural policy to imitate the same steps taken in human proofs. The RL approach first trains a language model on human theorems (not proofs), and uses the likelihood under the model as a reward function for an RL agent which must take forward proof steps.

Both approaches result in a policy that can be used to take proof steps, with the goal of producing new theorems which are similar to the human ones. Since the proof steps are known for the generated theorems, a prover agent (which operates in backwards mode, working from the goal back to the hypotheses) can be trained to imitate the steps taken in the synthetic proofs (along with the human ones, if any are present).

At test time, the learned prover imitation policy is then used to guide an MCTS agent, as described in the Holophrasm paper. It is compared against the original Holophrasm algorithm, rerun on modern hardware.

This is to my knowledge a novel approach in the neural theorem proving domain, and in my opinion one that offers a potentially significant advantage over the existing fixed-dataset appraoches.

The main result of the paper is that an extra 35/2720 (1.2%) of the test theorems are proven, a 6% improvement over the Holophrasm baseline of 539. It is difficult to judge how relevant of an improvement this is, and there is no analysis of the difficulty of the MetaMath problem set. In addition, due to the 10-1-1 train-validation-test split, the neural agents are likely shown relatively similar problems during training as at test time, including potentially stronger versions of the same theorems. There is also no comparison against non-neural approaches, such as Z3, Vampire, or similar theorem provers. 

To accept this paper, I would like to see stronger evidence that the introduced method produces significant improvements in prover ability. For example, the same method could be applied to datasets such as HOList, Mizar, and CoqGym which have received more attention recently than MetaMath.

Some additional questions and comments:
1. How big does the theorem graph G get? Since the relevance policy is over all nodes of the graph, this could lead to a very large neural network that would be difficult to fit into memory. Certainly not all 1M synthetic theorems could be generated in one graph.
2. The paper claims that all theorems from set.mm are used as background theorems in algorithm 1, including the test ones -- this potentially sounds like training on the test set, or even worse, having access to the test theorems as "proven background knowledge" at test time.
3. Please include some more details about the training of the Holophrasm baseline. Does it simply do RL on the human theorems, or does it also do IL on human proofs?
review_title: Official Blind Review #4

final_score: rating: 6: Weak Accept
review_content: This paper focuses on the task of automated theorem proving. To address the low availability of human-written data and low sample efficiency in reinforcement learning, the authors propose to augment data by generating synthetic theorem data with a deep neural network-based model. Experimental results show the usefulness of the generated synthetic theorem. 

This paper is well-motivated and the proposed method is quite novel for automated theorem proving. The paper is well-supported by theorems, however, the experimental analysis is a little weak. For the above reasons, I tend to accept this paper but wouldn't mind rejecting it.

Questions:
1. Maybe it's better if you can shorten section 3 and explain more about the problem setting (such as how to fit this problem in a graph?).
2. Can you show some examples of generated theorems?
3. You showed the prover has better performance with more synthetic data, but why is your model (generator) better? Can other generative models generate better proofs?
review_title: Official Blind Review #1

final_score: rating: 6: Weak Accept
review_content: This paper proposes a generative model for proofs in Metamath, a language for formalizing mathematics. The model includes neural networks, which provide guidance about which fact to try to prove next and how to prove the fact from the facts derived so far. The parameters of these networks are learned from existing proofs or theorem statements. The main purpose of this model is to generate synthetic theorems and proofs that can be used to train the neural networks of a data-driven search-based theorem prover. The experiments with the Metamath set.mm knowledge base show the benefits of the synthetically generated proofs for building a data-driven theorem prover.

I think that the paper studies an important problem and contains interesting ideas. The idea of using a language model for theorem statements (so that a generated theorem can be meaningfully compared with a given theorem even when they are not the same) looks sensible. Also, the conjecture that a good proof generator is likely to lead to a good theorem prover sounds plausible. 

I find the description of the training of the generative model in the experiments slightly confusing. Adding some clarification may help some readers. More specifically, here are some questions that I couldn't answer for myself. What theory is formalized by set.mm? Set theory? Among the proofs of 29337 theorems, which ones are used during the training of the generative model? 


Here are some minor comments. 

* p1: positive awards ===> positive rewards

* p2: A citation is missing in the first sentence of Section 2.

* AddNode, Algorithm1, p5: Merge h_q to h' ===> Merge h_q to h

* p6: uses a_v as a precondition ===> uses a_u as a precondition

* p6: and has been ===> has been

* p7: which demonstrate ===> which demonstrates

* p7: from these the relevance ===> from the relevance

* p7: wiht ===> with

* p9: languagee ===> language

review_title: Official Blind Review #3

Meta-review: This paper proposes to augment training data for theorem provers by learning a deep neural generator that generates data to train a prover, resulting in an improvement over the Holophrasm baseline prover. The results were restricted to one particular mathematical formalism -- MetaMath, a limitation raised one by reviewer. 

All reviewers agree that it's an interesting method for addressing an important problem. However there were some concerns about the strength of the experimental results from R4 and R1. R4 in particular wanted to see results on more datasets, an assessment with which I agree. Although the authors argued vigorously against using other datasets, I am not convinced. For instance, they claim that other datasets do not afford the opportunity to generate new theorems, or the human proofs provided cannot be understood by an automatic prover. In their words, 

"The idea of theorem generation can be applied to other systems beyond Metamath, but realizing it on another system is highly nontrivial. It can even involve new research challenges. In particular, due to large differences in logic foundations, grammar, inference rules, and benchmarking environments, the generation process, which is a key component of our approach, would be almost completely different for a new system. And the entire pipeline essentially needs to be re-designed and re-coded from scratch for a new formal system, which can require an unreasonable amount of engineering." 

It sounds like they've essentially tailored their approach for this one dataset, which limits the generality of their approach, a limitation that was not discussed in the paper. 

There is also only one baseline considered, which renders their experimental findings rather weak. For these reasons, I think this work is not quite ready for publication at ICLR 2020, although future versions with stronger baselines and experiments could be quite impactful.





Decision: Reject