Venue: ICLR 2023 Conference

Reviews:

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: This paper considers the automatic generation of formal math statements from (less formal) mathematical statements in natural language. The statements are translated using Codex in a few-shot setting. The contributions are a postprocessing technique for formalized statements, prompt engineering to improve results, and some first attempts at formalizing proofs (not only theorem statements).

The paper also introduces two simple evaluation sets that address the problem that Codex might have seen the formalizations in their regular evaluation set during pretraining.
strength_and_weaknesses: I am not sure about the novelty and impact of the contributions:
- The postprocessing technique presented in this work addresses the problem that most of the available training data is for Lean3, but the approach here used Lean4 syntax. So the problem addressed here is not of general interest. The technique itself seems to be rather adhoc as well.
- The prompt engineering is similar to Jain et al. (2022), which the authors attribute correctly. It uses similar examples in the few-shot prompt to improve the results.
- The formalization of proofs seems novel to me (it goes significantly beyond Wu et al. (2022)), but is restricted to a very small dataset and only 2 of the 18 attempts were successful.
- Other possible contributions, like the evaluation sets, may be nice, but I'm not sure if they carry the paper.

Minor questions:
- "For proofs quantitative analysis is infeasible" Why?
- "We focused on theorem statements at the undergrad and more advanced level from various areas of mathematics. These statements tend to be more challenging for autoformalisation compared to mathematics competition problems studied in prior work (Wu et al., 2022) as they often assume more in terms of implicit context and draw from a much larger background (Wu et al., 2022)." I do not understand the justification "as they often assume more in terms of implicit context". 
clarity,_quality,_novelty_and_reproducibility: The clarity of the write-up is good, but could be improved. Some formulations and claims are a bit confusing (see summary).
summary_of_the_review: Interesting paper, but I am not sure if the contributions make the bar for ICLR.
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: This paper investigates the application of language models to interactive theorem proving by doing a qualitative case study on input-dependent prompt engineering. It shows that Codex is capable of producing partially correct formal proofs (in Lean 4) that can be turned into correct proofs with a moderate amount of modification (possibly done by a human user).
strength_and_weaknesses: Strength:

+ The qualitative study is interesting. There hasn't been much work in the field of ML for interactive theorem proving that includes a case study like the one in this paper.

Weakness:

- The contribution looks a bit pale. While observing the consequence of prompt engineering is interesting, prompt engineering itself and the particular methodology (i.e., input-dependent prompts by similarity) adopted in this paper are not new.

- The postprocessing of a completion produced by Codex is claimed as part of the contribution. However, if I understand it correctly, the elaborator is technically a procedure that tranlates expressions in Lean 3 to their counterparts in Lean 4 while making sure that the translated expressions type check.  I appreciate the engineering efforts here, but this part is more of a Lean-specific tweak required to make things work, and does not seem general enough to be a significant contribution.
clarity,_quality,_novelty_and_reproducibility: The paper is mostly clear and easy to follow if one knows Lean well. The formatting of tables can be made more professional, though. I believe the results are reproducible as the prompts are well-documented.

For novelty, see comments above.
summary_of_the_review: I am glad to see the nice qualitative study in this paper, but the overall contribution of this paper is rather insufficient. I suggest the authors try to add more content before the paper can be accepted.
review_title: null

final_score: rating: 1: strong reject
review_content: summary_of_the_paper: The paper shows empirically that Codex LLM is able to generate mathematical formalizations in a recently developed proof assistant Lean from natural language using prompting. The results include formalization of the relatively short theorem statements with a modest accuracy of 75%, and attempts to formalize short proofs. The overall results are mixed, with proofs requiring significant post-processing and manual fixing. 
strength_and_weaknesses: Strength:

+ The paper builds on a recent line of promising work on using LLMs for mathematical reasoning task - the focus of this paper on autoformalization. 

Weakness: 

- Why only limit the work to Lean theorem prover? If the Codex LLM is capable of autoformalization, it should be able to work with Coq, Isabelle and PVS - theorem provers which have been around for decades and are widely used in academia and industry. They also have fairly large libraries that can be used for evaluation. The current simple theorems are not representative of typical need for formalization. 

