We thank the reviewer for their thoughtful and detailed feedback, as well as for recognizing the strengths of our work, including the promising results demonstrated using GPT-4 for informalization and GPT-2 for fine-tuning. We appreciate the opportunity to address your concerns and clarify our contributions.

For calibration purposes, we would like to clarify the ICLR 2025 review rubric compared to other conferences like NeurIPS 2024. Notably: A score of 8 on the ICLR 2025 rubric indicates an "Accept," whereas NeurIPS 2024 uses 7 for this designation. Similarly, a "Strong Accept" is represented by a score of 10 at ICLR 2025 compared to 9 at NeurIPS 2024.

We appreciate the opportunity to address concerns and clarify the contributions of our work:

1. Limited exploration of LLMs

Comparison with Gemini-Pro and other models: While we acknowledge the importance of comparing with specialized models like Gemini-Pro, Llemma-7B, and Qwen-Math, resource constraints necessitated our focus on GPT-2 for fine-tuning and GPT-4 for data generation. Despite this, our results on ProofNet validate the hypothesis that alignment and quality outperform diversity in task-specific performance. We consider comparisons with larger, specialized models a critical direction for future research.

Scaling beyond GPT-2: Although GPT-2 is limited in size, the observed improvements demonstrate the robustness of our methodology. GPT-4 data generation further supports the scalability of our approach, and future work will validate this on larger models.

2. Lack of comparisons with key datasets and approaches

Our comparison with MMA was intentional to contrast diversity-focused methods with our alignment-driven approach. While MMA is not the strongest baseline, the results underscore the superiority of high-quality, task-aligned data. Comparisons with datasets like Lean Workbook, Forml4, ProofNet, and FIMO are important and will be prioritized in future work but weren't in existence when this work was done.

3. Insufficient examples of backtranslation effectiveness

Examples of transformations are included in Appendices A and B, demonstrating the effectiveness of few-shot GPT-4 prompting and regex-based methods. These examples highlight alignment improvements and will be integrated into future iterations of the paper for clarity.

4. Cost analysis

Resource efficiency was a key focus, and methods like regex parsing are highly cost-effective compared to GPT-4-generated data. While a detailed cost analysis was not included in this iteration, future work will provide a comprehensive breakdown to guide practitioners.

5. Metrics beyond cross-entropy loss

Cross-entropy loss was used due to its alignment with the ProofNet benchmark and its reproducibility. Metrics like pass@10 or Lean4 compilation success are not directly applicable given the dataset size and current state of autoformalization evaluation. As this field evolves, future work will incorporate symbolic verification and proof-checking accuracy to better capture semantic alignment and correctness.

Questions

Q1: Concrete examples of autoformalization tasks:

Examples are included in Appendices A and B, showcasing formal-informal transformations from the AI4Math dataset. These illustrate alignment and quality improvements through GPT-4-generated data.

Q2: Human-in-the-loop feedback

We did not explore this due to resource constraints but recognize its potential to enhance informalization quality. Incorporating human feedback remains a promising direction for future research.

We thank the reviewer for their detailed feedback and for acknowledging the utility of our methodological tricks, such as online and offline backtranslation and line-by-line proof analysis.

For calibration purposes, we would like to clarify the ICLR 2025 review rubric compared to other conferences like NeurIPS 2024. Notably: A score of 8 on the ICLR 2025 rubric indicates an "Accept," whereas NeurIPS 2024 uses 7 for this designation. Similarly, a "Strong Accept" is represented by a score of 10 at ICLR 2025 compared to 9 at NeurIPS 2024.

We appreciate the opportunity to address concerns and clarify the contributions of our work.

1. Novelty of the proposed techniques compared to prior work

We appreciate the reviewer pointing out similarities with prior works like ProofNet and process reward modeling (PRM). While backtranslation is indeed a well-known practice, our contribution lies in adapting and optimizing it specifically for the autoformalization domain with resource constraints in mind. For example:

On-the-fly backtranslation integrates informalization and formalization dynamically within the training loop, which is a novel implementation compared to the static dataset-based approach used in ProofNet. Distilled backtranslation builds on ProofNet's technique but employs few-shot amplification with GPT-4, focusing on token efficiency and data quality. Line-by-line proof analysis extends beyond PRM-like approaches by embedding proof states before and after each tactic, aligning closely with the structure of interactive theorem proving. The takeaways ("quality over quantity/diversity," "intermediate steps matter") may align with established principles in the field, but our results explicitly quantify and demonstrate these concepts in the autoformalization setting, offering practical insights for future work.

2. Use of evaluation loss to demonstrate effectiveness

We recognize the limitations of evaluation loss as a sole metric and appreciate the suggestion to use more robust evaluation methods. However, pass@10 does not exist for autoformalization tasks, as there is no standardized way to measure generalization across multiple outputs in this domain. Additionally, while symbolic verification using Lean is a valuable metric for evaluating formal proofs, the small size of our datasets makes such an approach less impactful in this case.

