Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: This paper explores the prospect of theorem proving in natural mathematical language using large language models (LLMs). Two representative tasks are considered: generating the next step in a partial proof, and generating full proofs given only the statement of a theorem. A dataset for these tasks (based on the existing *NaturalProofs* benchmark) is contributed.

Unfortunately, naive attempts to fine-tune GPT-3 on these tasks are shown to fail -- generated proofs often contain "hallucinated" references or logical errors. To address this, the work proposes "NaturalProver" to enforce the inclusion of certain background references in the output. Empirically, NaturalProver is shown to outperform GPT-3 on a number of metrics, including usefulness and correctness (as determined by human evaluators). 

strengths_and_weaknesses: **Originality**: Recent research explores theorem proving with inputs in the form of natural mathematical language, including the paper that proposed the NaturalProofs dataset [1]. As the authors note, these works often focus on auxiliary tasks, such as reference retrieval or translation to a formal mathematical representation. This work, on the other hand, considers the ambitious (but important) task of generating proofs and proof steps end-to-end, *from* natural math language *to* natural math language. This is a novel problem setting for theorem proving, to my knowledge. 

**Quality**: 

[Method]
The proposed method motivates the separation of the problem into two parts: reference retrieval (either by a neural network, or a human) followed by proof generation, conditioned upon these references. This is well-justified, especially given how GPT-3 is shown to fail on the end-to-end task. 

One assumption that I did not agree with was that the relevant references would always appear in the final proof. This assumption holds in the experiments when the ground-truth set of references can be provided, but is too strong for practical uses. For unclear reasons, the proposed approach is not evaluated with references retrieved by a neural network. (Please also see question 1 below). 

[Experiments]
The various approaches are evaluated by human annotators on criteria that would otherwise be difficult to objectively measure. Automated metrics are proposed which correlate well with these criteria (with one exception). **I have a couple of concerns, which if addressed well would raise my score.**

- GPT-3 with beam search decoding should be a baseline to fairly compare against NaturalProver++.
- Error bars are missing on the main results, making it difficult to evaluate their significance. 

**Clarity**:
The paper is very well-written and clear. One part I could not understand was the meaning of the "In-context" column in Table 4. Does "not in-context" mean no references were conditioned upon, similar to the vanilla GPT-3 baseline? 

**Significance**:
End-to-end theorem proving in natural mathematical language is a highly significant problem. This paper presents many interesting and useful insights on the problem, including why naive applications of LLMs fail and challenges for the future. One concern that may discourage future work is the lack of objective measures of success, but this work also takes steps to address this by proposing automated metrics of proof quality. One limitation to the main contributed approach (the one that uses constrained decoding) is that it was only shown to succeed when provided with ground-truth references. 

[1]: Welleck, Sean, et al. "NaturalProofs: Mathematical Theorem Proving in Natural Language." Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1). 2021. 
questions: 1. Would a version of constrained decoding but with soft (rather than hard) constraints be well-motivated? To me, it seems like the stepwise beam search can almost be applied as-is to this other setting (or if not, please correct me). 

2. Is there a way to change NaturalProver to provide a measure of confidence in the correctness of the proof? This is arguably a key advantage of formal proof environments that's lost when dealing with natural language proofs. 
limitations: Yes, the limitations and societal impacts were addressed.
review_title: null

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: This paper presents, NaturalProver, a machine learning-based proof solver that leverages the augments large language models (e.g., GPT-3) with symbolic information so they can be utilized for more than just natural language processing. The authors demonstrate NaturalProver’s advances in two fundamental dimensions: (1) full mathematical proof generation and (2) next-step proof generation. While the full proof generation component is limited to only a small number of steps for proof generation (e.g., 5-6 steps) the next-step proof assistance, in theory, could potentially be applied to any proof, irrespective of the total proof step count. The authors claim the next-step assistant is correct (and useful) up to 40% of the time.

The authors compare NaturalProver against a GPT-3 baseline.

strengths_and_weaknesses: Strengthens:

This paper is well-written and well-motivated.

The research topic is both timely (e.g., leveraging large language models for more than just natural language processing) and valuable (e.g., assisting formal solvers in ways that may improve some of the intractable computational bounds that have historically limited their capabilities to only relatively small proofs to do exponential state space explosion).

The two-pronged approach of both full proof and, perhaps more interestingly, next-step proof assistance, is compelling and has a reasonable amount of immediate value both in academia and industry (in my opinion).

