Venue: ICLR 2022 Conference

Reviews:

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: The paper proposes an incremental learning approach to theorem proving that learns to prove theorems from scratch, using Hindsight Experience Replay (HER) to learn from unsuccessful proofs. The approach adopts ideas from goal-conditioned reinforcement learning and creates more training examples by turning intermediate steps of an unsuccessful proof attempt into proved conjectures and add these into positive examples to learn from. This significantly increases the number of examples to learn from compared to related work that only learns from successful proofs. The approach is shown to be competitive against E prover, a SOTA prover, on a subset of TPTP without equality.
main_review: Strengths:

The idea of creating positive examples from failed proofs seems new in theorem proving and, together with HER, shown to significantly improve performance of the learning-based prover. 

They propose a transformer based representation of logical statements.

Weaknesses:

It's hard to compare the proposed approach to other learning-based approaches in the literature. The authors create their own dataset instead of using benchmarks widely used in the literature (M2k [1] and MPTP2078[2]). This is probably due to their underlying prover not supporting entire first-order language as it cannot solve problems with the equality symbol. This can be addressed by replacing their underlying prover with any SOTA classical prover (e.g., E prover) but disabling its heuristics as done in some work in the literature (e.g., [3] uses Beagle as underlying prover with its heuristics disabled). 

The paper seems to downplay the performance of the approach proposed in [3] by saying it still doesn't get close to E. But the only reason they can say theirs is competitive against E is because their dataset is classified into domains, where we can clearly see their approach beating E in some domains but on aggregate results their approach still falls short to beat E, just like [3]. Furthermore, their subset of TPTP problems without equality and number of axioms less than 1000 could be much easier than problems with equality and have significantly more axioms.

Provers in their experiments are not given a time limit for attempting to prove theorems as typically done in the literature (100 seconds is used in [1] and [3]). Again, this makes it possible to evaluate the proposed approach in the context of related work. 

They proposed a new representation of logical statements based on transformers but a motivation of this new representation is not given, especially given that graph neural networks have been shown to represent logical statements well. Also, the benefit of such a representation is not shown empirically. So we don't know if this proposal adds any new value.

It's not clear if the incremental learning approach used should, in principle, be better than reinforcement learning based approaches used in the literature (e.g., [3]). In principle both approaches are learning from scratch, but their approach learns a scoring network from examples generated as successful proofs (included those added from unsuccessful ones) whereas RL based approaches use a reward mechanism.

By the way, recent work on building machine learning based proof guidance systems have come closer to beating E on M2k dataset and actually beat it on MPTP2078 dataset [4].

[1] Kaliszyk, C.; Urban, J.; Michalewski, H.; and Olsák, M. 2018. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems 31, NeurIPS 2018, 8836–8847.
[2] Alama, J.; Heskes, T.; Kühlwein, D.; Tsivtsivadze, E.; and Urban, J. 2014a. Premise selection for mathematics by corpus analysis and
kernel methods. Journal of Automated Reasoning 52(2):191–213.
[3] Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille. Fokoue. A deep reinforcement learning approach to first-order logic theorem proving.
Proceedings of the AAAI Conference on Artificial Intelligence, 35(7):6279–6287, 2021
[4] Ibrahim Abdelaziz, Maxwell Crouse, Bassem Makni, Vernon Austil, Cristina Cornelio, Shajith Ikbal, Pavan Kapanipathi, Ndivhuwo Makondo, Kavitha Srinivas, Michael Witbrock, Achille Fokoue, https://arxiv.org/abs/2106.03906#
summary_of_the_review: While the idea of using unsuccessful proof attempts with HER seems new and can benefit the learning-based theorem proving community, as it stands, the paper doesn't do a good job of showing the benefits of their overall theorem prover empirically. Combining these ideas with traditional ATPs and evaluating on published benchmarks is recommended.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: The paper proposes an incremental learning algorithm for training domain-specific provers for first-order logic without equality, and addresses the sparsity of training data by adapting hindsight experience replay. In short, it uses clauses generated during a proof attempt to generate new goals that can be explored further.
main_review: Strength: the idea of using hindsight experience replay is straightforward (which is good). The algorithms are well-thought-out (such as using time scheduling and subsampling the hindsight goals) and the experiments clearly show the gain of using hindsight goals.

Weakness: my major concern is the absolute performance of the resulting prover. Table 1 suggests that the resulting prover is marginally better than E — being able to prove 1 or 2 more theorems in some domains, while E finds ~10 more theorems on FLD1 and FLD2. It is fine that the resulting prover does not outperform E which is SOTA, but in that case I would like to see at least one comparison with other learning based approach, evaluated on either TPTP or another suitable data set. 