It is important to note that evaluation metrics for autoformalization are an ongoing area of research, as evidenced by the lack of universally accepted benchmarks beyond ProofNet and metrics. Evaluation loss provides a consistent and reproducible measure of a model’s ability to align with target outputs and is directly aligned with the ProofNet benchmark. While not exhaustive, this metric serves as a reliable proxy for comparing improvements in data quality and model training effectiveness.

Our focus in this work was to establish foundational methods for high-quality data generation, and future work will aim to incorporate broader evaluation techniques as this area of research matures. The foundation is to focus on data quality and alignment, not on diversity of unrelated languages to your autoformalization task.

3. Insufficient results with weaker models (e.g., GPT-2)

While we agree that testing on larger models like Llemma or Llama would provide stronger validation, our resource constraints necessitated a focus on smaller, cost-effective models like GPT-2. The observed improvements on ProofNet, despite using GPT-2, demonstrate the robustness of our methods. Furthermore, the performance gains from GPT-4-generated datasets highlight the scalability and applicability of our approach to larger models.

4. MMA as a baseline

We recognize the reviewer's concern that MMA may not represent the strongest baseline. However, its inclusion was deliberate and critical to our goal of demonstrating that diversity alone does not drive performance in task-specific domains like autoformalization in Lean. MMA represents a multilingual, highly diverse dataset, making it an ideal point of comparison for our hypothesis that alignment and quality outweigh diversity in such contexts.

The fact that our methods outperformed MMA, despite its significantly larger scale (we had 2 orders of magnitude less data), underscores the importance of high-quality, targeted data for improving performance in autoformalization tasks. The results against MMA strongly support our core thesis.

We thank the reviewer for their thoughtful feedback and for recognizing the strengths of our work.

For calibration purposes, we would like to clarify the ICLR 2025 review rubric compared to other conferences like NeurIPS 2024. Notably:
A score of 8 on the ICLR 2025 rubric indicates an "Accept," whereas NeurIPS 2024 uses 7 for this designation. Similarly, a "Strong Accept" is represented by a score of 10 at ICLR 2025 compared to 9 at NeurIPS 2024.

We address the specific points raised:

1. Limited effectiveness across generation methods

We appreciate the observation that the GPT-4-generated dataset achieved the best evaluation loss among our methods. This aligns with our hypothesis that data quality, as enhanced by GPT-4’s capabilities, is a critical driver of performance. The remaining methods (e.g., regex parsing) were included to explore cost-efficient alternatives, as noted in the paper. These approaches still provided meaningful improvements over the baseline, demonstrating the feasibility of resource-conscious solutions.

2. Lack of examples for generated data

We acknowledge the value of showcasing generated data and regret the omission in the main text due to space constraints. Examples of formal-informal translations generated via regex-based methods and GPT-4 are provided in the appendix (Appendices A and B), highlighting the diversity and quality of outputs. For instance, templated informalizations like “We simplify the current expression using the simp tactic” illustrate the process of converting formal proof tactics into understandable natural language.

The few-shot prompting strategy demonstrated in Appendix A shows that GPT-4 successfully captures nuanced translations of complex theorems, addressing this difficulty directly.

3. Why use evaluation loss to assess autoformalization performance?

We used evaluation loss because it provides a quantitative measure of the model’s ability to predict target outputs during training and aligns well with the ProofNet benchmark. While metrics like pass rates or human evaluations could provide additional insights, evaluation loss is a widely accepted proxy for task-specific performance in this context. Additionally, ProofNet’s structure as a formal dataset enables a direct and reproducible measure of model improvements via this metric. Additional metrics for autoformalization is itself an entire research area by itself.

4. Limited novelty and insufficient experiments

We appreciate the reviewer's concern about novelty and experiment breadth. The novelty of our work lies in demonstrating the impact of high-quality, token-efficient data generation techniques, particularly few-shot prompting and proof state integration. While we acknowledge that experiments with additional baselines or larger models would strengthen the work, resource constraints limited our ability to extend beyond GPT-2 fine-tuning.

Despite these constraints, the results provide strong evidence of our methods’ effectiveness, particularly in reducing evaluation loss and improving token efficiency compared to existing datasets like MMA. Future studies will address the pass rates of state-of-the-art LLMs fine-tuned with AI4Math.

We thank the reviewer for their thoughtful feedback and for recognizing the strengths of our work, particularly our focus on enhancing data quality and the demonstration that high-quality data can outperform larger multilingual datasets. We also appreciate the acknowledgment of the resource efficiency and potential of our approach for advancing autoformalization research.

For calibration purposes, we would like to clarify the ICLR 2025 review rubric compared to other conferences like NeurIPS 2024. Notably: A score of 8 on the ICLR 2025 rubric indicates an "Accept," whereas NeurIPS 2024 uses 7 for this designation. Similarly, a "Strong Accept" is represented by a score of 10 at ICLR 2025 compared to 9 at NeurIPS 2024.

