Multi-language Diversity Benefits Autoformalization

Authors: albert q jiang
wenda  li
mateja  jamnik
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-14 20:21:18

Abstract: Autoformalization is the task of translating natural language materials into machine-verifiable formalisations. Progress in autoformalization research is hindered by the lack of a sizeable dataset consisting of informal-formal pairs expressing the same essence. Existing methods tend to circumvent this challenge by manually curating small corpora or using few-shot learning with large language models. But these methods suffer from data scarcity and formal language acquisition difficulty. In this work, we create mma, a large, flexible, multi-language, and multi-domain dataset of informal-formal pairs, by using a language model to translate in the reverse direction, that is, from formal mathematical statements into corresponding informal ones. Experiments show that language models fine-tuned on mma can produce up to $29-31$\% of statements acceptable with minimal corrections on the miniF2F and ProofNet benchmarks, up from $0$\% with the base model. We demonstrate that fine-tuning on multi-language formal data results in more capable autoformalization models even on single-language tasks.

Main paper: 
 introduction: 
 Formal mathematics refers to mathematical content that is represented in a formal language that can be mechanically checked by a computer. Practitioners express mathematics in formal languages integrated into proof assistants like HOL Light [Harrison, 1996] , Isabelle [Paulson, 1994] , Coq [Barras et al., 1999] , and Lean [de Moura et al., 2015] . Autoformalization is the task of translating natural language materials into verifiable formalisations. An ideal autoformalization engine can reduce the excessive cost for modern mathematical results to be verified [Ball, 2012, Scholze and Stix, 2018] . It opens up the vast amount of mathematics expressed in natural language to automated reasoning research fields that rely on formal languages, like automated theorem proving [Wu et al., 2022] .The hope of automatically translating informal mathematics into formally verifiable content is as old as formal mathematics [Whitehead and Russell, 1925-1927] . Only very recently, the breakthroughs in neural networks and Neural Machine Translation (NMT) enabled autoformalization to be learned [Wang et al., 2020 , Wu et al., 2022 , Jiang et al., 2023b] . NMT methods typically require a large parallel dataset, that is, a dataset consisting of pairs of sequences expressing the same meaning in both the source and the target language. The most challenging part of autoformalization research is constructing such a parallel dataset in a natural and a formal language, satisfying two conditions simultaneously: (1) the natural language component is close to how mathematics is actually written; and (2) the number of datapoints is large enough for the data-hungry machine learning methods. This is hard, because manually translating informal mathematical content into a formal language is only doable by highly trained experts in both mathematics and computer science, hence costly.In this work, we address the lack of a parallel dataset by leveraging a state-of-the-art Large Language Model (LLM), GPT-4 [OpenAI, 2023] : we used it to translate the two largest formal corpora, Archive of Formal Proofs in the language of Isabelle, and mathlib4 in the language of Lean4, into natural language. This process was enabled by the key observations that informalisation is much easier than formalisation, and a powerful LLM can produce diverse natural language outputs. As a result, we The lemma named "eint_minus_le" assumes that an assumes "(b::eint) < c" extended integer "b" is less than another extended shows "c -b > 0"integer "c". It then shows that the result of "c" subtracted by "b" is greater than zero.The set of all pairs of elements (x, y) such that x is "closed {(x,y) | x y. x ≥ (y::greater than or equal to y, is a closed set in the ('a::{linorder_topology}))}" context of a linearly ordered topology. created a parallel dataset of 332K informal-formal pairs, which we refer to as the MMA (Multi-language Mathematical Autoformalization) dataset. To the best of our knowledge, this is the first dataset of natural-formal language aligned data with more than one formal language. The only similar work was that of Azerbayev et al. [2023] , which has only one formal language (Lean3) and is 4x smaller than our dataset. Four examples of MMA are shown in Table 1 .We fine-tuned two open-source LLMs, LLaMA-33B [Touvron et al., 2023] and Mistral 7B [Jiang et al., 2023a] , on MMA to generate corresponding formal expressions given the informal ones. The trained model was then evaluated on two autoformalization benchmarks, miniF2F and ProofNet.Manual inspection of 50 problems for each model from each benchmark showed that after fine-tuning, the models could produce 29 -31% of formal statements on the benchmarks that require no or minimal correction, whereas the raw model produced 0%. We also fine-tuned two identical models on the Isabelle and the Lean4 components of MMA separately for the same number of steps. Their autoformalization performances are significantly weaker than the model trained on multi-language data, demonstrating that parallel data containing multiple formal languages is crucial for autoformalization training.• We informalise all formal statements from the Archive of Formal Proofs and mathlib4, creating MMA, a dataset of informal-formal pairs. This is the first natural-formal language aligned dataset containing multiple formal languages. • We train the first language models that can autoformalize to multiple languages in the zero-shot setting, and manually evaluate them on two autoformalization benchmarks. • We verify that: (1) language models trained on MMA acquire strong autoformalization abilities; and(2) language models trained on MMA have greater autoformalization performance than those trained on single-language partitions of it with the same computational budget. • We release the fine-tuned models for inference. We also release the MMA dataset for people to train their autoformalization models on, and to enrich MMA with more domains and languages.Improving autoformalization ability of models has the potential of translating copious digital repositories of informal human knowledge into formal languages of reasoning tools, and thus presents an opportunity to formally verify human informal arguments and solutions. High quality datasets such as MMA and autoformalization models like ours pave the way towards this goal1 . 
