Multilingual Mathematical Autoformalization

We thank the reviewer for helpful suggestions and references. Below we address the specific points raised by the reviewer.

• Novelty:

  • As we specify in the Contributions subsection, the main contributions of this paper includes:

    1. Creating a large dataset
    2. Training multiple language models on it with different settings
    3. Evaluating these language models on held-out benchmarks manually to demonstrate that the dataset helps autoformalization
    4. Conducting ablation experiments to show the multilinguality in formal languages benefits autoformalization.

  • We want to emphasise that this is a dataset paper, not a method one. The paper by Fu et. al proposes “model specialization”, which distils from a large model to a small model. Ours is about utilising the power of model distillation and back-translation to construct the most useful dataset for autoformalization, and validating various scientific points with it, as mentioned in the contributions.

  • The proposed method is generic, but only evaluated on the narrow domain of autoformalization.

    Autoformalization is a new domain that poses unique challenges like the lack of a sizeable dataset, the integration of neural and symbolic methods, and the difficulty of model evaluation. We think the domain is important enough to warrant its own treatment: Numerous papers solely on the specialised domain of autoformalization have been published, with lots in top conferences within both the machine learning and the theorem proving communities [1-8].

  • Back-translation and sequence distillation are well-known techniques in the field of NLP and we do not make claims about inventing them. This is a dataset paper and we utilise these two techniques to create the dataset. The advantage of using back-translation for autoformalization is that informalising is much easier than formalising and hence we can get a high-quality dataset with it. Only the very first part of the process and experiments described in our paper is similar to Fu et. al and our novelty is elsewhere.

• References:

  • We note that autoformalization is quite different from both program synthesis and informal reasoning, with the aim of translating from a natural language to a formal one instead of creating formal programs from scratch. These papers are related to the method of creating the dataset, rather than the conclusions/contributions (which are about the dataset and the multilinguality) of the paper. We thank the reviewer again for the references. We have updated the paper to include these references and made a comparison of our paper to them.

• Data contamination:

  • This is a valid concern and we appreciate it. Three important pieces of information indicate that there is unlikely any data contamination with our paper:
    • We did not evaluate GPT-4. We only evaluated llama models.
    • The pre-trained model is not contaminated: We dedicate a subsection to the issue of data contamination with the pre-trained llama model in Section 6. Since it cannot even be instructed to write Isabelle or Lean, we think it unlikely that the pre-trained model is contaminated.
    • The fine-tuning datasets are not contaminated: The fine-tuning datasets come from Isabelle AFP + Lean Mathlib4. The test benchmarks come from miniF2F + ProofNet. These datasets are strictly disjoint. We use GPT-4 to create English descriptions of AFP and Mathlib4, which are extremely unlikely to include anything from the formal test benchmarks. Since we have an unlikely contaminated pre-trained model, and an unlikely contaminated fine-tuning dataset, we conclude that the test evaluations are not affected by data contamination, and our conclusions stand.

• Spelling:

  • We use British English spelling throughout, except for the word “autoformalization”, which has become a term.

We thank the reviewer for their insightful feedback. We are glad that the reviewer recognises the contribution of the dataset given the scarcity of mathematical autoformalization data. Below we respond to specific points raised by the reviewer:

• Evaluation:

  • The main conclusions can be supported by 100 datapoints per model/inference configuration
    • We sample evaluation datapoints randomly (not cherry-picked)
    • With this much data, we already demonstrate very strong differences between the models to support our conclusions (16-18% vs 6-11% vs 0% of trivial corrections).
  • It’s incredibly expensive to annotate the entire benchmarks in such detail
    • We would like to point out that for this paper, we manually examine 50 examples from each benchmark x 2 benchmarks x 6 different model/language inference settings = 600 individual examinations. Evaluating each example requires 2-10 minutes for expert-level formal mathematicians, and in practice it took ~30 expert hours to finish. This is quite expensive. To execute the complete testing process, it requires 8-12x more effort, hence roughly 240-360 expert hours. This is USD 12K - 18K at a rate of $50/hr for formal mathematics experts (>= PhD level).
  • However, we do understand that a sample size of only 50 examples per benchmark (10% of the entire dataset) is smaller than traditionally done. Therefore to address the issue of low sample size, since we release the evaluation datapoints, we will open the evaluation up for the Isabelle and Lean communities. We have already identified Isabelle and Lean experts who are willing to contribute to this annotation endeavour. Leveraging the power of open-source communities is the best way to scale the evaluations while maintaining the quality of them.

