Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach

Questions:

Introduction:

Why is dependency retrieval essential in the current context, and how does it address existing limitations?

As stated in line 070-075 and 090-100 of the paper, the current autoformalization paradigm suffers from the agnosia of context and dependency retrieval helps address this issue.

Due to the lack of prior knowledge of existing formalized definitions and theorems, current autoformalization models frequently generate hallucinated formal objects that do not exist in the library.

Dependency retrieval addresses this issue by retrieving potentially dependent formal objects from the formal library (e.g., Mathlib 4) conditioned on the informal statement to autoformalize. Given these retrieved objects, the autoformalizer model can generate more accurate formal statements with lower risk of hallucination.

What evidence supports the claims about β-reduction and type checking limitations? Can authors provide citations or examples?

Actually, we did not mention anything about the limitations of $\beta$-reduction in the paper. It seems that you need examples about the fragility of machine translation metrics (like BLEU) under $\beta$-reduction. Suppose we define a function def dummy (x : Nat) := 1. Then, the two expressions, dummy x and 1 are definitionally equal, but they have low token-level similarity, and thus struggle to be viewed "equivalent" in machine translation metrics like BLEU.

As for the limitation of existing metrics such as typecheck, BLEU and LLM Grader, please kindly refer to the two demonstrations in Fig.8 and Fig.9 of the paper, where all of the metrics fail. Here we provide a brief analysis of Fig.8. Its informal statement is "Show that $\sin\frac{\pi}{12}$ is an algebraic number", and two formal statments be isAlgebraic Rat (sin (pi/12)) and isAlgebraic Rat (Real.sin (Real.pi/12)). These two formal statements can both pass the Lean typecheck, have high token-level similarity and are very confusing for LLM (and people who is not proficient in Lean 4). However, they're completely different in Lean. pi in the former statement is an implicit argument of an arbitrary real number, while Real.pi in the latter statement means the true $\pi$.

BEq Evaluator:

How does BEq construction overcome the "non-determinant and highly prompt-dependent" limitations of LLM graders when it also uses LLMs and few-shot prompting? How does BEq's few-shot prompting actually reduce human design efforts compared to previous approaches?

Answers to these two questions are included in the response in the Weakness section. Please kindly refer to it.

Why choose InternLM2-Math-Plus-20B when: DeepSeek V2.5 shows better performance in majority voting? What makes its math pretraining superior? Why not implement BEq with other models? Can BEq work effectively across different math LLMs?

Interesting question. There is no special reason for us to choose InternLM2-Math-Plus-20B. Maybe the most important one is that the API calling of Deepseek V2.5 costs money. To better answer this question, we have evaluated BEq on different models with attempt number $k=8$ and temperature $T=0$ (For Deepseek-V2.5, $T=0.7$ due to the requirement of API calling), and the results are as follows.

As the results indicate, a 7B InternLM2-math-plus model can achieve 90.5% accuracy. There is not much difference among the various models, but the pretraining dataset and model architecture do play a significant role. Qwen1.5, which likely was not pretrained on a vast formal math corpus, shows inferior accuracy compared to all other models. In contrast, Deepseek-series and InternLM-series models exhibit slightly higher accuracy. Additionally, we believe there is substantial room for improving the LLM, potentially through data synthesis and fine-tuning, as the recall is not yet satisfactory.

We greatly appreciate your detailed reviews, as well as your constructive comments. There are too many points in the Weakness and Question sections. For clarity, we have omitted the repeated points in the Weakness section and will address the remaining points in the Question section. If there are any missing questions, please point them out, and we will respond promptly.

Weaknesses:

Authors state some disadvantages of "LLM graders". Could authors provide more citations stating this?

1. The paper critiques LLM graders as "non-determinant and highly dependent on prompts" but doesn't sufficiently distinguish how BEq (which also uses LLMs) overcomes these limitations.
2. The few-shot prompting used in BEq seems to face similar prompt-design challenges that the authors criticize.
3. While Table 1 shows improved performance, more analysis is needed to demonstrate that BEq fundamentally addresses the cited limitations of LLM graders raised in the introduction.

LLM grader[4] is a recently published work. As far as we know, BEq is the first work trying to address the non-deterministic, uninterpretability, and prompt-dependency of LLM Grader. However, an LLM being "non-deterministic and highly dependent on prompts" seems to be common knowledge in the LLM and DL community, and many methods are even built on this "non-deterministic" nature, for example, Majority Voting.

We've invested significant effort in reproducing the LLM grader and establishing it as a strong baseline. The 82.5% accuracy reported in Table 1 represents the best result among our experiments. Below are some findings from our preliminary experiments on the base model and prompt method used in the LLM Grader. We've also explored other base models and methods, recordings of the best results obtained.

It seems that you might have misunderstood BEq as a prompt-based method. In fact, BEq defines equivalence as bidirectionally "convertible" using simple transformations. Few-shot prompting LLM is just an implementation to approximate the ideal transformation function $T$. To assert that "$\boldsymbol s_P$ is BEq to $\boldsymbol s_Q$", one should provide (or the LLM is prompted to generate) two proofs (tactic sequence) of UDI (unidirectional definitional implication):