related work: 
 Autoformalization Datasets. Wang et al. [2018 Wang et al. [ , 2020] ] manually aligned a small parallel dataset and generated a larger parallel dataset with a rule-based informalisation tool [Bancerek, 2006] from Mizar to L A T E X. Manual alignment is almost as expensive as formalising mathematics anew. Moreover, unlike generative neural informalisation tools (e.g., GPT4), symbolic informalisation tools such as Naproche [Cramer et al., 2009] result in natural language content that lacks the inherent diversity and flexibility in expression: they are rigid and not natural-language-like. Finally, symbolic informalisation tools are hard to design and implement. They also differ a lot for different formal languages, hence the approach is not scalable for multiple formal languages. Wu et al. [2022] sought to eliminate altogether the need for a parallel dataset by leveraging the incontext learning ability of LLMs: they provided a couple of parallel examples, and asked the LLMs to find a formal counterpart for the informal problem (limited to high-school algebra or number theory). This approach is very effective when the test domain is limited. But when there are many test domains, finding the correct parallel examples becomes difficult: the LLM invents syntactically incorrect segments when it does not know the formal syntax for certain concepts [Wu et al., 2022, Case Study 3] . Liu et al. [2023] and Huang et al. [2024] both utilised autoformalization to create aligned informalformal pairs of data that are verified either manually or mechanically (for proofs), but did not perform large-scale synthesis of corresponding informal-formal theorem statements. Li et al. [2024] provides a more detailed survey on autoformalization datasets. In summary, there is no existing method, like the one we propose here, that is scalable both in terms of formal languages and mathematical domains.Back-translation. In natural language machine translation literature, the quality of translation heavily depends on the quality of the parallel data between two languages. However, for all but a few language pairs (e.g., en-fr), such parallel data is rare and hard to curate [Guzmán et al., 2019] .Back-translation is one of the most effective methods to improve translation quality [Sennrich et al., 2016 , Artetxe et al., 2018] in this setting, which is similar to ours. Back-translation uses an existing target-to-source model to turn ground-truth target sequences into noisy source sequences. Then, it bootstraps a source-to-target model to reconstruct the ground-truth target from the noisy source.Usually, the back-translation process is practised in both directions of translation, that is, from source to target and from target to source, and is iterated until convergence. When back-translation is practised in one direction only (because the model from target to source is called through an API and not trainable, for example), this process is referred to as "distilled back-translation". Azerbayev et al. [2023] used OpenAI's Codex [Chen et al., 2021] model to perform distilled back-translation to improve their own model's autoformalization capabilities. MMA differs from their dataset mainly in that MMA contains data from multiple formal languages and has four times as many datapoints.Language Models for Executable Programs and Reasoning. Since OpenAI's Codex [Chen et al., 2021] , multiple LLMs have been trained for code completion and infilling that stem from natural language [Yu et al., 2018 , Austin et al., 2021 , Fried et al., 2023] . Related is also the research on natural language mathematical and logical reasoning [Cobbe et al., 2021 , Lewkowycz et al., 2022 , Shi et al., 2022] that demonstrates that LLMs can comprehend mathematics and produce reasoning chains in natural language to a degree. Interestingly, distillation from larger, more capable models can effectively boost the reasoning ability of smaller models [Fu et al., 2023] . However, none of these works trained language models for the task of autoformalization, which is the gap that our work fills.Question: Does the paper discuss the limitations of the work performed by the authors? Answer: [Yes] Justification: In Section 6, we discussed aspects of the work that are subject to limitations. Guidelines:• The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper. • The authors are encouraged to create a separate "Limitations" section in their paper.• The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be. • The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated. • The authors should reflect on the factors that influence the performance of the approach.For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations. 
dataset: 
 As established above, there is no existing parallel corpus that satisfies the following crucial criteria for autoformalization model training:1. The informal data is diverse and flexible, similar to natural mathematical communication.2. The size is suitable for neural model training (≥ 100K datapoints).Informalisation. In this work, we use a powerful neural model (GPT-4) to generate informal data from existing formal libraries (informalisation) to create a high-quality parallel corpus. We argue, both analytically and empirically, that informalisation is an easier task than formalisation. Hence, our approach of leveraging the power and flexibility of language models for informalisation indeed produces a parallel corpus that satisfies both of the criteria above.Formal languages have two vital characteristics that distinguish them from natural languages: (1) precision and (2) syntactic rigidity. By precision we mean that every piece of information must be explicitly and precisely expressed and formalised; whereas in natural language, pieces of information are often left implicit or ambiguous. For example, one may write in natural language "Two roots of the equation x 2 -3x + 2 = 0, x 1 and x 2 , sum up to 3." meaning the two distinct roots have a sum of 3. Expressed formally, one must also write x 1 ̸ = x 2 to make the statement provable. Hence, the information in the formal statement is always sufficient for the informal statement to be inferred, while the reverse is not always true. By syntactic rigidity of formal languages we mean that formal grammars are usually much stricter than natural grammars, permitting less choice and diversity when expressing the essence of a piece of information. Wu et al. [2022] found that 76% of 38 high-school mathematical problems informalised by OpenAI's Codex model were "more-or-less correct". Azerbayev et al. [2023] did a more comprehensive study on 371 university-level problems and discovered that the same model has a 62.3% informalisation accuracy, while its formalisation accuracy is 13.4%. Empirically, informalisation has a much higher chance of being completely correct than formalisation.Curation Process. Lean4 and Isabelle are two of the most popular proof systems for formalising mathematics, with by far the largest formal proof repositories: Isabelle's Archive of Formal Proofs (AFP) and Lean4's mathlib4. They total over 5 million lines of code as of May 2024. In this paper, we consider the languages of these two systems due to their sizes and their popularity within the mathematical community, although the curation process can be easily extended to other proof languages as well. In neural translation systems, similar languages tend to have similar performances as source or target languages [Lample and Conneau, 2019, Roziere et al., 2020] . Given this fact and cost constraints (see Section 7 for the curation cost), we only use the languages of Lean4 and Isabelle as target languages in this paper, and expect conclusions reached with them to generalise to similar proof languages. Lean4 and Isabelle cover a wide range of topics, from advanced mathematics to software, hardware, and cryptography verification. We use Portal to Isabelle [Jiang et al., 2021] to extract 244K theorem statements, and the LeanDojo [Yang et al., 2023] library to extract 88K theorem statements. Isabelle AFP articles are under either a BSD-style license (a modified 3-clause BSD license) or the GNU LGPL license. Mathlib4 is under an Apache 2.0 license. The derived informal statements fall under licenses identical to their formal counterparts.We choose the most generally performant language model available to us, GPT-4 [OpenAI, 2023] , to informalise the statements, since its ability with code and natural language is superior to that of Codex [Chen et al., 2021] , which was used by previous works on autoformalization with LLMs [Wu et al., 2022 , Azerbayev et al., 2023] . Existing works on informalisation [Wu et al., 2022 , Azerbayev et al., 2023] typically use few-shot prompting to generate good informal statements. Our informalisation targets all available formalised content, going beyond high-school and undergraduate-level mathematical exercises. But targeting such a wide range of domains means that acquiring high-quality parallel pairs for every datapoint is challenging and expensive. Hence, instead of manually curating aligned pairs for every mathematical domain, we used an instruction prompting approach [Ouyang et al., 2022] , adopting the instruction prompt below for informalisations, with the text in curly brackets replaced by the individual datapoint content:Statement in natural language: {$natural_language_statement} Translate the statement in natural language to {Isabelle|Lean}:For all informalisations, we generated a maximum of 512 tokens from GPT-4 with greedy sampling (i.e., temperature = 0.0 in the OpenAI API). The responses received from this informalisation process often begin with "The lemma states that", which is mechanical and does not impact the meaning of the sentence. We remove such phrases and capitalise the remaining sentence.Statistics. In Table 2 (top) we give the relevant statistics of our MMA dataset, including the number of datapoints for each library and the statement lengths in characters for each language.Analysis. Since formal statements are precise and rooted in exact underlying definitions and complex contexts, the LLM informalisation process may sometimes fail to capture this precision. It might overlook or loosen crucial elements of the formal information, or introduce incorrect details (hallucination): this is a limitation of our work. To calibrate the extent of this limitation and further characterise the dataset, we conducted a qualitative study on 200 statement pairs from the MMA dataset, that we detail below.We randomly selected 100 Isabelle and 100 Lean4 datapoints from MMA, and manually examined each pair of informal-formal statements. We rated each pair along the following axes:• Correctness (whether the informalisation is completely correct)• Hallucination (whether the informalisation contains content not in the formal statement)• Misunderstanding concept (taking one concept in the formal statement for a different one)• Incorrectly translating assumption • Incorrectly translating conclusion • Incorrectly translating typeWe found that 67 of the 100 Lean statements are informalised correctly, and 81 of the 100 Isabelle statements are informalised correctly. The overall correctness rate is 74%. We estimate the total correctness rate of the MMA dataset to be similar. Wu et al. [2022] found that even when only 25.3% of the autoformalization statements are completely correct, downstream theorem proving applications were still able to benefit drastically from the parallel dataset. Hence, we expect our MMA dataset, which is 3x more accurate, to be of great usefulness for the community.In Table 2 (bottom) we present the types of errors out of the 200 randomly selected informalisations. Note that one informalisation can potentially have multiple errors. We notice that the most common mistake made by GPT-4 in informalising is "Misunderstanding concept", which happens in 14.5% (29/200) of the translations. This is either because there is an inherent ambiguity in the formal expression and the context is not enough to determine it, or that the language model is not able to determine the appropriate concept. Spotting these errors requires a significant amount of expertise in both mathematics and formal languages. Designing an automatic filter to remove incorrect informalisations seems to be highly non-trivial. We leave improving the informalising language model, such that it produces more accurate translations, for future work.Case Study. We study the informalisation examples from Table 1 : 3 of the 4 are correct, but when informalising the lemma "eint_minus_le", GPT-4 interprets the type "eint" to be extended integers, which are usually defined as normal integers extended with negative and positive infinities. This translation is sensible, but not entirely correct: "eint" is introduced in a theory of p-adic numbers to represent the codomain for the p-adic valuation -this means that it only extends integers with positive infinity, which serves as a maximal element in the order (i.e., the valuation of 0). Therefore, it is important to note that while we use a state-of-the-art LLM (GPT-4) to perform the informalisations, the resulting MMA dataset is not perfect: rather than the ground truth, informalisations in MMA should be treated as noisy approximations of it.Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) Justification: We do conform to the code of ethics in every respect.Guidelines:• The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.• If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics. • The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction). 
