FormalAlign: Automated Alignment Evaluation for Autoformalization
Authors: Jianqiao Lu
Yingjia Wan
Yinya Huang
Jing Xiong
Zhengying Liu
Zhijiang Guo
Venue: ICLR 2025 Poster (2025)
Keywords: Large Language models
Autoformalization
Lean 4
Formal Math
AI for Math
Primary area: applications to computer vision, audio, language, and other modalities
TL;DR: FormalAlign is a framework that automatically evaluates the alignment between informal and formal mathematical proofs, significantly improving performance and reducing reliance on manual verification.

Abstract: Autoformalization aims to convert informal mathematical proofs into machine-verifiable formats, bridging the gap between natural and formal languages. However, ensuring semantic alignment between the informal and formalized statements remains challenging. Existing approaches heavily rely on manual verification, hindering scalability. To address this, we introduce FormalAlign, a framework for automatically evaluating the alignment between natural and formal languages in autoformalization. FormalAlign trains on both the autoformalization sequence generation task and the representational alignment between input and output, employing a dual loss that combines a pair of mutually enhancing autoformalization and alignment tasks. Evaluated across four benchmarks augmented by our proposed misalignment strategies, FormalAlign demonstrates superior performance. In our experiments, FormalAlign outperforms GPT-4, achieving an Alignment-Selection Score 11.58\% higher on \forml-Basic (99.21\% vs. 88.91\%) and 3.19\% higher on MiniF2F-Valid (66.39\% vs. 64.34\%). This effective alignment evaluation significantly reduces the need for manual verification.

