FormalAlign: Automated Alignment Evaluation for Autoformalization

We would like to thank the reviewer for their time and effort in reviewing our paper. We very much appreciate the insightful suggestions. We hereby address the concerns below:

R W1: Use of Synthetic Data for Evaluation

Following your suggestion, we conducted an additional evaluation study using real-world autoformalization errors to validate our approach. We ran Gemini with few-shot prompting as our baseline AF system on a sample of 100 theorems from our test sets, collecting both successful and failed formalization attempts. Three expert Lean users then annotated these formalizations, providing corrections for incorrect ones, yielding 78 correct-incorrect formalization pairs.

The performance comparison between synthetic and real-world validation sets is shown below:

While performance on real-world errors is slightly lower than on synthetic cases, the results demonstrate that our model can effectively detect subtle misalignments in practice.

We are currently exploring two promising directions:

1. Using FormalAlign as a reward model for reinforcement learning to improve AF system outputs
2. Implementing rejection sampling during inference to filter out likely misaligned formalizations

Our preliminary experiments with rejection sampling (threshold = 0.8) show a 15% reduction in misaligned outputs while maintaining 92% of correct formalizations, suggesting this is a promising direction for improving AF system reliability.

We have incorporated this content in the Appendix M section, where it is highlighted in red.

R W2: Baselines and Comparison Strategy

Following your recommendations, we implemented two additional GPT-4 based approaches:

1. Binary Classification: Directly asking GPT-4 to make a true/false judgment about alignment correctness
2. Chain of Thought (CoT): Guiding GPT-4 through step-by-step reasoning about potential discrepancies

Here are our updated experimental results:

As shown in the results, both the binary classification and CoT approaches provide stronger baselines than the original score-based method, with CoT showing particularly notable improvements in precision across all datasets. However, FormalAlign still maintains superior performance, especially in precision, demonstrating the effectiveness of our specialized alignment detection approach. These results not only suggest that improved prompting strategies can enhance GPT-4's performance but also emphasize the significant value of having a dedicated, fine-tuned model for alignment detection. The fact that FormalAlign, a smaller model, achieves results comparable to GPT-4 underscores the effectiveness of our proposed training strategy.

We have incorporated this content in the Appendix I section, where it is highlighted in red.

R Q1:

Thank you for pointing out this confusion. The metrics described in Section 4.2 are indeed intended to be model-agnostic and should be presented independently of any specific implementation. We apologize for the lack of clarity caused by framing them in terms of $V_{\text{align}}$, which may have inadvertently suggested that these metrics are tied to the FormalAlign model.

To clarify, the metrics—Alignment Score (AS), precision, and recall—are general evaluation measures that can be applied to any system performing formalization alignment tasks. For example:

• When evaluating GPT-4 using a binary classification prompt, the Alignment Score is simply 0 or 1 based on whether the pair is deemed aligned.
• For our model, we compute $V_{\text{cer}}$ (as defined in Equation 3), which measures the model’s sequence-level confidence in the formalization, and $V_{\text{sim}}$ (as defined in Equation 4), which assesses the similarity between informal and formal representations. A threshold is then applied to determine alignment.

These metrics are designed to provide a consistent basis for comparison across different systems.

To address your concern, the details of how $V_{\text{align}}$ is computed and its role in our model's inference is relocated to Appendix C.3. We hope these changes can eliminate any ambiguity and provide a clearer distinction between evaluation metrics and model-specific inference processes.

R Q2:

For evaluating GPT and other baseline models, we employ a standardized approach that is independent of our model's internal mechanisms. Specifically, we prompt these models to assign an alignment score on a 1–5 scale for given informal-formal pairs, as detailed in Appendix C2. To facilitate consistent evaluation, the final Alignment Score is normalized to the [0,1] range by dividing by 5. Precision and recall metrics are then calculated based on these normalized scores using a defined threshold. In scenarios where multiple formalizations receive the same top score, one is randomly selected for evaluation to ensure fairness and reproducibility.

