Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 8: Top 50% of accepted papers, clear accept
review_content: This paper presents a simple theorem proving framework (supporting a limited logic e.g., no disjunctions) along with a sample set of axioms and algorithms that can be used to generate unlimited training data for proving theorems in this system.

Although the proof system itself is not of much practical interest, I really like this approach since it allows for a much more rigorous way to study the natural generalization questions that arise in theorem proving since the data generation can be controlled to a great extent. (The usual work in this area that uses existing proof corpora does not easily allow for answering such questions due to the lack of such control.) 

The authors use this framework to study the generalization of two classes of networks commonly used in theorem proving (transformers and graph neural networks), as well as to explore the utility of MCTS in theorem proving. Furthermore, the ability to generate a large amount of synthetic data is of independent interest, and the authors refer to a recent work that has used their framework to generate training data for a different system.

My main concern about this direction of research would be that perhaps these proofs are just too simple (e.g. like MNIST), and the results on this may not generalize to “real” proof corpora (e.g. ImageNet). But that remains to be seen, and I don’t necessarily consider that a drawback at the present time. However, the authors could bolster their case by doing a survey of other papers in this area which are using real proof databases and see to what extent their results in this simplified setting agree with or disagree with the results there.

Some important issues related to the writeup. Would like these to be addressed by the authors since it may reflect errors in understanding on my part.

1. I found Figure 1 confusing. In (a) (LEAN), how is the matching done i.e. do the rw rules match the LHS or the RHS of the equality? Would be good to explicitly bracketize the a + b + c rather than relying on implied left to right or right to left associativity of + (as is done in (b)).

2. In Figure 1 (c) shouldn’t the red circle for “Addition Associativity” be on the left child of the EQUALS node to provide the same example as (b)? (If so, this should also cause Goal 2 graph to change.)

3. In the worked example, I would encourage the authors to explicitly bracketize the expressions in the RHS of the different steps (to avoid any confusion with associativity).

4. At the bottom of page 3, you say that you initiate the core logic statement $C_0$ to be one of the initial conditions. But in the worked example, the initial conditions are $a = a, b = b,$ etc. So how do you get the expression a + (b + c) in Step 1? Shouldn’t C_0 be a simple equality like $a = a$ or $b = b$ rather than $a + b = a + b$?

Some questions about the experiments:

1. In Section 4.1, the training appears non-standard since you generate 1000 problems at a time and take 10 epochs; then generate another 1000 problems, and so on. Why not generate the 1.5 million problems up front and then train on the entire training set? What happens to the results if you do that?

2. How long does an experiment as set up in Section 4.1 take to run?

3. Related: Why not run for 5 seeds if computationally feasible. What is the variation in your results if you do that (rather than take the best)? I worry that with your current presentation of results, it is not clear what the inherent noise levels are, i.e. are the differences you find (e.g. that GNNs do better than Transformers on out of distribution) statistically significant or not? If 1.5MM examples is too computationally expensive, even running some of your experiments on a smaller set of examples would provide a sense of this variation.

*Post Rebuttal*

Thank you for your responses. I am bumping up the score.

review_title: Interesting approach to systematically study generalization in theorem proving but some questions about the experiments 

final_score: rating: 7: Good paper, accept
review_content: An approach to evaluate theorem proving using neural networks.

The paper describes a systematic approach to evaluating theorem provers in terms of generalization. Specifically, since for theorem proving the test data can be significantly different from the training data, the proposed approach develops a method to generate synthetic problems to simulate this. The main contribution is a theorem generator that can produce non-trivial theorems to evaluate a model.

The paper is well written and has extensive empirical analysis for neural network based theorem proving. It produces a general approach that can be used to improve the state-of-the-art in evaluation of neural network based theorem provers. I am not very familiar with  other approaches that can generate synthetic data for theorem proving, but it seems like this is first approach that can generate an infinite number of theorems with complex proofs which can evaluate generalization of the prover which to me seems to be a significant contribution. Further, the empirical analysis is extensive that includes several well-known methods along several dimensions. I think this paper has sufficient merit with potential for significant follow up research based on the proposed benchmark.
review_title: An approach for evaluating theorem proving and a detailed empirical study of different neural network architectures for theorem proving. The paper addresses an important problem and is well presented.

final_score: rating: 6: Marginally above acceptance threshold
review_content: The paper introduces a synthetic dataset for learning theorem proving
based on (ordered) field axioms. It also trains learning-based theorem
proving on them and in particular compares transformers and GNNs.  The
motivation is to provide a dataset for investigating the
generalization ability of various ML models.  Six different metrics
are used for the experiments.

The generator and the prover look nice and cleanly implemented and a lot of 
experiments have been done.

On the other hand, it is not quite clear how the six metrics actually
reflect generalization ability on theorems encountered in practice,
and what new insights are gained from the experiments.

The dataset also looks quite simple and seems comparable to previous
synthetic arithmetical datasets released e.g. as part of [1]. Other
synthetic datasets were released as part of [2,3] where the tasks
belong to those found interesting and previously used by
well-established ATP researchers.