- Some of the prompt examples appear to be imprecise. For example, the natural language talks about vector space and the formalization uses division_ring and module. While one could argue that this is okay because the formal statements are correct but nonetheless the English statement was more specific and one would expect formalization to stay at the same level. Given this example, the reviewer fears that the paper is using a rather liberal notion of "correct" statement. This is particularly concerning given the very simple nature of this "theorem" statements, which aren't really the challenging aspects of formalization in proof assistants. 

- There appears to be significant shift in technique and results for theorems and proofs. Input-dependent prompting is not feasible for proofs. Elaboration is also not feasible. The results for proofs appear to be far worse and no correct proof were generated. The notion of identifying "easily repairable" proof is unclear and rather vague. Looking at figure 3, the error in constructed proof were significant. The expansion of absolute value would have created branches and led to severe difficulty in the proof. It is much better not to expand before applying triangle inequality.
clarity,_quality,_novelty_and_reproducibility: The paper does not have a novel contribution from the ML point of view. Its contribution in demonstrating utility of LLMs to proof assistants is marginal. Please see weaknesses for specific limitations. 
summary_of_the_review: In its current form, the draft appears to be a work in progress. The focus of the work is empirical demonstration of LLM for autoformalization and the draft falls far short of presenting enough empirical evidence. Expanding to other proof assistants (Coq, PVS etc) and using their large corpus of theorems and proofs to test whether Codex LLM can complete these would be useful. Also, given the lukewarm results, perhaps, prompt engineering can help improve results.
review_title: null

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: This paper applies a large language model, Codex to the autoformalisation of proof statements and of proofs. Two main contributions resulting are: (1) translating theorem statements of a form similar to docstrings of mathlib to theorems, and (2) translating (outlines of) NL proofs to Lean proofs.




strength_and_weaknesses: Strengths:
The paper is very interesting and has good novelty. 

Weaknesses:
The main drawback is that the article is very hard to read. The paper is written in a very loose style with almost no technical basis on which to understand what is going on. No model for a mathematical statement is provided, or of the technical basis for the rewriting. It is fully an application of existing tools to a rewriting process, with no details of what the technical novelty is. 
clarity,_quality,_novelty_and_reproducibility: The results are hard to understand. For this most part, the description is too high-level to comprehend. The descriptions of results are frustratingly vague: for example "Our chosen proofs are much longer than a typical theorem statement and we didn’t observe Codex outputting a completely correct proof. We instead relaxed the requirement of autoformalisation to produce a (faulty) proof that is easy to repair for humans, saving time and effort compared to formalising from scratch."
Here, there is no notion of key concepts, such as "much longer than a typical theorem" (what is the metric for length?); produce a (faulty) proof (what is faulty?); "easy to repair for humans" (what is easy/hard?).

As such, it is virtually impossible to measure progress in this paper.

Detailed issues:

prompts: there are many questions about this aspect, such as

--what is the formal basis?
--when are prompts too strong/weak? (Example 1 seemed like a very strong prompt, but there is no basis to estimate that)
--can one learn prompts? This seems like a natural sub-task of this work.

Section 3 is very hard to understand. What is the scope of allowable prompts? Figure 1 "Example of a prompt" seems far beyond the scope of the original text.

The data used is not the clearest. 
--The definition of data sets is far too abstract to understand what they contain.

--Data in tables 1 and 2 is far too abstract to understand what they contain.

The authors proposed a classification of proofs, but the main body did not contain this material, or a summary of results by proof type.
summary_of_the_review: This is a paper of high novely, yet the results are hard to understand. Further, the technica basis of the approach is lacking.
review_title: null

Meta-review: metareview:_summary,_strengths_and_weaknesses: The authors tackle an interesting subject, autoformalization of mathematical statements and proofs. The authors use Codex with an engineered prompt and perform output postprocessing. Though the reviewers found the work interesting, there was consensus that it does not meet the threshold for publication. In particular, the reviewers felt that the proof autoformalization dataset was too small, and that the postprocessing method was too narrow.
justification_for_why_not_higher_score: Quoting: Though the reviewers found the work interesting, there was consensus that it does not meet the threshold for publication. In particular, the reviewers felt that the proof autoformalization dataset was too small, and that the postprocessing method was too narrow.
Decision: Reject