Additionally, we conducted experiments using binary classification prompts and chain-of-thought (CoT) prompting strategies to construct diverse baselines. These approaches allow us to perform a thorough comparison across different evaluation methodologies. Details regarding these experiments and their results can be found in our response to R W2.

R Q3:

The second prompt in Appendix C.2 is indeed our evaluation prompt for the FormalAlign model, though its role may not be immediately obvious from its translation-like format. Unlike other approaches that rely on explicit alignment score prompting, our method leverages this prompt to compute alignment scores through our model's combined loss architecture.

As described in lines 214-215 of our paper, our model is trained with a combined loss that captures both sequence-level and representation-level alignment. During the evaluation, this prompt allows us to compute both the certainty score $V_{\text{cer}}$ through equation (3), which measures the model's sequence-level confidence in the formalization, and the similarity score $V_{\text{sim}}$ through equation (4), which captures representation-level alignment. The final alignment score is derived from these computational measures rather than from direct prompting.

This evaluation approach fundamentally differs from prompting-based methods used for baseline models. Instead of asking the model to output an explicit alignment score, we utilize our model's learned representations and certainty measures, enabled by our combined loss training, to compute alignment scores analytically. This allows us to leverage both the autoformalization patterns and representation relationships that our model learned during training. Moreover, we conducted experiments on the autoformalization task, please check R W3 for more details.

We revised Appendix C.2 to better explain how this prompt facilitates our computational evaluation approach and distinguish it from the prompting-based evaluation used for baseline models.

R Q4: To confirm, we do not use synthetically generated misalignment data for training - these examples serve purely as evaluation cases to test model robustness.

R Q5: Regarding the SIM() function in Figure 2, it is indeed equivalent to Cos() - we apologize for this inconsistency in notation and updated the figure to use consistent terminology throughout.

R W3: Rationale for AF Task Exclusion

While our paper primarily focuses on alignment evaluation, we did conduct experiments on the autoformalization task itself, as noted in lines 433-434, "We then explore the effect of incorporating contrastive learning loss on the performance of autoformalization of natural language statements to formal language statements (Appendix F)"

The results are placed in Appendix F due to space constraints. We attach it here for your convince.

As shown in the table below, our combined loss approach demonstrates meaningful improvements in autoformalization performance:

The results show that incorporating contrastive learning alongside cross-entropy loss yields consistent improvements across both FormL4 Basic (+2.22%) and FormL4 Random (+0.14%) datasets. This improvement stems from the model learning more discriminative representations through contrastive learning while maintaining strong generation capabilities via cross-entropy loss.

We chose to focus the main paper on alignment evaluation since it represents our primary technical contribution, but we agree that the autoformalization improvements deserve mention. We will revise our abstract and introduction to more clearly distinguish between these two aspects of our work and better highlight the dual benefits of our approach.

R Typos and Edits

We express our sincere gratitude for your insightful comments. Regarding the presentation issues raised, we carefully incorporate all suggested improvements in our uploaded revision.

I want to thank the authors for the very detailed response, for answering all my questions and the significant additional efforts they have made in experimental evaluations in such a short time period, which is highly commendable.