The method for generating problems looks like quite a straightforward
application of the axioms to an initial statement. I would
think that using actual state-of-the-art ATPs for such forward runs is
probably easier and applicable to an arbitrary domain. Such things have
been done in the past - e.g. to generate the AIM dataset in CASC
2016 [23] by sampling increasingly long inference chains from Prover9
runs on actual mathematically interesting problems.

A great danger of synthetic datasets is that it is completely
unclear how useful the methods are on real-world math data. The
argument that there are not enough real-world math data is flawed. All
of the larger ITP corpora (Isabelle, Mizar, HOl, Coq) are capable of
easily exporting millions of problems and proofs.
Already the first version of MPTP and the AI/TP
experiments based on it [3] allowed and announced a straightforward
generation of 630000 related proof tasks from Mizar. Further millions
of "synthetic" tasks can be created easily by chasing the large
derivation graphs of MML and other ITP libraries. This has been to some
extent used later e.g. in works such as [4,9], where the benefit of
learning from additional proof tasks was also demonstrated.

I would also say that much larger improvements have been achieved by
iterating learning and reasoning and thus "synthesizing" the body of
training proofs.  Such proofs are also created "synthetically" in some
sense - as a result of diversely parameterized proof attempts on a
curriculum of relevant theorems. This goes back at least to MaLARea
[11,12] and continues in systems like ATPBoost [13]. Hence the most
straightforward iterative approach to producing more *real-world*
proof data to learn from seems far from saturated at the moment.

There have also been many ways how to synthesize relevant new
problems/conjectures, some of them neural [15-22].

The comparison of transformers and GNNs is perhaps the most interesting
part of the work. While both settings have been used for ATP tasks
before, this may be their first head-to-head comparison.

Overall, there is a lot of work here, but I am not quite sure how
interesting it is, how much difference it makes to the number of other 
methods for generating problems, and if this is going to be a useful dataset.

My feeling is that there has been a lot of "real-world" ATP/ITP datasets out there for a long time, and 
that those are very easy to augment further to corpora that will be larger than the number of particles in the universe.
The AI/TP researchers should really focus on developing strong theorem proving methods on them rather than on coming up with more and more datasets, especially very synthetic ones.

I am hesitating between 5 and 6, going now for 5.

Some more detailed comments:
==================

- Formalized mathematical theorems in ITPs include the Feit-
Thompson theorem (Huang et al., 2019)
==> certainly not the right citation?

... the Kepler Conjecture (Bansal et al., 2019).
==> dtto

- Time and memory requirements for the proof assistant have often been an obstacle for using theorem
provers as RL environments. Most existing proof assistants require a large software library to define
numerous mathematical theorems, leading to slow simulation.
==>
What is meant by slow simulation here? Why would a large library lead
to it?  As for RL toolkits, the first RL-for-TP experiments done over
a large part of the Mizar library [5] required orders of magnitude less
resources than e.g. training of AlphaGo/Zero .

- The GNN used does not seem to be logic-aware as the one by Olsak used to extend rlCoP [7] and ENIGMA [8].


[1] Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban:
Towards Finding Longer Proofs. CoRR abs/1905.13100 (2019)

[2] Thibault Gauthier:
Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic. LPAR 2020: 230-248

[3] Thibault Gauthier:
Deep Reinforcement Learning in HOL4. CoRR abs/1910.11797 (2019)

[4] Cezary Kaliszyk, Josef Urban:
Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69: 109-128 (2015)

[5] Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák:
Reinforcement Learning of Theorem Proving. CoRR abs/1805.07563 (2018)

[6] 	Jan Jakubuv, Josef Urban:
Hammering Mizar by Learning Clause Guidance. CoRR abs/1904.01677 (2019)

[7] Miroslav Olsák, Cezary Kaliszyk, Josef Urban:
Property Invariant Embedding for Automated Reasoning. ECAI 2020: 1395-1402

[8] 	Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban:
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). IJCAR (2) 2020: 448-463

[9] Kaliszyk, C., Urban, J. & Vyskocil, J. Lemmatization for Stronger Reasoning in Large Theories in
FroCoS 2015 9322 (Springer, 2015), 341–356.

[10] Thibault Gauthier, Cezary Kaliszyk:
Sharing HOL4 and HOL Light Proof Knowledge. LPAR 2015: 372-386

[11] Urban, J. MaLARea: a Metasystem for Automated Reasoning in Large Theories in CADE-21 Work-
shop on Empirically Successful Automated Reasoning in Large Theories 257 (CEUR-WS.org, 2007).

[12] Urban, J., Sutcliffe, G., Pudlák, P. & Vyskocil, J. MaLARea SG1- Machine Learner for Automated
Reasoning with Semantic Guidance in IJCAR 2008 5195 (Springer, 2008), 441–456.

[13] Piotrowski, B. & Urban, J. ATPBoost: Learning Premise Selection in Binary Setting with ATP
Feedback in IJCAR 2018 10900 (Springer, 2018), 566–574.