1. Proof of $\boldsymbol s_Q$ assuming $\boldsymbol s_P$ to be True, and this proof is limited to only use tactics in $\mathcal R$ and must use the hypothesis that $\boldsymbol s_Q$ holds.
2. Proof of $\boldsymbol s_P$ assuming $\boldsymbol s_Q$ to be True, and this proof is limited to only use tactics in $\mathcal R$ and must use the hypothesis that $\boldsymbol s_P$ holds.

These proofs are interpretable and formal-verified. This approximation becomes more effective as the base LLM becomes more capable or the number of attempts $K$ increases (discussed in Appendix A.1).

However, despite its interpetability, accuracy and formal-verified nature, we couldn't overclaim that BEq fundamentally addresses all limitations of existing methods. As described in Sec.6.Limitations of BEq, carefully designing the limitation of transformation primitives $\mathcal R$ and improving the LLM's capabilities to approximate $T$ is crucial. We sincerely invite community efforts to delve into refining BEq and eventually set a domain standard to facilitate subsequent research.

[1] Azerbayev, Zhangir, et al. "Proofnet: Autoformalizing and formally proving undergraduate-level mathematics." arXiv preprint arXiv:2302.12433 (2023).

[2] Wu, Yuhuai, et al. "Autoformalization with large language models." Advances in Neural Information Processing Systems 35 (2022): 32353-32368.

[3] Jiang, Albert Q., Wenda Li, and Mateja Jamnik. "Multilingual mathematical autoformalization." arXiv preprint arXiv:2311.03755 (2023).

[4] Ying, Huaiyuan, et al. "Lean Workbook: A large-scale Lean problem set formalized from natural language math problems." arXiv preprint arXiv:2406.03847 (2024).

[5] Li, Zenan, et al. "Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency." arXiv preprint arXiv:2410.20936 (2024).

[6] Lu, Jianqiao, et al. "Process-driven autoformalization in lean 4." arXiv preprint arXiv:2406.01940 (2024).

Experimental Questions:

How would results differ with multiple LLM backbones?

We have reproduced all fine-tuning-based methods on DeepseekMath-Base-7B as the base model with training recipes identical to Appendix A.8. The results are added to Appendix A.3, which demonstrate consistent (and even clearer) advantage of our methods over all baselines, and the ablative improvement of Dependency Retrieval.

Why weren't standard reasoning baselines (COT, TOT, Self-Consistency) included? Comparing with such basic reasoning mehtods is crucial.

Because our task, statement autoformalization, which translates a math statement from natural language to formal language, resembles more to machine translation than reasoning. None of the previous autoformalization literatures (including but not limited to [1-4,6]) have included prompt-engineering methods such as CoT and ToT in their baselines. A recent work [5] (later than our submission) proposes an implementation of self-consistency on the Isabelle theorem prover instead of Lean. However, reproducing it on Lean faces many technical challenges and mismatches of language features.

We have hand-crafted a CoT implementation of autoformalization, and the evaluation results are as follows:

Results show that the results of CoT is unstable. CoT might be better on in-distribution, multiple-trial settings.

How does this work differ from ReProver?

1. RAutoformalizer addresses a completely different task to ReProver. RAutoformalizer concentrates on statement autoformalization, translating a math statement from natural language to formal language, while ReProver focuses on theorem proving, searching for a formal-verified proof given a formal statement.
2. The retrieval tasks are completely different. We firstly propose to augment autoformalization by dependency retrieval, retrieving dependent math objects from a formal library given a natural language statement, while ReProver augments theorem provers by premise selection, retrieving applicable premises from a formal library given a formal proof state.

Does the framework only work effectively with InterLLM2-math? More implementations of different families of LLMs with BEqs are required.

RAutoformalizer is not limited to InternLM2-Math. We have reproduced all fine-tuning-based methods on DeepseekMath-Base-7B as the base model with training recipes identical to Appendix A.8. The results are as follows, which demonstrate consistent (and even clearer) advantage of our methods over all baselines, and the ablative improvement of Dependency Retrieval.

Thanks for your suggestion. We've added this experiment to Appendix A.3.

Con-NF Questions:

What are the construction details and distributions of Con-NF?

The construction process is described in detail in Sec.4.1 Con-NF: OOD Benchmark. During construction, rejective sampling and post-informalization filtering policies are applied in benchmark construction, including:

1. Length filtering: Generated informal statements which are too long or too short are rejected.
2. Format filtering: Generated informal statements which do not match the given format are rejected.
3. Special token filtering: Generated informal statements which contain some special tokens (which we think to be a signal of low-quality informalization) are rejected.
4. Semantic filtering: Sophisticated rules are applied to filter out samples with large semantic gaps with the corresponding math object.
5. Source filtering: Samples whose all dependencies are in Mathlib 4 are filtered out to ensure the OOD nature of this benchmark.

Moreover, human supervision is conducted on statements that fail to pass the filters after several samplings. The sophisticated filtering process reduces the size of the Con-NF benchmark from 85762 to 961.

The discipline distribution of statements in Con-NF benchmark are 100% on Quine's set theory New Foundations, which is not included in Mathlib 4.

How do ProofNet and Con-NF differ in terms of discipline, problem distributions and theorem or dependencies?

ProofNet is a benchmark for autoformalization on undergraduate-level mathematics, with the following problem source distribution:

• Analysis: 88
• Examinations: 15
• Linear Algebra: 28
• Number Theory: 21
• Topology: 60
• Abstract Algebra: 162