• Real vs Synthetic data. These results indeed show that performance of your system is not very significantly lower on the real data, which is reassuring. However, my actual suggestion was to use such a dataset for your main evaluation in comparison with baselines. The key question: on real world data such as this, does FormalAlign perform better at alignment evaluation than baselines?
• Including more advanced baselines. These results indeed show that the stronger baselines perform better and reduce the gap with your system, but I agree the gap is still significant especially in terms of precision (note however: do not bold your AS score of 66.39 for FormalL4-Random since CoT performs better with 67.24). I would say that these stronger baselines should be included in the main paper results rather than appendix as they are more important comparisons than the numbering-based prompt.
• Performance on the Autoformalization task. This remains my main concern. These results look very incremental with an average improvement of only 1.18% on these two datasets (and only 0.14% on one of them). Can we see these numbers on the other datasets (MiniF2F-Valid and MiniF2F-Test)? I am curious if they can be better or if they may actually show regressions in these other datasets (where alignment results were weaker)? From my understanding, improvement to AF is the real ultimate goal of having an alignment evaluation technique isn’t it? So this should be the ultimate test of how well the technique is working. If even in comparison to your own base model the results are so incremental, that is concerning. In general, one may expect a strong argument that here is an AF system that has X% accuracy, and when we extend it with our alignment evaluation technique it improves it’s accuracy significantly by Y% – do you have such a summary result that is more significant improvement than the 1.18% above? And if it is more significant on another AF system then would be good to understand why it is so much better than on your own AF model. This seems to me to be an important question in showing the ultimate value of your technique towards the AF task for which it is meant.

We would like to thank the reviewer for their time and effort in reviewing our paper. We very much appreciate the insightful suggestions. We hereby address the concerns below:

R W1: Broader Significance and Formal Definition

Thank you for this valuable feedback. We agree that better contextualizing autoformalization's broader significance and providing a formal definition would enhance the paper's accessibility and impact.

We propose adding the following formal definition of autoformalization alignment:

Given a natural language statement N and its formalization F, assuming F is verified as syntactically valid by the formal language compiler, alignment A(N, F) is defined as a binary relation where A(N, F) = 1 if and only if:

1. F preserves all mathematical constraints specified in N
2. F maintains the same logical relationships between components as expressed in N
3. F does not introduce additional constraints not present in N

We agree that better contextualizing the broader significance of autoformalization would enhance the paper's accessibility and impact. We propose adding a comprehensive discussion of why autoformalization is a crucial research direction:

Autoformalization - the automated conversion of natural language mathematics into formal languages - serves as a critical bridge between human mathematical knowledge and machine-verifiable formal systems. Its significance extends across multiple domains:

1. Software Engineering and Verification

• Enables automated translation of natural language specifications into formal verification properties
• Reduces the manual effort required to formally specify system requirements
• Helps detect ambiguities and inconsistencies between informal specifications and implementations

2. Mathematical Knowledge Management

• Facilitates the preservation and verification of mathematical knowledge by converting informal mathematics into machine-checkable formats
• Enables systematic organization and cross-referencing of mathematical content
• Supports automated reasoning systems by expanding available formal mathematical content

3. Automated Reasoning Research

• Expands the scope of automated theorem provers by allowing them to work with natural language inputs
• Enables hybrid reasoning systems that combine formal and informal mathematical knowledge
• Accelerates the development of more powerful mathematical reasoning systems with feedback from formal compilers.

We expanded this discussion in Appendix N in our revised paper to better articulate how advances in autoformalization can benefit these broader research communities.

R W2: Running Example Concerns

Thank you for these astute observations about our running example. You raise valid points about both the detectability through proof checking and the generation probability.

While this specific misalignment can indeed be detected through proof checking (as demonstrated by your counterexample), we chose it as a running example primarily for its clarity in illustrating our approach. However, we acknowledge that a more nuanced example might better demonstrate the unique value of our alignment detection method.

In practice, many real-world misalignments are more subtle and challenging to detect through proof-checking alone:

1. Type-level misalignments where statements are well-typed but semantically misaligned
2. Cases where the proof search is computationally expensive or intractable
3. Misalignments in assumptions or preconditions that don't affect provability
4. Situations where formal statements are provable but don't capture the intended informal meaning

For instance, consider cases where variables are accidentally swapped or constraints are slightly modified - these might still result in provable statements that don't match the informal intent. Our alignment detection approach can identify such mismatches more efficiently than proof search, especially for complex theorems where automated proof finding is challenging.

R W3: Dataset Construction Validity