Augmenting large language models to handle mathematical proof texts for the authors two-pronged approach is, to my knowledge, novel and clever. Additionally, the fact that the authors added LaTex support for mathematical proofs seems to imply it may have immediate value to other mathematicians in the research community, many of which write their mathematical proofs entirely in LaTex (myself included).

Weaknesses:

While GPT-3 is obviously one of the most well-known and effective LLMs to date, it would have been nice to see a comparison to other language models.

Because humans were used to evaluate the correctness of the system, it seems as though there may have been some bias in the results for numerous reasons. First, if the students were aware which proofs were generated by the research team’s system, they may have intentionally (or unintentionally) scored such proofs higher. Second, because the graders are human – and of varying degrees of mathematical competence – there is some chance the grading for some proofs were incorrect. Third, according to the authors, the students were first shown a “golden proof” which is used as a key for the synthesized proofs. However, there can exist many different correct proofs for mathematical problems. Because of this, it could be the case that some of the generated proofs are correct but were flagged is incorrect because they deviated from the “golden proof” steps or solution.

Minor nits:

Some of the written language in the paper seems a bit misplaced and perhaps in appropriate for a tier-1 research venue. This should hopefully be easy to correct, but I felt it worthwhile to mention. In the abstract there is mention that the LLMs generate “proofs riddled with hallucinations” – I have no idea what this means, but it seems like an inappropriate and unprofessional classification of results in a scientific research paper. In Section 5 under “human evaluation setup” the authors claim that “The human annotators were trained and compensated accordingly.” I have no idea what “compensated accordingly” means nor how to evaluate the accuracy of such a claim. Best to simply eliminate it entirely. I suspect it is fine to say that “students were trained on how to evaluate proof correctness.”

questions: Can the authors please try to explain the ways they prevented the weaknesses I have listed above (pasted below) in the evaluation method for the paper?

Because humans were used to evaluate the correctness of the system, it seems as though there may have been some bias in the results for numerous reasons. First, if the students were aware which proofs were generated by the research team’s system, they may have intentionally (or unintentionally) scored such proofs higher. Second, because the graders are human – and of varying degrees of mathematical competence – there is some chance the grading for some proofs were incorrect. Third, according to the authors, the students were first shown a “golden proof” which is used as a key for the synthesized proofs. However, there can exist many different correct proofs for mathematical problems. Because of this, it could be the case that some of the generated proofs are correct but were flagged is incorrect because they deviated from the “golden proof” steps or solution.

limitations: I'm not aware of any potential negative societal impact this research could incur.
review_title: null

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: The authors use the NaturalProofs-Gen dataset to fine-tune GPT3 using two new loss functions: proof generation using in-context references and reference reconstruction. Additionally, they perform constrained decoding by adding lexical constraints to encourage generations that contain the input references. They evaluate the system on multiple metrics like the usefulness and correctness of the proof steps. Lastly, they compare the model's errors by human evaluation on sampled subsets of the eval dataset.
strengths_and_weaknesses: Strengths:
* Overall, the approach is very nicely presented and easy to follow through
* The experiments and ablations are comprehensive and well presented
* Error analysis of the model is pretty detailed and well-categorized. This will help future research in this area to solve these challenges.

Weakness:
* Please consider adding some details about the specific GPT-3 model being used here (curie) in the appendix. At the very least, cite the related papers/websites when describing baselines around lines 190-199.
* It'd help to have some examples in the main text about the difference between using stepwise and stepwise++ for decoding. That would make these sections more accessible to new readers.
questions: * What is the order of the training data shown to GPT3 during fine-tuning - between in-context and reference reconstruction? Is it just randomly sampled or do you first show some reference reconstruction and then an in-context example that uses the previously shown references?
limitations: The authors clearly discuss the main limitations of the work, along with a comprehensive error analysis
review_title: null

Meta-review: metareview: The paper addresses an exciting problem statement--generating theorems directly in natural language--and shows how to adapt large language models to this task, both for autocompletion, proof reference generation, and wholecloth proof generation. While previous works have considered various auxiliary mathematical tasks posed in natural language, this work takes an important step by making progress toward doing proofs directly in natural language. This is a hard problem, and the authors support their work with experiments showcasing and analyzing different kinds of successes and failures. The reviews are unanimous in recommending acceptance.
confidence: Certain
Decision: Accept