[14] Gauthier, T., Kaliszyk, C. & Urban, J. TacticToe: Learning to Reason with HOL4 Tactics in LPAR
21 46 (EasyChair, 2017), 125–143.

[15] Gauthier, T., Kaliszyk, C. & Urban, J. Initial Experiments with Statistical Conjecturing over Large
Formal Corpora in (CICM 2016 - Work in Progress Proceedings 1785 (CEUR-WS.org, 2016), 219–
228.

[16] Thibault Gauthier. Deep reinforcement learning in HOL4. CoRR, abs/1910.11797,
2019.

[17] Karel Chvalovsky, Thibault Gauthier & Josef Urban:
First Experiments with Data Driven Conjecturing, AITP'19, 2019.
http://aitp-conference.org/2019/abstract/AITP_2019_paper_27.pdf

[18] Josef Urban, Jan Jakubuv:
First Neural Conjecturing Datasets and Experiments. CICM 2020: 315-323

[19] Lenat, D.B.: AM: an artificial intelligence approach to discovery in mathematics
as heuristic search. Ph.D thesis, Stanford (1976)

[20] Fajtlowicz, S.: On conjectures of Graffiti. Ann. Discrete Math. 72(1–3), 113–118
(1988)

[21] Colton, S.: Automated Theory Formation in Pure Mathematics. Distinguished 
Dissertations. Springer, London (2012).

[22] Johansson, M., Rosén, D., Smallbone, N., Claessen, K.: Hipster: integrating theory
exploration in a proof assistant. In: Watt, S.M., Davenport, J.H., Sexton, A.P.,
Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 108–122.
Springer, Cham (2014).            

[23] Geoff Sutcliffe: The 8th IJCAR automated theorem proving system competition - CASC-J8. AI Commun. 29(5): 607-619 (2016)

==================

UPDATE

Thanks to the authors for their detailed replies and paper updates.

I am still quite skeptical about the necessity of the use of INT for the 2% improvement of the Metamath GPT experiments. As I mentioned, just using the millions/billions of internal ITP/ATP lemmas has raised the performance much more in previous experiments. And given the "feed our GPT anything mathy" approach, I would expect that training on any sufficiently big ATP corpus might help the GPT.

In general, I am also still quite skeptical that generating more and more synthetic corpora without good relation to real-world math (and motivation by it) has much meaning and will lead to much progress in the ML-for-TP area. 

The fact that some teams have burnt a lot of CPU/GPU power on dubious AI/TP setups does not mean that this is the way how things should be done (and how good AITP research is actually done in many cases). In fact, ATP is quite a good example of a domain where brute force helps only to a very limited extent. Rather than being impressed by the wasted resources, I would advise the authors to focus on resource-controlled setups and competitions such as CASC and CASC LTB.

All this said, I do appreciate the relatively large amount of work the authors have invested in this research. So I increase the score and vote for the paper being published mostly for that reason, while encouraging the authors to focus their energy on more realistic setups.    











review_title: A lot of work but in unclear direction

final_score: rating: 6: Marginally above acceptance threshold
review_content: The paper describes a synthetic dataset generator for inequality
statements over ordered fields.  The reason is to provide a test of
generalization ability of models in interactive theorem proving tasks
with Lean examples given as motivation. A lightweight syntax tree
based prover is used by the machine learning agents to attempt solving
the generated statements. GNN experiments with various masures show
some generalization ability.

I appreciate the developed inequality theorem generator and the
provide API. They indeed could be useful for further investigations.

I am however still not convinced that the considered measures
correspond well to the generalization ability that the paper wants to
show. For me the task is very simple in comparison with the claims.
I am happy about the one given generalization example, but other than
this what I can read from the paper is agents can solve test problems
similar to those seen during training. As such, I do not think that the
research done in the paper supports the conclusions the authors draw.
The same holds for the out-of-distribution generalization where again
the experiments show a small generalization capability but I am not
convinced that this approach can in general lead to generalization.

I appreciate the addition of the Monte Carlo tree search to the base
model and the consideration of some models (even if still short).

review_title: Synthetic dataset generator for inequality statements over ordered fields

Meta-review: This work proposes an algorithm for generating training data to train automatic theorem proving models. In particular, it allows users to pose specific generalization challenges to theorem proving models and evaluate their performance. In doing so, it provides a degree of control over the task space that is greater than when working with 'organic' corpora of real theorems and proofs.

 The authors demonstrated the utility of their generated data by training well-known models such as transformers and GNNs, and were able to derive insights such as the value of MCTS-style planning for finding proofs in particular settings. 

After the rebuttal period, all authors agreed that the work was well executed and that the algorithm creates datasets that will be of value to the (learning-based) theorem proving community. As such, they all recommended acceptance to a greater or lesser degree. I am convinced by their arguments, because I think there is real value in using controlled synthetic data alongside real data when making scientific progress on hard problems like theorem proving. I am particularly convinced by the observation that the data generated by this method has already led to improved performance on a real corpus of proofs, as the authors state in their rebuttal. If they have not done so already, I encourage the authors to report this fact in the camera ready version of their paper citing the relevant work. 
Decision: Accept (Poster)