To further validate our approach in real-world cases, we few-shot prompted Gemini as our autoformalization baseline on a sample of 100 theorems from our test sets. Three expert Lean users annotated these formalizations, providing corrections for misaligned ones, yielding 78 aligned-misaligned formalization pairs. The performance comparison between synthetic and real-world validation sets is shown below:

While performance on real-world errors is slightly lower than on synthetic cases, the strong results demonstrate that our model can effectively detect subtle misalignments in practice.

Our dataset construction method is designed with the following considerations combined, balancing between practicability, coverage, and analysis:

1. Automated ground truth instead of expensive and time-consuming manual labeling by human experts
2. Provides systematic coverage across different error types
3. Enables precise and thorough analysis of model capabilities for various misalignment patterns

We view our synthetic dataset as complementary to real-world examples:

• Synthetic data provides comprehensive coverage of potential error types
• Real LLM errors help validate practical effectiveness
• A combined approach ensures both breadth and real-world applicability

We have incorporated this content in the Appendix M section, where it is highlighted in red.

We fully agree that with more human expert resources, incorporating more real-world LLM errors into our training data could further improve our model's practical utility. In future work, we plan to create a hybrid dataset that combines synthetic mutations with collected LLM autoformalization errors (annotated with human experts) to provide both comprehensive coverage and realistic error patterns.

R W4: Reference Section Improvements

Thank you for catching the duplicate citation and suggesting these relevant works. Indeed, these papers represent important contributions to autoformalization that deserve discussion.

$1$ tackles autoformalization in the specific domain of Euclidean geometry, where they develop a neuro-symbolic framework that addresses the unique challenge of diagram-dependent proofs. Their approach differs from FormalAlign by focusing on domain-specific autoformalization rather than alignment evaluation, using theorem provers to fill in diagrammatic information that makes formalization easier for language models. While both papers aim to improve autoformalization, Murphy's work complements FormalAlign by providing domain-specific solutions that could potentially benefit from FormalAlign's alignment evaluation capabilities.

$2$ addresses the gap between pass@1 and pass@k accuracies in LLM-generated formalizations by introducing a framework that scores and selects the best result from multiple candidates using symbolic equivalence and semantic consistency. While both Li's work and FormalAlign aim to improve autoformalization quality, they approach it from different angles - Li focuses on improving candidate selection through verification methods, while FormalAlign develops an automated evaluation framework for alignment. Their methods could be complementary, with Li's verification approach potentially enhancing FormalAlign's alignment evaluation capabilities.

$3$ focuses on improving consistency in large-scale autoformalization for mathematical libraries through three mechanisms: most-similar retrieval augmented generation, denoising steps, and auto-correction with syntax error feedback. Their work differs from FormalAlign by emphasizing the practical challenges of building consistent mathematical libraries, while FormalAlign focuses on the fundamental problem of evaluating alignment between informal and formal statements. Zhang's approach to consistency could potentially be integrated with FormalAlign's alignment evaluation framework to create more robust autoformalization systems for large-scale applications.

We revised our reference section to remove the duplicate Deepseekmath citation and discuss these three relevant papers in the Appendix B.

Thank you for helping us improve the completeness and accuracy of our literature review.

$1$ Murphy, Logan, et al. "Autoformalizing Euclidean Geometry." ICML, 2024

$2$ Li, Zenan, et al. "Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency." NeurIPS, 2024.

$3$ Zhang, Lan, et al. "Consistent Autoformalization for Constructing Mathematical Libraries." EMNLP, 2024.

R Q1: Extending FormalAlign to Proof Autoformalization

Thank you for this interesting question about extending FormalAlign to proof autoformalization. The primary challenge stems from the structural mismatch between formal proofs and their natural language counterparts. In Lean 4, proofs often rely on specialized tactics and proof environments that have no direct natural language equivalents.

This mismatch manifests in two key ways:

1. Tactic-based reasoning: Lean commands like linarith encode complex mathematical reasoning in single operations, while natural language proofs typically express these steps through multiple sentences using informal reasoning. This many-to-one mapping makes alignment particularly challenging.
2. Environment dependencies: Formal proofs often reference pre-defined lemmas and proof environments specific to Lean 4. These formal structures may lack clear natural language counterparts that non-experts can understand, and the translation would require extensive "unpacking" of these formal constructs.

While Lean 4's compiler provides automated and reliable correctness checking for the logical validity of formal proofs, this verification differs from semantic alignment. Our alignment framework could help validate whether a formal proof captures the intended reasoning steps from its natural language counterpart. However, achieving reliable end-to-end proof alignment would require significant extensions to handle the fundamental structural and semantic disparities between formal and natural language proofs, even with Lean's strong verification capabilities.

R Q2: Combining Certainty and Similarity Scores

Thank you for this question about our score combination strategy. While the certainty and similarity scores indeed operate on different scales, we chose to average (weight=0.5) to place balanced emphasis on both metrics during inference. To validate this design choice, we conducted an ablation study testing different weighting schemes. We note that the weight for similarity is 1 - Weight (Certainty):

The results demonstrate that a balanced weighting (0.5/0.5) achieves optimal performance across both datasets. We observe that heavily favoring either score (weights of 0.9/0.1 or 0.1/0.9) leads to decreased performance, suggesting that both metrics contribute complementary information to the alignment decision. The relatively small performance variations (within ~2 percentage points) also indicate that our approach is fairly robust to weight selection, though balanced weighting consistently yields the best results.

R Q3: Evidence for Reducing Manual Verification

Thank you for raising this important point about quantitative evidence. We have conducted several experiments to validate FormalAlign's practical impact on reducing manual verification needs (as detailed in R W3). In our real-world validation study, we applied Gemini to 100 theorems, yielding 78 formalization pairs, where our system achieved 83.5% accuracy in detecting misalignments. This suggests a potential ~80% reduction in manual verification needs for typical autoformalization outputs.

When integrated into an autoformalization pipeline with a confidence threshold of 0.8, FormalAlign successfully filtered out ~85% of incorrect formalizations while maintaining 92% of correct formalizations, reducing manual review time by approximately 75% compared to the baseline. These quantitative results demonstrate a significant practical impact on reducing verification workload while preserving high reliability.

Looking forward, we see significant potential for further improvements through incorporating FormalAlign directly into the autoformalization pipeline, either as a reward model for reinforcement learning to improve AF system outputs or through rejection sampling during inference to filter out likely misaligned formalizations. We plan to validate these approaches through larger-scale deployments and more diverse use cases.

We would like to thank the reviewer for their time and effort in reviewing our paper. We very much appreciate the insightful suggestions. We hereby address the concerns below:

R W1: Fixed Alignment Score Threshold and P-R Curves & Q1: P-R Curves and Performance at P@R=0.9

Thank you for these valuable comments regarding our presentation of alignment score thresholds and P-R curves. To address this, we have conducted additional experiments and generated comprehensive P-R curves. These curves are presented in Figure 4 (Appendix K) of our revised paper, providing a detailed view of model performance across varying alignment score thresholds. Below, we summarize key observations and enhancements:

When evaluating FormalAlign at GPT-4's recall level (≈0.9), our model achieves:

• FormL4-Basic: 88% precision at 89% recall
• FormL4-Random: 83% precision at 90% recall
• MiniF2F-Valid: 45% precision at 91% recall
• MiniF2F-Test: 48% precision at 88% recall

The P-R curves reveal several interesting characteristics of FormalAlign's behavior:

1. On FormL4 datasets, precision remains robust (>75%) even at high recall levels, demonstrating strong alignment capabilities for structured formal mathematics.
2. For MiniF2F datasets, we observe a more pronounced precision drop at higher recall points, reflecting the increased complexity of these problems.

R W2: Non-Uniform Distribution of Misalignment Types & Q2: Non-Uniform Strategy Application for Negative Examples

