Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 8: Strong Accept: Technically strong paper, with novel ideas, excellent impact on at least one area, or high-to-excellent impact on multiple areas, with excellent evaluation, resources, and reproducibility, and no unaddressed ethical considerations.
review_content: summary: Language models (LMs) have difficulty selecting the correct premise for a proof when the library of available premises is large. The authors use a data pre-processing step to train an LM to use an automatic theorem prover to improve premise selection. Combining the best of both worlds (LM theorem proving and automatic theorem proving), they achieve new state of the art performance on the PISA dataset and computationally efficient methods for matching best methods for MiniF2F.
strengths_and_weaknesses: Originality
This paper claims to be the first to use hammers for LM-based automatic theorem proving. A logical strategy to use, but nonetheless (as far as this reviewer is aware) novel.

Quality
The paper is thorough in its ablations, and presents a compelling case for their findings.

Clarity
The general writing style of this paper is straightforward and clear.
The paper could be more clear about the fact that their technique is primarily a data-preprocessing step that allows a language model to take advantage of an ATP, rather than a novel architecture.

Significance
Improved results on LM-based theorem proving is an exciting new development.
questions: Expert iteration (EI) is able to achieve similar performance to Thor, but this paper fails to give an explanation for why.
At one point in the paper (line 104), you are able to identify empirically that premise selection is a major bottleneck in LM-based theorem proving, and that Thor improves LMs by improving premise selection. Does EI also improve premise selection? If not, do you know why it improves LM performance? If EI improves LM performance in another way, is there an estimation for how much combined Thor and EI would improve performance?
limitations: The authors primarily give methodological limitations (rather than discussing negative societal impacts). This seems reasonable given the domain (automatic theorem proving) primarily impacts the mathematical research community and is less of a "real world" application.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: This paper presents Thor, a new learning-based theorem prover in the Isabelle interactive theorem prover. Thor combines the neural-based search heuristics with the Sledgehammer hammer in Isabelle. A language model is trained to generate the next proof steps, and Sledgehammer is one of the actions the model could output. This new prover achieves the new state-of-the-art result on the PISA dataset and performs comparatively with the best existing methods on the MiniF2F dataset.

=========================================
The authors' responses addressed my concerns about if it is necessary to learn to call the hammer. I increased my rating to weak accept. 
strengths_and_weaknesses: Strengths
1 It is a reasonable idea that we can improve the neural theorem provers with the hammers, considering that hammers would call the automated theorem provers that are designed and tuned carefully by the experts. 
2 Experiments show that Thor has significant advantages over the provers that are based on language models or hammers only.

Weakness
The approach to combining the hammers with the language models is fairly simple and straightforward. I doubt if it is necessary to have the language model learn to call Sledgehammer. Can we simply call Sledgehammer on each new proof state we want to expand during the proof search? What would be the performance of this simple baseline?
questions: How often are Sledgehammer called by the language models? How often do the Sledgehammer calls solve the goals?
limitations: I didn't find specific limitations of this paper. The proposed approach is general and can be simply combined with many neural theorem provers.
review_title: null

final_score: rating: 8: Strong Accept: Technically strong paper, with novel ideas, excellent impact on at least one area, or high-to-excellent impact on multiple areas, with excellent evaluation, resources, and reproducibility, and no unaddressed ethical considerations.
review_content: summary: The paper presents a method to integrate language models and hammers (Automated
Theorem Provers) for Interactive Theorem Proving. The authors train the language
model to recognize an opportunity to invoke a hammer by transforming the
training data: they check whether the hammer can be applied at each proof state,
and if it can, then they change the next proof step the model should output to
<hammer>. A language model trained on this data can thus output either the next
proof step, or <hammer> to indicate that a hammer should be invoked at that
proof step.


strengths_and_weaknesses: ## Strengths

The core idea of the method is very simple and elegant, could be applied widely,
and it outperforms the state-of-the-art.

The paper is very clearly written and explains the concepts from theorem proving
which are needed to understand the paper.

There are some directions of future work mentioned which could improve the
system further (e.g., expert iteration).

## Weaknesses

One weakness of the method could be that it requires the processing of the whole
training corpus and applying the hammers, which could be costly.


questions: Can you think of another domain where the idea of the paper could be applied?

limitations: The limitations are properly addressed.
review_title: null

Meta-review: metareview: The paper presents a method to integrate language models and hammers (Automated Theorem Provers) for Interactive Theorem Proving. The authors train the language model to recognize an opportunity to invoke a hammer by transforming the training data: they check whether the hammer can be applied at each proof state. 

The approach is novel, while being simple. The reviewers are generally happy with the writing of the work. There were some concerns (such as obvious baselines, pointed out byuriH) that seem to be mitigated. 
vtgR pointed out the slowness of preprocessing, which I think is an issue that should be explicitly acknowledged in the revision and addressed in future work. 

Given the overall positive feedback of the reviewers, I am recommending an "accept" for this work.
confidence: Certain
Decision: Accept