Venue: NeurIPS 2022 Conference

Reviews:

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 studies the ability of LLMs to automatically translate mathematical statements (written in natural language) to formal statements in the language of a theorem prover (in this case, Isabelle/HOL). The authors also demonstrate the usefulness of such a translation system by incorporating it in an expert iteration procedure for training a neural theorem prover. The main contributions are as follows.

+ Few shot learning experiments demonstrating that LLMs (Codex, in particular) can autoformalize a large fraction (25.3%) of mathematics competition problems in Isabelle.
+ Case study characterizing incorrect formalizations among 150 problems formalized by Codex.
+ A neural theorem prover trained using expert iteration with the help of theorems autoformalized by Codex that achieves state-of-the-art proof rate.
strengths_and_weaknesses: ### Strengths

+ __The paper is well written and is easy to follow.__ Lots of examples are provided to illustrate the autoformalization capabilities of LLMs as well as the failure cases. In particular, I found the insights about teaching the concept of a linear function quite fascinating. 
+ __The problem studied is interesting and relevant.__ The ability to autoformalize statements is very helpful in reducing human effort required to formalize paper proofs in a proof assistant such as Isabelle.

### Weaknesses

- __Limited novelty in terms of methodology.__ Although the application here is different, the methods used for few shot learning using LLMs as well expert iteration for training neural theorem provers have been studied before. However, it is interesting to see that these ideas can be successfully applied in this context.
- __Experiments limited to mathematics contest problems.__ It was good to see this mentioned in the paper. It would be interesting to see how few shot learning helps with autoformalization of theorems about safety-critical software or complex theorems requiring understanding of many math concepts as, according to me, these appear to be the cases where autoformalization would be most valuable. Achieving autoformalization of a statement such as the one in Figure 3 would also require new methods for incorporating understanding of concepts such as products of spaces.
- __A few unexplained choices in the experiments.__ As far as I understand, a single prompt (with two fixed examples) was used for all the few shot experiments. Although it was random, it would have been interesting to see the results for a few choices of training examples. The proof rate of the neural theorem prover is measured using greedy decoding, however, the baseline FMSCL seems to achieve better pass@8 performance. It would be nice to see if pass@8 performance improves as well.
questions: * It is mentioned that FMSCL baseline [35] uses human written formal statements for expert iteration. Is it possible to generate formal statements at random or train a statement generator for this purpose? Since many of the autoformalized theorems may not actually correspond to the problem statement in the dataset, it might be worth comparing to randomly generated theorems for expert iteration.
* It is mentioned that the amount of Isabelle data used for training is a very small fraction and it is likely that some of the syntax is learned from the few-shot examples. In order to understand if that is the case, did you consider modifying the Isabelle syntax slightly, such as changing "shows" to "prove" etc., and repeating the few-shot experiments (at least some of them)?
limitations: Limitations w.r.t. advanced math statements and scalability are discussed in the paper.
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: This paper studies the problem of autoformalization that translates the statements of the math problems in natural language to formal language, and demonstrates how the autoformalized formal problem statements in Isabelle/HOL can be used to improve the performance of theorem provers. The formal statements are generated by LLMs (PaLM and Codex) in the manner of few-shot prompting. They are used in expert iteration to train the neural theorem prover. By manually inspecting the autoformalized statements of 150 problems in the MATH dataset, 38 of them are translated correctly by Codex. Experiments demonstrate that 3363 autoformalized statements of the problems in the Math dataset can effectively improve the pass rate of the prover on the MiniF2F benchmark after expert iteration (from 29.9% to 35.2% after 2 iterations). 
strengths_and_weaknesses: Strengths:
1 This paper studies the problem of autoformalization, an very important and promising topic in the domain of automated theorem proving.
2 It is a reasonable initial attempt to formalize the informal statements by few-shot prompting LLMs. The performance of this simple approach seems to be quite positive. By manually inspecting a few translated formal statements in the appendix, although most of the translations are not perfect, they capture the overall meanings of the informal statements with misaligned details. I think this also explains why these formalized statements are useful for training the provers.
3 Experiments on MiniF2F validate that the formalized problem statements could be useful training targets for advancing the neural theorem provers. 

Weakness:
The settings of BFS in the evaluation on MiniF2F are not mentioned. It is unclear if the comparison with the prior works is proper since different interactive theorem provers are used. 

questions: 1 Why do you choose Isabelle/HOL for autoformalization compared with HOL Light, Coq and Lean?
2 Could you provide more details about the settings of BFS in expert iteration and evaluation and the training hyperparameters of expert iteration?

limitations: The limitations of the proposed methods are mentioned in sections 6 and 7. I have no more concerns to discuss.
review_title: null

final_score: rating: 4: Borderline reject: Technically solid paper where reasons to reject, e.g., limited evaluation, outweigh reasons to accept, e.g., good evaluation. Please use sparingly.
review_content: summary: The paper evaluates the ability of pre-trained large language models such as Codex and PaLM on the problem of auto-formalizing natural language mathematics to formal specifications. The paper also shows how the model-generated formal specifications can be used to improve a neural theorem prover iteratively using expert iteration algorithms. 
strengths_and_weaknesses: STRENGTHS: 