Thank you for these thoughtful observations about the non-uniform distribution of misalignment strategies. This distribution pattern is actually intentional in our design, though we recognize it warrants careful explanation.

The non-uniform application of strategies reflects two key aspects of our approach. First, it accounts for the inherent constraints and characteristics of mathematical contexts in different datasets. For example, "Constant Modification" appears more frequently in miniF2F datasets (~31%) compared to FormL4-Basic (~11%) because miniF2F contains more theorems with explicit numerical constants that can be meaningfully modified. Similarly, the "Change of Variable Type" strategy varies across datasets (from ~14% in FormL4-Basic to ~18% in miniF2F-Valid) because its applicability depends heavily on the theorem's type constraints – it's only meaningful when changing the variable type would affect the theorem's validity, such as changing from ℤ to ℝ in problems requiring integer solutions.

This varied distribution of strategy application serves a dual purpose: it ensures our negative examples remain mathematically meaningful while also testing FormalAlign's robustness against a diverse range of misalignment types. Rather than creating artificial misalignments that might be too obvious or mathematically invalid, this approach helps us assess how well the model can generalize across different types of errors, from simple modifications to more complex transformations.

In our future experiments, we plan to explore more uniform sampling strategies to provide a clearer assessment of the model's performance across balanced misalignment types. We will also clarify in the paper that our current approach prioritized covering a wide spectrum of mathematically meaningful misalignment scenarios rather than achieving uniform distribution.

R W3: Model Performance Breakdown by Misalignment Type & Q3: Per-Misalignment-Type Data for Case Study and LLM-as-Judge Results

We agree that providing per-misalignment-type data for both the case study and the LLM-as-judge results would be valuable for understanding how FormalAlign performs on different types of misalignments. To provide a comprehensive understanding of the strengths and limitations of our proposed method relative to human judgment and baseline LLM performance, we conducted an in-depth analysis focusing on performance across various misalignment types. The detailed results are shown below:

Easiest and Most Challenging Misalignment Types:

• Random Pairing Misalignments: Performance was highest across all methods for random pairings, with human experts achieving 85.9%, our method at 72.4%, and GPT-4o at 54.0%. This finding aligns with expectations, as random pairings involve significant structural or contextual discrepancies that are more readily identifiable.
• Subtle Modifications (Constant and Exponent Changes): These types of misalignments proved to be the most difficult to detect, evidenced by the lowest scores across all evaluated methods. Human performance dropped to 75.2% for constant changes and 73.8% for exponent modifications, with corresponding lower scores for our method and GPT-4o. This highlights the need for more sophisticated mechanisms capable of identifying nuanced numerical and syntactic changes in mathematical reasoning.

Performance Gaps:

• Human vs. Our Method: Human evaluators consistently outperformed our method by approximately 15-20 percentage points across all misalignment types. This consistent gap underscores the advantage of human intuition and mathematical insight, particularly in recognizing subtle logical shifts and contextual meanings that automated methods still struggle to replicate.
• Our Method vs. GPT-4o: Our method maintained a clear advantage over GPT-4o, with a performance margin of 15-20 percentage points across all misalignment types. This gap indicates that the enhancements in our approach, including targeted modeling of structural and semantic relationships, yield significant improvements over standard LLM capabilities.

Our method shows marked improvement in handling structural changes, such as equality modifications and random pairings, compared to more local, subtle modifications. This suggests that while the model is adept at identifying broader, more evident shifts in alignment, fine-grained detection still poses a challenge. The findings suggest future enhancements should prioritize the model’s ability to detect minute variations, such as constant and exponent changes, potentially through integrating deeper mathematical reasoning frameworks or improved training with synthetic examples that emphasize such subtleties.

We have incorporated this content in the Appendix L section, where it is highlighted in red.

R W1: Misalignment Strategy "Change of Variable Type"

We appreciate this insightful observation about variable type changes. You are correct that changing from real numbers (ℝ) to rational numbers (ℚ) may not constitute misalignment since both types can represent the same mathematical concepts in many cases. This prompted us to revise our examples and strengthen our screening criteria for type-based misalignments.