All formal statements in ProofNet totally depends on Mathlib 4 (only about ~10 of them slightly dependes on user-defined function or abbreviation). Mathlib 4 is a user maintained library with both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the latter. Many Lean users view Mathlib as a "standard library" of Lean.

However, the Con-NF benchmark is constructed on Con(NF), a formal consistency proof of Quine's set theory New Foundations. After our filtering, statements in this benchmark all belong to this theory and have novel dependencies that don't exist in Mathlib 4.

Why create new datasets instead of using existing ones like ReProver?

Because this paper focuses on a completely different task than ReProver. This paper concentrates on statement autoformalization, translating a math statement from natural language to formal language, while ReProver focuses on theorem proving, searching for a formal-verified proof given a formal statement.

What are exact features considered as OOD comparing to exisitng benchmarks so that authors have to spend efforts in annotating a new benchmark?

RAutoformalizer is trained on statements in Mathlib 4, for which all dependencies are also included in Mathlib 4. However, for the Con-NF benchmark, all statements are based on a novel theory that is not included in Mathlib 4 and have novel dependencies that don't exist in Mathlib 4.

Human Equivalence Benchmark:

How were ground truth pairs created and validated in details?

As detailedly described in Sec.3.2 and Appendix A.4, we randomly sample 200 successfully typechecked model predictions on the ProofNet[1] benchmark: 1) 100 from an early version of the RAutoformalizer; 2) 100 from closed-source ICL prompted OpenAI o1-preview.

These predictions are generated with hyperparameters:

1. greedy decoding with $T=0.0$ for RAutoformalizer;
2. temperature decoding with default hyperparameters of OpenAI API for o1-preview.

Then, 4 experts, one from formal verification and three from computer science, are invited to label the model generated formal statement as “equivalent” or “inequivalent” with the corresponding ground-truth statements.

Experts first separately evaluate the equivalence, and finally discuss in round-table to reach an agreement for each sample.

What are the expert qualifications, payment structures, and annotation guidelines?

Thank you for your careful review. More details about the construction of human equivalence benchmark have been added in our revised version in Appendix A.4 Human Equivalence Benchmark. The expert group consists of 1) one professor in formal verification; 2) one PhD student in EECS; 3) two master students in CS. However, In accordance with the principles of anonymity, we regret to inform you that we cannot disclose any additional information. As stated in Sec.7 Reproducibility Statement, the human equivalence benchmark will be released after acceptance and whoever interested can check then.

How was sampling bias controlled in terms of the following aspects:

• LLM-generated examples?
• non-uniform distribution in Figure 3?
• O1 bias control mechanisms to make sure the quality of evaluation?

Good question. Actually, we've tried our best to control the biases of the Human Equivalence Benchmark and make it suitable for general cases.

1. We collect model predictions from both few-shot prompting closed-source OpenAI o1-preview and fine-tuning InternLM-Math-Base-7B (an early version of RAutoformalizer) to avoid biases introduced in 1) Generation mode (ICL vs. Fine-tuning); 2) Model size; 3) Open-source model and closed-source model.

2. The non-uniform distribution in Fig. 3 can be attributed to two aspects:

   1. The original discipline distribution of ProofNet is imbalanced. Its distribution is as follows:
      • Analysis: 88
      • Examinations: 15
      • Linear Algebra: 28
      • Number Theory: 21
      • Topology: 60
      • Abstract Algebra: 162
   2. As detailed in line 296, 200 formal statements are uniformly sampled from the typechecked predictions generated by RAutoformalizer and OpenAI's o1-preview (100 predictions from each). Since the ratio of samples to pass typecheck differs between disciplines, the distribution becomes more unbalanced.

3. It seems that we didn’t mention anything about the "O1 bias control mechanisms". Actually, the prompts we used for OpenAI o1-preview, GPT-4o, and Deepseek-V2.5 to perform ICL autoformalization are shown in Appendix A.7.3.

If you still feel that the Human Equivalence Benchmark may not fully address your concerns, please refer to Appendix A.2.1, where the results of our manual evaluation may provide further insights into BEq and RAutoformalizer.

Method:

How effectively do RAG methods specifically reduce hallucinations in depth? Can authors quantify the improvement in Table 3 attributed to hallucination reduction for "non-existing dependencies" especially?

Sure, we quantitatively analyzed it by delving into the error distribution of autoformalizations that do not pass typecheck. We parsed the Lean error messages of autoformalizations that fails to typecheck and coarsely classified them into hallucination errors and other errors (detailed taxonomy can be found in Appendix A.2.3). The statistics are reported below:

Results show that both types of errors are reduced by Dependency Retrieval, especially Hallucination errors. This might be one of the root causes of RAutoformalizer’s ablative improvement.

Thank you for the appreciation of our work and the inspiring suggestions. We sincerely hope the following explanations can help resolve your concerns.

Weekness1. BEq requires gold label formal statements.

Admittedly, this is one of the biggest limitation of BEq, as well as an open problem of the whole ML community for years. It is difficult to evaluate a task of the form $\boldsymbol y=f(\boldsymbol x)$ without a ground-truth $\boldsymbol y$. All discriminative tasks need to compare predictions with gold ground-truth labels. For generative tasks, to coarsely summarize, there are mainly 4 types of automated evaluation methods:

1. Using learning-based metrics, such as FID (Fréchet inception distance) in image generation tasks;
2. Using symbolic metrics, such as calculator or formal verifier (in theorem proving);
3. Partial evaluation. For example, existing informal reasoning benchmarks such as MATH[2] and MMLU[1] only perform identity matching between model-predicted answers and the ground-truth answers, neglecting the reasoning trajectory;
4. Proxy metrics, such as BLEU in machine translation.

1,3,4 either depend on ground-truth labels or an “evaluator” DNN, which is uninterpretable and vulnerable to adversarial attacks. And 2 is not suitable for our task, because the space of free-form natural language statements in autoformalization is intractable for symbolic verifier. We currently have no idea of this limitation and believe solving this can lead to strong contribution for the whole ML community. As for autoformalization, all existing benchmarks (e.g. ProofNet[3], FormL4[4]) have ground-truth formal statements. And it should be the benchmark authors' responsibility to ensure the quality of ground-truth.

Weekness2. BEq requires a 20b parameter model to execute.

To address your concern, we have evaluated BEq on different models with beam search using temperature $T=0$, generation number $k=8$ (samples 8 tactic sequences candidates for each input). For Deepseek-V2.5, we use temperature sampling with $T=0.7$ due to the limitation of API call. The results are as follows.

Question1. Experiments of different model sizes for BEq?

Thank you for your constructive comment. The experiment results are detailed in the response to Weakness2. During case analysis, We observe that all models share similar failure patterns, as analyzed in Appendix A.4, Failure Case Analysis. We find that ICL prompting is relatively weak and fails to generate proper transformations for complex scenarios. Therefore, fine-tuning an expert model might be a viable solution. This work focuses on proposing the neural-symbolic method of BEq and demonstrating the potential of RAutoformalizer. To establish a widely-recognized evaluation standard for statement autoformalization, we sincerely invite community efforts to refine BEq.

[1] Hendrycks, Dan, et al. "Measuring massive multitask language understanding." arXiv preprint arXiv:2009.03300 (2020).

[2] Hendrycks, Dan, et al. "Measuring mathematical problem solving with the math dataset." arXiv preprint arXiv:2103.03874 (2021).

[3] Azerbayev, Zhangir, et al. "Proofnet: Autoformalizing and formally proving undergraduate-level mathematics." arXiv preprint arXiv:2302.12433 (2023).

[4] Lu, Jianqiao, et al. "Process-driven autoformalization in lean 4." arXiv preprint arXiv:2406.01940 (2024).

Dear Reviewer 9PuK,

As the rebuttal deadline approaches, please kindly check the papers' discussion threads and respond to the authors' rebuttals. If you haven't had a chance to respond yet, I’d greatly appreciate your input soon. Your insights are invaluable to the authors and the review process.

Thank you for your effort and support!

Best regards,

Area chair

Thank you for your helpful suggestions. We have added more details in the revision and hopefully the explanation can resolve your concerns.

Weekness1. Missing of details.

Thanks for your suggestion, we have added the following details:

1. The prompt template details of BEq in Appendix A.7.1;
2. The prompt template details of LLM Grader to Appendix A.7.2;
3. The prompt template details of ICL autoformalization to Appendix A.7.2;
4. More details in constructing the Human Equivalence Benchmark in Appendix A.4;
5. More ablative experiments on RAutoformalizer in Appendix A.2.2 and A.2.3;
6. A more thorough evaluation of BEq in Appendix A.2.1;
7. Reproduction experiments of all fine-tuning-based methods on DeepseekMath-7B in Appendix A.3;
8. Ablative experiments of augmenting ICL methods in Appendix A.10.

Hopefully, these details can enhance reliability, logical coherence and reproducibility of this work.

Weekness1. Explanation of why the dense embedding is sufficient.

We adopt dense embedding for the following reasons:

1. Dense embedding is one of the simplest and most prevalent method used in RAG [1,2].
2. ReProver[3] adopts dense embedding in premise selection tasks, and we follow their choice in dependency retrieval.
3. We do not conclude that dense embedding is sufficient in the paper. On the contrary, we believe there is significant room for improvement, as indicated by the metrics in Table 2 and the comparison between RA and RA (+R) in Table 3. In this paper, our focus is on proposing the task of dependency retrieval and demonstrating its importance. We leave more sophisticated upgrades, such as multi-vector embeddings, re-ranking, and query augmentation, to the community, as mentioned in Section 6 Limitations of RAutoformalizer.

[1] Zhao S, Yang Y, Wang Z, et al. Retrieval Augmented Generation (RAG) and Beyond: A Comprehensive Survey on How to Make your LLMs use External Data More Wisely[J]. arXiv preprint arXiv:2409.14924, 2024.

[2] Gao Y, Xiong Y, Gao X, et al. Retrieval-augmented generation for large language models: A survey[J]. arXiv preprint arXiv:2312.10997, 2023.

[3] Yang, Kaiyu, et al. "Leandojo: Theorem proving with retrieval-augmented language models." Advances in Neural Information Processing Systems 36 (2024).

Dear Reviewer YeoP,

As the rebuttal deadline approaches, please kindly check the papers' discussion threads and respond to the authors' rebuttals. If you haven't had a chance to respond yet, I’d greatly appreciate your input soon. Your insights are invaluable to the authors and the review process.