The paper does a good job of motivating the autoformalization problem. The case studies in this paper allow us to get some preliminary insight into the challenges of this problem and the capabilities of existing LLMs. 

The idea of using autoformalized theorems to generate a dataset of natural theorems and using them with the expert iteration algorithm to improve a neural theorem prover is well executed and the results are impressive with almost a 5% performance improvement. 

WEAKNESSES:

The main disappointment with the paper is the lack of a rigorous evaluation. Most of the insights presented in this paper are gathered from just a few small case studies or a small-scale user study. The paper does not thoroughly explore various baselines/ablations. More details specifically, 
   * For table 1, why not also include PaLM Coder model to make it a fair comparison to Codex which is trained on more formal code? Also, it will be useful to look at the performance of some publicly available models such as GPT-J.  Table 1 should also report other metrics such as CodeBleu since Bleu is not always the best metric for code. 
   * The paper infers the need for few-shot prompting from just a single task case study, but there are no ablations with respect to the number of few shot examples for the results in table 1.
   * The neural theorem proving experiments also lack several baselines such as (i) using various different models for autoformalization (ii) temperature sampling/non-greedy decoding for autoformalization to collect more theorems (since we do not really need perfect autoformalization for these experiments) (iii) randomly sampled formal theorems from a DSL. 
   * Section 6 is very hand-wavy and again derives insights from a few case studies. Why not do Isabelle to Natural language on the miniF2F dataset and report Bleu scores for various models/ablations?  

Overall, the contribution of this paper is very thin --- the paper neither produces new techniques nor produces new datasets for training/evaluation nor does a thorough evaluation. So, in my opinion, this paper does not pass the bar for a NeurIPS paper. 

questions: The details about the neural theorem provers in section 5.2/5.3 are confusing.
- What is Sledgehammer and what is the purpose of invoking it?
- It is not clear what is the $M_0$ model here --- is it the LISA model or GPT-2 style decoder that is pretrained on the Pile.  
- Why the last fine-tuning step in lines 268-269 in Section 5.3?
limitations: Limitations are addressed.
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: In this work, the authors use large language models, specifically PaLM and Codex, to automatically formalize natural language text into Isabelle. In addition, the authors demonstrate that training a previous neural theorem prover on these automatically formalized theorems increases the success rate, achieving a new SoTA on miniF2F. 

strengths_and_weaknesses: Strengths:
- The paper provides a new and interesting application of LLM’s: automatically formalizing text into theorems. I find that this is an important direction of research: research in automatic formalization is scarce, and there is not much data for formalizations in Isabelle, Lean, Coq, etc. 
- Even just using Codex out of the box, the results are very impressive, showing that LLM’s are able to generalize beyond their training data to unseen tasks. This work will likely be a starting point and inspire future work and ideas in the area.
- The authors do a detailed human evaluation of failure cases, helping us understand when Codex can fail to generate correct programs. 
- The authors provide an analysis, in the appendix, on the effect of LLM scaling, which shows the benefits of scaling.

Weaknesses:
- Of the 150 problems, Codex is only able to translate 38 problems perfectly. Thinking of the use cases of LLM’s, it can be tedious and time consuming for users to verify if a generated output is correct (see https://tianyi-zhang.github.io/files/chi2022-lbw-copilot.pdf). As with systems such as Copilot, generating an almost-correct formalization of an input statement, for example one that compiles but is missing a minor detail and can be quite dangerous. Therefore, I believe it is important to include a way to verify (with reasonable accuracy) if a generated formalization indeed matches the specification. The authors also acknowledge, at the end of Section 6, that almost-perfect translations may occur. Relatedly, the use case of the system described in Section 5.1 relies on being able to identify the set of successful proofs S_i, which the paper does not include.
- I feel that a one-shot approach is not particularly fitting for a problem of this complexity. Rather, I feel that a more compositional approach of breaking down the formalization problem into smaller pieces is more appropriate here. For example, in Case Study 2, the model might first pick up on the “line up in rows of eight, there are seven left over” piece and formalize that, and then continue with the rest of the prompt.

questions: - You give a detailed analysis of the failure modes of your system. Given this, is it possible at all to predict (or assign a probability) when your formalization of a natural language prompt will be correct?
- In order to learn problems of a given domain, my understanding is that it needs to be trained on problems in that domain. In this sense, it's not clear to me how much overfitting is being done here. Could the authors elaborate on this?

limitations: Yes
review_title: null

Meta-review: metareview: The reviewers appreciated the importance of the problem studied. The reviewers had concerns regarding novelty of the proposed solution but were convinced by a detailed empirical evaluation. Overall, this is a clear accept. Congratulations to the authors; please take all the feedback into account while preparing the final version. 
confidence: Certain
Decision: Accept