We address the specific points raised:

1. Experiments are limited to GPT-2

We acknowledge that our experiments were conducted using GPT-2 due to resource constraints, which may limit generalizability to larger models. Despite this, our approach demonstrated substantial improvements over the baseline on ProofNet, underscoring the efficacy of high-quality data generation. Importantly, the token efficiency achieved suggests scalability to larger models. Future work will explore fine-tuning state-of-the-art models like GPT-4 and Llemma to validate the broader applicability of our method.

2. Generalization to real-world mathematical texts

We focused on curated datasets like ProofNet, MathLib4, and LeanDojo to evaluate performance rigorously within a controlled setup. While broader evaluations on real-world texts (e.g., informal papers or textbooks) would strengthen our findings, the curated datasets used in this work already encompass a diverse range of mathematical domains, providing a strong foundation. Expanding evaluations to datasets like MiniF2F or real-world examples is a priority for future research.

3. Generalizability to other formal languages such as Metamath

This is a valuable question. Although our experiments focused on Lean and ProofNet, the techniques proposed (e.g., backtranslation and proof state integration) are not specific to Lean and could be applied to other formal languages like Metamath. Generalizing to multiple formal languages would require adapting our templates and prompts, a promising avenue for future work.

1. ProofNet Test is the only evaluation performed, so generalizability is hard to see.

We appreciate this observation. We chose ProofNet as it is a widely recognized benchmark for evaluating autoformalization, offering clear alignment with our goals of testing mathematical formalization accuracy. While additional evaluations would strengthen generalizability claims, we emphasize that ProofNet serves as a strong proxy for broader tasks in formal reasoning, given its diversity in mathematical domains (Azerbayev et al., 2023a). Future work will explore other benchmarks like MiniF2F or GSM8K to further validate generalizability.

2. Without multiple evaluations, the risk of data contamination with ProofNet is high, but the paper did not address this.

We acknowledge the importance of controlling for data contamination. Our methodology relies on curated datasets (e.g., MathLib4 and LeanDojo) that are distinct from ProofNet, mitigating overlap risks. Specifically, we parsed data directly from Lean community repositories and employed regex-based filtering to create our training data, ensuring minimal contamination. Moreover, the curated nature of our datasets provides confidence that our evaluation reflects genuine improvements, not data leakage.

3. The only model trained was GPT-2 124M, and as the authors addressed, performance could be better for larger models.

We appreciate this observation and agree that larger models could yield stronger performance. However, resource constraints necessitated a focus on smaller, cost-effective models like GPT-2 for this work. Our results still demonstrate significant improvements over the baseline, validating our methodology’s effectiveness. Importantly, the consistent reduction in evaluation loss suggests scalability, and we hypothesize that the gains observed would extend to larger models like GPT-4 or Llemma 7B. In addition, work like Why Has Predicting Downstream Capabilities of Frontier AI Models with Scale Remained Elusive? and the LLama3 tech report, demonstrate that predictable evaluations with loglikelihoods alone (eg by using loglikelihoods of the correct answer).

4. There was no investigation into the scaling laws of this approach.

While our primary focus was on data quality and efficiency, we agree that scaling laws are critical to understanding long-term performance trends. The results in Table 2 suggest strong token efficiency, indicating potential scalability. The sharp improvements with GPT-4-generated data further support this hypothesis. Future research will address this limitation by testing scaling properties with larger models and token budgets.

5. There was no analysis of the types of proofs that the method performs well at.

This is an excellent point. Due to time constraints, we prioritized aggregate metrics like evaluation loss. However, our method inherently focuses on mathematical theorems with formal-informal alignment (e.g., algebraic and group-theoretic proofs). For instance, the few-shot prompting strategy particularly benefited structured proofs like those in the MathLib4 dataset. A detailed error analysis across proof categories is a planned extension.

Questions

Q1. How does the dataset impact performance on other datasets?

While we did not test explicitly on other datasets, the token efficiency and improvements observed on ProofNet suggest that our method is not overfitted to a specific dataset. The diversity in MathLib4 and LeanDojo implies generalizability across formal-informal translation tasks.

Q2. How does fine-tuning a larger model impact performance?

We hypothesize that scaling up to larger models like GPT-4 or Llemma 7B would yield substantial improvements, as seen in related work (Azerbayev et al., 2023b). Larger models would likely benefit more from the high-quality, structured data generated using our backtranslation methods, improving fine-tuning efficiency and accuracy.

Q3. What is the evidence that there is a high likelihood that this approach scales?

The observed token efficiency and performance gains, even with a small model like GPT-2, indicate that our methodology maximizes data utility. Scaling laws in prior works (Brown et al., 2020) show that larger models benefit disproportionately from high-quality data, supporting our approach. Additionally, the significant improvement using GPT-4-generated data (Table 2) highlights the scalability potential of our techniques.