Thank you for your effort and support!

Best regards,

Area chair

Many thanks for your constructive comments. Responses to the aforementioned weaknesses and questions are as follows. We sincerely hope them to resolve the concerns.

Weakness1. Potential limitations of BEq.

1. BEq focuses on comparing model prediction to ground-truth formal statement, which requires ground-truths.
2. BEq relies on the tactic features of Lean 4.
3. Evaluation of BEq on synthesized benchmarks like Con-NF is unreliable.
4. BEq distills the problem of evaluating autoformalization into the problem of evaluating 'Definitional Equality' between two formal statements in Lean 4.

We beg to differ with some of your comments.

1. Admittedly, this is one of the biggest limitation of BEq, as well as an open problem of the whole ML community for years. It is difficult to evaluate a task of the form $\boldsymbol y=f(\boldsymbol x)$ without a ground-truth $\boldsymbol y$. All discriminative tasks need to compare predictions with gold ground-truth labels. For generative tasks, to coarsely summarize, there are mainly 4 types of automated evaluation methods:

   1. Using learning-based metrics, such as FID (Fréchet inception distance) in image generation tasks;
   2. Using symbolic metrics, such as calculator or formal verifier (in theorem proving);
   3. Partial evaluation. For example, existing informal reasoning benchmarks such as MATH[3] and MMLU[2] only perform identity matching between model-predicted answers and the ground-truth answers, neglecting the reasoning trajectory;
   4. Proxy metrics, such as BLEU in machine translation.

   1,3,4 either depend on ground-truth labels or an “evaluator” DNN, which is uninterpretable and vulnerable to adversarial attacks. And 2 is not suitable for our task, because the space of free-form natural language statements in autoformalization is intractable for symbolic verifier. We currently have no idea of this limitation and believe solving this can lead to strong contribution for the whole ML community. As for autoformalization, all existing benchmarks (e.g. ProofNet[1], FormL4[9]) have ground-truth formal statements. And it should be the benchmark authors' responsibility to ensure the quality of ground-truth.

2. The idea of BEq, which defines an equivalence relation as bidirectionally convertible under restricted transformations, can be applied in broader areas. Our implementation of BEq on Lean relies on two key components: definitional equality and tactics. Definitional equality is a widespread concept in formal verification environments, especially dependent-type-theory-based languages such as Coq and Lean; Tactics are intrinsically metaprograms that transform the current goal, which can also be replaced by similar concepts in other formal verification environments.

3. Thank you for pointing out this issue. We have conducted comprehensive human evaluation on the autoformalization results of multiple settings (including Con-NF) and added it as Appendix A.2.1. Results show that BEq even better aligns with human experts on Con-NF.

4. We respectfully disagree with you as evaluating autoformalization results between model prediction and ground-truth is a mainstream paradigm adopted by perplexity, BLEU, E3[4]. Only two exceptions exist: 1) Typecheck, which only checks whether Lean kernel can successfully compile and totally neglects semantic difference. 2) LLM Grader[5], which is NOT used as an evaluation method but a filtering method in the original paper.

   We believe it should be the benchmark authors' responsibility to ensure the quality of ground-truth, including semantic correctness (the ground-truth formal statements are aligned with the informal statements) and syntactic correctness (the ground-truth formal statements are successfully type-checked).

Weakness2. Potential quality issue of Human Equivalence Benchmark.

Thank you for your careful review. More details about the construction of human equivalence benchmark have been added in our revised version in Appendix A.4 Human Equivalence Benchmark. The expert group consists of 1) one professor in formal verification; 2) one PhD student in EECS; 3) two master students in CS. However, In accordance with the principles of anonymity, we regret to inform you that we cannot disclose any additional information. As stated in Sec.7 Reproducibility Statement, the Human Equivalence Benchmark will be released after acceptance and whoever interested can check then.

Weakness3. Unclear prompt details of BEq and LLM Grader.

Thank you again for your careful review. We have added these details in our revised version in Appendix A.7.

Weakness4. Writing clarity.

Many thanks for the advice. We have revised all writing clarity issues in the main text and Fig.1.

Weakness5. Construction of Con-NF benchmark

1. Lack of quality control
2. Discrepancy between the informal statements and ground-truth formal statements
3. Possibility of the informal statements to contain formal identifiers or even raw formal statements

1. Rejective sampling and post-informalization filtering policies are applied in benchmark construction, including

   1. Length filtering: Generated informal statements which are too long or too short are rejected.
   2. Format filtering: Generated informal statements which do not match the given format are rejected.
   3. Special token filtering: Generated informal statements which contain some special tokens (which we think to be a signal of low-quality informalization) are rejected.
   4. Semantic filtering: Sophisticated rules are applied to filter out samples with large semantic gaps with the corresponding math object.
   5. Source filtering: Samples whose all dependencies are in Mathlib 4 are filtered out to ensure the OOD nature of this benchmark.

   Moreover, human supervision is conducted on statements that fail to pass the filters after several sampling attempts. Post-informalization filtering reduces the size of the Con-NF benchmark from 85762 to 961.