experiment: 
 To validate that MMA is a useful dataset for models to gain autoformalization abilities, we train two models from the LLaMA family and the Mistral family on a series of MMA data partitions. We manually evaluate the resulting models on two downstream benchmarks: miniF2F [Zheng et al., 2022] and ProofNet [Azerbayev et al., 2023] , consisting of high-school mathematical competition and undergraduate-level mathematical exercise problems respectively.Experimental Details. We take LLaMA [Touvron et al., 2023] 33B (under the LLaMA license) and Mistral [Jiang et al., 2023a ] 7B (under an Apache 2 license) as the base models, for they were the most performant open-weights model that we could fine-tune at the time of experimenting. We deliberately choose two models of different sizes and families to show that the improvement brought by MMA dataset is not sensitive to model size or family. For fine-tuning, we use the cross-entropy loss with the loss on the input masked out. We use the EasyLM [Geng, 2023] software framework on a TPUv4-64, with 32 megacores. We parallelise the model across 16 devices, and use a local batch size of 8 sequences, with each sequence having a maximum of 512 tokens. We use the AdamW optimiser [Loshchilov and Hutter, 2019] , perform 5000 linear warmup steps with a peak learning rate of 3 × 10 -5 , and then decay the learning rate with a cosine schedule for 35000 steps to 3 × 10 -6 . Preliminary experiments suggest that the final checkpoints of models are the strongest ones, so we use those to represent fine-tuning runs.Fine-tuning Data Regimes. We trained the models for the same number of training steps to generate formal statements given their informal counterparts, on different partitions of MMA: Isabelle + Lean4; Isabelle only; Lean4 only. For each datapoint, we used a prompt format identical to the one in Section 3 but with reversed input/output languages, and instructed the model to translate the statement in natural language to Isabelle or Lean accordingly. There are 88K informal-formal pairs of Lean4 data in one epoch of MMA, while for Isabelle there are 244K, 3 times as many. To reflect these proportions fairly, we fine-tuned the jointly trained model for 3.3 epochs, the Isabelle only model was fine-tuned for 4.4 epochs, and the Lean4 only model was fine-tuned for 13.2 epochs.It is possible that the ratio between data of the two formal languages influences the models' performances and a sweep of experiments over this ratio is potentially valuable. However, since fine-tuning the LLaMA model costs $2885 by TPU pricing, we are constrained by our budget and unable to perform this sweep. 