Consider instead this illustrative example from our dataset:

-- Original theorem
theorem mathd_algebra_478
  (b h v : ℝ)
  (h₀ : 0 < b ∧ 0 < h ∧ 0 < v)
  (h₁ : v = 1/3 * (b * h))
  (h₂ : b = 30)
  (h₃ : h = 13/2) :
  v = 65 :=

-- Misaligned version
theorem mathd_algebra_478
  (b h v : ℤ)
  (h₀ : 0 < b ∧ 0 < h ∧ 0 < v)
  (h₁ : v = 1/3 * (b * h))
  (h₂ : b = 30)
  (h₃ : h = 13/2) :
  v = 65 :=

This example demonstrates misalignment because the theorem relies on fractional values (e.g., $h = \frac{13}{2}$) and calculations ($v = \frac{1}{3} \cdot (b \cdot h)$) that cannot be represented in the integer domain ($\mathbb{Z}$). Such arithmetic operations inherently require non-integer values, leading to a semantic contradiction where the original mathematical meaning is lost when confined to integers.

In our empirical analysis of 100 sampled cases, potentially ambiguous scenarios, such as conversions from $\mathbb{R}$ to $\mathbb{Q}$, were observed in only 3% of samples. Our revised screening process effectively filters these edge cases, ensuring focus on changes that result in true mathematical contradictions.

In the revised paper, we have updated this case and plan to further improve our misalignment datasets by replacing the $\mathbb{R}/\mathbb{Q}$ example with the $\mathbb{R}/\mathbb{Z}$ case presented above, which more clearly illustrates misalignment. Additionally, we will clarify our criteria for identifying true misalignments, particularly emphasizing cases where type constraints directly alter the mathematical meaning.

These updates aim to provide a more thorough and transparent discussion, enhancing both the clarity of our presentation and the robustness of our analysis.

R W2: Applicability of Misalignment Strategies to Advanced Mathematics

We would like to address this concern from several perspectives:

We applied our misalignment strategies to generate adversarial examples in advanced mathematical domains (MiniF2F), demonstrating their effectiveness beyond basic arithmetic. Specifically, MiniF2F includes problems from mathematical olympiads (AMC, AIME, IMO) and undergraduate-level mathematics. These problems encompass sophisticated mathematical reasoning across domains like abstract algebra, real analysis, and number theory, where our strategies successfully generated meaningful misalignments to test model robustness.

Furthermore, we acknowledge that our current strategies might have limited applicability to highly abstract mathematical domains (e.g., pure logic, set theory, and quantifier-heavy statements). However, contextualizing our work within the current capabilities of language models in mathematical reasoning, we believe the current dataset choice and its complexity level are sufficient. Even state-of-the-art models struggle with theorem proving, achieving less than 50% pass@1 rates on the MiniF2F test sets. Extending our framework to handle more sophisticated mathematical domains is an important direction for future work.

R W3: Ablation Study on Loss Function Components (LCE vs LCL)

Our current approach employs equal weighting between these components, as outlined in our paper (lines 214-215): "We train an alignment-aware FormalAlign model by minimizing a combined loss, enabling it to benefit from both the sequence alignment inherent in the autoformalization and the representation alignment facilitated by the contrastive learning process." To validate this design choice, we conducted a comprehensive ablation study varying the relative weights between LCE and LCL:

Note: To ensure fair comparison, we normalize to keep total loss magnitude across different weight ratios.

The ablation results strongly support our original design choice of balanced weighting. The balanced 1:1 ratio consistently outperforms other weightings across all metrics, achieving optimal trade-offs between sequence-level and representation-level alignment. Performance drops substantially when moving too far in either direction (4:1 or 1:4), confirming that both components play essential, complementary roles in robust autoformalization - LCE ensures accurate sequence-level alignment for precise formalization, while LCL maintains semantic coherence through contrastive learning.