2. Thank you for the comment. Human evaluations are conducted on 20 samples of informal-formal pairs. The results indicate that 2 of them show obvious semantic discrepancies, 9 of them contain raw formal identifiers, and none of them failed to translate. We must admit that there is some noise in the benchmark. However, this noise is significantly smaller than the $\ge 25\\%$ noise found in ProofNet[8]. The conclusion of RAutoformalizer's ablative improvement is not influenced because we can observe that RAutoformalizer (-R) and all baselines show similar low accuracy on Con-NF ($\le 4.58\\%$), while RAutoformalizer and RAutoformalizer (+R) have substantial improvements ($\ge 16.86\\%$).

3. This possibility does exist. As in (2.), we find 9 out of 20 samples contain formal identifiers in the informal statements. However, we don't think these formal identifiers might make the evaluation inaccurate or unfair. As the results show, all non-retrieval methods, including RAutoformalizer (-R), have significantly lower accuracy than retrieval-augmented ones ($\ge 10\\%$ absolute improvement).

Weakness6. Human evaluation in comparing RAutoformalizer.

Thank you for your suggestion. We have conducted human evaluation for RAutoformalizer and its ablative variants (-R, +R) on ProofNet and Con-NF, respectively. For each experiment, we evaluate about 100 samples from generated formal statements that passed typecheck. Since the number of type-checked generations from RAutoformalizer (-R) was fewer than 100, we evaluated all of them. Please refer to Appendix A.2.2, where the human-rectified accuracies more strongly supports the ablative improvement of Dependency Retrieval. The comparison between human-annotated equivalence labels and BEq results (as shown in Appendix A.2.1) also show BEq's high-fidelity in alignment with human experts.

Question1. Writing clarity:

• What the notion ‘transformation primitives’ in line 215/ line 221 means?
• How the authors derive the Unidirectional Denitional Implication (2) from equation (1)?
• Ambiguous symbol usage is 's_P' versus 'theorem P'

Sorry for causing your misunderstanding. We have polished our writing in the revision. Here are some explanation of terminology and symbol.

• "Transformation primitives" indeed refers to tactics in Lean (cf. Line 233 "concretize $\mathbb R$ to be the set of all tactics in Lean").
• $T(\boldsymbol s_P | \boldsymbol s_Q, \mathcal R)$ is an oracle function that given a target statement $\boldsymbol s_Q$ and a set of available transformation primitives $\mathcal R$, it applies primitives in $\mathcal R$ and tries to transform $\boldsymbol s_P$ to be definitionally equal to $\boldsymbol s_Q$. If unable to transform (the semantics discrepancy between $\boldsymbol s_p$ and $\boldsymbol s_Q$ are too large or restriction on $\mathcal R$ is too tight), it returns a dummy placeholder. In our implementation, to approximate this oracle function, we prompt a LLM to try to generate a transformation from $\boldsymbol s_P$ to $\boldsymbol s_Q$. More concretely: firstly, assume $\boldsymbol s_Q$ to be true (by closing it with sorry). Then we sample proofs from a few-shot prompted LLM for proofs of $\boldsymbol s_P$ which should use $\boldsymbol s_Q$ and be composed of the tactics in $\mathcal R$.
• "theorem P" refers to the semantics of a theorem, while $\boldsymbol s_P$ refers to its formal statement (or more precisely, one of the elements in the equivalence class of theorem P in human perspective).

Question2. Is the T in (2) an approximation of T in (1)?

No, they mean the same oracle function. Please refer to Answer Point 2 to Question 1 for more explanation.

Question3. Comparison to FormalAlign

An intriguing question. It is worth noting that FormalAlign is also an ICLR submission, and its Arxiv date is later than ICLR submission date, so we will not include it into the main text. However we still provide a comparison to satisfy readers' curiosity (and also ours). Actually, FormalAlign addresses a different task compared to BEq. FormalAlign aims at measuring the alignment between a formal statement and an informal statement, while BEq is used to determine the equivalence between two formal statements. Since FormalAlign's models, training code and inference code are all unavailable, it is quite difficult to evaluate on Human Equivalence Benchmark. Fortunately, the authors have published their synthesized benchmarks, on which we can evaluate BEq. For a fair and comprehensive comparison, many efforts are made, including extracting formal statements from contaminated text (seems due to incorrect response from their GPT calling), identifying imports and namespaces, filtering out statements that do not pass the typecheck, fixing broken tokens stemming from over-augmentation, etc.

Finally, we evaluate BEq($k=4$)'s capabilities to discriminate misaligned statements with their ground-truths (misalignment). The results are as follows.

We find the following error patterns of BEq on this benchmark.

1. (constant, exponent, unpaired) Samples marked error in this category modify natural number constants, but the modified expression has the same value as the original one. This might stem from two reasons.
   1. The modified number reduces to the same value in type conversion. For example, changing {n : ℕ} : (n : ZMod 2) = 0 ↔ Even n to {n : ℕ} : (n : ZMod 2) = 44 ↔ Even n. When Lean instantiates this statement, it firstly converts the natural number $44$ into type ZMod 2, where it reduces to 0 : ZMod 2.
   2. The modified expression is composed of natural numbers and natural number operators, and reduces to the same value. For example, changing (29 * 79 + 31 * 81) % 10 = 2 to (29 * 89 + 31 * 81) % 10 = 2. Because both left hand sides (29 * 79 + 31 * 81) % 10 and (29 * 89 + 31 * 81) % 10 reduces to 2 in Nat literal reduction[6], they are definitionaly equal in Lean.