results: 
 In this section, we analyse the performance of the trained models and their formalisation of realistic mathematical problems from high-school competitions and undergraduate-level courses.Loss and Accuracy. In Figure 1 , we plot the loss and the token accuracy with teacher-forcing [Goyal et al., 2016] for the LLaMA model, on the Isabelle and the Lean4 validation sets for all 3 models. That is, we assess whether the ground truth token has the highest likelihood assuming every preceding token was predicted correctly. The figure illustrates that fine-tuning on MMA with one or both formal languages can drastically improve the language model's autoformalization capability, boosting their final validation token accuracies to above 90%. Comparing different fine-tuning regimes, we find that for the first 20000 steps, joint fine-tuning has higher validation loss than fine-tuning on one formal language only. Afterwards, the single-language fine-tuning validation loss starts to increase while the joint fine-tuning one starts to plateau. At 40000 steps, joint fine-tuning's validation loss is ∼0.15 lower on the Isabelle validation set and ∼0.1 lower on the Lean4 validation set, respectively. The joint fine-tuning's final token accuracy on Isabelle's validation set is 1% higher than single-language fine-tuning, and 0.7% lower on Lean4's validation set. This 0.7% accuracy drop is likely because the single-language fine-tuning has seen 4 times more Lean4 material than the joint fine-tuning. We emphasise that the jointly fine-tuned model has seen 3/4 Isabelle and 1/4 Lean4 tokens of the single-language models, and conclude that fine-tuning with multiple formal languages is much more data-efficient than with single-formal-language autoformalization data. We note that both loss and accuracy are proxy metrics of autoformalization capabilities, and in the rest of this section, we will examine autoformalization metrics that are better proxies, albeit more costly to evaluate. benchmarks: miniF2F [Zheng et al., 2022] and ProofNet [Azerbayev et al., 2023] . miniF2F is a suite of 488 high-school competition mathematical problems in multiple formal languages, and Jiang et al. [2023b] collected their ground truth informal counterparts. ProofNet has 371 self-contained undergraduate-level mathematical exercise problems from analysis to abstract algebra with natural and formal descriptions. Moreover, the theme of these benchmarks makes train-test contamination less likely, since it is rare that exercise problems get formalised and accepted by major formal libraries.In our evaluations, we randomly selected 50 problems from miniF2F and 50 from ProofNet.We tested if the generated formalisations are syntactically correct by the formal language (if they "compile"). The base models do not produce anything that compiles in Isabelle or Lean4 on the two benchmarks we used. The models fine-tuned on Isabelle generate 36% and 30% of Isabelle statements that compile on miniF2F and ProofNet respectively, while the jointly fine-tuned model generates 24% and 18% respectively. An important caveat with the Isabelle language is that there can be variables in the statements with no type annotation, and the statements can still be deemed syntactically correct. We observed that such statements generated by the model fine-tuned on Isabelle only are responsible for the high compilation rate, which effectively shows that while the compilation rate caps the proportion of completely correct formalisations, it does not fully capture how good/useful the formalisations are. 14% and 6% of the formalisations generated by the model fine-tuned on Lean4 compile on miniF2F and ProofNet respectively. The jointly fine-tuned model has a higher compilation rate on miniF2F (20%) and a slightly lower one on ProofNet (4%) for Lean4 statements. Next, we go into how much assistance the model generations can offer to the actual formalisation practice on miniF2F and ProofNet benchmarks.Formalisation Quality. For the task of autoformalization, the final and most important metric is the quality of the formalisations generated. For each model, we inspect the 100 formalisations for: Generally, the models fine-tuned on both languages produce outputs that require less effort to correct than models fine-tuned on one.EQUATION(1) whether they are completely correct formalisations; and (2) the amount of effort required to correct the formalisations. Two experts in Isabelle and Lean4 formal languages evaluated the formalisations, blind to which model generated them. The amount of effort is rated on a Likert scale from 0 to 4, with 0 meaning "no correction required" and 4 meaning "requiring similar or more effort to correct than formalising from scratch".Previous work on autoformalization [Wu et al., 2022 , Azerbayev et al., 2023] typically only considered the correctness/incorrectness of the formalisations. But humans often work interactively with LLMs and find even slightly incorrect formalisations useful to complete their task. This suggests that the evaluation metrics should be more nuanced [Collins et al., 2024] . Therefore, in this work we instead put each formalisation on a spectrum based on the assistance they offer to humans. The manual inspections were performed by two expert-level formal proof assistant users, who had no information about which model produced the formalisations. The evaluations are in the Supplementary Material.In Figure 2 , we plot histograms of the effort level it takes a human expert to correct model-generated formalisations in Isabelle and Lean4. We define formalisations that have correction effort levels 0 (none) or 1 (trivial) as "acceptable with minimal corrections". We can see that models not fine-tuned cannot autoformalize to Isabelle and Lean4 at all: the vast majority of their formalisations require , respectively. This suggests that there is considerable transfer between data in different formal languages, which benefits autoformalization, evidenced by the fact that the jointly fine-tuned models have superior autoformalization abilities in two formal languages with the same computational cost as the models fine-tuned on zero or one language. We further note that there is a considerable discrepancy between the direct examination of autoformalization (Figure 2 ) and the metrics of loss, accuracy, and syntactic correctness (Figure 1 ). This highlights the unreliability of the proxy metrics.Comparison with Few-Shot Prompting. Prior works on autoformalization have made heavy use of few-shot prompting. Here, we contrast the autoformalization quality of models with fewshot prompting and fine-tuning. It was found that the Codex model with few-shot prompting can correctly autoformalize 13-16% of ProofNet theorems [Azerbayev et al., 2023] and 25.3% of MATH [Hendrycks et al., 2021] theorems (which are much simpler than miniF2F and ProofNet).Our best autoformalization models with zero-shot fine-tuning can formalise 22% on miniF2F and 12% on ProofNet that require none or trivial corrections (see Figure 2 ), which are similar or better than previous models, despite being much smaller (Mistral 7B instead of Codex). We use two benchmarks purposefully built for autoformalization as per standard, instead of MATH. Therefore, we think fine-tuning is a promising approach to specialise and improve models for autoformalization.Statistical Significance. We now investigate whether the improvement in models' autoformalization ability with the MMA dataset is statistically significant. In Table 3 , we display the average effort level to correct outputs of models trained on each data mixture, and the 95% confidence interval estimated based on the 200 (100 from LLaMA and 100 from Mistral) evaluation samples. We see that for autoformalizing to Isabelle, fine-tuning the models on Isabelle and Lean4 gives outputs that are strictly better than just Isabelle, since the former has a confidence interval entirely to the left of the latter. Both are significantly better than the base models. For autoformalizing to Lean4, we see that fine-tuning with one or two languages on the MMA dataset are both significantly better than not fine-tuning. Fine-tuning on both languages results in a smaller average effort level to correct Lean4 autoformalization outputs.6 Discussion and Limitations Data Contamination. Since the base LLaMA model we chose was pre-trained partially on data from the internet and GitHub, naturally we need to ask the question: "Has the LLM seen the evaluation materials during its pre-training phase and therefore the result is invalidated?". To answer this, we closely inspected the generations by the raw model and examined if any of them were repeating the ground truth formalisation. Our investigation found that in none of the cases did the base model generate anything resembling the ground truth: most of its generations when instructed to translate a statement from natural language to Isabelle or Lean4 is either L A T E X or Python code. Interestingly, one of its generations is a L A T E X code listing (the complete generation is in Appendix B) that looks like Isabelle code, but is ultimately not even syntactically correct. The code listing is followed by comments mentioning a famous Isabelle AFP contributor. We hypothesise that this is caused by the model having noisily memorised arXiv papers containing Isabelle content. Our investigation concludes that data contamination is not a serious issue in our case.Evaluation. Evaluating autoformalization is difficult: language models are very capable of generating formal statements that are syntactically correct, but do not express the meaning of the informal statements, as we have seen in Section 5. Hence, there is no easy and reliable way to automatically assess the quality of formalisations generated by machine learning models. Two fairly reliable approaches to indirectly assess the quality of the generated formal statements exist: Wu et al. [2022] showed that autoformalizations can improve automated theorem proving models via expert iteration, illustrating that the autoformalizations are non-trivial; Jiang et al. [2022] proposed to consider statements that can be proven and serve as lemmas for other theorems as good formal statements. However, these approaches require the use of automated theorem proving, which is expensive to set up. In our work, we manually evaluated formalisations on 100 randomly sampled formalisations for each of the 12 model-inference language pairs, and analysed the amount of effort needed to correct the outputs in Section 5. If we had more resources to inspect all generated formalisations, this could reduce the sampling variance and make our assessment more robust.Continuously Pretrained Models for Mathematics. There are models that are continuously pretrained on mathematical materials from base models such as Llemma [Azerbayev et al., 2024] and DeepSeekMath [Shao et al., 2024] . They demonstrate significant improvements on informal mathematical problem solving over the base models and can serve as better starting points for finetuning models. We did not experiment with them since they were published after our experiments. 