Table 1 also seems to suggest that TPTP is probably too easy for both E and IL w/HER. Have you considered using other benchmarks (e.g., [GRUNGE](https://arxiv.org/abs/1903.02539))?

Also note that [TacticZero](https://arxiv.org/abs/2102.09756) uses policy gradient which implicitly uses subgoals in failure proof attempts to train the neural networks. 

Minor: 
1. The representation seems a bit too complicated. Would a graph neural network make life easier? Or perhaps simply a transformer encoder.
2. “Although the set of active clauses is an important factor … we ignore it …”. This is probably the right place where you can introduce hand-engineered features that summarize the information of the set of active clauses.
3. Since the hindsight goals probably contain the information similar to the original goal, I suspect that HER wouldn’t offer too much when evaluated on goals from another domain. I would like to see a bit more cross-domain evaluation, but since the paper already made it clear that the approach is domain-specific, the current experiments are fair.
summary_of_the_review: Although the absolute performance of the proposed framework is not at a state-of-the-art level, the usage of HER (though not entirely novel) is justified and the overall algorithm is novel and well-designed. It is unclear how the framework compares to other learning-based systems. The paper is well-written.
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: The paper applies hindsight experience replay (HER) to automatic theorem proving (ATP). ATP attempts to prove logic statements by (roughly speaking) showing that there are no counterexamples, i.e. showing that nothing resolves the negation of a statement. HER is a technique from reinforcement learning which mitigates sparse rewards by treating failed attempts as successful attempts on a different problem, namely that with the end state of the attempt as the goal.

The paper is not quite an HER method however ; it does not use reinforcement learning but rather incremental learning, where clauses generated during proof attempts are used as additional data for (incremental) supervised learning.
main_review: Including the primer on first order logic is an excellent idea, thank you.

Overall the writing is clear and well structured. The presentation of the figures and tables is a pleasure to behold.

The title of the paper seems somewhat misleading given that this is not RL but an HER inspired incremental learning method.

The notation in appendix C is unusual for an ML audience. I would recommend to write something like p(X=k)=... instead of stating w_s which we must infer is the value of the pmf (e.g. copy the notation of https://en.wikipedia.org/wiki/Poisson_distribution).

TacticZero by Wu et al 2021 is missing in the references. That work includes an RL reward for sub goals which are proved, so is highly related to hindsight experience replay in the sense that attempts that do not prove a main goal nonetheless serve as training data. Moreover by training end to end the scoring functions of Wu et al are properly coupled to the search process. This is not the case for the submission, where the training of the scoring is not optimally matched with the search process.

The experimental performance is reasonable. Losing out to E suggests that the heuristics of E could be included as features for the scoring rule - though it is not essential to add that here of course, this is just a suggestion.
summary_of_the_review: This is a nicely presented work with a novel approach to using clauses generated during proof search for training. The approach is somewhat ad hoc however, and could benefit from a principled RL scheme which learns an optimal policy, rather than fixing a heuristic search and combining that in an ad hoc way with a scoring rule.
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: This paper proposes an “incremental learning” algorithm for training a distribution (domain)-specific theorem prover for FO formulae without the need of a classical prover to generate training examples (intermediate clauses of a proof). Given a set of axioms and the negation of the (to be proven) conjecture, the prover iteratively 1. finds factors of clauses; and 2. applies resolution, until either an empty clause is reached (conjecture is proven) or no more new clauses can be generated (the conjecture is dis-proven). It is important for the prover to select clauses for factorization and/or resolution, that would lead to an empty clause faster. To that end, the AI-based theorem provers are augmented with a ML model (policy) that assists the prover by scoring the candidate clauses based on the probability of their applicability in building a proof. This in turn leads to construction of shorter proofs. The authors incorporate Hindsight Experience Replay (HER) in order to mitigate the lack of expert (machine and/or human generated) training sets. They show that HER indeed helps their incremental learning scheme to a point that the resulting ML-aided prover achieves comparable performance wrt. to the SOTA conventional prover E. Additionally the authors propose the use of spectral encoding to represent formulae instead of positional encoding of transformers.

The resulting architecture is tested on TPTP benchmark against E, along with an ablation to show the effectiveness of HER. The comparison with E is to measure both the number of proven conjectures within a cutoff as well as the proof quality (proof length).

main_review: Strength:
=======
- It is clear that this work took a substantial engineering effort to produce the experimental results. 
- The results are encouraging at least on the dataset that the authors tested their thesis on, which motivates further exploration on applying HER in ATP domain.
- The proposed use of spectral encoding in this context can be a useful contribution however no experimental results were reported to ablate that [see below].

Weakness:
=========
- The idea of using HER, although novel in the context of theorem proves, is a fairly immediate idea to apply in any search setting with sparse signal. 
- The use of spectral encoding is not properly justified and no ablation is performed to compare its superiority to more conventional means of formula representation, e.g., GNNs. Of course the choice of using spectral encoding over GNNs can be regarded as merely a design decision that seems to work in this context but since it was explicitly positioned as a contribution, in both introduction as well as the conclusion section, it merits more empirical elaboration. 
- Head-to-head comparison of IL against E in terms of wall-clock time could be misleading in that E is running on a single core per conjecture whereas IL is benefitting from 1000 actors running in parallel (presumably on 1k cores). This criticism does not lessen the validity of the contribution, as it can be argued that IL enables parallelism in provers, however including a comparison in terms of FLOPS or total CPU time (even in the appendix) can paint a clearer picture.
- The premise of the manuscript is that reliance of most ML-based methods on high-end provers limits their potential of surpassing human capabilities. The proposed technique might be a solution for that issue particularly in cases where generating training data is either expensive or impossible. In the particular case of TPTP however, we **are** capable of generating the training set. Indeed E manages to prove almost all of the instances at around the $10^4$ second mark. So why not train a model (with the same architecture) on this training set and compare it against IL+HER as a baseline? That would further strengthen the authors’ claims.

Questions:
========
- What is the justification for using 10 learners? Is it to spread the load of processing new samples across them or is it to introduce some diversity in the clause scoring?

Typos:
=====
- [Page 2 - subsection (2.1)] - 1st sentence: The word “simple” is repeated twice: “... we opted for a simple simple baseline...”
summary_of_the_review: The paper demonstrates an experimental signal in support of using HER for bootstrapping ML-based ATPs without expert labeled data on TPTP dataset. The reliance of ML-based provers on expert data is a serious issue and efforts to alleviate that reliance are definitely encouraged. However just showing the effectiveness of a well-known technique such as HER, which perhaps is one of the most immediate remedies that comes to mind for sparse reward tasks, seems like an incremental contribution, especially since some critical baselines are missing which could’ve made the claims stronger. Note that incremental learning has been used in other shapes or forms before in this context and thus the main value proposition of the manuscript is the addition of HER to that scheme.
review_title: null

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: The authors present an incremental learning (self-bootstrapped), Hindsight-Experience-Replay-based ATP learner, that learns to reordering candidates in a queue during a search process. The key insight is the data scarcity of ATP, wherein most searches do not lead to the goal, while the use of HER enables the use of failed searches as positive examples of alternate goal proofs
main_review: Strengths:
- The paper tackles an important problem in computer science: automated theorem proving, and more specifically seeks to resolve the data-scarcity issue that prevents large neural networks from being applied to this area
- the proposed approach extends hindsight experience replay to the domain of theorem proving. While not controlled in this experiment, the use of length-based bucketing and sampling ensure that the overwhelming amount of training data produced by the relabelling do not overwhelm the system, nor over-emphasize long (later) goal proofs.
- The proposed approach presents strong results that compete with E, and improve greatly over the two baselines: original system, and original system w/o HER.
- the spectral representation is novel. Its utility is harder to asses without ablations, but given a code release, building upon this work and performing further experiments could prove fruitful as well
- the use of a tabula rasa approach (purely incremental) is remarkable, and bodes well for adaptability to new domains where we lack starting theorems or data


Weaknesses
- For learnt automated theorem proving systems to become practically useful they would need to outperform or be complementary to existing systems. The proposed approach, while providing shorter proofs, fails to outperform E in terms of number of theorems proven. It may be valuable to include an experiment where the results from E can be combined with those from the proposed system to see if a union is actually better
- Experiments, while costly, are not repeated with confidence intervals and uncertainties -- thus, while the results are compelling, it is hard to rule out whether the specific ordering or randomness of the search process could impact the results in a strong way
- certain design decisions such as size of goal sampling are not ablated, and while the comparison between HER and not HER is excellent in Figure 2, such as comparison at a smaller scale would be welcome.
- Similarly the importance of "a separate network is trained per domain" is not measured, and this decision could be impactful when designing future experiments.

summary_of_the_review: The authors propose a very compelling solution to the data scarcity problem in automated theorem proving: relabelling failed searches by the sub-goals reached. Several important details for getting this to work are laid out, and the system is able to outperform baselines and compete with the existing E prover. The main shortcoming of the paper is a lack of repeat experiments, and missing desirable ablations for high-level design decisions.
review_title: null

Meta-review: Four reviewers acknowledged the author's response and did not change their largely negative scores.  The one enthusiastic reviewer did not respond to the more negative reviewers and has not worked in the theorem proving area. The main problem with the paper seems to be that the reviewers were not convinced by the empirical results.  They felt that results should have been presented on more widely used benchmark datasets.
Decision: Reject