2. (variable_new) Samples marked error in this category introduce new variables of nonempty types, but they are not incorporated in any hypothesis or the goal statement. For example, changing {p : α → Prop} {x : α} : { x | p x } x ↔ p x to {p : α → Prop} {x k : α} : { x | p x } x ↔ p x. The two statements are equivalent under BEq since they can prove each other by adding a dummy parameter or omitting a parameter. Significantly, if the introduced variables are of some empty type, the modified statements are not equivalent anymore, e.g. (x : Nat) : x + 1 > x are inequivalent to (x : Nat) (hN : False) : x + 1 > x.
3. (equality): Samples marked error in this category change statements like a * b = b ↔ a = 1 to a * b ≠ b ↔ a ≠ 1. These two expressions are trivially logically equivalent.
4. (variable_type): Samples marked error in this category change expressions like ((2 : ℝ)^3 + Real.sqrt 9) to ((2 : ℚ)^3 + Real.sqrt 9). In the latter, (2 : ℚ) is finally converted to 2 : ℝ due to the subsequent addition with (Real.sqrt 9) : ℝ. Therefore, these two expressions are definitionally equal in Lean 4.

Note that this comparison is slightly unfair because these two methods attends to different tasks. And hopefully, the above analysis can inspire the readers.

Question4. Typos.

Many thanks for your careful review. These typos and grammatical issues are fixed in our revision.

[1] Azerbayev, Zhangir, et al. "Proofnet: Autoformalizing and formally proving undergraduate-level mathematics." arXiv preprint arXiv:2302.12433 (2023).

[2] Hendrycks, Dan, et al. "Measuring massive multitask language understanding." arXiv preprint arXiv:2009.03300 (2020).

[3] Hendrycks, Dan, et al. "Measuring mathematical problem solving with the math dataset." arXiv preprint arXiv:2103.03874 (2021).

[4] Murphy, Logan, et al. "Autoformalizing Euclidean Geometry." arXiv preprint arXiv:2405.17216 (2024).

[5] Ying, Huaiyuan, et al. "Lean Workbook: A large-scale Lean problem set formalized from natural language math problems." arXiv preprint arXiv:2406.03847 (2024).

[6] https://ammkrn.github.io/type_checking_in_lean4/type_checking/reduction.html#nat-literal-reduction

[7] https://ammkrn.github.io/type_checking_in_lean4/type_checking/definitional_equality.html#eta-expansion

[8] https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/ProofNet.20fix

[9] Lu, Jianqiao, et al. "Process-driven autoformalization in lean 4." arXiv preprint arXiv:2406.01940 (2024).

Dear Reviewer pPF9,

As the rebuttal deadline approaches, please kindly check the papers' discussion threads and respond to the authors' rebuttals. If you haven't had a chance to respond yet, I’d greatly appreciate your input soon. Your insights are invaluable to the authors and the review process.

Thank you for your effort and support!

Best regards,

Area chair

I thank the authors for their detailed response. Some of the concerns or disagrements remain as follows.

Weakness 1:

W1.1.

It is difficult to evaluate a task of the form y=f(x) without a ground-truth y. All discriminative tasks need to compare predictions with gold ground-truth labels. For generative tasks, to coarsely summarize, there are mainly 4 types of automated evaluation methods: ...

This claim is inaccurate. Generation evaluation metrics do not always require ground-truths. In theory, an ideal evaluation can independently assess a task-specific generation without given ground-truths, as long as the task objective is clearly defined. In practice, model-based "evaluator" or LLM-as-judge can both be reference-free. Listing their limitations such as "uninterpretable" does not mean they can be simply disregarded. Rather, some neural networks or LLMs perform extremely well and robustly in evaluation tasks.

Regarding the paper itself, I have two concerns:

1. I agree that "it should be the benchmark authors' responsibility to ensure the quality of ground-truth". So you can say that it is more like a limitation in methodology rather than a fatal flaw. However, it should be highlighted to the readers Beq's assumption on dataset quality when introducing the metric in the paper (e.g., in section 3). Large-size datasets like Forml4, MMA are not 100% manually verified that the informal and formal statements are perfectly aligned, so they are actually not applicable.

2. The authors mentioned the limitation in L518-522. However, based on the points above, I think the subsequent line is far too absolute and defensive, stating "This limitation is unavoidable throughout the machine learning community".

W1.2.

The logic link from evaluating formal statement equivalence (your metric) to evaluating autoformalization (your motivation) is still missing. E.g.,. L101 says "identify two key limitations in statement autoformalization: the absence of faithful and universal automated evaluation...", while Beq is defined as "a neuralsymbolic equivalence relation between formal statements" (L77). I think more clarification should be made early in the paper to stress your assumption to transform the problem of evaluating informal-formal statement alignment into evaluating equivalence between generated and ground-truth formal statements. Admittedly, it is a mainstream paradigm, so you can make analogies to e.g., the evaluation metrics in cross-lingual machine translation.

Other Weaknesses:

Thank you for the detailed responses, especially the human evaluation results and the inspiring comparison with FormalAlign.

Thank you for your appreciation of this work.

Weakness1. More discussions on BEq are required.