conclusion: 
 In this paper, we constructed MMA, a large, flexible, multi-language, and multi-domain dataset of informal-formal pairs. We demonstrated that language models can acquire superior autoformalization abilities by training on MMA, and its use of multiple languages improves sample efficiency and final performance for autoformalization. We are convinced that MMA can very effectively benefit the theorem proving and AI for maths community by two facts: (1) the analytical fact that MMA's estimated correctness rate is 3 times higher than the parallel autoformalization data used by Wu et al.[2022] which was very helpful; and (2) the empirical fact that fine-tuning language models on MMA make them significantly better autoformalization models. We release MMA for public exploration.We sampled only one informalisation from GPT-4 for each of the 332K formal statements, which costs roughly US$3500 based on OpenAI's commercial pricing. If we had more resources, we would further boost the diversity of the informal statements by sampling more than one informal statement for each formal statement, and could extend to more formal libraries such as Isabelle's standard library, and more languages such as HOL Light and Coq.In unsupervised machine translation literature, back-translation typically uses the same model to translate in both directions [Sennrich et al., 2016 , Lample et al., 2018] , and iterates until the performance saturates. We were unable to do this, because GPT-4, the model we used for informalisation due to its strong performance, is proprietary. The possibility of examining the full potential for iterated back-translation hinges on the existence of an open-source language model that is generally performant in both natural and formal languages. Since state-of-the-art open models appear at great frequency, we leave the work of unifying and iterating language models for informalisation and autoformalization for the future with great hope. 