Published as a conference paper at ICLR 2025
FORMALALIGN: AUTOMATED ALIGNMENT EVALUATION FOR AUTOFORMALIZATION
Jianqiao Lu'r, Yingjaa Wan Yinya " Xiong', Zhengying Liu", Zhijiang Guo The University of Hong Kong University of Cambridge
3 Huawei Noah's ' Ark Lab *ETH Zurich
"Hong Kong University of Science and Technology (Guangzhou) jqluêcs. hku. hk, yingji awan alisa gmail.com, zhijiangguo@hkee @ whuus-gzzedu.cn
ABSTRACT
Autoformalization aims to convert informal mathematical proofs into machine- verifiable formats, bridging the gap between natural and formal languages. How- ever, ensuring semantic alignment between the informal and formalized statements remains challenging. Existing approaches heavily rely on manual verification, hindering scalability. To address this, introduce FORMALALIGN, the first auto- mated framework designed for evaluating the alignment between natural and formal languages in autoformalization. FORMALAALIGN trains on both the autoformaliza- tion sequence generation task and the representational alignment between input and output, employing a dual loss that combines pair of mutually enhancing auto- formalization and alignment tasks. Evaluated across four benchmarks augmented by our proposed misalignment strategies, FORMALALIGN demonstrates superior performance. In our experiments, FORMALALIGN outperforms GPT-4, achiev- ing an Alignment-Selection Score 11. 1,8%% higher on FormL Basic (99.21 vs. 88.91 %) and 3. 3.19% higher MiniF2F- Valid (66.39% vs. 64.34%). This effective alignment evaluation significantly reduces the need for manual verification.
INTRODUCTION
Autoformalization is the task of automatically converting informal theorems and proofs into machine-
verifiable formats (Wang et al. 2018; (Szegdyy 2020; Wu et al. 2022 Jiang al., 2023cb.
bridges the gap between natural and formal languages, leveraging the strengths of both: natural language carries extensive logical reasoning and human knowledge. In contrast, formal language enables rigorous verification and proof, ensuring accurate and clear reasoning (Kaliszyk et al. 2014). While promising, autoformalization faces challenges ensuring semantic alignment between these languages. The availability of fully formalized and computer-checker content is limited (Kaliszyk ct al. 2017). This lack of alignment information hinders the development of robust autoformalization models ls (Bansal & Szegedy 2020).
Current evaluation methods for autoformalization (Jiang et al. 2023c Huang et al. 2024: Lu et al.
2024) focus solely logical validity, which can be easily verified by formal language compilers (e.g., the Lean 4 compile Another direct but suboptimal evaluation resort to surface form matching
via BLEU (Papineni et al. 2002), which is widely used by recent works (Wu et al.. 2022 Diang et al.
2023c Azerbayev et al. 2023a) but struggles with semantic alignment or logical equivalence (Li
al. 2024b).
Take the case in Figure as an example, to correctly translate the natural language proof target into a Lean 4 statement, first, the variables for the objects "ligs", "lags". and "lugs" should be included and real numbers greater than zero. Then, the two equations should be translated into two corresponding hypotheses h and h2. Finally, the proof target "How many ligs are equivalent 80 lugs? Show that 63" needs to be formalized into "63 a = 80 c", which is failed in this case by omitting the
"Leading co-authors with equal contribution.
1 'Corresponding Author.
Details of the compiler are provided in Appendix

---

Published as a conference paper at ICLR 2025
Natural Language
On Larky, ligs lage, lags lugs. How many ligs equivalent to lugs?
Autoformal zation
Misaligned Formal Language
matho algebra_ 398 (a (he
(ha b):
LENN
BLEU
FormalAlign
Erro mestage: None
BLEU score 0,9022
Aligner score 0.5938
Valge (Ver Vay (02474 -054442 0.598
Concuusion Legically volid.
Conclusion: Alignad.
Conclusion Misaligned
Miselignment undetected
Misalignment undetected
Miselignment detected!
comparison of current methods and FORMALALIGN evaluating autoformalization. The formal statement is misaligned with the natural language statement: incorrectly ends with 80 x 63 when the aligned equation should be 63 80 Current methods only verify the surface-form integrity of the autoformalized sequence via BLEU or by passing it to a formal language compiler, while FORMALALION successfully detects the semantic misalignment of the autoformalized statement with the informal sequence.
Figure 1:
pronounced "ligs". However, because the incorrectly translated "80 c 63" is logically valid in Lean 4 and similar to the ground truth in surface form, is flawless to a theorem compiler or the BLEU score. The semantic misalignment of lacking "lig" the equation is undetected. Moreover, due to its elusive nature. this misalignment is often challenging to detect, even with methods like BERTscore (Zhang et al. 2020b), which are designed to assess semantic similarity, Therefore, robust and effective approach to Automated Alignment Evaluation (AAE) is urgently needed.
To bridge this gap, we introduce the FORMALALIGN framework, which assesses the alignment between informal and formal languages during autoformalization. As demonstrated in Figure FOR- MALALIGN learns both the sequence generation task autoformalization (top half in Figure and the representational alignment (bottom half in Figure 2) between input and output. FORMALALIGN jointly trains the pair of mutually enhancing tasks. This encourages the model to generate similar embeddings for corresponding pairs and distinct embeddings for non-corresponding pairs, enhancing its ability to differentiate between aligned and misaligned sequences, as the case in Figure I
We evaluate FORMALALIGN four benchmarks sourced from MiniF2F (Zheng et 2022b) and F4rmL4 (Lu et al. 2024). Compared with GPT-4, FORMALA FORMALALIGN ALIGN achieves a substantially higher precision score across these datasets, e.g., in the FormL4-Basi dataset (93.659) vs. 26.33%). also outperforms GPT-4 in alignment-selecteo 99.21% % vs. 88.91% 1 in BommL-BBasie and 66.39% vs. 64.34% in MiniF2F-Vais Valid. Extensive experi- mental results demonstrate the effectiveness of FORMALALIGN, significantly reducing the reliance on manual verification. Our contributions are summarized as follows:
score across multiple datasets, including a remarkable
To the best of our knowledge, we design the first method for automatically evaluating alignment in autoformalization. reducing the reliance for manual verification.
We develop a combined loss framework that simultancously enhances a model for both autoformalization and semantic alignment.
Extensive experiments on established autoformalization benchmarks demonstrate the effec- tiveness and robustness of FORMALALIGN.
RELATED WORKS
Autoformalization Early efforts (Wang et al., 2018: Bansal Szegedy 2020) employed encoder-
decoder neural networks translate informal statements into formal languages like Mizar (Rudnicki
2

---

Published as a conference paper at ICLR 2025
Natural [NLg)
Language (PLi)
Mly:
Fly.
"The and vector is equal the angle between vector and Vector
Autoformalization Task
angle y angle y
Cross Entropy Loss (Cee)
Hidden States
(C)
S,RL MLo
2,FL
2,860
Alignment Task Contrastive Loss
(Cct)
RyNial
Hight toh
Figure 2: An overview of FORMALALIGN, which combines the cross cross-entropy loss in sequence autoformalization and the contrastive loss hidden states enhance the informal-formal alignment.
1992). HOL Light (Harrison, 1996). and Coq (Barras et al.
1997). The advent of LLMs (Chen
al. 2021 Chowdhery al. 2022, Lewkowyez et al. 2022 Achiam et al.) 2023) enhances the
capabilities of autoformalization (W et al.] 2002 Jiang et al. 2023a). Some approaches directly
prompt LLMs (Wu et al. 2022 Jiang al., 2023c Zhao et al. 2023 Diang al. 2023a to
translate mathematical problems into formal languages like Isabelle (Wenzel et al.
2008 and
Lean (de Moura al. 2015). On the other hand, training or fine-tuning LLMs with paired formal- informal data (Azerbayev et al. 2023b Ying et al. 2024; Shao et al. 2024 Lu et al. 2024) garner increasing attention for its effectiveness in enhaneing LLMs performance in autoformalization. The evaluation of autoformalization primarily depends on manually verifying the alignment between informal and formalized statements (Li al. 2024b). There is pressing need for an efficient and less labor-intensive method for automated autoformalization alignment.
Text Generation Evaluation The challenges of automatically evaluating natural language gener- ation tasks grow as the difficulty of tasks increases. N-gram-based metrics (Papineni et al. 2002
Lin 2004 resort to surface-form matching, which has been beneficial for evaluation tasks with
specific and static references such as image-captioning (Young et al. 2014 Chen et al. 2013 and text summarization (Young et al.) 2014 Cohan al. 2018). Semantics rarely considered until embedding-based metrics emerge, especially metrics leveraging the evolving pre-trained language models (Zhang al. [2020a] Yuan al. 2021 Qin al. 2023) and LLMs (Xu al., 2023 Jiang
et al. 2023d Liu el al.) (202bb). The growth of LLMs continues empowering parameter- based metries for vancee evaluation such as multi-agent (Chan et al. (203)) and multi-aspect (Liu et al.
2023a). The other line of work fine-tunee language models for scoring (ee et al., 2023] Kim et al.
2023 Wang al., 2023), labeling (Gekhman al. 2023 Yue et al. 2023 Kim al. 2023 Liu
et al. 2023a), text probability calculation (Gekhman et al. 2023 Yue et al. 2023) Kim et al. 2023
Liu et al. 2023a), or comparison (Wang et al. 2023 Zheng et al. 2023 to enhance and adjust for evaluation targets. In this paper, propose automated evaluator for the challenging yet under-explored autoformalization evaluation that requires both rigorous logical validity and aligned semantics between the natural- forrmll pair. To this end, we fine-tune LLMs via joint autoformalization generation and representational alignment tasks and obtain logically and semantically empowered aligner.
3

---

Published as a conference paper at ICLR 2025
3 METHOD: FORMALALIGN
In this section, we introduce the FORMALALIGN framework, designed to train a FORMALALIGN model that can evaluate the alignment between natural (informal) and formal languages during autoformalization (detailed definition in Appendix[M] As illustrated in Figure 2 FORMALALIGN combines two types of loss the training process: one for the sequence generation task of autofor- malization and another for the representational alignment between input and output. This dual loss framework mutually enhances autoformalization and alignment.
3.1 NOTATIONS
We first define the notations follows:
NL; The jth informal input sequence in a batch, NL, = (NL1,,, NL, NL,m,) where m is the sequence length of NL,
FL; The zth ground-truth formal output sequence in a batch, FL; 1FL,,1, FL, 1......... ..... FL,,)) where n is the sequence length FL;
Po (FL,, [F,,,, NL,): : The probability of predicting the jth token the formal sequence FL, by the auto regresseees language model with parameters ø given the previous tokens FL,,es in the formal sequence and the informal input NL,
Za(NL,): The hidden state from the auto uugo-regreesive language model with parameters e for the final position in the 2th informal input NL; i.c.. NL
(L.) The hidden state from the rugo-regressive language model with parameters é for the final position in the ith ground-truth formal output FL, i.e. FL,,, conditioned on the paired 7th informal input NL,
(FL INL;) The hidden state from the auto-regressive language model with parameters d for the final position in the (t²) unpaired formal output FL, in a batch, conditioned on the jth informal input NL; cos(-, The cosine similarity between embeddings, defined as cos(r,y)
2-1
N: The batch size.
3.2 TRAINING
Autoformalization Task For the autoformalization task of converting an informal input sequence NL, to a formal output sequence FL,, we use the cross-entropy loss function. This function measures the error in predicting each word in the formal sequence given the previous words and the informal input. It is defined as:
LCE = E log Po (FL FLayye NL.)
Alignment Task To ensure that the embeddings the informal and formal sequences are well- aligned in the FORMALALIGN model, introduce contrastive loss Lar Let u, and v, denote the hidden state representations of the i -th informal input NL; and its corresponding formal output FL; respectively u, Z (NL,) and v: Zo (LL.
The contrastive loss encourages the cosine similarity cos cos(u, v:) between the representations of corresponding informal-formal pairs to be higher than the cosine similarity cos(u,, v.)) between non-corresponding pairs:
1
N Σ
exp pcos(u; V:)/T)
Lel = N
log
Σn exp (u; vz)/7)
where is temperature parameter that scales the cosine similarities. By minimizing this contrastive loss, the FORMALALIG, model lears to align the embeddings of corresponding informal-forma sequences while ensuring that the embeddings of non-correspondiig sequences dissimilar.
4

---

Published as a conference paper at ICLR 2025
FORMALALIGN Loss We jointly train evaluator model with the autoformalization task and the alignment task, resulting in a FORMALALIGN model. The combined training loss is:
L = LCE + LCL
(2)
We train alignment-aware FORMALALIGN model by minimizing 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.
3.3 INFERENCE
During the inference phase, the FORMALALIGN model generates an alignment evaluation score Valign for each pair of informal input NL, and formal output FL,, This score is a combination of two metrics: the certainty score and the similarity score.
The certainty score Vear measures the confidence the fine-tuned FORMALALIGN model in predicting the formal output based on the corresponding informal input. It is calculated by taking the exponential of the average log-probability assigned by the model to each token in the formal sequence:
Certainty Score
Veer = exp
log P FLL NL,)
where P& represents the probability output the model with parameters Φ FL,,ęj denotes the tokens in the formal sequence up to position j 1,, and n is the length of the formal sequence.
Similarity Score The similarity score Vam measures alignment between the embedding representa- tions of the informal input and the formal output. It is computed using the cosine similarity between the hidden states of the informal input and the formal output conditioned on the informal input:
Vin cos (N., Zo (FL, (NL))
where Za (NL,) represents the hidden state from the final position in the informal input, and 2 (FL, represents the hidden state from the formal output conditioned on informal input.
Alignment Score The overall alignment evaluation score Valign is computed by taking the average of the certainty score and the similarity score:
Valign (Veer + //2
This combined score reflect both the accuracy of the translation from informal to formal expressions and the alignment of the internal representations of the sequences, providing a robust evaluation metric during the inference stage.
4
EXPERIMENT
4.1 DATASETS
In our experimental setup, we conduct fine-tuning on the FormL4 (Lu al., 2024) and MMA (Tang et al.) 2023a) training sets, both of which are derived from Mathlib, a library of fundamental mathematical statements. This training data enables our model to align informal mathematical statements with their formal counterparts.
To thoroughly evaluate our method's ability to align informal mathematical statements with formal language, employ comprehensive set of test sets that covers both in-domain and out-of-domain data. Specifically, we use four distinct test sets: the basic and random test sets from FormL4, and the valid and test sets from MiniF2F (Zheng et al.] (022a). FormL4, designed to assess the autoformalization capabilities LLMs Lean (de Moura Ulinch 2021) sourced from Mathlib, provides comprehensive evaluation framework. The basic and random test sets from FormL. allow
5

---

Published as a conference paper at ICLR 2025
FormiL-Basic
FormLA-Random
Minil'FF-aaid
MiniF2F-Test
40,00%
40 0075
25,00%
24 07%
5,00%
14,20%
L
19%
4.99%
6,10%
46.2%
13.0%
18.1855
17.90%
oppnnet
gyp
opecity
Figure 3: Distribution Misalignment Types across Four Datasets. This figure illustrates the variety and proportion of misalignment strategies applied to generate negative examples in the Forml. .4 Basic, BormL4-Random MiniF2F--alli Valid, and MiniF2F-Test datasets, providing a comprehensive evaluation basis for the AAE task.
us to gauge the model's performance in autoformalizing fundamental math statements that are similar to the training data. In contrast, the validation and test sets from MiniF2F serve out-of-domain test data, providing a more challenging evaluation setting. MiniF2F is a benchmark containing 488 manually formalized mathematical competition statements sourced from various mathematical olympiads (AMC, AIME, IMO) and high-school and undergraduate math classes.
These datasets primarily provide paired input-output instances, lacking the negative examples crucial for a more robust assessment our model. Consider one aligned informal- pair shown in Table 1 as example. We detail our approach generating misaligned formal outputs with the natural (informal) input employing strategies outlined in Table 2 The distribution of these misalignment types visualized in Figure
Table 1: Natural Language Statement and its aligned Lean Formal Statement.
Natural Language Statement
The volume of cone is given by the formula V 3/2 Bh, where B is the of the base and h is the height. The area of the base of a cone is 30 square units, and its height is 6.5 units. What is the number of cubic units in its volume? Show that it is 65.
Lean Formal Statement
theorem mathd_a Bachd_algebre algebraaaaaa..... (b h R)
(ho
00
v)
(hı v =
/ 3 (b * h))
(h2 b 30)
(ha -h 13
65
4.2 METRICS
To assess the performance of models in evaluating the alignment of informal and formal language pairs, we introduce three automated metrics:
Alignment Selection (AS) This metric quantifies how well model selects the aligned formal output from multiple candidates when given an informal input. We calculate the alignment evaluation score Valign with details described in Appendix C,3 for each eiformal-forma pair. The pair with the highest score is selected the aligned pair.
Alignment Detection We introduce predefined threshold to detect the alignment for each informal-forme pair. If Valgon exceeds 0 the model considers the pair to be aligned. We evaluate this

---

Published as a conference paper at ICLR 2025
Table 2: Misalignment Strategies.
Misalignment Strategies
Constant Modification (constant) This type of misalignment involves changing constant value within the expression.
Exponent Modification (exponent)
This misalignment targets the exponents in the expression.
theorem mathd_ alghbra_ge
theorem mathd_algebra.
(b h v IR
(b v : R)
(h_0 0 < A0 < A0 v)
(h_0 0 < A8 < Ao < v)
(h_1
1 3 (b h))
(h_1
1 (b^2 h))
(h_2 31) changed constant
changed exponent
(h_3 = 2)
(h_2 : b 30)
65 :
(h_3 : h = 13 2)
v = 65 :=
Introduction of New Variable (vari- able_new)
Change of Variable Type (variable _ypee
This misalignment introduces completely new variable into the expression.
In this case, the misalignment involves chang- ing the type of a variable within the expres- sion. The function identifies the type of randomly selected variable and changes it to different type from a predefined list of types.
theorem mathd_a mathd_algebra____ _488
(b h R) added new
variable
(h_0 b h A8 < v)
theorem aathd_algebra__
(h_1 = 1 3 (b h))
(b v 2) changed type to
(h_2 bb = 30)
(ho 0 < A0 < h A0 < v)
(h_3 h 13 2)
(h: .v= 1/3 * (b h))
65
(h2 30)
(hs 13/2) :
v = 65 :=
Modification of Equality (equality) This misalignment switches between equality and inequality f symbols within the ex- pression.
Random Pairing (random)
This creates mismatch between the informal input and its formal output. Instead of pairing the informal input with its correct formal out- put, this strategy randomly selects formal output from other examples.
theorem mathd_alee mathd_algebra. algebra__42
(b h v RR)
(h_0 0 b A0 h 00
(h_1 #1 3 (b h))
swapped inequality
(h_2 :b= 30)
(h_3 h 13 2)
65
detection method using two metrics: precision and recall. Firstly, the Precision metric measures the fraction of pairs identified as aligned by the model that are truly informal- pairs. It is calculated Precision T. where TP represents the number of true positives (correctly identified aligned pairs) and FP represents the number of false positives (incorrectly identified aligned pairs). Secondly, the Recall metric measures the fraction of true informal-forma pairs correctly identified by TP the model. It is calculated Recall TP where FN represents the number of false negatives (missed aligned pairs).
TP
4.3 MAIN RESULTS
We fine-tune Mistral-7B model (Jiang al. 2023b) the FORMALALIGN model and evaluate its performance on various autoformalization benchmarks. The datasets used in this study include Forml 4-Baiic F Random, MiniF -aliid, and MiniF2R-Test. Each data example consists
7

---

Published as a conference paper at ICLR 2025
Table 3: Automated Alignment Evaluation (AAE) results across different autoformalization bench- marks. The table compares the performance of our fine-tuned Mistral-7B model (FORMALALIGN model) with GPT-4 and GPT-3.5 on four datasets: FormL4-Basic, FormLA-Random, MiniF2F- and MiniF2F-Test. Performance metrics include Alignment Score (AS), Precision (Prec.), and Recall (Rec.).
FormI-4-Bawd
FormL4-Randee
MiniF2F-Vatie
MiniF2F-Test
Datasets
Prec.
Rec.
AS
Prec.
Rec.
AS
Prec.
Rec.
Prec.
Rec.
GPT4
90.23
42.68
88.15
91.85
45.72
89,95
67.24
59.85
89.87
70.82
62.45
92.88
GPT-3.5
50.23
25.21
90.83
47.00
23,42
67.26
47.32
22.29
62.55
40.74
21.97
61.73
FORMALALIGN
99.21
93.65
86.43
85.85
86,90
89.20
66.39
68.58
60.66
64.61
66.70
63.37
of an aligned informal-formi pair, which is considered positive example. To comprehensively assess the model's performance and robustness, we augment each positive example with 21 negative examples generated through carefully designed misalignment strategies outlined in Table
To balance precision and recall in the FORMALALIGN model's alignment detection, we set 6 = 0.7. presents the detailed experimental results, including Alignment-Selectee Selection (AS), Precision (Prec.), and Recall (Rec.) metrics. The table compares the performance of our fine-tuned Mistral-7B model (FORMALALIGN model) with GPT-4 (Achiam et al.) 2023) and GPT-3.5 (OpenAl 2023) across the different datasets. For more information on the query prompts used in the experiments, please refer to Appendix C.2
Effective and Robust Alignment Evaluation: The experimental results demonstrate the effec- tiveness and robustness of our FORMALALIGN evaluating the alignment between informal and formal languages. The model achieves impressive performance, with high alignment, precision, and recall scores across all datasets. Notably, on the FormL4-Base dataset, it attains an exceptional Biignment-Selectionn score of 99.21 % and a Precision of 93.65%. These results highlight the model's ability to accurately identify aligned informal-formal pairs.
Generalization Across Datasets: The FORMALALIGN model exhibits consistent performance across four diverse datasets, demonstrating its ability to generalize its autoformalization evaluation capabilities. Particularly noteworthy are the model's AS scores of 66.39% and 64.61% % on the challenging M and MiniF2F-Test datasets, respectively. These scores are comparable to those achieved by GPT-4, which obtained AS scores of 64.34% and 68.31 % on the same datasets, The FORMALALICO model's strong performance on the MiniF2F theorem proving benchmark, which poses significant challenges due to its complexity and diversity, highlights the effectiveness of our proposed FORMALALIGN in enhancing the model's generalization ability.
The experimental results validate the effectiveness of FORMALALIGN improving the performance of LLMs for autoformalization alignment evaluation. The integration of cross-entropy loss with contrastive learning in the model's s training process has proven to be a powerful combination, resulting in robust model capable of achieving high alignment-selection precision, and recall scores across various datasets. The model's 's ability to generalize its performance to challenging benchmarks like MiniF2F further underscores the benefits of our approach.
4.4 COMPARISON WITH HUMAN EVALUATION AND LLM-AS-JUDGE
To comprehensively assess our FORMALALIGN model in autoformalization alignment evaluation, we conduct an extensive human evaluation along with an L.M-as-judee evaluation and compared their correctness rates. This analysis offers an in-depth understanding of our automated evaluation method's performance compared to human experts and tate-oof-thear language models.
The experiment design, statistical results, as well as detailed discussions are specified Appendix G As listed in G human experts achieved the highest correctness ratio in matching with the ground-truth alignment evaluations with an average of 79. 79.58%. followed by our FORMALALIGN (65.00%). The LLM-as-jude method achieves the lowest precision in autoformalization alignment evaluation. Each human expert takes approximately 3 hours to review 80 items, while the FORMALALIGN model requires less than 2 minutes conduct the automated evaluation. These findings emphasize the value
8

---

Published as a conference paper at ICLR 2025
of our FORMALALIGN framework in providing efficient and reliable automated evaluation method for autoformalization alignment.
ANALYSIS AND DISCUSSION
To further validate the robustness and effectiveness of our FORMALALIGN framework, we conducted seven additional experiments, some of which are detailed in the Appendix due to limited space. We begin by validating the generalized effect of our FORMALALICE across different baseline language models (Section 5.1). We investigate the necessity and effectiveness of combined training loss (Section 5.2) and the impact of our proposed alignment score Valign (Section 5.3)
Furthermore, address concerns regarding potential data contamination in pre-trained language models through comprehensive analysis of our experimental data (Appendix DD) Next, we investigate the generalization ability our method and the impact of different training datasets on its performance (Appendix(E) E). We then explore the effect of incorporating contrastive learning loss on the performance of autoformalization of natural language statements to formal language statements (Appendix [ To ensure the comprehensiveness and true representation of potential misalignments, we conduct an extensive manual review and evaluation of our FORMALALIGN framework (Appendix G
5.1 EFFECTS OF DIFFERENT BASELINES
In this section, validate the generalized effect of our FORMALALIGN across different baseline language models. These baselines are Phi2-2.7B (Javaheripi et al. 2023) (Phi), LLaMA2-7B (Touvron)
al. 2023) (LLaMA), DeepSeekMath-Bade 7B (Shao et al. al. 2024) (DeepSeek) and Mistral-7B (Jiang ct al. 2023b) (Mistral). Table 4 presents the Alignment-Selection performance of the different baseline models across four datasets:
Table 4: Alignment Selection Performance of different baselines across 4 datasets.
FormL4
MiniF2F
Datasets
Basic
Random
Valid
Test
Phi
80.77
71.07
31.56
32.51
DeepSeek
90.29
77.08
54.66
55.19
LLaMA 98.08
76.42
54.51
57.20
Mistral 99.21
85.85
66.39
66.70
The experimental results indicate that the Mistral model outperforms the other baseline models across all datasets, demonstrating the highest Aliganent-Selection performance. The LLaMA and DeepSeek models perform strongly, particularly on the FormL. datasets. We note that the Phi model still performs adequately on the Forml.4 .4 datasets but struggles on the MiniF2F datasets, highlighting that our method is easily applicable smaller models, Phi2 has less than half the parameters compared to the other three models.
These results validate the effectiveness of FORMALALIGN in improving the automated alignment evaluation performance across various baseline language models, with Mistral showing the most significant improvements. This suggests that our FORMALALIGN can generalize well across different model architectures.
5.2 EFFECTS OF DIFFERENT TRAINING Loss
We investigate the necessity and effectiveness of our combined training loss, defined in Eq. by conducting ablation study with different loss configurations. The results, presented in Table provide valuable insights into the impact of each loss component on the model's performance.
The configuration using only the cross-entropy loss (w/ CE) achieves comparable performance, particularly on the FormL4 dataset. This result suggests that the autoformalization task, optimized by the cross-entropy loss, inherently learns alignment between informal and formal sequences.

---

Published as a conference paper at ICLR 2025
Table 5: Comparison of overall alignment-sellctionn performance across different configurations: with only cross-entropy loss (w/ CE), with only contrastive loss (w/ CL), and the complete model (Ours).
FormL4
MiniF2F
Datasets
Basic
Random
Valid
Test
w/ CE
98.64
82.81
52,45
54.32
w/ CL
59.05
57.55
36.07
30.86
Ours
99.21
85.85
66.39
66.70
Although the configuration using only the contrastive loss (w/ CL) shows limited performance, it plays crucial complementary role to the cross-entropy loss. The combined approach (Ours), which incorporates both cross-entropy and contrastive losses, achieves the best performance across all datasets.
5.3 EFFECTS OF DIFFERENT ALIGNMENT SCORE VALIGN
We investigate the necessity our proposed alignment score Valign as described Eq. 5 Table provides a comprehensive evaluation of the effectiveness of our proposed alignment score Valign By analyzing different configurations of the model, we derive the following key insights:
Table 6: Comparison of overall aligmment-selection performance across: with only the certainty score (w/ cer), with only the similarity score (w/ sim), and the complete model (Ours).
FormL4
MiniF2F
Datasets
Basic
Random
Valid
Test
cer
98.98
85.64
53.69
55.55
w/ sim
45.25
20.75
20.49
21.81
Ours
99.21
85.85
66.39
66.70
The configuration using only the certainty score (w/ cer) achieves high performance, particularly on the FormL4 dataset. This result indicates that the model's language generation capabilities are robust and significantly contribute to the alignment evaluation. The certainty score measures the model's confidence in predicting the formal output, underscoring the importance of accurate language generation in our method.
While using only the similarity score (w/ sim) shows limited performance, the combined approach (Ours), which integrates both certainty and similarity scores, achieves the best result across all datasets. This result demonstrates that combining both scores provides more holistic and reliable evaluation metric. The combined score captures language-based and representation-level information, ensuring a robust evaluation during inference.
CONCLUSION
In this study, we introduce FORMALALIGN, a framework designed to automate the alignment evalua- tion the autoformalization process using LLMs. Our approach utilizes dual loss function that combines cross-entropy and contrastive learning loss, significantly enhancing the model's ''s ability to discern and align informal-formal language pairs. This methodology not only preserves the integrity of logical constructs but also improves the accuracy of alignment between informal and formal sequences. Extensive experiments conducted across four datasets demonstrate that FORMALALIGN effectively reduces the reliance manual verification processes, thereby streamlining the autofor- malization workflow. The results confirm that our method provides reliable, effective, and robust evaluations, proving its practical utility in real-world scenarios. We believe that FORMALALIGN opens new avenues for research and application in the autoformalization field, offering a scalable and efficient solution to of the most pressing challenges in the domain.
10

---

Published as a conference paper at ICLR 2025
REFERENCES
Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, lige Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. CoRR, abs/2302. 124333 2023a. doi: 10.48550/ARXIV.2302.111 124333 URL hhttps://doi. org/10 48550/arXiv. 2302. 12433
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng. Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. CoRR, abs/2310. 10631, 2023b, doi: 10.45550ARRXV:331000611 URL https 7/doi. 10. 48550/ 2310. 10631
Kshitij Bansal and Christian Szegedy. Learning aligmment between formal & informal mathematics. In 5th Conference Artificial Intelligence and Theorem Proving, 2020.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, -ha-CChrsttophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard P. Huet, César A. Muñoz, Chetan R. Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The coq proof assistant reference manual, version 6.1. 1997. URL httpss//aap sww.nticscholar org/CorpusIID 54117279
Chi-Min Chan, Weize Chen, Yusheng Su, Jianxuan Yu, Wei Xue, Shanghang Zhang, Jie Fu, and Zhiyuan Liu. Chateval: Towards better Ilm-based evaluators through multi-agent debate. CoRR, abs/2308. 072011 2023, doi: 10448500AARXIV.3388.7777 URL WRL/https://dol httg//..4855000
arXiv. 2308. 07201
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray. Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert-Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Joshua Achiam, Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katic Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojeiech Zaremba. Evaluating large language models trained on code. CoRR, abs/2107.03374 2021. URL htt.httss///aiv..oottt abs/2107. 03374
Xinlei Chen, Hao Fang, Tsung-Y Yi Lin, Ramakrishna Vedantam, Saurabh Gupta, Piotr Dollár, and C. Lawrence Zitnick. Microsoft COCO captions: Data collection and evaluation server. CoRR, abs/1504.00325, 2015. URL http:://aaxii.orrrgeee/////////t hwt.:////////////e/ee 00325
Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko. Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emily Reif, Nan Du, Ben Hutchinson, Reiner Pope, James Bradbury, Jacob Austin, Michael Isard, Guy Gur-Ari, Pengcheng Yin, Toju Duke, Anselm Lev- skaya, Sanjay Ghemawat, Sunipa Dev. Henryk Michalewski, Xavier Garcia, Vedant Misra, Kevin Robinson, Liam Fedus, Denny Zhou, Daphne Ippolito, David Luan, Hyeontaek Lim, Barret Zoph, Alexander Spiridonov, Ryan Sepassi, David Dohan, Shivani Agrawal, Mark Omernick, Andrew M. Dai, Thanumalayan Sankaranarayana Pillai, Marie Pellat, Aitor Lewkowycz, Er- ica Moreira, Rewon Child, Oleksandr Polozov, Katherine Lee, Zongwei Zhou, Xuezhi Wang, Brennan Saeta, Mark Diaz, Orhan Firat, Michele Catasta, Jason Wei, Kathy
Douglas Eck, Jeff Dean, Slav Petrov, and Noah Fiedel. Palm: Scaling language modeling doi: 10.4850/ARXXW22244022
with pathways. CoRR, abs/2204.022 12 2022.
URL
https://doi. 20 48550 10.50//axiv..00 22w..xiwiii22222222 02311

---

Published as a conference paper at ICLR 2025
Arman Cohan, Franck Dernoncourt, Doo Soon Kim, Trung Bui, Scokhwan Kim, Walter Chang, and Nazli Goharian, A discourse-aware attention model for abstractive summarization of long documents. In Marilyn A. Walker, Heng Ji, and Amanda Stent (eds.), Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguisties: Human Language Technologies, NAACI-HITT, New Orleans, Louisiana, USA, June 1-6, 2018, Volume 2 (Short Papers), pp. 615-621, Association for Computational Linguistics, 2018. doi: 10.18653/V 1/N18-2097.
URL https: ptttps://oo..co org./...rg///// 18853/11/118-2000
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe (eds.), Automated Deduction CADE 28 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pp. 625 635. Springer, 2021. doi: 10.1007/ 3--33--98777-----1 79876-51 51. URLhhttps://dot http:://dooooor/////// org/10 10. 1007/978- 3- 030-0-13-0 000-09876------1 79876- 5_37
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction CADE-25 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pp. 378-388, Springer, 2015. doi: 111000/9778-3331--14001111 //doi.org/1e
URL https
Zorik Gekhman, Jonathan Herzig, Roee Aharoni, Chen Elkind, and Idan Szpektor. Trueteacher: Learning factual consistency evaluation with large language models. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing. EMNLP 2023, Singapore, December 6-10, 2023, pp. 2053-222220 2070. Association for Computational Linguistics, 2023. doi: 10. 00.18653/V1/20233358 120.3/11222..MM.PMMM.... emnlp-main. 127
URL hwtphhttp///oo.... http://d...rrr//1111166/////////
John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri (eds.), Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Pulo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1 1166 of Lecture Notes in Computer Science, pp. 265-269. Springer, 1996.
Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang. Zhenguo Li, Linqi Song, and Xiaodan Liang. MUSTARD: Mastering uniform synthesis of theorem and proof data. In The Twelfth International Conference on Learning Representations, 2024. URL http://ppreerieeeeeeeee/oorrnaep
Mojan Javaheripi. Sébastien Bubeck, Marah Abdin, Jyoti Aneja. Sebastien Bubeck, Caio César Teodoro Mendes, Weizhu Chen, Allie Del Giorno, Ronen Eldan, Sivakanth Gopi, al. Phi-2: The surprising power of small language models. Microsott Research Blog, 2023.
Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalizationn CoRR. abs/2311.03755. 2023a. doi: 10,48550ARRIV.2311 1.03755. URL http:s::///o....g///..eoo 17Xiv.2311.03755
Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de Las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas Wang, Timothée Lacroix, and William El Sayed. Mistral 7b. CoRR, abs/2310.0683 2023b. doi: URL https://o/// org/ 10. 18850//axivv 2310.06825
10.46550/ARXX1.231000666
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023c. URL httpp:://openreview.nett het.:pdfiid-SMMMSAAoO.
Dongfu Jiang, Yishan Li. Ge Zhang, Wenhao Huang, Bill Yuchen Lin, and Wenhu Chen. Tigerscore: Towards building explainable metrie for all text generation tasks. CoRR, abs/23 10.0075,, 2023d. doi:
httpht//s/// org/10 48550/ a 2310.00752
12

---

Published as a conference paper at ICLR 2025
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, and Herman Geuvers. Developing corpus-based translation methods between informal and formal mathematics: Project description. CoRR, abs/ Abs//440.3341, 2014. http::////a httpaaawwwv...r/aaaa berrg/bss/1ae .4511
Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil. Automating formalization by statistical and semantic parsing of mathematics. In Mauricio Ayala-Rincón and César A. Muñoz (eds.), Interactive Theorem Proving 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, volume 10499 of Lecture Notes in Computer Science, pp. 12-27. Springer, 2017. doi: 10. 10007998-33311--61100
2. URL https: orgoorg///10 10.
Pei Ke, Bosi Wen, Zhuoer Feng, Xiao Liu, Xuanyu Lei, Jiale Cheng, Shengyuan Wang. Aohan Zeng. Yuxiao Dong, Hongning Wang. Jie Tang, and Minlie Huang. Critiquellm: Scaling Ilm- as-critic for effective and explainable evaluation of large language model generation. CoRR. abs/2311.18702, 2023. doi: 1048550/ARXI.2311.88800
/tLhs:sss://do http::///oooooogg//// wttpo/..../000...
Tae Soo Kim, Yoonjoo Lee, Jamin Shin, Young-Ho Houng-Hooooe Kim, and Juho Kim. Evallm: Interactive evaluation of large language model prompts on user-defined criteria. CoRR, abs/2309. abss//39..1333,, 2023. URL h/tps:////// 0r0/ 48550/arKiit 2309. 13633
doi: 10.48550/ARXVV2230011138
Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurlPS 2022, New Orleans, LA, USA, November 28 December 9, 2022, 2022. URL http: http:://appprrrs nips. cc/ cc/paper____ paaaperfflle Lillss/paper2022/2 hash/ html
Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Autofor- malize mathematical statements by symbolic equivalence and semantic consistency. arXiv preprint vrXiv:2410.20986 2024a.
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li. Xian Zhang, Kaiyu Yang, and Xujic Si. A survey on deep learning for theorem proving. CoRR. abs/2404.09939, 2024b. doi: 10. 00448550/AXXXI..344009999
http::ttts://diiii http:///oooooor///// a85vv/ 2404.049999
Chin-Yew Lin. ROUGE: A package for automatic evaluation of summaries. In Text Summarization Branches Out, pp. 74-81, Barcelona, Spain, July 2004. Association for Computational Linguistics.
org/Wo4-1013
Minqian Liu, Ying Shen, Zhiyang Xu, Yixin Cao, Eunah Cho, Vaibhav Kumar, Reza Ghanadan, and Lifu Huang. X-eval: Generalizable multi-aspect text evaluation via augmented instruction tuning with auxiliary evaluation aspects. CoRR, abs/2311 1.8788,, 2023a. doi: 10.48550/ARXIV.2311 08788. URL hhtpt::tt//det org/10..r010... 48550/arXiv..o 231. 2311.08788....11
Yang Liu, Dan Iter, Yichong Xu, Shuohang Wang, Ruochen Xu, and Chenguang Zhu. Gpteval: Nlg evaluation using gpt-4 with better human aligmment. arXiv preprint arXiv:2303.16633 2023b.
Jianqiao Lu, Zhengying Liu, Yingjia Wan, Yinya Huang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. Process-drives autoformalization in lean 4. 2024. URL https://api Somaaniissccol..rr.rrr/oooosopoo orgg///rrpss1102222228333
Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Aut- oformalizing euclidean geometry. In Forty-first International Conference on Machine Learn- ing, ICML 2024, Vienna, Austria, July 21-27, 2024. OpenReview.net, 2024. URL https
OpenAl. GPT-3.5 Turbo, 2023. URL
wpw.:fffrrooopeaiii..o openai. wttp://p....////////////e///////
Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics. July 6-12, 2002, Philadelphia, PA, USA, pp. 311-318, ACL, 2002. doi: 10.31155/00733333173311 URL /tt./httpss///claaannoooggg https//////l.annoooollooor/g////
13

---

Published as a conference paper at ICLR 2025
Yiwei Qin, Weizhe Yuan, Graham Neubig, and Pengfei Liu. T5score: Discriminative fine- tuning of generative evaluation metrics. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023, pp- 15185-15202. Association for Computational Linguistics, 2023. doi: HTN.//22....FI
URL.httts:://oi..rrg/// 11653///111133
findings-emnip 1014
Piotr Rudnicki. An overview of the mizar project. 1992. URL https::/.ap....mmmttniicc 10:
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. CoRR, abs/2402.03300 2024. doi: 1044850AARX1.22220033000 URL
https://do1 org/10 48550 2402. 03300
Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics - 13th Interna- fional Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of doi: 10.10077978-3-030-533111 URL https: org/ 10. 1007 000-0000--5533 53518-6_1
Lecture Notes in Computer Science, pp. 3-20. Springer, 2020.
Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cristian Canton-Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller, Cynthia Gao, Vedanuj Goswami, Naman Goyal, Anthony Hartshorn, Saghar Hosseini, Rui Hou, Hakan Inan, Marcin Kardas, Viktor Kerkez, Madian Khabsa, Isabel Kloumann, Artem Korenev, Punit Singh Koura, Marie-Anne Lachaux, Thibaut Lavril, Jenya Lee, Diana Liskovich, Yinghai Lu, Yuning Mao, Xavier Martinet, Todor Mihaylov, Pushkar Mishra, Igor Molybog, Yixin Nie. Andrew Poulton, Jeremy Reizenstein, Rashi Rungta, Kalyan Saladi, Alan Schelten, Ruan Silva, Eric Michael Smith, Ranjan Subramanian, Xiaoqing Ellen Tan, Binh Tang. Ross Taylor, Adina Williams, Jian Xiang Kuan, Puxin Xu, Zheng Yan, Iliyan Zarov, Yuchen Zhang, Angela Fan, Melanie Kambadur, Sharan Narang, Aurélien Rodriguez, Robert Stojnic, Sergey Edunov, and Thomas Scialom. Llama 2: Open foundation and fine-tuned chat models. CoRR, abs/2307.092a 09288, 2023, doi: 10.48550/ARXIV.20007. 099288 URL https::: .rgg /8550/ arXiv 200. 092888
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef (eds.), Intelligent Computer Mathematics 11th International Conference, CICM 2018, Hagenberg. Austria, August 13-17, 2018, Proceedings, volume 11006 of Lecture Notes in Computer Science, pp. 255 270. Springer, 2018. doi: 10.1007/978-3-3199968812 22. URL https://doi, org 1007/908-3--111-11111
Yidong Wang, Zhuohao Yu, Zhengran Zeng. Linyi Yang, Cunxiang Wang, Hao Chen, Chaoya Jiang, Rui Xie, Jindong Wang, Xing Xie, Wei Ye. Shikun Zhang, and Yue Zhang. Pandalm: An automatic evaluation benchmark for LLM instruction tuming optimization. CoRR, abs/2306. 0ttps//220000007.... 2023. doi: 01.48550/ARXII.2366.60
URL htt.::tts://// //dii. org/ 10. 48550/ 18550/arXiv arxiv 2306 05687
Tianwen Wei, Liang Zhao. Lichang Zhang, Bo Zhu, Lijie Wang. Haihua Yang, Biye Li, Cheng Cheng, Weiwei LU. Rui Hu, Chenxia Li, Liu Yang, Xilin Luo. Xuejie Wu. Lunan Liu, Wenjun Cheng, Peng Cheng, Jianhao Zhang, Xiaoyu Zhang, Lei Lin, Xiaokun Wang, Yutuan Ma, Chuanhai Dong, Yanqi Sun, Yifu Chen, Yongyi Peng, Xiaojuan Liang. Shuicheng Yan, Han Fang, and Yahui Zhou. Skywork: A more open bilingual foundation model. CoRR, abs/2310. 19341, 2023. doi: 10.48550/ARXI.2210009999
URL htRLsttps::// //doi org/ 10. 48550/arXin 2310. 19341
Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The isabelle framework. In Ot- mane Aït Mohamed, César A. Muñoz, and Sofiène Tahar (eds.), Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008. Montreal, Canada, August 18-21 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science pp. 33-38. Springer, 2008 doi: 111007/978-3-540-7100
URL http://///6oi.ooo/11111000////// -0077788--5---710 3-540-71067-77
14

---

Published as a conference paper at ICLR 2025
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jam- nik, and Christian Szegedy. Autoformalization with large language models. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho. and A. Oh (eds.), Ad- vances in Neural Information Processing Systems 35: Annual Conference on Neural Infor- mation Processing Systems 2022, NeurlPS 2022, New Orleans, LA, USA, November 28 December 9, 2022, 2022. URL
wttpp/ercpppp....pppppp/pp wwtpppperfilee/eppeeeeeeeeeeeeee hilles/paper/2222/aass
html
Wenda Xu, Danqing Wang. Liangming Pan, Zhenqiao Song. Markus Freitag, William Wang. and Lei Li. INSTRUCTSCORE: towards explainable text generation evaluation with automatic feedback. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, EMNLP 2023, Singapore, December 6- 6-10, 2023. pp. 5967-5994, Association for Computational Linguistics, 2023, doi: 10. 10.18653/V1/2 1/2023. mmmnp--miin..
URL hdtps://ooi. org/ 10. 18653/v1/2220
Huaiyuan Ying, Shuo Zhang. Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong. Kuikun Liu, Ziyi Wang. Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-mate Open math large language models toward verifiable reasoning. CoRR, abs/2402.06332, 2024. doi: 10.44550/ARXI..2400.000 URL httpt:://oi..rrr 18550/arXiv. 2402. 06332
Peter Young. Alice Lai, Micah Hodosh, and Julia Hockenmaier. From image descriptions visual denotations: New similarity metrics for semantic inference over event descriptions. Trans. Assoc, Comput. Linguistics, 2:67-78, 2014. doi: 10.1 A\ 00166. URL /ttps::/doi..rg/
10. 10.1162/tacl_a_00111 00166
Weizhe Yuan, Graham Neubig, and Pengfei Liu. Bartscore: Evaluating generated text as text generation. In Marc' Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (eds.), Advances in Neural Information Processing Systems 34: Anmual Conference on Neural Informatinn Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual, pp. 27263-27277 2021. URL http://eeeeeeeeeeeeeaaaeeeeeeeee Abstratttttbbttttttttat.
newrrnnss.eeerrreeee ips cc/papprr/22////ahl
Xiang Yue, Boshi Wang, Ziru Chen, Kai Zhang, Yu Su, and Huan Sun. Automatic evaluation of attribution by large language models. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 10, 2023, pp. 4615-4635. Association for Computational Linguistics, 2023. doi: 10.18653/V1/2023 FINDINGS-EMNNPPS.
URL
18653/v1/2023. http://w///22....innngn/.../ Sindings-emnlyy 307 307
Lan Zhang, Xin Quan, and André Freitas. Consistent autoformalization for constructing mathematical libraries. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen (eds.). Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing. EMNLP 2024, Miami, FL. USA, November 12- 16, 2024, pp. 4020-4033 Association for Computational Linguisties, 2024. or 20240022244222 emnlp-main. 233
URL https://aclantholleee
Tianyi Zhang, Varsha Kishore, Felix Wu, Kilian Q Weinberger, and Yoav Artzi Bertscore: Eval- uating text generation with BERT. In 8th International Conference on Learning Representa- fions, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020a. URL net
https://openreww wwt..e//foorrmiiisseettttteceeee
Tianyi Zhang, Varsha Kishore, Felix Wu, Kilian Q. Weinherger, and Yoav Artzi. Bertscore: Evaluating text generation with bert, 2020b.
Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving. CoRR, abs/2305. 16366, 2023. doi: 10.48550/ARXIV.2060 16366. /ttps://////
orgg/0 1010. 48550/arXiv. 2305. 16366
Kunhao Zheng. Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022a. URL|https /ttsss////pp/eeeeie//ee
het//forumIdd-9PPgFFFFFF
15

---

Published as a conference paper at ICLR 2025
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minifff: cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations. ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022b. URL httpt:://pppeereieir
het/forum?id-92Pegg. TF
Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang. Zhanghao Wu, Yonghao Zhuang. Zi Lin. Zhuohan Li, Dacheng Li, Eric P. Xing, Hao Zhang, Joseph E. Gonza- lez, and Ion Stoica. Judging Ilm-as-a-judge with mt-bench and chatbot arena. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: Annual Conference Neu- ral Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA. USA, Decem- ber 10 16, 2023, 2023. URL http: hwtp/papppe.a.aaameeepeeeeeee..p nips. ccppaper_pppppc /T1le//paper/2223/aaaa 9111881227639867782255555 1832 1tt.:33--bbstatcac Dataccttt-atttttss...mmmm Bew.saaandnnnccaass..s...m html
A LEAN 4 COMPILER
The Lean 4 Compiler is a critical component of the Lean 4 programming language. This tool enables users to craft effective proof automation tactics within the Lean environment and transform them into optimized C code. The Lean 4 Compiler in our scope is referred to as the tool available at https://gi wwt../tttttu...... thub. ctw htmm///eeerrove-commmm ty/repl This particular resource provides read- eval-print loop (REPL.) designed for Lean 4, which supports user interaction through JSON formatted input and output streams (stdin and stdout, respectively). Our compilation projection is therefore founded on REPL.
B MORE RELATED WORKS
Formal Mathematics Formal languages, such as Isabelle (Wenzel et al. 2008), Lean (de Moura & Ullrich 2021). HOL Light (Harrison 1996), and Coq (Barras et al. 1997). ) have become integral tools in modern mathematics verification systems. These interactive theorem provers (ITPs) function as programming languages, allowing users to input statements and proofs in a formal language for automatic correctness verification. Recent work has explored various approaches to automate the formalization process across different contexts. Murphy et al.) (2024) developed neuro-symbolic framework for Euclidean geometry that specifically addresses diagram-dependent proofs, using theorem provers to incorporate diagrammatic information into the formalization process. Taking a different approach, [i et al.] (2024a) focused on improving candidate selection in LLM LLM-generated formalizations through symbolic equivalence and semantic consistency verification. At a larger scale, Zhang et al. (2024) tackled library-level consistency challenges through retrieval-augmented generation, denoising, and syntax error feedback. While these works address different aspects of formalization from geometric reasoning to candidate selection to library-scale consistency they highlight the diverse challenges in bridging informal and formal mathematics.
C EXPERIMENTAL DETAILS
C.1 FINETUNING DETAILS
Our experiments conducted in a computing environment with 8 NVIDIA A100 GPUs, each with 40GB of memory. All models are fine-tuned in a full-parameter setting.
We employ the AdamW optimizer for model training over epoch, with batch size of 512. The learning rate is set at 2e x 10 incorporating a 3% learning rate warmup period. Below, we present a comprehensive overview of the training hyperparameters utilized. These parameters are consistently applied across training all L.MMs.
C.2 PROMPT DETAILS
In this section, we provide two key prompts used to evaluate the alignment between informal mathematical inputs and their formalized theorem outputs. The first prompt is designed for querying
16

---

Published as a conference paper at ICLR 2025
Table 7: Finetuning Hyperparameters.
Hyperparameter
Value
Global Batch Size
128
LR
5 10
Epo.
1
Max Length
2048
Weight Decay
0
Warmup Ratio
0.03
GPT-based models using explicit scoring mechanisms, while the second prompt demonstrates how our FORMALAL.IGN model computes alignment scores through a computational framework enabled by its combined loss training.
We report greedy decoding results for GPT-4 and GPT-3.5 using a temperature setting of 0.0. Additionally, For the GPT-3.5 version, we query the API of gpt-3.5-turb--112. For GPT-4, we query the API of gpt-4-1106-previset
Prompt for Querying GPT for Automated Alignment Evaluation (CoT-based)
This prompt guides GPT-4 through step-by-step reasoning process to identify potential discrepancies and evaluate alignment systematically.
Below, we provide the CoT-based prompt used to query GPT for automated alignment evaluation:
Given informal mathematical input and formal theorem statement, your task is to evaluate the alignment between them. Assign binary value (0 or 1) to each formal output, where:
indicates that the formal output does not align with the informal input. indicates that the formal output aligns with the informal input.
To ensure a thorough and accurate evaluation, follow these steps:
1. Understand the Informal Input: Identify the key semantic and structural elements in the informal input.
Analyze Formal Output: Compare the formal output against informal input based on the following criteria:
Semantic Consistency: Does the formal output accurately capture the meaning of the informal input?
Structural Correspondence: Does the structure of the formal output reflect the structure implied Completeness: Does the formal output include all relevant information from the informal input?
informal input?
Precision: Is the formal output free from extraneous incorrect information that is not present in the informal input?
3. Identify Discrepancies: Note any mismathhes or issues based on the criteria above. Use specific reasoning to justify your assessment.
4. Decide Alignment: Based your step-by -teeppp analysis, assign value of (not aligned)
(aligned) to each formal output.
Your response should include:
1. brief explanation of your reasoning for each formal autput, focusing on the key criteria.
final alignment score of or for each output.
*uи Task Format:
Informal Input: [inpormal_Input]
Pool of Formal Outputs: (Formal_Outputs)
For each formal output:
17

---

Published as a conference paper at ICLR 2025
Step by Step Reasoning:
[Your reasoning here]
Final Decision:
Alignment Score: [0 or 1]
#*# Example:
Informal Input:
"The sum of two odd numbers is even."
Formal Outputs:
1. V( theorem sum sum_of_ wwwo_odds___soooodd (a Int) (ha 1) (hb b 1)
(a + b) x
\)
Step by Step Reasoning:
Semantic Consistency: The formal output captures meaning of the informal input correctly.
-Structural Correspondence: The quantifiers and logical structure align with the informal statement.
Completeness: All relevant information is included.
Precision: extraneous information is present.
Final Decision:
Alignment Score:
2. 1( a + \text(even) V)
Reasoning:
The statement does not specify that M(a)) and \bb) odd numbers, which is critical part the informal input.
While it correctly indicates that the sum is even, the lack of context about \(al)
and \(b)) makes it incomplete and less precise.
Final Decision:
Alignment Score:
We apply the prompt below our FORMALALIGG model obtain the alignment score without involving language generation settings.
Prompt for Querying FORMALALIGN Model for Automated Alignment Evaluation: The second prompt appears simpler but plays more nuanced role in evaluation framework. Instead of requesting explicit scores, frames the task as translation from informal input to formal output. However, unlike other methods, this prompt operates computational anchor for evaluating alignment to by calculating both Eq. aad Eq. 4 Below, we provide the prompt used to query the FORMALALIGN model for automated alignment evaluation.
Statement in natural language:
(Informal_Input)
Translate the statement in natural language to Lean:
[formal_outpur
C.3 ALIGNMENT SCORE CALCULATION DETAILS
The alignment evaluation score, Valign- is core component used rank informal-formal pairs during the evaluation process. While the metrics described in Section 4.2 are caneral-purposs. and agnel-agn this section provides detailed instructions on how Valign calculated for different systems.
For FormalAlign Model: In FORMALALIGN model, Vaiggn combines two key measures:
18

---

Published as a conference paper at ICLR 2025
Certainty Score (Veer): This score represents the model's sequence-level confidence in the formalization. It is calculated as described in Eq
Similarity Score (Vam): This score captures the representation--eva alignment between the informal and formal statements. It is computed as described in Eq
The final alignment score is then computed combination of the two measures described in Eq in S This formulation ensures that both sequence-level confidence and representation-leve alignment contribute to the overall score.
For each informal input, Valign is computed for formal outputs in the candidate pool. The pair with the highest Valign is selected as the aligned pair.
For GPT Systems: GPT-based systems, Valign simplified binary classification outcome. Each informal-fone formall pair is assigned score of either or based whether the model deems the pair aligned or not:
1, if aligned according to GPT's binary classification,
Valign
0, otherwise.
In where multiple formal outputs have the formal output is randomly selected from the set of tied candidates. This ensures that a decision is always made, even in cases of ambiguity.
(e.g., all scores are 0 or all 1),
General Applicability: While Valign is computed differently for various systems, the process is designed to enable fair comparisons:
For models like FORMALALIGN, the score combines sequence-level confidence and representation- level similarity.
For GPT-based systems, the score is binary classification outcome with random sampling for ties.
For rule-based systems, Valign can be derived using predefined scoring rules or heuristics.
This framework ensures that all models can be evaluated under the same metrics (e.g., Alignment Selection, Precision, Recall), as described in Section 4.2
D DATA CONTAMINATION ANALYSIS
To address concerns regarding potential data contamination in pre-trained language models, we conducted comprehensive analysis of our experimental data. This analysis is crucial, language models are often trained on large amounts unsupervised data, which may include samples similar those used in experiments.
Experiment Design We designed our experiments mitigate the risk of data contamination by sourcing MiniF2F data from math olympiads such AMC, AIME, and IMO. These datasets differ significantly from Mathlib, the largest Lean thcorem library and the primary source of Lean data, reducing the likelihood of data contamination. Additionally, involves augmenting aligned pairs with 20 negative examples using our proposed six misalignment strategies, ensuring that these data not included in the pre-training corpus of LLMs..
automated alignment evaluation task
Results We calculated the loss of different pre-trained models on the MiniF2F test/valid sets the autofrmalization task to further analyze the potential data contamination issue. This approach is inspired by the data contamination detection method in (Wei et al. 2023), which suggests that if a language model has not been exposed dataset during tre-training, its loss the dataset should be relatively high and approximately equivalent to its loss on a reference dataset composed of new, similar samples. The losses of the models in experiments shown below:
19

---

Published as a conference paper at ICLR 2025
Table 8: Performance of Pre-trained Models MiniF2F Datasets.
Pre-trained Model
MiniF2F-valid
MiniF2F-test
Phi2-2.7B
2.4563
2.4377
Mistral-7B
1.4892
1,4660
DeepSeckMath-Bar 7B
1.3148
1.2896
LLaMA2-7B
1.5343
1.5165
Analysis The loss values for each pre-trained model fall within the range of to 3, consistent with and even higher than the findings in (Wei et al. 2023), which reports that losses higher than around on the GSM8K test set indicate low data leakage. These results suggest low level of data contamination in our experimental data. The combination of carefully sourced datasets and the augmentation of aligned pairs with negative examples using our misalignment strategies further strengthens the robustness of our experiments against data contamination.
E GENERALIZATION ANALYSIS
To explore the generalization capabilities of our FORMALALIGN method, we conduct a series of experiments analyzing
the impact of different datasets on the model's 's performance. These experiments aim to provide insights into the method's adaptability and effectiveness across various mathematical domains.
Experiment Design We design our experiments to assess the model's performance when trained on different datasets:
1. Our original model is fine-tuned on a combination of the F training set and the MMA training set from Mathlib.
2. To evaluate the impact of individual datasets, we separately train models on FormL4 and MMA.
3. We test all models on the MiniF2F test and valid sets, which are sourced from math olympiads such as AMC, AIME, and IMO, providing a fair comparison across challenging and diverse problem types.
This approach allows to gauge the generalization ability of our method and understand how different training datasets influence its performance.
The results of our experiments, focusing on the siigmment-selection score for clear compar- ison, are presented the following table:
Results
Table 9: Alignment--election scores of different models MiniF2F dataset.
Model
MiniF2F Test
MiniF2F Valid
Ours (FormL4 + MMA)
66.39
64.61
FormL4 only
62.18
58.18
MMA only
58.97
57.32
Our results highlight several key findings:
Dataset Content Impact: TThe FormL4 dataset, which contains both statements and proofs, outper- forms the MMA dataset, which only contains statements. This suggests that the inclusion of proofs provides richer information about the underlying mathematical concepts, leading more robust understanding of the alignment process.
Combining both FormL4 and MMA datasets for training results in improved performance compared to using either dataset alone. This demonstrates the potential benefits of leveraging diverse data sources enhance the model's capabilities.
Synergy of Datasets:
20

---

Published as a conference paper at ICLR 2025
Generalization Ability: The strong performance on MiniF2F sets, which contain problems from challenging domains like math olympiads, indicates that our method can effectively handle diverse and complex mathematical problems. This suggests that FORMALALIGN has the potential for wider applicability across various mathematical domains.
These findings highlight the robustmess of FORMALALIGN method and its ability to generalize across different types of mathematical problems. The experiments demonstrate that by leveraging diverse datasets and considering both the quality and quantity of training data, we can enhance the method's performance and adaptability to new, unseen mathematical challenges.
F AUTOFORMALIZATION PERFORMANCE ANALYSIS
Given our model is primarily trained for the autoformalization task, we conduct additional experiments explore its capabilities in converting natural language (NL) statements formal language (FL) statements. These experiments aim to provide comprehensive evaluation of our model's performance and demonstrate the effects of incorporating contrastive learning loss on autoformalization.
Experiment Design To assess the impact of contrastive learning loss on autoformalization perfor- mance, compare models:
1. A baseline model trained with cross-entropy loss only (CCl)
2. Our proposed model, which incorporates both cross-entropy loss and contrastive learning loss (Cos, + LCF)
We evaluate both models the FormL4 4 Basic and FormL4 Random test sets obtain compre- hensive understanding of their autoformalization capabilities across different complexity levels. The results of our comparison experiments presented in the following table:
Table 10: Autoformalization performance of different models on FormL4 dataset.
Model
FormL4 Basic (%)
FormL4 Random (%)
Baseline (LO1.)
40.92
35.88
Ours (Lor + LCE)
43.14
36.02
The results demonstrate that incorporating contrastive learning loss improves autofor- test sets. This improvement can be attributed to several factors: Enhanced Discrimination: Contrastive learning acts form of data augmentation, introducing additional negative examples that enhance the model's ability to distinguish between correct and incorrect formalizations.
Analysis
malization performance on both
Improved Representation Learning: The contrastive approach helps the model learn more robust and discriminative representations of mathematical concepts, leading more accurate autoformaliza- tion results.
Generalization Across Complexity: The performance improvement is observed in both the Basic and Random test sets, suggesting that the benefits of contrastive learning extend to various levels of problem complexity.
These findings highlight the potential of contrastive learning in improving autoformalization perfor- mance. By leveraging this approach, we not only enhance our model's ss capabilities but also pave the way for future research in this area. The success of incorporating contrastive learning loss suggests promising directions for developing more effective autoformalization techniques and advancing the field of automated mathematical reasoning.
Our experiments demonstrate that combining traditional cross-entropy loss with contrastive learning leads to more robust and accurate autoformalization model. This approach could inspire further innovations in the field, potentially leading to even more sophisticated methods for bridging the gap between natural language mathematics and formal mathematical representations.
21

---

Published as a conference paper at ICLR 2025
G COMPARISON WITH HUMAN EVALUATION AND LLM-AS-JUDGE
Experiment Design
We design our experiment as follows:
1. Sample Selection: We sample 80 items from the MiniF2F test set in our dataset. Originally, each item consists of:
An informal natural language problem
A formal statement
ground-truth label indicating alignment or misalignment between informal and formal statements
The misalignment type (if the formal statement is misaligned with the informal one)
2. Sample Distribution: We ensure balanced distribution between misalignment and align- ment labels and include diversity of misalignment types for a robust and representative evaluation.
3. Human Evaluation:
The same informal and formal statements the 80 samples are provided to four human experts in Lean 4, who are tasked to independently evaluate autoformalization alignment (i.e., binary classification of alignmen/miislignmeent)
4. Performance Metrics: We calculate the correctness ratio each human evaluator by comparing their assessments with the ground-truth labels.
We similarly calculated the correctness ratio of our FORMALALIGN model by comparing its alignment selection results with the ground-truth labels (i.e., aligned/ The performance of GPT-4o, atate-of-the-art language model L.L--as-judge research, was also obtained on the same task as our automated baseline. We used scoring method with the instruction prompt provided in C.2 and searched for the best threshold to optimize the final correctness ratio.
Results The correct ratio (i.e., total percentage of the aligoment evaluation results matching ground- truth labels) of GPT-4, FORMALALIIGN model, and four human experts are listed below:
Table 11: Correctness ratio and agreement statistics of different evaluation methods sampled M2niF2F test set.
Evaluation Method
Correct Ratio (%)
GPT-4o
47.50%
FORMALALIGN
65.00%
Human Expert
83.75%
Human Expert 2
77.50%
Human Expert 3
77.50%
Human Expert Average
79.58% %
Fleiss' K
0.49
As shown, human experts evaluation achieved the highest correctness ratio in matching with the ground-truth alignment evaluations with an average of 79.58%, followed by our FORMALALIGN (65.00%). The LLM-as-judge method achieves the lowest precision autoformalization alignment evaluation. Each human expert takes approximately 3 hours to review 80 items, while the FOr- MALALIGN model requires less than minutes to conduct the automated evaluation.
Our findings reveal several important insights:
Efficiency and Robustness FORMALAL LIGN: Our FORMALALIGN framework provides a valu- able automated method for evaluating autoformalization alignment due to its efficiency, robustness, and comparable accuracy. FORMALALIGN achieved a correctness ratio 65.00%, which is signifi- cantly higher than that of GPT-4o (47.50%). With scaling, we believe that our automated method FORMALALIGN is promising to even on par with the performance of human experts while requiring significantly less time for evaluation.
22

---

Published as a conference paper at ICLR 2025
Subjectivity of Manual Review: Manual review is subjectively dependent the experts' domain knowledge and does not always achieve high accuracy or consistency. Notably, the human experts only reached moderate interrater agreement ratio of 0.49. This highlights potential variability and inconsistency among the experts' evaluations.
Complementary Role of Automated Evaluation: The results underscore the need for automated evaluation methods to complement human reviews and ensure more consistent and objective alignment assessments. By leveraging the strengths of both manual and automated approaches, we can achieve a more comprehensive and reliable evaluation of autoformalization alignment.
The experiment also highlights the potential for further research in improving automated evaluation methods, as well as investigating the authentic representations of potential misalignments through detailed misalignment type analysis.
H
CASE STUDY
We present a case study of a randomly selected informal-foree statement from our test dataset. We compare how our method and three other metrics (BLEU, BERTscore, Lean 4 Compiler) evaluate the alignment of various types of incorrect formal statements.
Table 12: Case Study: Comparison of Alignment Scores among misalignment types. Each evaluated formal statement is misaligned differently, summarized in the table. All misaligned statements pass the Lean Compiler without errors.
Misalign type
FORMALALIGN
BLEU
BERTscore
Missing conditions
0.56
0.82
0.98
Wrong Constant
0.57
0.95
1.00
Variable Type
0.56
0.95
1.00
Equality
0.55
0.95
1.00
Unpaired Statement
0.57
0.12
0.90
Table 13: Case Study: Visualized Examples of Misaligned Formal Statements.
Natural Language (Informal) Statement
Prove that if x + 2x 5y, and 7y 102. then z/z 7/25.
Misaligned Formal Statements
theorem mathd_alle allebraag
theorem atth_aaggebra_33 y z R)
theorem @athd_algebra_3]
(x y z : B)
(x y z : Q)
(ho 2 x x 5 x y)
(ho *0)
(ho #0)
(h, 7 & = 10 2)
(h, 2 x x x
(h, 2 x =
/ = 7
(h2 7 x
(h2 7 x
2)
2 x = 7 :5
2 7 25
theorem mathd_algebra_33
theorem amc 12 b_2002_p 2 : Z)
y
(ho x =
(ho x 4)
(h) 2 x x x
(3 * x - 2) * (4 *
(ha 7 x 25:-
1) (3 x 2) *
(4 x)
Five types of misaligned formal statements are listed Table I3 together with the original natu-
ral language statements. As shown in Table 12 for misalignments involving missing conditions,
23

---

Published as a conference paper at ICLR 2025
wrong constants, variable type mismatches, and equality violations, the FORMALALIGN consistently below a threshold of 0.7, indicating low semantic precision of the formal statement and likely misalignment. In contrast, both BLEU and BERTscore reported similarly high scores regarding various types of misalignment, demonstrating an inferior performance in evaluating the elusive misalignment in autoformalization.
I ABLATION STUDY OF LOSS FUNCTIONS
To rigorously investigate potential interactions between cross-entropy and contrastive losses in our training framework, we conducted extensive ablation experiments examining models trained with individual loss functions versus our combined approach. This analysis supplements the ablation studies presented in Section 5.2 of the main paper.
We trained three variant models:
Cross-entropy Only (LCE): Trained using only cross-entropy loss with certainty scores as the optimization objective
Contrastive Only (LCL): Trained using only contrastive loss with similarity scores as optimization objective
Combined (Ours): Our proposed approach combining both losses
We maintained consistent hyperparameters across all training configurations to ensure fair comparison. Table 14 presents the comprehensive comparison of different training approaches:
Table 14: Performance comparison of models trained with different loss functions. Higher scores indicate better performance.
Training Method FormL4-Basic
FormL4-Random
MiniF2F Valid
MiniFFF Test
LCE (w/ cer)
95.45
82.31
50.12
51.89
LCL (w/ sim)
42.76
18.92
18.33
19.45
Combined (Ours) 99.21
85.85
66.39
66.70
Our analysis reveals several key findings:
Individual Loss Limitations: Models trained with single loss functions demonstrate significantly reduced performance. The LCE model achieves moderate results but falls short of the combined approach, while the LCL model shows particularly poor performance isolation.
Complementary Effects: The superior performance of the combined approach across all datasets suggests that the two loss functions capture complementary aspects of the autoformalization task:
Cross-entropy loss helps capture sequence-level patterns crucial for autoformalization
Contrastive loss enhances representation--lvel relationships between formal and informal expressions
The combined approach maintains its performance advantage across different evaluation settings, with relative improvements ranging from 4-16
Consistent Improvement:
These findings complement the ablation studies presented in Section 5.2 of the main paper in several ways: They provide empirical validation for our theoretical motivation behind combining the losses. They demonstrate that the performance improvements consistent across different datasets. They show that the combined approach does not compromise either aspect of the learning objective
Furthermore, when considered alongside the metric bias analysis in Section 5.3, these results strengthen our conclusion that the combined loss structure genuinely enhances model performance rather than exploiting evaluation metrics. The consistent improvement across different evaluation schemes suggests that the model learns a more robust understanding of the autoformalization task through the complementary training signals.
24

---

Published as a conference paper at ICLR 2025
Table 15: Comparison of Different Alignment Evaluation Methods.
FormL4-Basi
FormL4-Randond
MiniF2F-Valid
MiniF2F-Test
Models
Prec.
Rec.
A$
Prec.
Rec.
AS
Prec.
AS
Prec.
Rec.
GPT-4 (Scorc)
88,91
26.33
88.69
90.52
28.56
90.02
64.34
44.58
90.98
68.31
51.11
94.65
GPT-4 (Binary)
89.45
35.21
87.92
91.12
38.45
89.76
65.82
52.33
89.54
69.45
58.92
93.21
GPT-4 (CoT)
90.23
42.68
88.15
91.85
45.72
89.95
67.24
59.85
89.87
70.82
62.45
92.88
GPT-4 (Two-Phase)
89.35
38.21
87.95
91.20
41.10
89.55
65.75
53.30
89.10
69.40
57.80
92.10
FormalAlign
99.21
93.65
86.43
85.85
86.90
89.20
66.39
68.58
60.66
64.61
66.70
63.37
J ANALYSIS OF ALTERNATIVE ALIGNMENT EVALUATION STRATEGIES
To thoroughly evaluate alternative approaches for autoformalization alignment checking, we explored several variants of GPT-4-based evaluation methods. Table 15 includes binary classification approach that directly assesses alignment correctness, a Chain of Thought (CoT) strategy that employs step-by-step reasoning, and two-phase evaluation process that separates back-translation from alignment checking.
The binary classification approach simplifies the evaluation task by having GPT-4 make direct true/false judgments about alignment correctness, replacing the original 1-5 scoring system. This modification addresses potential ambiguity in score interpretation and provides more well-defined evaluation criterion. The Chain of Thought strategy extends this further by prompting GPT-4 to explicitly reason about potential discrepancies between informal and formal representations before making alignment decisions. The two-phase method separates the evaluation process into distinct Pack-translation and alignment checking stages encourage more detailed analysis.
Our experimental results reveal several key insights about these evaluation strategies. The binary clas- sification approach shows moderate improvements over the baseline scoring method, with increased precision across all datasets while maintaining similar recall levels. The Chain of Thought strategy demonstrates the strongest performance among GPT-4 variants, achieving notable precision gains of up to 16 percentage points compared to the baseline. This improvement suggests that explicit reasoning steps help GPT-4 better identify subtle alignment issues. The two-phase approach shows comparable improvements to binary classification but introduces additional computational overhead and potential error propagation between phases.
Despite these improvements in GPT-4- bassed methods, FormalAlign maintains superior performance, particularly in precision metrics. The significant performance gap between FormalAlign and even the enhanced GPT-4 approaches underscores the value of our specialized alignment detection model. Notably, Formal Align achieves these results with a smaller model size, demonstrating the effectiveness of our proposed training strategy over pure scaling of model capabilities.
These findings suggest that while improved prompting strategies can enhance GPT-4's alignment evaluation capabilities, a dedicated model trained specifically for aligmment detection offers more robust and reliable performance. The results also highlight the importance of explicit reasoning in alignment evaluation, as evidenced by the strong performance of the Chain of Thought approach among GPT-4 variants.
K PERFORMANCE ACROSS MISALIGNMENT TYPES
This section presents a detailed analysis of how different methods perform across specific types of mathematical misalignments, providing insights into the relative strengths and limitations of automated versus human evaluation approaches. We analyze performance across six distinct mis- alignment categories: constant modifications, exponent alterations, variable type changes, new
25

---

Published as a conference paper at ICLR 2025
Table 16: Performance Comparison Across Misalignment Types
Misalignment Type
Human
Method
GPT-4o
À (Human-Method)
A (Method-GPT4o)
Constant
75.2
58.4
42.1
16.8
16.3
Exponent
73.8
60.2
44.3
13.6
15,9
Variable_ type
78.9
64.5
46.2
14.4
18.3
Variable_nes new
81.3
66.7
48.9
14.6
17.8
Equality
82.4
67.8
49.5
14.6
18.3
Random
85.9
72.4
54.0
13.5
18.4
Overall
79.6
65.0
47.5
14.6
17.5
variable introductions, equality relationship modifications, and random pairings. The result is shown in T6
Our analysis reveals a consistent hierarchical pattern in detection capabilities across all evaluation methods. Random pairing misalignments proved most detectable, with human experts achieving 85,9% accuracy, our method 72.4%, and GPT-4o 54.0%. This superior performance on random pairings is attributed to the substantial structural and contextual discrepancies these misalignments introduce, making them more readily identifiable by both automated and human evaluators.
Conversely, subtle modifications involving constants and exponents presented the greatest challenge. Human performance decreased to 75.2% for constant changes and 73.8% for exponent modifications, with proportional decreases observed automated methods. This performance degradation on nuanced mathematical changes highlights critical challenge in automated alignment detection: the ability identify and evaluate fine-grained numerical and syntactic modifications that can substantially alter mathematical meaning while maintaining surface-level similarity.
The performance gap between human evaluators and our method remains relatively consistent, averaging 14-16 percentage points across all misalignment types. This consistency suggests that while our method successfully captures fundamental patterns in mathematical alignment, still lacks certain aspects of human mathematical intuition, particularly in recognizing subtle contextual shifts. Similarly, our method maintains a consistent advantage of 15-20 percentage points over GPT-4o across all categories, demonstrating that our targeted modeling of structural and semantic relationships yields substantial improvements over standard language model capabilities.
The observed performance patterns carry significant implications for future development of alignment detection systems. While our method shows particular strength identifying structural modifications, such as equality alterations and random pairings, the relatively weaker performance subtle variations suggests a need for enhanced mathematical reasoning frameworks. Future work might focus on developing more sophisticated mechanisms for detecting and evaluating minor mathematical modifications, potentially through integration of formal mathematical reasoning systems or expanded training with synthetic examples emphasizing these nuanced changes.
L QUALITY ASSURANCE OF DATASET CONSTRUCTION
To validate the effectiveness of our synthetic dataset construction methodology, we conducted a com- prehensive empirical study comparing model performance on synthetic test cases versus real-world autoformalization errors. This analysis aims to assess whether our synthetic error generation approach adequately captures the characteristics of errors that naturally occur during autoformalization.
We first established a real-world validation set by having Gemini perform autoformalization on 100 randomly sampled theorems from our test sets using few-shot prompting. Three expert Lean users independently reviewed these formalizations, annotating misalignments and providing corrections where necessary. This process yielded 78 pairs aligned-misalee misaligned formalizations, providing a ground truth dataset of authentic autoformalization errors.
26

---

Published as a conference paper at ICLR 2025
Table 17: Performance comparison between synthetic and real-world evaluation
Evaluation Set
Accuracy (%)
Precision (%)
Recall (%)
Synthetic Test
85.8
86.9
89.2
Real-world Validation
83.5
80.2
79.8
The performance comparison between our synthetic test set and the real-world validation set is presented in Table 17
Our analysis reveals that while model performance real-world enrors shows slightly lower metrics compared to synthetic cases (approximately 3-9% difference across metrics), the strong overall results suggest our synthetic dataset effectively captures many key aspects of natural autoformalization eroos. The comparable performance indicates that the error patterns generated through our synthetic approach meaningfully align with those encountered in practice.
Further examination of error cases revealed that synthetic examples tended to produce more systematic and well-defined misalignments, while real-world errors occasionally exhibited more nuanced patterns involving multiple simultaneous misalignments. This observation suggests that while our synthetic dataset provides comprehensive coverage of individual error types, real-world autoformalization errors can manifest in more complex combinations.
These findings validate our synthetic dataset construction approach while highlighting opportunities for future enhancement. The strong correlation between performance on synthetic and real-world cases demonstrates that methodology produces training data that effectively prepares models for practical autoformalization tasks. Future work could potentially benefit from a hybrid approach that combines synthetic error generation with curated real-world examples to capture both systematic coverage and naturally occurring error patterns.
M FORMAL DEFINITION AND BROADER SIGNIFICANCE OF AUTOFORMALIZATION ALIGNMENT
M.1 FORMAL DEFINITION OF AUTOFORMALIZATTOO ALIGNMENT
To standardize the evaluation and understanding of autoformalization alignment, we propose the following formal definition:
Given a natural language statement and its formalization F, where F is verified as syntactically valid by the formal language compiler, the alignment A(N, F) is defined as binary relation such that:
1. F' preserves all mathematical constraints specified in N,
A(N,F) =1 A) =
2. F maintains the same logical expressed in N,
3. F does not introduce additional constraints not present N.
In essence, A(N,F) 1 if and only faithfully captures the mathematical intent and logical structure of N, without introducing extraneous constraints or omitting critical elements. This definition provides precise framework for evaluating whether formalization accurately aligns with its informal counterpart.
M.2 BROADER SIGNIFICANCE OF AUTOFORMALIZATION
Autoformalization, the automated conversion of natural language mathematics into formal languages, represents transformative research direction with implications across diverse fields. By bridging human mathematical reasoning and machine-verifiable systems, it unlocks new opportunities for innovation and efficiency.
Applications in Software Engineering and Verification
27

---

Published as a conference paper at ICLR 2025
Automated Translation of Specifications: Autoformalization enables the conversion of natural language system specifications into formal properties for verification, reducing the time and effort required for manual formalization.
Ambiguity Detection: It helps identify ambiguities and inconsistencies in informal specifi- cations, ensuring that implementations faithfully adhere to their intended design.
Enhanced Verification Workflows: By integrating autoformalization into software engi- neering pipelines, developers can achieve faster and more reliable verification of complex systems.
Impacts on Mathematical Knowledge Management
Converting informal mathematical content into machine-checkabee formalizations ensures its longevity and accessibility for future generations.
Preservation of Mathematical Knowledge:
Organization and cosss-eferencing: Formalized content can be systematically organized, enabling researchers easily locate and cross-reference related concepts and proofs.
Support for Automated Reasoning Systems: By expanding the corpus of formalized math- ematics, autoformalization facilitates advanced reasoning and discovery within automated reasoning tools.
Advances in Automated Reasoning Research
Broader Applicability of Theorem Provers: With autoformalization, theorem provers can operate natural language inputs, significantly expanding their usability for non-expert users.
Hybrid Reasoning Systems: Autoformalization enables systems that combine formal and informal reasoning, allowing for more flexible and powerful problem-solving approaches.
Acceleration of Mathematical Research: Automated reasoning systems informed by autoformalization can provide immediate feedback, improving their utility and effectiveness for mathematicians and researchers.
M.3 CONCLUSION
The formal definition of aligmment provides a rigorous basis for evaluating the correctness and fidelity of autoformalization systems. Coupled with the broader contextualization of its signifi- cance, this framework underscores why advancing autoformalization technologies is critical for enhancing software engineering, mathematical knowledge management, and automated reasoning research. These contributions highlight the profound potential of autoformalization as a comnestone of interdisciplinary innovation.
28


Reviews:
[{"review_id": "wKFtpRYiJv", "reviewer": "Reviewer_Y3AS", "summary": "This paper introduces FormalAlign, an automated alignment evaluation framework designed for autoformalization tasks. FormalAlign addresses the challenge of ensuring semantic alignment between informal and formal mathematical statements, a critical issue given the limitations of traditional manual verification methods. By employing a dual loss framework that combines cross-entropy loss and contrastive loss, FormalAlign enhances its alignment detection ability in a comprehensive way. Evaluations on FormL4 and MiniF2F demonstrate FormalAlign’s superior performance over GPT-4, with notable improvements in precision scores.", "questions": "Have you considered splitting the alignment-checking baseline for GPT-4 into two steps: back-translation followed by a natural language alignment check? This approach could encourage GPT-4 to capture more details during the back-translation phase and minimize any impact from its limited familiarity with Lean during the alignment-checking stage.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "- FormalAlign demonstrates high precision across two major datasets, maintaining robust recall scores. \n- In the LLM-as-judge setting detailed in Appendix G, FormalAlign notably outperforms GPT-4o in identifying nuanced misalignments and step further to human experts' level.\n- FormalAlign's approach shows strong potential for enhancing the quality of autoformalized statement datasets in Lean, providing a valuable contribution to training more effective automatic theorem-proving models.", "weaknesses": "- The misalignment strategy \"Change of Variable Type\" in Table 2 may create examples that should be considered aligned rather than misaligned. Specifically, the example provided, where the variable type is changed from real numbers (R) to rational numbers (Q), does not necessarily create a misaligned example. The original natural statement does not explicitly require the variable to be real numbers. The proposition with the variable in Q still accurately reflects the original question. \n- The misalignment strategies discussed in the paper appear to be primarily applicable to high-school-level mathematics or below. When dealing with more advanced mathematical statements, such as those only involving logic, quantifiers, or set theory, half of the proposed misalignment methods, including constant modification, exponent modification, and modification of equality, become less relevant or inapplicable. This limitation suggests that the strategies may not generalize well to more complex mathematical domains.\n- A more extensive ablation study to determine the optimal balance between the two components of the loss function, $ L_{CE} $ and $ L_{CL} $, is recommended. Specifically, the study could explore how different balancings affect the model's performance on the pure autoformalization task. Understanding this balance could provide insights into the trade-offs between the two loss components and potentially enhance the model's ability to accurately formalize mathematical statements.\n- The ablation experiment in Section 5.2 may not effectively demonstrate the benefits of combining cross-entropy and contrastive loss, as these two loss functions have distinct objectives and may steer the training process in different directions. This discrepancy is particularly pronounced when using the hidden state of a decoder-only model, which is not inherently optimized for capturing semantic information. Since the alignment-selection metric (the average of certainty and similarity scores) naturally favors models trained with the combined loss, the improvement in scores may reflect a metric bias rather than a genuine enhancement from the augmented loss.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "jsDh4iRoyi", "reviewer": "Reviewer_G7JL", "summary": "The authors propose to check the alignment between informal and formal mathematical statements using a model trained both on the autoformalisation and alignment tasks. This approach is automatic, avoiding the scaling issues of manually checking, while enhancing previous approaches that relied either on BLEU relative to a ground-truth statement or checking for logical consistency, since statements can be logically consistent but misaligned. To validate their approach, the authors create a dataset by mutating knowing correct informal-formal pairs using one of the following operators: modify constant, modify exponent, introduce variable, change variable type, and modify equality. Further, they also introduce misalignments by shuffling the formal/informal data for random pairings. The authors demonstrate improvements in alignment score and precision across FormL4 and MiniF2F.", "questions": "1. Looking at the Table 3 results, and considering that you have an alignment threshold, would it be possible to obtain P-R curves for FormalAlign? If so, I would like to know the performance of the approach when matching GPT-4 recall (So P@(R=0.9)). Further, presenting the P-R curves would allow people to have a better understanding of the performance, while providing such curves to users of the approach for evaluation could make a more informed choice of the threshold value depending on the expected manual load afterwards.\n\n2. Is there a reason why the strategies were applied non-uniformly to generate negative examples? (The strategies are in Table 2, while Figure 3 presents the distribution of misalignments generated.)\n\n3. For the case study and LLM-as-judge results, do you have per-misalignment-type data? Would it be possible to report that, as it would be interesting if any category is especially difficult/easy to spot?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 4, "strengths": "+ Solving the autoformalisation as an autoformalisation and alignment joint task which should enable better inner representations.\n+ Ablation study to empirically show the value of both tasks (hence the value of cross-ent and contrastive loss and the value of considering both sequence probability and similarity for the alignment score).\n+ Empirical justification of the foundation model that is used/fine-tuned for FormalAlign.\n+ \"Mutation\" based construction of a known ground-truth dataset.", "weaknesses": "- Results are presented at a fixed alignment score threshold instead of P-R curves. (I suspect this is due to a lack of access to create such curves for GPT models).\n- The misaligned types generated are not uniform (Figure 3)\n- Model performance by misalignment type is not reported, the case study is only vs BLEU and BERTScore, which is welcomed, but a comparison with GPT-4 would also be welcomed. (A similar breakdown for the LLM-as-judge study would also be welcomed)", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "E8vhvUxJ3v", "reviewer": "Reviewer_8v22", "summary": "This paper introduces a novel framework, FormalAlign, which trains a Large Language Model (LLM) to evaluate autoformalization alignment. Beyond the standard cross-entropy loss derived from viewing autoformalization as a sequence generation task, FormalAlign incoperates a new loss term as a dual objective. This new loss measures alignment between the informal and formal versions by leveraging the cosine similarity between their representations. Experiments on the FormL4 and MiniF2F datasets demonstrate the effectiveness and robustness of FormalAlign.", "questions": "- FormalAlign appears to focus exclusively on statement autoformalization. Could this framework be extended to proof autoformalization as well?\n- The certainty score and similarity score operate on different scales ([0,1] and [-1,1] respectively). Why are these combined using a simple average?\n- The authors claim that FormalAlign can significantly reduce the need for manual verification, but only limited evidence is presented in the experiments. Could the authors provide more quantitative results on this claim? For instance, by deploying FormalAlign in a complete autoformalization pipeline, how many formalizations can be automatically verified?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- The paper addresses an important and relatively unexplored problem—improving the autoformalization of mathematical statements.\n\n- The proposed framework is intuitive and easy to understand, achieving promising empirical performance on challenging evaluation datasets.", "weaknesses": "- The discussion on the broader significance of autoformalization is lacking, which limits the accessibility of this problem to researchers in other fields (e.g., software verification). Furthermore, providing a clear formal definition of autoformalization alignment would enhance the reader’s understanding of the paper’s objectives.\n-  The running example is somewhat unconvincing to me. First, in this example, the alignment issue can be detected easily by verifying whether the statement is provable. Using the lean-set tool, a counterexample [b := 7/8, a := 1/2, c := 63/160] can be found. Second, the low certainty score suggests that LLMs may only generate this example with low probability (correct me if not).  \n- The construction of datasets is a bit unnatural. The authors generate negative examples by mutating correct input-output pairs, but these synthetic examples may not realistically reflect the types of errors typically produced by LLMs during autoformalization.\n- The reference section contains a duplicated citation for Deepseekmath, and some related works are missing, such as [1, 2, 3].\n\n[1] Murphy, Logan, et al. \"Autoformalizing Euclidean Geometry.\" ICML, 2024\n\n[2] Li, Zenan, et al. \"Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency.\" NeurIPS, 2024.\n\n[3] Zhang, Lan, et al. \"Consistent Autoformalization for Constructing Mathematical Libraries.\" EMNLP, 2024.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "hbYPqJpEX5", "reviewer": "Reviewer_ok2Q", "summary": "This work presents a technique for automatically evaluating the semantic alignment between a natural language description and its corresponding formal representation that may be produced by an AutoFormalization system (Autoformalization aims to convert informal mathematical proofs to formal proofs that can be automatically checked by existing theorem provers). The technique is based on fine-tuning a base LLM with respect to a dual loss function that combines cross-entropy loss in the sequence generation with a contrastive loss based on cosine similarity of the informal/formal pairs. The technique is evaluated on existing datasets for autoformalization that are augmented with misalignment strategies proposed by the authors to test negative examples of incorrect formalizations. It is shown to have superior performance in many cases against GPT models prompted with a similar alignment evaluation task.", "questions": "1. I am confused  about the Metrics description in section 4.2. I thought this should describe the metric itself independently of the system being evaluated (whether is your system or any other baseline system). But the AS and detection metrics are defined with respect to the V_align function which seems specific to your model only and used in its inference. Is that specific for the FormalAlign model only or otherwise how are these metrics computed for the other models like GPT4? (I hope that is not the case as they would then be really problematic metrics to be using that are specific to your model). And if that is not the case then please move this discussion to the inference section - since they look like modes of inference in which your model can be used: it can either select the best formalization from a given set (selection), or return a true/false label for a given informal/formal pair (detection). The metrics are then just to measure the quality of these two selection and detection modes of inference using standard precision/recall. \n\n\n2. Similarly, can you clarify exactly how you compute AS, precision and recall numbers for the GPT models? (As above, I hope you are not computing the alignment scores for them in the exact way you describe in section 4.2). I am assuming it is based on you prompting the models to predict an \"alignment score\" from 1-5 as in the prompt in Appendix C2? Please confirm this is correct and it should be explained clearly in the evaluation section. Also please explain the details - how is AS inferred from 1-5 score generated by GPT model? How is precision measured? What if there are ties on the top score between multiple candidate formalizations? \n\n\n3. I dont understand the second prompt in Appendix C.2 - it is just doing a translation task? How is it used in your evaluations? Or is it just the prompt used to run your final fine-tuned model for the sake of generating and extracting the alignment scores?\n\n4. Just to confirm - you do not use the synthetically generated misalignment data for training at all right? \n\n5. What is SIM() function in Figure 2? - is it the same as Cos()? If so please fix for consistency.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "1. Innovative focus on the alignment problem in Autoformalization. Translating informal mathematical proofs into formal, machine-verifiable formats is an important problem in fields like theorem proving and formal verification, since formal systems (e.g. Lean, Isabelle) are highly precise but difficult for humans to use. This work brings an explicit focus on a key issue that plagues autoformalization: to ensure semantic alignment between the informal input and formal output. This is an important problem to address, since formal provers can check for syntactic but not semantic correctness with respect to the original intent, and other metrics such as BLEU scores are very imprecise. Addressing this alignment problem explicitly seems a novel angle taken by this work, and such focus could help further progress in the field of autoformalization.  \n\n2. Dual-Task Training Approach. The technique of simultaneously training to generate formal statements and check alignment is interesting. While multi-task learning and contrastive learning have been used in other areas (e.g., machine translation, image-text alignment), the combination of sequence generation with contrastive alignment seems to be a novel application in the context of autoformalization. \n\n3. Clarity and presentation. Though some parts unclear (see below), in general the paper clearly explains and motivates the problem, and explains the technique well, including definitions of the combination of cross-entropy loss (for sequence generation) and contrastive loss (for semantic alignment). The evaluation covers some important aspects to show that on the synthetically augmented datasets the technique performs well in general, and also better or comparable to alignment inference based on prompting GPT models. This demonstrates the core value of the technique. The authors also  include ablation studies that provide insight into the contribution of both kinds of loss functions, as well as comparison with human evaluation.", "weaknesses": "1. Use of synthetic data for evaluation. To evaluate alignment, the authors create a synthetic dataset of negative example formalizations based on explicit misalignment strategies that they propose. I do not have a sense of how realistic those misalignments are in practical terms. I think addressing this issue is important,  especially since the whole purpose of the task is to detect the errors made by existing AF systems: we should be testing the ability to detect those kinds of variations, which could be very much smaller and more subtle than the ones produced by the explicit misalignment strategies here - would the contrastive loss be able to help distinguish between those kinds of variations (for which the task is actually intended)? While I understand such data is not readily available, I think it should be possible to obtain some real data perhaps in the following way: since you already have access to human judges (which you used for a similar task), perhaps you can run a SoTA AutoFormalization system on the standard datasets you use here, get the outputs and ask the human judges to label correct/incorrect for the formalizations produced and also provide corrected formalizations. Then just check the alignment evaluation against this data (which would provide one positive and one negative example for each case where the AF system had failed). The dataset need not be very big as it is only to be used for evaluation. Such an approach would also show the actual improvement you can make to a SoTA AF system. \n\n2. Lack of compelling baselines in comparison. The prompt used for GPT models Appendix C.1 seems to ask GPT to assign an \"alignment score\" from 1 - 5. This seems a pretty vague and not well-defined task that may be difficult for the model (or even a human) to interpret. A more well-defined question is to simply ask if the formalization correctly represents the informal NL or not - since that is the main (only) problem we are trying to solve? Scoring seems to make it a subjective/continuous domain problem - e.g. it may be possible that a given formalization correctly represents the problem, but perhaps the model may still assign it a score 4 rather than 5 due to some stylistic differences with the informal input it detects. Having a true/false binary judgement would make a more well-defined task for the model to address. Also, this seems a very obvious case of where Chain of thought (CoT) reasoning should be tried as another baseline - the evaluation task is very reasoning based and the GPT models can be expected to do much better with CoT reasoning to infer any discrepancies between the informal and formal representations - rather than just predicting some number score from 1 to 5. Especially since you do not have other baseline or SoTA methods to compare against (do there exist such methods?), using a CoT baseline is easy to implement and would be very relevant here. You also provide all the candidate formalizations in the same prompt - perhaps evaluating each one of them separately will be a better approach so not to confound the model with too many tasks at the same time. \n\n3. Some problems with positioning/presentation. You state in the abstract: \"FORMALALIGN trains on both the autoformalization sequence generation task and the representational alignment between input and output, employing a dual loss that combines a pair of mutually enhancing autoformalization and alignment tasks.\" and make similar statements in the introduction. That sounds like you are addressing both the autoformalization task as well as the alignment evaluation task - but you have not shown any evaluation of the autoformalization task - if that is not an intended contribution of the work then such statements are a bit misleading or confusing in the intro and abstract. It should be clarified that you are only providing an evaluation method to test alignment of given candidate informal-formal pairs. Also, if the AF task itself is not a contribution - why not? If the combination of cross-entropy and contrastive loss accurately infers alignment, why can't the fine-tuned model based on that dual loss function be better at the autoformalization task overall? Could you have compared it to prior auto-formalization approaches? \n\nTypos: \n- \"The challenges of automated evaluating natural language\"\n- \"to train an FORMALALIGN\"\n- \"Eq. equation 5. Table 6\"", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)