Intuitively, equivalence in human perspective is generally one that can be quickly determined and reasoned. Therefore, the key lies in how to define an equivalence relation that can be demonstrated through brief proofs. Thus, we choose to build BEq by extending definitional equality with limited tactical proofs

Then we analyze BEq's limitation.

BEq is based on three central components, definitional equality, proving and tactic restriction. We separately discuss them and list corresponding potentially controversial points as follows.

• Definitional Equality in Lean is an equivalence relation under a series of conversion rules[1][2]. Some of them are quite intuitive, such as $\beta$-reduction (function application), $\zeta$-reduction (eliminating let-in definitions), $\delta$-reduction (unfolding variable and constant definitions). But some might be controversial:
  1. $\alpha$-conversion, which means two formal statements are equivalent to renaming bound variables. For example, ∀ x : Nat, x + 1 > x is definitionally equivalent to ∀ y : Nat, y + 1 > y.
  2. Nat literal reduction, which reduces all natural numbers as well as related operations to the final result. For example, 1 + 2 + 3 reduces to 6, and 6 also reduces to 6, thus statements 1 + 2 + 3 = 6 and 6 = 6 are definitionally equal.
• Proving.
  • Introducing satisfiable dummy variables. For example, (x : Nat) : x + 1 > x and (x y : Nat) : x + 1 > x are equivalent under BEq since they can prove each other by adding a dummy parameter or omitting a parameter. Significantly, if the introduced variables are unsatisfiable (of some empty type), the modified statements are not equivalent anymore, e.g. (x : Nat) : x + 1 > x is inequivalent to (x : Nat) (hN : False) : x + 1 > x.
  • Some trivial logically equivalent statements do not differentiate in BEq. For example, a * b = b ↔ a = 1 and a * b ≠ b ↔ a ≠ 1.
• Tactic restriction. Tactics must be carefully restricted, with the related experiments detailed in Appendix A.1.

Several failure cases and success cases of BEq can be found in Appendix A.4. We also more comprehensively compare BEq with expert labels in multiple settings in Appendix A.2.1. The results highlight BEq's robustness on Con-NF, reaching nearly 100% accuracies.

Weakness2. More ablative analysis of RAutoformalizer is required.

Intriguing question. We quantitatively analyzed the ablative improvement of dependency retrieval by delving into the error distribution of autoformalizations that do not pass typecheck. We parsed the Lean error messages in the un-typechecked autoformalizations and coarsely classified them into hallucination errors and other errors (detailed taxonomy can be found in Appendix A.2.3). The statistics are reported below:

Results show that both types of errors are reduced by Dependency Retrieval, especially Hallucination errors. This might be one of the root causes of RAutoformalizer's ablative improvement.

This discussion is added to Appendix A.2.3.

Weakness3. Experiments on Dependency-retrieval-augmented ICL LLMs are required.

Sure. Thank you for the constructive suggestion. We have evaluated the performance of augmenting ICL methods by Dependency Retrieval, and the results are as follows. ICL denotes the vanilla in-context learning method, ICL+RA denotes in-context learning with retrieval-augment (retrieve $5$ dependencies for each statement using fine-tuned BGE-M3 described in Sec.4.2) and ICL+RA(+R) denotes in-context learning augmented by ground-truth dependencies.

For GPT-4o, the results meet our expectations: RA consistently improves all metrics on all benchmarks (except BEq@1 on ProofNet), and RA(+R) shows the potential of dependency retrieval. However, for Deepseek-V2.5, RA doesn't work well. We hypothesize this might result from insufficient instruction-following and long-context capabilities of Deepseek-V2.5. The noise in retrieved dependencies degrades autoformalization. But RA (+R) shows significantly better performance as expected.

Thank you again for this interesting idea. This discussion is also added to Appendix A.10.

[1] https://ammkrn.github.io/type_checking_in_lean4/type_checking/definitional_equality.html

[2] https://ammkrn.github.io/type_checking_in_lean4/type_checking/reduction.html#nat-literal-reduction

Dear Reviewer fV7x,

As the rebuttal deadline approaches, please kindly check the papers' discussion threads and respond to the authors' rebuttals. If you haven't had a chance to respond yet, I’d greatly appreciate your input soon. Your insights are invaluable to the authors and the review process.

Thank you for your effort and support!

Best regards,

Area chair

The response satisfactorily addresses my concerns. I thank the authors for their detailed response and effort during the rebuttal!

Good question! In fact, the published version of ProofNet [1] contains 374 informal-formal statement pairs (with 3 from Cambridge-Tripos.lean, which was not mentioned in the original paper). The Lean 4 version of ProofNet we adopted ([2], Table 9 in our submission) also contains 374 problems.

We evaluate on the whole benchmark, where $12.83\\% \approx \frac{48}{374}$

Actually, there was a footnote in the initial submission explaining this issue: "The published version of ProofNet (Azerbayev et al., 2023) consists of 374 informal-formal statement pairs of undergraduate-level mathematics". However, in the subsequent revisions, since we needed to add more important content and to make room for that, we removed this footnote. We apologize for the misunderstandings and confusions caused by this.

[1] https://github.com/zhangir-azerbayev/ProofNet/tree/main/benchmark/benchmark_to_publish/formal

[2] https://github.com/rahul3613/ProofNet-lean4/tree/main/formal