broader impacts: 
 Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?Answer: [NA] Justification: This work advances formal mathematics, which has no societal impacts as far as we can see.Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.• The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?Answer: [NA] Justification: The paper poses no such risks.Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort.12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?Answer: [Yes] Justification: We clearly indicate the licenses for the datasets in Section 3 and the models in Section 4.Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided. • If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode.com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset. • For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.• If this information is not available online, the authors are encouraged to reach out to the asset's creators. 13. New Assets Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets? Answer: [NA] Justification: The new assets are derivatives of the LLaMA and Mistral models, whose original documentations apply. Guidelines:• The answer NA means that the paper does not release new assets.• Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc. • The paper should discuss whether and how consent was obtained from people whose asset is used. • We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution. • For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review. 
 
 Appendix: In this section, we present some additional autoformalization examples.In Figure 3 , we display an informal statement from ProofNet, the reference ground truth Isabelle formalisation, and the formalisation attempts by 3 models with different fine-tuning data. Here we analyse their autoformalization behaviours. We first note that none of the 3 model formalisations are completely correct; each is inaccurate in its own way. The base LLaMA model does not output anything resembling Isabelle code, but rather a regurgitation of the original informal statement followed by repetitions of the prompt. The model fine-tuned on Isabelle only and the model jointly fine-tuned on Isabelle and Lean4 both correctly translate the main assertion of the problem, but are wrong with the assumptions. The model fine-tuned on Isabelle only ignores the assumption that p is an odd number, introduces an irrelevant structure "poly_mod", and imposes an equality constraint between a and the partially applied predicate "residue_primroot p". The imposed equality causes a compiling error. The model jointly fine-tuned on Isabelle and Lean4 data does not state the correct assumptions that p is an odd prime, but gives the lemma a name "let_p_odd_prime" instead. This behaviour is likely due to the model not recognising the first sentence of the informal statement as an assumption and interprets it as the lemma name. In this example, both fine-tuned models give significantly better formalisations than the base model, while the model fine-tuned on multi-language formal data makes fewer mistakes.Let p be an odd prime. Show that a is a primitive root modulo p iff a (p-1)/q ̸ ≡ 1(p) for all prime divisors q of p -1.Ground truth in Isabelle: lemma exercise_4_8: assumes "prime p" "odd p" shows "residue_primroot p a ←→ (∀ q ∈ prime_factors (p -1).[a ^((p -1) div q) ̸ = 1] (mod p))"Base LLaMA model: Let p be an odd prime. Show that a is a primitive root modulo p iff a (p-1)/q ̸ ≡ 1(p) for all prime divisors q of p -1.The statement in natural language is a theorem. The statement in Isabelle is a theorem.The statement in Isabelle is a definition. The statement in natural language is a lemma.Fine-tuned on Isabelle only: lemma (in poly_mod) residue_primroot_iff: assumes "prime p" defines "a ≡ residue_primroot p" shows "residue_primroot p a ←→ (∀ q ∈ prime_factors (p -1).[a ^((p -1) div q) ̸ = 1] (mod p))"Fine-tuned on Isabelle + Lean4: lemma let_p_odd_prime:shows "residue_primroot p a ←→ (∀ q ∈ prime_factors (p -1).[a ^((p -1) div q) ̸ = 1] (mod p))" In Figure 4 , the model attempts to autoformalize the statement that the remainder of 2003 divided by 11 is 1. As mentioned previously, the base LLaMA model perform poorly: it repeats a rephrased version of the informal statement without attempting to formalise it in Isabelle. The model jointly fine-tuned on Isabelle and Lean4 finishes the task nicely. Despite not being identical to the ground truth (e.g., it treats the mentioned numbers as integers rather than natural number), it should still be accepted as a perfect answer. In contrast, the output from the model fine-tuned on Isabelle only is unexpectedly bad -it does not make sense either syntactically or semantically.What is the remainder when 2003 is divided by 11? Show that it is 1.Ground truth in Isabelle: Prove that there is no rational number whose square is 12.Ground truth in Isabelle:theorem exercise_1_2: assumes "∃ x ∈ Q. x^2 = 12" shows FalseBase LLaMA model:Theorem square_of_12_is_not_rational: "(1/x)^2 = 12" "x = 12" "x = 1/12" "x = 1/12" by (simp add: square_of_one_divide_by_square_of_one) "x = 12" by (simp add: square_of_one_divide_by_square_of_one) "x = 12" by (simp add: square_of_one_divide_by_square_of_one) "x = 12" by (simp add: square_of_one_divide_by_square_of_one) "x = 12" by (simp add: square_of_one_divide_by_square_of_one) "x = 12" by (simp add: square_of_one_divide_by_square_of_one) "x = 12" by (simp add: square_of_one_divide_by_square_of"Fine-tuned on Isabelle only: In Figure 6 , the model is prompted to formally state that 10a ≤ 28a 2 + 1 for any real number a.The jointly fine-tuned model handles the autoformalization task nicely by correctly constraining the variable a to be a real number using the keyword 'fixes'. The base LLaMA model rephrases the informal statement and keeps repeating the prompts. The model fine-tuned on Isabelle only attempts to formalise this problem using limits in mathematical analysis, which is beyond our comprehension.For any real number a, show that 10a ≤ 28a 2 + 1.theorem algebra_binomnegdiscrineq_10alt28asqp1: fixes a :: real shows "10 * a ≤ 28 * a^2 + 1"Base LLaMA model: For all a: real, 10 * a <= 28 * a 2 + 1 Translate the statement in natural language to Isabelle: For all a : real, 10 * a <= 28 * a 2 + 1 Translate the statement in natural language to Isabelle: For all a : real, 10 * a <= 28 * a 2 + 1.Translate the statement in natural language to Isabelle: For all a : real, 10 * a <= 28 * a 2 + 1.Translate the statement in natural language to Isabelle: For all a: real Fine-tuned on Isabelle only:lemma fixes a :: real assumes "a ≥ 1"" shows "(λ n. a powr n / (n * (1 + a powr (2 * n)))) \<longlonglongrightarrow> 1 / (1 + a powr (2 * n))" "(λ n. (1 + a powr (2 * n)) / n) \<longlonglongrightarrow> 1 / (1 + a powr (2 * n))"Fine-tuned on Isabelle + Lean4: Figure 7 presents a non-trivial problem in point set topology. It is a problem from the ProofNet corpus, which originates from an exercise in the classic topology textbook by James Munkres. The jointly fine-tuned model correctly encodes S 1 using the term 'sphere 0 1' in Isabelle and manages to identify the predicate continuous_map to encode the continuity of a function from one set to another. Nevertheless, it makes a couple of common mistakes, such as neglecting to convert the open set 'sphere 0 1' to a topology and not recognising the inherent Euclidean topology on R. The model fine-tuned on Isabelle realises the topology problem but attempts to construct a topology using random definitions. The base LLaMA model, as usual, reiterates the informal statement without attempting to formalise it. Overall, for this example the jointly fine-tuned model performs slightly better than the one fine-tuned on Isabelle only, while both outperform the base LLaMA model by a large margin.Let f : S 1 → R be a continuous map. Show there exists a point x of S 1 such thatf (x) = f (-x).Ground truth in Isabelle:theorem exercise_24_2: fixes f::"'a::metric_space ⇒ real" assumes "continuous_map (top_of_set (sphere 0 1)) euclidean f" shows "∃ x ∈ sphere 0 1. f x = f (-x)"Base LLaMA model:Let f : S 1 → R be a continuous map. Show there exists a point x of S 1 such that f (x) = f (-x).Translate the statement in Isabelle to a mathematical statement: Let f : S 1 → R be a continuous map. Show there exists a point x of S 1 such that f (x) = f (-x).Translate the statement in Isabelle to a mathematical statement in the language of set theory: Let f : S 1 → R be a continuous map. Show there exists a point x of S 1 such that f (x) = f (-x). Translate the statement in the language of set theory to a mathematical statement in the language of set theory with the axiom of choice: Let f : S 1 → R be a continuous map. Show there exists a point x of S 1 such that f (x) = f (-x). Translate the statement in the language of set theory with Fine-tuned on Isabelle only: lemma continuous_map_lemma2: fixes f :: ""'a::topological_space ⇒ 'b::t2_space"" assumes "continuous_map S (subtopology (powertop_real UNIV) (standard_simplex p)) f"" shows "∃ x. x ∈ S ∧ f x = f (-x)"Fine-tuned on Isabelle + Lean4: lemma continuous_map_sphere_exists: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "continuous_map (sphere 0 1) S f" shows "∃ x. x ∈ S ∧ f x = f(-x)"" Still, the model performs slightly better than the one fine-tuned on Isabelle only, which brings unrelated concepts like holomorphic functions from complex analysis.Let n be a positive integer, and letf n (z) = n + (n -1)z+ (n -2)z 2 + • • • + z n-1 . Prove that f n has no roots in the closed unit disk {z ∈ C : |z| ≤ 1}.theorem exercise_2018_b2: fixes n::nat and f::"nat ⇒ complex ⇒ complex" assumes "n > 0" "f n z = ( i < n. (n-i)*z^i)" shows "∀ i > 0. ∀ z. cmod z ≤ 1 -→ f i z ̸ = 0"Base LLaMA model: Let n be a positive integer, and letf n (z) = n + (n -1)z+ (n -2)z 2 + • • • + z n-1 . Prove that f n has no roots in the closed unit disk {z ∈ C : |z| ≤ 1}.Translate the statement in Isabelle to formal language: Let n be a positive integer, and letf n (z) = n + (n -1)z+ (n -2)z 2 + • • • + z n-1 . Prove that f n has no roots in the closed unit disk {z ∈ C : |z| ≤ 1}.Translate the statement in formal language to formal language with quantifiers: Let n be a positive integer, and letf n (z) = n + (n -1)z+ (n -2)z 2 + • • • + z n-1 . Prove that for all z ∈ C, if |z| ≤ 1, then f n (z)Fine-tuned on Isabelle only: lemma no_proots_in_unit_disc: fixes f::"complex ⇒ complex" and z::complex defines "n ≡ zorder f z" and "fn ≡ f n" assumes "open s" "z ∈ s" "a ∈ s" "f a ̸ = 0" defines "S ≡ {z. z ∈ s ∧ f z ̸ = 0}" defines "I ≡ (λ n. (fn) / (f n))"shows "(∀ n.(f n) holomorphic_on S) ∧ (∀ n z. z ∈ s ∧ f z ̸ = 0 -→ (f n) z ∈ S) ∧ (∀ n z. z ∈ s ∧ f z ̸ = 0 -→ (f n) z ̸ = a) ∧ (∀ n z. z ∈ s"Fine-tuned on Isabelle + Lean4: NA answer to this question will not be perceived well by the reviewers. • The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. • It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper.38th Conference on Neural Information Processing Systems (NeurIPS 2024).The MMA dataset and the fine-tuned models are available from the official repository: MMA. 


Decision: This paper introduces MMA, a large-scale multi-language dataset for autoformalization, created using a back-translation approach with GPT-4. The dataset's quality and diversity enable improved performance in autoformalization tasks, particularly when training on multiple formal languages. The paper's strengths lie in its well-written presentation, valuable dataset contribution, and insightful experiments. However, there's room for improvement as suggested from reviewers (e.g., addressing the noise introduced by zero-shot prompting.) Overall, the paper provides a significant resource and insights for advancing the field of autoformalization.

Reviews: review: paper_summary: paper_summary: This paper introduces MMA, a large-scale dataset consisting of informal-formal pairs of mathematical statements (i.e., parallel autoformalization data) in two types of formal languages, Isabelle and Lean4. The dataset encompasses statements from multiple domains and exhibits high quality. It was constructed using a back-translation method, converting from a formal language to an informal language, to improve data quality.
strength_weakness: strength_weakness: The experiments and the corresponding analysis are not robust enough.
1.	The metrics “loss” and “token accuracy” used on the validation set are limited, as there could be multiple correct autoformalization results beyond the given reference. One piece of evidence for the limitation of these metrics is that in Figure 1, the model fine-tuned on Lean4 alone shows a higher loss, suggesting worse performance, yet its token accuracy is actually better.
2.	In line 242-243, the paper claims, “This 0.7% accuracy drop is likely because the single-language fine-tuning has seen 4 times more Lean4 material than the joint fine-tuning”. However, another potential explanation could be that the joint fine-tuning training data contains more Isabelle than Lean4, potentially leading to a deterioration in Lean4 performance. The authors should investigate this possibility.
questions: questions: 1.	Is it fair to control the number of training steps across different set of training data? Why not control for the size of the training dataset and the number of training epochs instead?
2.	In line 262-265, "it does not fully capture how good/useful the formalisations are", why are the formalizations considered not good/useful as long as they lack type annotations? What proportion of the statements are of this type? If these are removed, what is the proportion of syntactically correct statements generated by models that have been fine-tuned singly or jointly?
limitations: limitations: The metrics “loss” and “token accuracy” on the validation set are limited, as stated above. This could affect the correctness of all analyses and the corresponding conclusions.
paper_summary: paper_summary: The authors use backtranslation to create a large (~332k samples) dataset of formal-informal statement pairs in the Lean4 and Isabelle formal proving languages: they take formal samples from a Lean4 and an Isabelle proof library, and ask GPT4 to restate them informally. They use this dataset to finetune two open source LLMs (Llama 33B and Mistral 7B) on the task of autoformalisation: converting informal statements to formal ones, in Lean4 and in Isabelle, comparing the result of this finetuning to the initial state of the LLMs and ablating on training with both languages as opposed to just the target languages.

The authors invest time and manually evaluate the performance of their trained models on 50 samples from each of two small benchmarks, proofnet and miniF2F (total 100 per evaluated model), to draw their conclusions.

For both languages, the fine tuned models outperform the base models on autoformalisation. For Isabelle, they find that training with the combined dataset (containing both Lean4 and Isabelle samples) is better than the relevant monolingual, for Lean4 the difference is slightly less clear. 

I note the mixed dataset contains mostly Isabelle statements: 244k/332k, and personally wonder if this relates to the found results - the influence of this ratio is not explored. This makes sense however: evaluating the correctness of autoformalised statements is non trivial, and easily automated metrics such as training loss, or per-token accuracy in a teacher forcing setting, are not immediately indicative of correct formalisation.
strength_weakness: strength_weakness: 1. Dataset is automatically generated by an LLM, and no filters were applied or considered. Naturally, some of the LLM's informalisations will be incorrect (manually inspecting 200 samples from the dataset, the authors find 52 with errors (table 2)). I wonder if further manual inspection would have raised any obvious failure cases that could be automatically flagged and filtered from the full dataset. 
2. I would have liked an investigation of impact of the [ratio of different languages in the training set] on the [performance of the fine tuned model]. Specifically because the models fine tuned on the full dataset did better on Isabelle than when trained only on Isabelle, whereas for Lean this wasnt as clear, despite Isabelle having the larger dataset, I wonder if the issue for Lean was that it was 'drowned out' by the amount of Isabelle samples in the data.
3. I don't know how open NeurIPS specifically is to dataset rather than method contributions, and this seems mostly a dataset contribution. I do think it is a valuable one though.
4. The dataset is based on GPT4 backtranslations, and the evaluations are of open source models before and after fine tuning with these backtranslations. I wonder, is this actually just a distillation of GPT4 capacities into open models, or does this dataset actually advance autoformalisation? A comparison with GPT4 autoformalisation ability (eg just on proofnet and minif2f) would help settle this question.
5. Majority of improvement in token accuracy and loss of the models happens in first few k steps (fig 1). Would have been nice to do an evaluation of the models (ie on the benchmarks) at that stage, to see if remainder of steps is necessary
6. *Important!* Missing baselines/discussion: the question of whether fine tuning (as done in this work) is at all the correct approach for autoformalisation is not raised. Given that there is existing work on using few-shot learning for autoformalisation, the question is relevant and cannot be ignored. The few shot alternative should be properly discussed. At minimum, the existing reported results (Azerbayev at al, Wu et al) should be recalled and compared to in this paper (to the extent the comparison is possible, see next point). (Ideally, the models would have been evaluated in a few shot setting on the same benchmark-subset as used in the paper, though I recognise this is a labour intensive request.)
7. *Important!* Nonstandard benchmarking: The models in this paper are evaluated on the (mixed) subsets of two different benchmarks, proofnet and minif2f. This makes it hard to compare the results to those reported in other autoformalisation works, which use the benchmarks in whole and separately from each other. I hope the authors can at least update the report to list the disaggregated results on the two benchmarks. Independently, please list exactly which samples were taken from the two datasets for the combined one, to allow accurate comparisons to these results in the future. The use of only a small subset of the main benchmarks (50 samples each) also weakens the significance of the results.
questions: questions: Clarifications, nits, comments:
1. Are the MMA statements disjoint from those of ProofNet and MiniF2F?
2. line 62 "strong" autoformalisation: subjective
3. section 2 "rule based informalisation" vs "symbolic informalisation" it is not clear to me if these are the same or different. If the same, choose one term, if different, clarify difference.
4. "Manual alignment" also unclear
5. line 86: appreciate the reference to specific case study, but would appreciate some lines on what "syntactically incorrect segments" are directly in this paper for completeness.
6. line 93: some lines on how there is a setting where there is a target-to-source model, but not the other way around, would be appreciated. Speaking of which: given all this dataset is based on GPT4 backtranslations: how does GPT4 perform at autoformalisation?
7. line 95: "usually, the back translation process is..." - would appreciate a/some sources on this!
8. line 99 what language is Azerbayev et al 2023 on?
9. line 116 "high quality": subjective, not clear by what measure this is said
10. line 119 "satisfies both of the criteria": did you check for diversity of the informal statements? how did you measure it?
11. line 142 do you mean "generation" (not curation) cost?
12. nice to have: line 148 does gpt4 add further licenses? what is the license of the combined dataset (is it just "both", or do they merge)?
13. table 2: what's that massive isabelle statement (24331 characters)? is it an anomaly? what happened there?
14. line 178: what is misunderstanding a concept - can you give a concrete example? similarly line 181 with "type".
15. line 191 vs lines 168 and 126: are formal expressions complete and precise or inherently ambiguous? soften/clarify statements to resolve this apparent contradiction
16. line 205: "train" -> "finetune"
17. line 208: what languages are miniF2F and ProofNet in? comes up again in line 250
18. nice to have: would be nice to see metrics on lean when fine tuned on just isabelle, and vice versa. correctness evaluation probably too labour intensive, but loss/token-accuracy curves maybe. but maybe they'll just be zero. i recognise this data may not be obtainable now that models have already been trained (don't know how hard/expensive it is to train the models)
19. line 227: number of epochs doesn't seem to quite line up with equalising number of samples seen/steps made, maybe because you are giving rounded numbers? doesn't particularly matter but strange
20. line 235: figure shows loss and per-token accuracy, which are not necessarily indicative of autoformalization capability, rephrase.
21. fig 1: not so clear what the per token accuracy of the models are in first 2k train steps, would appreciate knowing - maybe can have a line on this in body of paper if dont want to distort images
22. line 243: it has seen lean material 4x more, but it has not seen 4x more lean material (i.e. it is seeing same material)
23. line 242-243: unconvincing/invalid interpretation: if this were the explanation, we would see a similar (but weaker) drop for Isabelle, but instead, Isabelle sees a gain.
24. lines 245-246: lean4 results dont support this
25. line 258: "... generate 36% and 30% of Isabelle statements that compile..." unclear, rephrase
26. lines 256-269: seems compilation rate is discussed for only one model (Llama?). Would prefer to have information on both models. If not, at least clarify which model is being discussed here.
26. lines 262-265: need elaboration - I imagine you have support for this claim, but need to see it. Are you saying that a lot of the generated Isabelle statements type checked, but were incorrect? Give numbers
27. lines 265-267: more mixed results regarding whether it is better to train with mixed or monolingual data. I wish the paper was more up front on this inconclusivity, it appears to have a slight "joint-is-better" narrative, that is not critical to its contribution. 
28. line 296: "mdoel"
29. line 308 again insufficiently up front about inconclusive results regarding mono/multi lingual data for lean4 (choosing to focus only on the comparison to not fine tuning at all)
30. line 309-310 don't particularly like this statement when the confidence intervals overlap (table 3), can be up front
31. need more of a gap under table 3
32. line 320: did fine tuning surface any memorised info? would have been interesting to check
33. line 340: call to "sample efficiency" - define and clarify how this relates to findings?
34. last 2 paragraphs of conclusion belong more in "limitations" in my opinion