R W4: Ablation Experiment and Metric Bias

To directly address this concern, we conducted comprehensive experiments comparing models trained with individual loss functions, i.e., training each model with their corresponding metrics as optimization objectives (certainty scores, similarity scores) against our combined approach:

The results clearly demonstrate the superiority of our combined loss approach. Models trained with individual loss functions show significantly lower performance - the cross-entropy loss (LCE) model achieves limited performance when evaluated with certainty scores, while the contrastive loss (LCL) model struggles when assessed using similarity scores. In contrast, our combined approach consistently outperforms both individual methods across all datasets.

This empirical evidence aligns with our theoretical motivation: the combined loss structure was intentionally designed to capture complementary aspects of alignment - the sequence-level patterns inherent in autoformalization and the representation-level relationships revealed through contrastive learning (as noted in lines 214-215). Rather than creating conflicting objectives, these components work together to develop a more comprehensive understanding of the alignment task.

Our previous ablation studies further support this design choice. The ablation in Section 5.2 examines the necessity of the combined loss structure itself, while Section 5.3 specifically investigates potential metric bias through a systematic evaluation using individual components of our alignment-selection metric. The results in Table 6 demonstrate that models trained with the combined loss maintain strong performance even when evaluated solely on certainty scores, indicating no degradation of language generation capabilities. Additionally, the superior performance of the combined metric across all datasets suggests it successfully integrates both language-based and representation-level information, rather than reflecting any inherent bias in the evaluation approach.

We have incorporated this content into the revised version, specifically in the Appendix I section, where it is highlighted in red.

R Q1: Splitting the Alignment-Checking Baseline for GPT-4 into Two Steps

Thank you for your suggestion to split the alignment-checking process for GPT-4 into two steps: back-translation followed by a natural language alignment check. We tested this approach, referred to as "Two-Phase Alignment Checking (Two-Phase),". The "GPT-4 (Score)" baseline refers to the original method using the prompt listed in Appendix C.2. The results are shown in the table below:

The "Two-Phase Alignment Checking" method performs slightly better than GPT-4's baseline approach. While this method does encourage GPT-4 to capture more details during back-translation, we identified several weaknesses that might outweigh its potential benefits:

1. Splitting the task into back-translation and alignment-checking phases requires consistency across three representations: the original formal statement, the back-translated natural language, and the final alignment judgment. This decoupling introduces opportunities for error propagation, as inaccuracies in back-translation may compromise the subsequent alignment stage.
2. Moreover, the two-step approach adds overhead, both in computational time and model interaction complexity.

We have incorporated this content in the Appendix J section, where it is highlighted in red.

Dear Reviewer Y3AS,

Thank you for your detailed feedback regarding our paper's technical methodology and experimental evaluations. We have carefully considered your points and made several improvements to address them.

1. Regarding the misalignment strategy "Change of Variable Type," we acknowledge your observation about the ℝ to ℚ conversion example. We have revised our approach to focus on more definitive cases of misalignment, such as ℝ to ℤ conversions where fractional values are essential to the theorem's meaning. Our empirical analysis shows that potentially ambiguous type changes occurred in only 3% of samples, and we have updated our screening process to filter these edge cases.

2. On the concern about misalignment strategies' applicability to advanced mathematics, while we acknowledge certain limitations with pure logic and set theory, our framework has demonstrated effectiveness on MiniF2F's olympiad-level problems. Our ablation studies have revealed optimal performance with balanced (1:1) weighting between LCE and LCL losses, showing significant improvements over individually trained models across all datasets.

3. For your suggested two-phase GPT-4 baseline, we implemented and tested this approach. While it showed slight improvements over the original baseline, we found that the decoupled process introduced potential error propagation issues and increased computational overhead.

We would appreciate your thoughts on whether these clarifications address your concerns, or if any points need further elaboration. Thank you for your time and consideration.

Best regards,

Authors of Paper Submission 1997