• MMA dataset quality

  • Please see the overall comment for an in-depth analysis of the quality of the MMA dataset: https://openreview.net/forum?id=QqdloE1QH2&noteId=Z8PeCPad8b
  • To summarise the findings of the analysis:
    • Around 75% of the examined 200 problems were informalised completely correctly by GPT-4.
    • The failure cases are mostly due to ambiguity from the lack of appropriate context. And to ameliorate this issue is an exciting avenue for future research, possibly leveraging retrieval-augmented generation.

• Confusion about the use of “language”

  • When we use the word “language”, we try to make sure that it has relevant context around it to distinguish between a natural or a formal language.

We thank the reviewer for their insightful feedback. We are glad that the reviewer recognises the contribution of the paper. Below, we respond to specific questions:

• The use of the word multilingual:

  • We think it’s an appropriate word, since there are multiple formal languages. However we do admit that there can be confusion in this word. We will make the best attempt to contextualise it by making clear that the languages refer to formal languages whenever we use the word “multilingual”

• Dataset quality

  • We thank the reviewer for this comment. Indeed the dataset is noisy since it was generated by GPT-4. Hence it warrants an in-depth analysis, which we perform in the overall comment: https://openreview.net/forum?id=QqdloE1QH2&noteId=Z8PeCPad8b
  • To summarise the gist of the analysis:
    • Around 75% of the examined 200 problems were informalised completely correctly by GPT-4.
    • The failure cases are mostly due to ambiguity from the lack of appropriate context. And to ameliorate this issue is an exciting avenue for future research, possibly leveraging retrieval-augmented generation.
  • Moreover, in the paper, we demonstrate with comprehensive experiments that the dataset can be used in practice to boost the autoformalization ability of language models; and the ablation experiments highlight the importance of the multilinguality of formal languages.

• Clarification of the mix-data training

  • For all fine-tuned language models, we perform 40000 steps of training. Each model was trained on 40000 * 8 (local batch size) * 2 (world size) * 512 (sequence length) ~= 328 million tokens (containing pad tokens). Each model has seen an equal number of tokens.
    • For the model trained on the mixture of two formal languages, one epoch is 332K sequences. It was trained for 3.3 epochs (~246 million Isabelle tokens, 82 million Lean4 tokens).
    • For the model trained on Isabelle only, one epoch is 244K sequences. It was trained for 4.4 epochs (~328 million Isabelle tokens).
    • For the model trained on Lean4 only, one epoch is 88K sequences. It was trained for 13.2 epochs (~328 million Lean4 tokens).

We thank the reviewer for their careful examination of our paper and insightful feedback. We are glad that the reviewer recognises the contribution of the dataset. Below we address the specific points raised by the reviewer.

• Dataset quality

  • We fully realise the importance of the dataset quality and hence conducted an in-depth examination of the dataset quality, posted in the overall comment: https://openreview.net/forum?id=QqdloE1QH2&noteId=Z8PeCPad8b
  • To summarise the findings of the analysis:
    • Around 75% of the examined 200 problems were informalised completely correctly by GPT-4.
    • The failure cases are mostly due to ambiguity from the lack of appropriate context. And to ameliorate this issue is an exciting avenue for future research, possibly leveraging retrieval-augmented generation.

• Contribution of the paper

  • Our contributions are
    1. Creating a large dataset
    2. Training multiple language models on it with different settings
    3. Evaluating these language models on held-out benchmarks manually to demonstrate that the dataset helps autoformalization
    4. Conducting ablation experiments to show the multilinguality in formal languages benefits autoformalization.
  • This will enable other researchers to conduct meaningful work on top of ours and advance science. As an investigative scientific work, we think that our contributions merit a broader audience.