35. what are the (math) domains of the data used to create MMA (within AFP and mathlib4), and the domains of miniF2F and proofnet, and how do they relate to each other? I.e., are miniF2F and proofnet in- or out-of- distribution for the MMA training set, with respect to type of math considered? What about specifically the subsets of miniF2F and proofnet that were used for the evaluations in this work?
limitations: limitations: yes
paper_summary: paper_summary: The paper presents a dataset MMA and a model trained on the same. The dataset comprises informal-formal pairs of theorem which are generated using LLM. The experiment shows decent results on the autoformalization tasks of miniF2F and ProofNet benchmarks. The authors also claim that autoformalization performance improves when trained on multi-lingual data. These characteristics generalize over different sizes of models, supporting the hypothesis that multi-lingual training is good for autoformalization.
strength_weakness: strength_weakness: 1. Even though, authors try manually to sample from the data, the sample size is often small (which is understandable). However, I want to see how the numbers change with varying sample sizes. For example, instead of just one experiment with 100 sample size, the same experiment with varying sample sizes of 50, 75, and 100 showing similar trends will be appreciated.

2. Authors make a key observation that informalization is much easier than formalization, however, I don't find enough justification for this in the paper. Some studies are mentioned on Page 4, but these observations may not generalize well on the dataset in question.

3. The authors accept that the GPT-4 informalizations should be considered as a noisy approximation. This actually is a big limitation. Since not every informalization is verified, there is a potential chance of leakage of the test data itself. Since informalization is generated by GPT-4, it might as well generate informalization for theorems other than the formal statement in question (maybe something which was similar to the formal statement). If such a similar formal statement is present in the test data, then this potentially can help the model perform better on test data (this can be considered a type of leak in the training data). I can understand that this may not be a common case. However, some case studies about the resemblance between the train and test data should be conducted.
questions: questions: 1. Can you separate Table 2 (Right) into various Error Types per language? Right now all the 200 MMA formalizations from the samples are presented together without the distinction between Lean vs Isabelle.

2. The authors talk about few-shot prompting vs instruction prompting on Page 4. I understand the budget reasons, however, I would like to see some case studies showing the qualitative differences between the two strategies (for a small subset of data) in this domain.

3. In Figure 2 (top), the bar plot for "Llama Autoformalization Isabelle" shows almost no correct formalization for the Isabelle-only model. I would like to the examples of those autoformalization that were possible because of the Isabelle + Lean model. A qualitative analysis of when this type of transfer is effective will be appreciated.
limitations: limitations: The authors do try to discuss some limitations, however, I would like to see more. I'm interested in seeing the resemblance of the test and train data since it was generated by GPT-4, and there is a potential chance of data leakage. Since the generation of informalization cannot be controlled, this risk always exists and hence just a comparison with the baseline is not sufficient.
paper_summary: paper_summary: This paper introduces MMA, a large multi-language dataset for autoformalizing theorem statements. MMA employs a back-translation approach using GPT-4 to convert two formal corpora (AFP for Isabelle and mathlib for Lean4) into informal-formal pairs. Experiments demonstrate that LLMs such as LLaMA and Mistral, fine-tuned on MMA, achieve significant improvements over base models (from 0% to 29%-32% with no or minimal correction), outperforming their single-language counterparts in autoformalization on the miniF2F and ProofNet benchmarks.
strength_weakness: strength_weakness: * I think the main weakness of this paper is that MMA is constructed solely based on zero-shot prompting for informalization by GPT-4, resulting in a dataset that is not perfectly aligned. Table 2 shows that the formalization accuracy is around 75%, indicating significant room for improvement. While the choice of zero-shot prompting may be due to cost considerations given the large scale of the dataset, there are potential ways to improve quality. For example, filtering out obvious errors in informalized statements or using more advanced prompting techniques (e.g., few-shot, self-consistency, or prompt to refine the misunderstanding concept) could help construct a smaller but higher-quality dataset. I am also curious about the effectiveness of fine-tuning with a small high-quality dataset compared to a large but noisy dataset for autoformalization.

* Minor: Missing references: There are some other works that leverage autoformalization to generate informal-formal data [1, 2]. [3] also surveys methods for autoformalization and theorem proving.

[1] FIMO: A Challenge Formal Dataset for Automated Theorem Proving, arXiv preprint 2023

[2] MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data, ICLR 2024

[3] A Survey on Deep Learning for Theorem Proving, arXiv preprint 2024
questions: questions: * In the discussion, the author mentions plans to expand to other languages like Coq. However, I believe that a significant portion of Coq projects focuses on software verification, which is often challenging for human readability. One success of informalization by GPT-4 is that the formalized concepts are easily understood by GPT-4. Do you think your approach could still be effective for such Coq projects?

* (optional) If applicable, I am curious about the performance of DeepSeekMath or Llemma as the base model to be fine-tuned on MMA. These models have been pre-trained on large-scale informal and formal datasets and exhibit some basic autoformalization abilities.
limitations: limitations: I appreciate the detailed statement of the limitations in the paper. Moreover, I believe the most significant limitation is the presence of noisy aligned informal-formal pairs, which could be improved further.

Comments: title: Thank you
comment: We thank the reviewer for their response! We will do our best in making the comparisons and evaluations more compelling in the updated paper.
thank you for the updates! i will be glad indeed to see this paper updated with a discussion of & comparison (to extent that this is reasonably achievable) to few shot prompting, and disaggregated results on the benchmarks. 

ideally, i would also like results on the full benchmarks and not just subsets - regardless of whether other papers have also strayed in this way!
We want to thank the reviewer again for their valuable time and input. It has greatly helped us improve the paper. Thank you!
Thank you for your detailed response. I acknowledge that the MMA is the first large-scale approach to building an aligned informal and formal corpora, and I appreciate the manual efforts involved in the experiments. Your clarification has addressed my concerns, and I have revised my score positively in light of this.
We thank the reviewer for such a swift response and appreciate their reconsidering the score!
I'm satisfied with the author's responses and their experiments. Hence, I have increase my score. I hope to see more nuanced examples showing the effectiveness of the transfer between languages.