Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
Authors: Zenan Li
Yifan Wu
Zhaoyu Li
Xinming Wei
Xian Zhang
Fan Yang
Xiaoxing Ma
Venue: NeurIPS 2024 poster (2024)
Keywords: Automated theorem proving
Autoformalization
Large language model
Self-consistency
Primary area: machine_learning_for_other_sciences_and_fields
TL;DR: A new framework for autoformazing mathematical statements

Abstract: Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@1 and pass@k accuracies in LLM-generated formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k autoformalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Elaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using automated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings of the original and informalized texts. 
Our extensive experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.35x relative improvements across various LLMs and baseline methods.

Autoformalizing Mathematical Statements by Symbolic Equivalence and Semantic Consistency
Zenan Li Yifan Wu Zhaoyu Li Xinming Wei?
Fan Yang² Xian Zhang' Xiaoxing Ma
State Key Lab of Novel Software Technology, Nanjing University, China 2Peking University, University of Toronto *Microsoft Research Asia
1 njju en, yifan. wuêstu, p.u.ppuu.ee edu. cn, 2hxian@miccrosofu com, xxm@nju. edu.
Abstract
Autoformalization, the task of automatically translating natural language descrip- tions into formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@ and pass@k @k accuracies in LLM- L-M-eenertted formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k auto- formalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Flaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using au- tomated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings experiments the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.355 rela- tive improvements across various LLMs and baseline methods. The data and code are available at https::/ //github. com/ Miracle- Messi/Iese Isa- AutoFormal
the original and informalized texts. Our extensive
Introduction
Autoformalization is the automated process of translating from natural language expressions into a formal language [[4]. Successful autoformalization alleviate the demand for extensive human expertise and reduce the substantial manual formalization efforts [5)8], as well as fundamentally bridging the gap between natural (or so-called "informal") and formal languages [9) which potentially catalyzes breakthroughs in many fields such as mathematical theorem proving, /oftware/hardware verification, and autonomous planning [4]. Despite decades of research, the practical application of autoformalization remains limited because traditional methods often necessitate either predefined domain-specific languages hard-coded translation rules 115
Recently, large language models (L..Ms) have shown promising performance in autoformalization, especially in formalizing mathematical statements [11 For instance, using Codex [22] with few shot examples can achieve a 25.3% success rate formalizing high-school level problems from the MATH [24] dataset. Nevertheless, the autoformalization capability of LLMs has not been fully exploited. As shown in Figure D even advanced LLMs like GPT-4 24 struggle with translating a
Eqqual contribution. This work was partially done during Zenan's and Yifan's internships at MSRA.
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

Prompt:
Natural language version: "Find the product of 0. \overline(6) and 6. The answer is 4." Translate the natural language version to Isabelle version.
GPT-4 output (No.1): theorem
GPT-4 output (No.2): thearem
GPT-4 output (No.3): thearem
GPT-4 output (No.4): thearem
fixes y :: real
fixes a :: real
fixes x y :: real
fixes x y :: real
assumes "x = 0.66"
assumes "a 2/3"
assumes "x 2/3"
assumes "x 0.6666"
and "y 6"
and "b 6"
and "y 6"
and "y 6" shows "x * y 4"
shows "x * y 4"
shows "a
4"
shows "x y 4"
An illustrative example of autoformlization. The mathematical statement from the MATH dataset is translated into formal version by GPT-4. Only two formalization results (No.2 and No.3) are correct, while the others fail in the grounding (0.) oveerline + 2/3).
Figure I:
seemingly straightforward statement (i.c., calculating 0.6 6), due to its unreliability of grounding recurring decimal to its exact fractional equivalent (0.6 + 2/3).
Although the initial attempt formalizing the previous example fails, we observe that multiple generations of GPT-4 can often successfully cover the correct formalization. In other words, a significant disparity exists between pass@1 (the top-1 generation correct) and pass @K k (one of the top-k generations is correct) in autoformalization by LLMs. We further confirm this phenomenon by checking the autoformalization accuracy on the MATH and miniF2F (25) datasets. The curves de- picted in Figure demonstrate that pass@E & accuracy can be consistently improved with additional gen- erations, resulting in an accuracy gap ranging from 19.5% to 26.5% between pass@1 and pass @ 10.
Pongt: Nwwdtt.oogaa Aormayy
60.0%
Pawst Acsmmey &
52.4%
33.5%
32.9%
To bridge the performance gap between pass@1 and pass@k, k, natural approach is employing the idea of self-consistency [26]] 27 to rank the autofor- malization candidates and then selecting the most consistent one. However, compared the standard self-con self-consistency techniques used in mathematical rea- soning and code generation with LLMs, applying this method faces unique challenges. In mathematical reasoning, self-consistency always derived by com- paring the final answers from different generations, yet this approach struggles with inconsistencies in symbolic variable declarations ((a, b) vs (x, y)). In code generation, while self-consistency relies on comparing execution behaviors across different generations, this approach is less viable for formalized mathematical statements, which lack the necessary test cases for such evaluations.
Number of Geaeeations
Number of Generntiens (k)
Figure Pass@k curves for GPT-4 autofor- malization on the MATH (left) and miniF2F (right) datasets. The results show that LLMs can achieve higher coverage of correct formal statements with an increasing number of gen- erated candidates up to k = 10. Beyond this point, the improvement gradually diminishes as & continues to increase.
To address these challenges, we propose novel framework that establishes the self-coonistency of autoformalization from two innovative and complementary dimensions: symbolic equivalence and semantic consistency. Symbolic equivalence generalizes traditional comparisons like final answers and execution behaviors to verify the logical equivalence among autoformalization candidates. This is achieved by using automated theorem provers such as Sledgehammer (28). Z3 (2), and CVC5 (30 On the other hand, semantic consistency rectifies unintended reasoning discrepancies that symbolic cquivalence might overlook by mcasuring the embedding similarity between the re-informalized (back-translar (31)) result and the original natural language statement. This comparison helps to ensure that the autoformalization process preserves the intended meaning and coherence of the original statement. To harness the strengths of both consistency methods, we also develop three strategies to combine the scores from these approaches.
We conduct extensive evaluations on two widely used mathematical datasets, MATH and miniF2F, to validate the efficacy our proposed methods. The experimental results demonstrate that symbolic equivalence and semantic consistency are synergistic, and our combination strategy can achieve final improvements up to 7.8% and 10.7% using GPT-4 compared with the baseline approaches. The relative efficiency of our method, ranging from 8.4% to 21.9%, indicates that our approach

---

can significantly reduce the manual effort required for verifying or labeling formalization results, efficiently minimizing human intervention correcting and validating outputs. Additionally, we extend our experiments to five proprietary or open-source L.MSs, showing the consistent effectiveness of the proposed methods.
In summary, this paper makes the following main contributions: (I) identifying the performance gap between pass and pass@k for LLMs in autoformalization tasks; (2) introducing two self- consistency methods, symbolic equivalence and semantic consistency, and three combination strate- gies to enhance LLM autoformalization performance; (3) providing extensive experiments across various model sizes on two popular datasets, confirming the efficacy of the proposed approach.
2 Background and Related Work
Formal mathematics. Formal mathematics aims to establish a rigorous framework to express math- ematical theorems and proofs in a format that can be verified by a computer through the application of logical rules. Interactive theorem provers, such as Isabellc/HOL (2). Coq [33], and Lean [34), provide environments for encoding and verifying mathematical proofs programmatically. For decades, researchers have used these tools to manually formalize a range of challenging mathematical concepts and theorems 7 37). However, translating mathematics into a language that theorem provers can interpret often requires deep understanding of both the mathematics involved and the syntax of the target formal language. Therefore, the formalization process is always labor-intensive even for large groups of experts, creating significant bottleneck in this field.
Autoformalization with LLMs. To mitigate the laborious process of manual formalization, recent advances have explored the potential of LLMs in autoformalization (38. A stream of research focuses on autoformalizing mathematical statements [19211 33942]. For instance, FIMO [4]] employs GPT-4 with reflection formalize problems from the International Mathematical Olympiad.
ProofGPT (20] and MMA [2]] train LLMs on large-scale datasets with both informal and formal mathematical data to evaluate their performance on statement autoformalization. Concurrently, another research direction investigates the autoformalization of mathematical proof' [10] 43 48). For example, DSP [00] utilizes LLMs to draft informal proofs and map them into formal sketches, with automated theorem provers employed to fill in the missing details in the proof sketch. Besides these efforts, several studies [19 21 explore the performance of LLMs for the inverse process of formalization, i.e., informalization, which translates formal statements back into natural language.
Self-consisenccy for LLMs. Self-consistency was originally proposed to boost the mathematical reasoning capability of LLMs (26 52) This approach aims to identify the homogeneity among multiple generations, thereby bridging the performance disparity between pass @ and pass@ k. In
contrast to other techniques, such training additional crifier//rerrnnke [53] 54 or directly fine-tuning the model [55], self-consistency is entirely data-free, making it readily implementable with off-the-shelf LLMs without incurring the so-called "alignment tax" associated with additional computational costs [55]. Recently, self-consistency has been further adapted to code generation, which closely resembles autoformalization since they both involve formalizing natural language statements. However, in code generation, self-consistency for LLMs typically relies on the execution information from test cases [27 56)58) e.g., whether the two programs produce the same output for identical test inputs. Therefore, this strategy is not applicable to autoformalization due to the absence of test cases for mathematical statements.
3 Methodology
Our framework, as illustrated in Figure comprises four steps to enhance the autoformalization process of LLMs. Initially, LLMs generate & autoformalization candidates for given mathematical statement in natural language. Subsequently, our framework establishes the symbolic equivalence among these candidates and assigns a symbolic score to each based on the derived equivalence classes. Each formal statement then re-informalized using LLMs, and the semantic score computed by comparing the embeddings of the re-informalized text and the original statement. Finally, our framework normalizes and combines these scores to rank the autoformalization candidates and determine the final formalization results.
3

---

Mathematical statement in formal language
Mathematical statement natural language
Fornalization
Informalization
Lobuues..... thoores tireal *x 2/3" stows
"Find the of
()everline(S) and
sic Prove that wheneyou
Flams :cneal acsumen and
Sheomenn
The answer is 4."
add
muttipyy
Autoformalize
Informalize
Symbolic equivalence
rSxen :ireal Resures ta 2/3"
Semantic equivalence
and
Scoring and output
Symbolic Equivalence
Semantic consistency
Figure 3: The overview of our autoformalization framework. In the framework, symbolic equivalence constructed among formalized statements, and semantic consistency is computed between the informalized statements and the original statement. The scores from these two evaluations are combined to rank and select the final formalization results.
3.1 Symbolic Equivalence
We first instantiate self-consiste consisteny as symbolic equivalence among autoformalization candidates. The rationale behind the symbolic equivalence is straightforward: correct formalizations are logically equivalent, even when expressed with varied symbols. To establish symbolic equivalence, we decompose formal statements into their premises and conclusions. Symbolic equivalence between two statements is then defined by the logical equivalence of both their premises and conclusions.
The formal definition of symbolic equivalence presented in the following. Within this definition, we further assume that the premises are not intrinsically contradictory, ensuring that the two involved mathematical statements are well-defined.
Definition 1 (Symbolic equivalence) Let two mathematical statements V and 12 in formal lan- guage be expressed as P, - Q1 and P2 + 22, and suppose their premises P1 and P2 are not tautologies. Then, the two statements are called symbolically equivalent if the two logical equivalences, ie., P1 = P2 and Q = 22, both hold.
The two logical equivalences induced by the symbolic equivalence be determined through existing automated theorem provers (ATPs). Additionally, the validity of the premises can also be checked by replacing the conclusion Q with contradietory result (e.g.. 0 and verifying P Q. If this vacuous form can be proved, then the corresponding premise P is a contradiction.
It is also worth noting that variable misalignment between two statements remains challenge for validating symbolic equivalence using ATPs. For instance, the examples in T (No.2 and No.3) not be proved symbolically equivalent due to the inconsistent variable declarations. Therefore, we should perform variable matching beforehand, ensuring that the symbolic equivalence can be well recognized even in these cases.
Nevertheless, exhaustively checking possible variable mappings is always impractical due the combinatorial explosion. For two statements expressed as Pi (.1,.... (.,) - ( Fn and P2(y1 Vn)) Q2(11..... Vv)), each has variables, there are nl possible bijective mappings to be checked, which is excessively time-consuming when n is large. To address this issue, we propose to standardize the formal statement P(II,..... (I,,)
)=
Q(x (.,) by the following two cases:
(1) If the conclusion is in the form of a numerical relation, i.e., Q(x == f( v.,) ba O, where f represents any function and D {S. 2, <, =,,, we introduce new variable a and derive the standard format P(a; (I,,;,,......... - ((a) with
Pa = P(Ii, In) A (a [(1,,..., Rn)); Õ(a) a ax 0.
The two statements are reduced to Pi (I + (a) and (l. Mn) v1,
(a). and thus the logical equivalences Pi = P2(a) and (a) @2(a: can be checked through leaving 3 Fn and yy.....y4 V/ as auxiliary variables.
Rn)
(2) For num-numerical cases (e.g., Q(x) is (x)) we have to conduct variable alignment. Instead of enumerating all variable mappings, we view the variables each statement as set of graph vertices, and thus the variable alignment is transformed into bipartite matching task (where

---

(eI....,Tx) and (Vi....., Br)) form two disjoint and independent vertex sets) [59
60]. Furthermore,
we simply set the edge weight of the graph by the string edit distance [6 62]. and only partially enumerate variable mappings corresponding top-k maximum bipartite matching.
To further clarify, we provide example for each alence, we assign the symbolic score to each formalization using the proportion of its corresponding equivalence class, which is also commonly used in mathematical reasoning and code generation.
in Appendix C For evaluating symbolic equiv-
3.2 Semantic Consisteney
Next, the consissnsit is instantiated as the semantic consistency between the formalization and its corresponding informal version. The rationale of the semantic consistency is also clear: An auteformalization result accurate if it can be re-informalized to a version consistent with the original statement in natural language. By introducing the embedding similarity [33 64 to measure the consistency between the original text and the twice-processed (autoformalized then informalized) version, we can define the 7-semantic consistency as follows.
Definition 2 (Semantic consistency) Let the original mathematical statement in natural language and its formalization candidate be &b and 1), and suppose that Vi is further informalized into a new natural language statement LU. Then, the formal statement V is T-semantically consistent with the original statement & if the embedding similarity between V and & satisfies Sim (V, Ø) 2 T.
Semantic consistency primarily measures the error incurred in both the formalization and informal- ization processes. However, in most cases, it can be approximately reduced to measuring the error in autoformalization. This is because informalization is much easier and accurate than formaliza- tion (1]. For instance, considering the formalization of the statement "Determine the range of e².. LLMs should inference the type of the exponential e, determining whether to use powr or as the grounding of 'power'. On the contrary, these two expressions are both translated back into the term 'power' during informalization.
Compared symbolic equivalence, semantic consistency can avoid the unintended reasoning problem. Elaborately, continuing the example in Figure 1 the correct formalization "(x = 2/3 A y= - x* y=y=d = 4" is identified as symbolically equivalent the formalization "4 = 4". while the latter is trivial and unexpected. However, the difference between these formalizations can be successfully recognized by semantic consistency since the latter ruins the semanties in the informal statement.
Following existing machine translation techniques 665677 we employ the BERT model [68] to generate embeddings for the informal statements. These embeddings then compared using cosine similarity to evaluate semantic consistency.
3.3 Combination of Two Scores
Given & autoformalization candidates, and denote their scores of symbolic equivalence and semantic
consistency by 5 Sk..,5k Sk sym and sqem 88 sem respectively. We first normalize them using the
softmax function, i.e., sty = sym /> jj Sj sym and spem = s.em />/ Then, we propose three strategies, i.c., log, linear, and quadratic, for the combination of two scores. In particular, the final score 8, of the i-th autoformalization candidate is computed by
22j=1 of
sem for = 1,..., k.
Log combination:
6; = a log asyu + (1 - ax) log $ axem
Linear combination:
6, as;" syy + (1 a) spmm
Quadratic combination:
6, = a + (1 a)) a) (s
where E [0, 1] is the hyperparameter controlling the trade-off between the symbolic equivalence and the semantic consistency, which practically can be tuned based on the validation set.
The overall procedure of our autoformalization framework is presented in Algorithm [] The primary efficiency bottleneck of the algorithm lies in verifying symbolic equivalence. In the worst case, where no pair of autoformalization candidates are symbolically equivalent, and symbolic equivalence must be exhaustively validated kiAk - 1)/2 times. However, many verifications of symbolic equivalence can be bypassed by leveraging the transitivity property of symbolic equivalence. Moreover, when requested to provide n formalization results, we iteratively conduct the algorithm rank the formal statements, with the selected result and formal statements in its equivalence class removed.
5

---

Algorithm Autoformalization based on symbolic equivalence and semantic consistency
Input: A mathematical statement in natural language 4, transform function (log, linear, or quadratic), hyperparameter o;;
Output: the autoformalization result with the highest score.
Generate & autoformalization candidates II...., v by prompting LLMs;
2: Compute scores of the symbolic equivalence
3: fori=1,.... do
4: for j 1,................ do
5: Standardize V, and J into V = P. - Q and L == := + Qzi
6: Check the logical equivalence P. = P, and C = 2 using ATPs;
7: end for
8: Compute Si shy as the size of the derived equivalence class;
9:
end for
Compute scores of the semantic consistency
for L.....,, do
Obtain the twice-processed version e by using LLMs informalize V/; Compute seem as the cosine similarity between the embeddings of 4 and 4;
14: end for
15: Combine the scores
sym 16: Normalize 5; i 1,..., k and s,m,, = I,..., k using the softmax function;
for .,.., k do
18: Compute the final score s, by = ap(s)ym) = (1 a)p(s?mm)
end for
4
Evaluation
In this section, we conduct series of experiments to answer the following four research questions:
RQ1: Efficacy Compared with baselines and alternatives, do our proposed methods (symbolic equivalence and semantic consistency) achieve better autoformalization performance?
RQ2: Synergy Are symbolic cquivalence and semantic consistency mutually complementary? Does the combination of them further boost the autoformalization performance?
RQ3: Labeling-efficinncy How much human effort in verifying or labeling the formalization results can saved using our proposed methods?
RQ4: Scalability - Can our proposed methods be further enhanced by using stronger LLMs or ATPs?
4.1 Experimental Setup
Dataset. We evaluate the proposed methods on the MATH 23 and miniF2F (5 datasets, both of which encompass wide range of mathematical problems designed for different levels of complexity and abstraction. The MATH dataset includes a variety problem types, e.g., Algebra, Number Theory, Geometry, and on. We randomly select subset of 400 problems from the dataset to serve as our benchmark. The miniF2F dataset is specifically curated for evaluating LLM abilities in autoformalization and mathematical reasoning. It contains 488 Olympiad-level mathematical problems, each equipped with formal statement as an oracle in Isabelle and Lean.
Model. We carry out the experiments five proprictary and sourcs models of varying parameter sizes, including Mistral-7B [69], Llemma-34D [45), DeepSeek-v2 v2 [70], Codex (completion api) [22], and GPT-4 (version 07 10) [71]. In addition, we employ few-shot prompting, and set the temperature of the generation process to 0.7 for all LLMs. The eight examples used, along with detailed prompts for autoformalization and informalization.
provided in Appendix [F]
Metric. We use the unbiased n@ k accuracy (with l: generations) for performance evaluation, i.e., the percentage of problems for which the top-1 formalizations of & generations can cover a correct version 22] We apply different policies to determine autoformalization correctness on the MATH and miniF2F datasets, respectively. Specifically, the MATH dataset does not contain aligned formal

---

Table 1: Performance (n@k) of our methods (SymEq and SemCo) and comparison methods (Baseline, Naïve, and Cluster) on MATH and miniF2F datasets. The best performance of each n is in bold. The results show that our proposed methods consistently achieves superior performance.
METHODS
BASELINE
NAIVE
CLUSTER
SYMEQ
SEMCO
3
2
3
2
3
2
3
2
3
MATH
Mistral-7B
18.1
30.6
37.2
15.7
15.7
15.7
21.8
30.3
37.5
26.7
33.1
37.9
22.0
32.2
38.8
Llemma-34pp 34B
33.4
48.0
26.5
27.0
27.0
35.4
50.4
41.1
52.6
36.5
50.6
DeepSeok-v2
37.3
42.4
44.4
24.7
26.6
27.0
34,9
41.7
45.6
42.4
44.9
46.9
38.6
43.6
45.8
Codex
43.8
48.7
52.4
22.4
22.9
23.1
42.6
48.0
51.2
46.1
50.8
54.3
44.9
49.6
52.9
GPT-4
37.5
47.7
53.5
24.5
25.7
26.5
39.7
48.0
53.5
42.0
50.7
54.5
39.5
47.2
54.5
MINIF2F
Mistral-7B
12.1
13.9
10.5
11.5
12.1
7.5
11.8
12.8
14.5
17.4
18.4
12.1
16.4
Llemma-34B
21.3
28.3
34.5
19.4
23.1
24.6
20.5
28.8
33.5
32.0
40.1
41.7
27.2
31.9
38.2
DeepSock-v2
26.8
29.8
31.7
28.0
31.3
32.9
27.6
30.1
30.9
28.4
31.7
33.8
27.6
30.1
30.9
Codex 30.0
37.3
39.0
29.7
37.7
39.4
24.2
24.6
25.2
36.5
42.0
42.7
33.2
37.5
39.8
GPT-4
32.9
40.3
43.4
24.6
26.6
27.0
34.8
41.
45.0
41.1
48.1
49.3
34.9
41.7
45.6
statements, we manually check each formalization result. For the miniF2F dataset, the correctness is automatically derived by checking the symbolic equivalence between the formalization result and the provided oracle using ATPs. In the experiments, the number of generations (k) is fixed at 10, as we i
observe that improvements in pass@k (see Figure 2 become marginal with more generations.
Baseline. In our experiments, we compare our methods, symbolic equivalence (SymEq), semantic consistency (SemCo), well as combination strategy (log-comb, linear-comb, and quad-comb), with one baseline and two alternatives. The baseline method uses the log-probability predicted by LLMs the k autoformalization candidates. For Codex and GPT-4, which do not provide access log-proben hog-probability, they are prompted to rank the candidates instead. We also introduce two additional methods the alternatives, i.c., a naīve strategy that filters the candidates by whether the ATPs can prove the formalization, and a clustering method that applies the adaptive k-means algorithm [72 on BERT embeddings of formal statements.
Implementation. For the SymEq method, we implement an equivalence checker as well as periph- eral logic based scala-isabelle [73]. Specifically, the equivalence checker integrates 12 tactics (i.e., auto, simp, eval, smt, blast, fastforce, force, arith, linarith, presburger, (auto fuep:fiedd_ssee
and sledgehammer (timeout=300s]) provided in Isabelle/HOL. (74), as well as two SMT solvers Z3 [29] and CVC5 [30]. For the SemCo method, we use the pretrained compute the embedding of the informal statement.
BERT 68
4.2 Empirical Results
RQ1: Efficacy, We compute n@k results for n = 1,2,3 and five LLMs on the two datasets. As shown in Table SymEq demonstrates superior performance all cases. For Codex and GPT-4, SymEq achieves the best n nk accuracy with 46.1 (Codex) at n = 1 on the MATH dataset, and the miniF2F dataset. For the smaller LLMSs Mistral-7B and Llemma- 34B. SymEq also exhibits a notable improvement 1@k accuracy, surpassing the competitors by at least 4.9%. As for the recently released LLM DeepSeek-v2, SymEq is still effective, resulting in 1 @ improvements of 5. % and 0.8% on the two datasets, respectively.
41.1% (GPT-4)
For SemCo, it successfully achieves the best performance in three cases @3@k of Mistral-7B, 2@ of Llemma-34B, and @@ of GPT-4) on the MATH dataset. Compared to the bascline, SemCo also performs improvement, ranging from 0.8% 3.9% in @K accuracy. Compared with the alternatives, SemCo still slightly more effective, wining 4 out of cases (except for GPT-4) in accuracy. On the miniF2F dataset, although the improvement of SemCo is narrower, it still wins the alternatives 4 out of cases, and achieves equal results for the rest (DeepSeek-Ve v2) in @@ accuracy. However, SemCo is much less effective than SymEq in most cases, it does not grasp the logical nature of formal statements.
RQ2: Synergy. We first conduct detailed analysis of the performance of SymEq and SemCo across different categories of the MATH dataset. The results presented in Table 2 reveal an interesting finding: SymEq and SemCo demonstrate distinctly differrntt performances for each category. This

---

Table 2:
Performance (1@k) of our methods (SymEq and SemCo) across various categories from MATH dataset. The formalization results are generated by GPT-4, and the best performance is bold. The results show that SymEq and SemCo exhibit different behaviors various categories.
Figure 4: Performance curve of log-comb for different values of The formalization results are generated by GPT-4. The results show that the combination can further improve the auto- formalization accuracy with a large sweet spot.
CATEGORY
#PROBS
SYMEO
SEmCo
47.5
Algebra
102
57.8
59.8
Counting Probability
36.9
30.3
Geometry
32
28.1
25.1
465
Intermediate Algehra
77
31.1
25.9
Number Theory
33.3
38.0
Preculculus
Prealgebra
33.3
40.3
35.8
45.5
0.0
02
Verious values of
0.4
0.6
0.5
1.0
ScnCo
46.2
40.4
25.1
41.
42.5
41.4
14/
31:2
lgkk (g) acctency
Logoomb
33.0
34.1
100k (N)
10-
26.3
22:0
20
755
Miseal 718
Lieoma 34B
DeepSeek
Codex
GP:4
Misral 7B
Libstno 3418
DeepSesk22
Codex
GFT4
Figure 5: The performance our proposed combination strategy (log-comb) on the MATH (left) and miniF2F (right) datasets. The results show that the log-comb further boost the autoformalization performance across various LLMs on the two datasets.
variation likely stems from the differing nature and requirements autoformalizing problems in different categories. For example, geometry problems more sensitive semantic consistency since they often involve the translation of visual images, while number theory problems pose greater challenges for checking symbolic equivalence.
Therefore, combining SymEq and SemCo (i.e., log-, linear-, and quad-comb) to further improve autoformalization accuracy is reasonable. We explore the optimal setting for the hyperparameter In particular, we compute the @@k results of log-comb for various values of a on the MATH dataset, and plot the performance curve in Figure 4 The results demonstrate that the combination strategy can further improve autoformalization accuracy, with large sweet spot for a (0.32 0.6).
The performance curves for the other two combination strategies (linear-comb and quad-comb) are provided in Appendix D We observe that log-comt more effective and stable than the other two strategies. Furthermore, we fix = 0.5 based on the performance curve and present the overall performance (n@k) of log-comb Figure 5 The results show that log-comb consistently improves autoformalization accuracy across various I.MMs on the two datasets, by ranging from 2.3% to 22.6%. Particularly, compared to SymEq, even for the most powerful model GPT-4, log-comb can still further boost the @ k accuracy by 3.3% the MATH dataset and by 2.5% on the miniF2F dataset. For the Mistral-7B, log-comb presents significant improvements, i.e., 22.6% and 10.5%, respectively.
RQ3: Labeling-efficienccy We define average labeling cost for given & autoformalization candidates: [>>1) n (n@k- (n 1)@k)) (1 k@k)). Based on the average labeling cost for N mathematical problems, the total number formal statements to be labeled can be computed by a.N. Subsequently, introduce the relative efficiency of two methods E'
a a/ō. By using the baseline as a reference (ō), we compute the relative efficiency of each method in Table
It can be observed that our methods, especially log-comb, achieve higher to the alternatives. On the MATH dataset, log-comb achieves the relative efficiency ranging from 17.7% to 21.6%, with up to three times improvement (on Mistral-7B) than the Cluster method. On the miniF2F dataset, log-comb still very efficient, by using GPT-4, the relative efficiency achieves 1..%, outperforming Cluster by 9.2%, SymEq by 3.6%, and SemCo by 5,4%, respectively.
compared

---

Table Relative efficiency (%) of our methods (SymEq. SemCo, and Log-comb and alternatives (Naive, and Cluster) on MATH and miniF2F datasets. The best performance is in bold. Note that the negative results achieved by Naïve are reasonable since less effective compared to the baseline. The results show that our proposed methods exhibit higher efficiency enhancement.
METHODS
NAIVE
CLUSTER
SYMEQ
SEMCO
LOG-COMB
Dataset
MATH
miniF2F
MATH
miniF2F
MATH
miniF2F
MATH
miniF2F
MATH
miniF2F
Mistral-7B
-14.2
1.5
5.6
2.6
12.9
6.9
12.6
4.6
21.6
8.4
Llemma-34Dp
-14.2
4.1
10.4
4.6
15.2
15.8
14.3
8.4
18.9
19,5
DeepSeck-v2
-30.9
-6.9
17.2
8.3
18.7
8.0
16.3
6.8
20.5
10.0
Codex
-31.4
-5.1
13.7
10.4
15.3
9.6
13.5
13.6
19,9
15.3
GPT-4
-16.9
-7.0
15.6
12.7
16.3
18.3
14.7
16.5
17.7
21.9
Table 4: Performance (1 (I) across various diffi- culty levels from the MATH dataset, with formal- ization results generated by GPT-4. The results show that autoformalization accuracy is signifi- cantly influenced by the difficulty of the problem.
Figure 6: Performance of SymEgq using differ- ent ATP settings, with formalization results gen- erated by GPT-4. The results indicate that the performance improvement is very narrow by increasing the capability of ATPs.
DIFF.
BASELINE
SYMEQ
SEMCO
LOG-COMB
(37)
64.8
67.5
64.8
75.6
Nomnll ATPs
48.1
47.5
(70)
44.2
47.1
47.1
52.8
3 (91)
48.3
57.1
47.2
53.8
40-
41.1
4 (91)
26.3
34.0
31.8
40.6
35-
(111)
24.3
24.3
26.1
27.0
abb) refers to the difticulty level (# problems).
16k
20kk
36kk
RQ4: Scalability. As illustrated by our experimental results in Table Figure 5 more powerful LLM, such GPT-4, often exhibits better autoformalization performance. We provide an additional evidence by examining the performance differences across various difficulty levels in the MATH dataset. The results shown in Table 4 reveal significant gap in autoformalization performance between Levels 1-3 and Levels 4-5. Hence, the difficulty of the problem is highly correlated with the autoformalizaiton performance, suggesting that an LLM with stronger mathematical reasoning capabilities is more effective in this task.
To investigate the impact of ATP capability, conduct additional ablation study. Specifically, build limited equivalence checker, which only two tactics Isabelle/HOL. (auto and simp) are reserved and the other tactics and SMT solvers are removed. The results are shown in Figure which illustrate that the performance improvement of SymEq is minimal when using ATPs with stronger capability. One possible reason is that, although normal ATPs can prove more symbolic equivalences (2. vs. 2.33 per problem average) than the limited version, this is still not enough to have major impact on the final symbolic equivalence score.
5 Conclusion
In this paper, we present new framework for improving the autoformalization performance of LLMs. Our techniques address the inherent challenges autoformalization by overcoming the limitations of traditional self-consistency methods, which struggle to cope with the variance in LLM outputs. Specifically, our framework achieves this goal by combining symbolic equivalence, which grasps the logical nature among formal statements, with semantic consistency, which inspects the semantic coherence between the re-informalization result and the original text. Empirical evaluation on the MATH and miniF2F datasets demonstrates new level of autoformalization accuracy. Furthermore, our quantitative and case analysis elaborates on the limitations of current LLMs and automatic theorem provers in the task of autoformalization, shedding light directions for future optimization.
The future directions for our proposed framework could include: (1) Method Adaptation: Extending the framework to support additional theorem provers, such as Lean 4; (2) Model Enhancement: Integrating more advanced or specifically fine-tuned LLMs like ProofGPT (20] and MMA (2] to
further enhance the framework's performance; (3) Data Synthesis: Generating higher-quality. aligned informal and formal datasets using the framework. detailed discussion of the limitations and
broader impacts can be found in Appendix A and Appendix B

---

Acknowledgment
We We appreciate the anonymous reviewers for their valuable insights and helpful comments. This work supported by the National Natural Science Foundation of China (Grants #62025202) and the Frontier Technologies R&D Program of Jiangsu (BF2024059). Xian Zhang (zhxian@mi crosoft.. com) and Xiaoxing Ma (xxm@nju. edu. cn) are the corresponding authors.
References
[1] J Mc Carty and PJ Hayes. Some philosophical problems from the standpoint of artificial intelligence. d. michie (ed), machine intelligence 4, 1969.
[2] Donald Simon. Checking natural language proofs. In International Conference on Automated Deduction, pages 141-150. Springer, 1988.
[3] Cezary Kaliszyk, Josef Urban, Jifí Vyskočil, and Herman Geuvers. Developing corpus-base based translation methods between informal and formal mathematics: Project description. In Interna- tional Conference on Intelligent Computer Mathematics, 2014.
[4] Cezary Kaliszyk, Josef Urban, and Jiří Vyskoëil. Learning to parse on aligned corpora (rough diamond). In 6th International Conference on Interactive Theorem Proving. 2015.
[5] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207-220, 2009.
[6] Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Chris- tian Ferdinand. Compcert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, 2016.
[7] Georges Gonthier. The four colour theorem: Engineering of a formal proof. In Computer Mathematics: 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers, pages 333-333. Springer, 2008.
[8] Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the kepler conjecture. In Forum mathematics, Pi, volume 5, page e2. Cambridge University Press, 2017.
[9] Christian Szegedy. A promising path towards autoformalization and general artificial intel- ligence. Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings 13, pages 3-20. Springer, 2020.
[10] Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee 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, 2022.
[11] Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don't t trust: Verify-groundee Ilm quantitative reasoning with autoformalization. arXiv preprint arXiv:2403.1 18/20, 2024.
[12] Emily First. Automating the formal verification of software. 2023.
[13] Christopher Wang, Candace Ross, Yen-Ling Kuo, Boris Katz, and Andrei Barbu. Learning natural-language to Itl executable semantic parser for grounded robotics. In Conference on Robot Learning, pages 1706-1718. PMLR, 2021.
[14] Roma Patel, Roma Pavlick, and Stefanie Tellex. Learning to ground language to temporal logical form. In Conference of the North American Chapter of the Association for Computational Linguistics (NAACL), 2019.
10

---

[15] Martin D. Fraser, Kuldeep Kumar, and Vijay K. Vaishnavi. Informal and formal requirements specification languages: bridging the gap. IEEE transactions on Software Engineering, 17(5): 454, 1991.
[16] Alessandro Fantechi, Stefania Gnesi, Gioia Ristori, Michele Carenini, Massimo Vanocchi, and Paolo Moreschini. Assisting requirement formalization by means of natural language translation. Formal Methods System Design, 4:243-263 263, 1994.
[17] Claire Grover, Alexander Holt, Ewan Klein, and Mare Moens. Designing a controlled language for interactive model checking. In Proceedings of the third international workshop on controlled language applications, pages 29-30. Citeseer, 2000.
[18] Tobias Kuhn. survey and classification of controlled natural languages. Computational linguistics, 40(11112 2014.
[19] Yuhuai Wu, Albert Qiaochu Jiang. Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353-32368, 2022.
[20] Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-Ievel mathematics. arXiv preprint arXiv:2302./24::: 2023.
[21] Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:23/1.0375: 2023.
[22] Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained on code. arXiv preprint 111::2007700374. 2021.
[23] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Truck (Round 2), 2021.
[24] Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, llge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, al. GPT-4 technical report. arXiv preprint arXiv:2303.08774, 2023.
[25] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics, In International Conference on Learning Representations, 2021.
[26] Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations, 2022.
[27] Bei Chen, Fengji Zhang, Anh Nguyen, Daoguang Zan, Zeqi Lin, Tian-Guang Lou, and Weizhu Chen. Codet: Code generation with generated tests. arXiv preprint arXiv:2207, 10397, 2022.
[28] Sascha Böhme and Tobias Nipkow. Sledgehammer; judgement day. In Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings
5. pages 107-121. Springer, 2010.
[29] Leonardo De Moura and Nikolaj Björner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008
[30] Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cve5: A versatile and industrial-strengll smt solver. International Conference on Tools and Algorithums for the Construction and Analysis of Systems, pages 415-442. Springer, 2022.
11

---

[31] Sergey Edunov, Myle Ott, Michael Auli, and David Grangier. Understanding back- trecstrannlltiin scale. arXiv preprint arXiv: 09381, 2018.
[32] Lawrence C Paulson. Isabelle: A generic theorem prover. Springer. 1994.
[33]
Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq' Art: the calculus of inductive constructions. Springer Science & Business Media, 2013.
[34] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Peduction-CADE-22 25th Inter- national Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378-388 Springer, 2015.
[35] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, et al. A machine- checked proof of the odd order theorem. In International conference on interactive theorem proving, pages 163-179. Springer, 2013.
[36] Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 299-312, 2020.
[37] Peter Scholze. Liquid tensor experiment. Experimental Mathematics, 31(2)339-3344 2022.
[38] Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey deep learning for theorem proving, arXiv preprint arXiv:2404.09) 2024.
[39] Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards a mathematics formalisation assistant using large language models. arXiv preprint arXiv:2211.077 2022.
[40] Siddhartha Gadgil, Anand Rao Tadipatri, Ayush Agrawal, Ashvni Narayanan, and Navin Goyal, Towards automating formalisation of theorem statements using large language models. In 36th Conference on Neural Information Processing Systems Workshop on MATH-AI, 2022.
[41] Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving, arXiv preprint arXiv:2309.0422 2023.
[42] Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. SATLM: Satisfiabilty-aiieed language models using declarative prompting. In Proceedings of the 37th International Conference on Neural Information Processing Systems, 2023.
[43] Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving, arXiv preprint 2rXiv:2305.16366 2023.
[44] Chuanyang Zheng. Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309. 1 15806, 2023.
[45] 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. arXiv preprint 20.ivv2310. 10631, 2023.
[46] Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao. Yinya Huang, Jing Xiong, Han Shi, Eaze Xie, et al. L.EGO-prover Neural theorem proving with growing libraries. The Twelfth International Conference on Learning Representations, 2024.
[47] Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Wu, and Daya Guo. DeepSeekMalt Math: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300 2024.
12

---

[48] Huaiyuan Ying. Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. IntemLM- Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332, 2024.
[49] Xinyun Chen, Renat Aksitov, Uri Alon, Jie Ren, Kefan Xiao, Pengcheng Yin, Sushant Prakash, Charles Sutton, Xuezhi Wang, and Denny Zhou. Universal self-consistency for large language 2023.
model generation. arXiv preprint 2rXiv:231..773:
[50] Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuurmans, Claire Cui, Olivier Bousquet, Quoc Le, et al. Least-to-most prompting enables complex reasoning in large language models. arXiv preprint 22X.::2205.106225. 2022.
[51] Angelica Chen, Jason Phang, Alicia Parrish, Vishakh Padmakumar, Chen Zhao, Samuel R Bowman, and Kyunghyun Cho. Two failures of self-consistency in the multi-step reasoning of Ilms. arXiv preprint SttI::2305.122799 2023.
[52] Furui Cheng, Vilém Zouhar, Simran Arora, Mrinmaya Sachan, Hendrik Strobelt, and Menna- tallah El-Assady. Relic: Investigating large language model responses using self-consistency. In Proceedings of the CHI Conference on Human Factors in Computing Systems, pages 1-18, 2024.
[53] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:21 /0. /4/68, 2021.
[54] Romal Thoppilan, Daniel De Freitas, Jamie Hall, Noam Shazeer, Apoorv Kulshreshtha, Heng- Tze Cheng, Alicia Jin, Taylor Bos, Leslie Baker, Yu Du, et al. Lamda: Language models for dialog applications. arXiv preprint arXiv:2201.0822 2022.
[55] Shen Zheng. Yuyu Zhang, Yijie Zhu, Chenguang Xi, Pengyang Gao, Xun Zhou, and Kevin Chen- Chuan Chang. fat-fathom: Benchmarking large language models to decipher the evolutionary path towards gpt-4 and beyond. arXiv preprint arXiv:2309. 16583, 2023.
[56] Baizhou Huang, Shuai Lu, Weizhu Chen, Xiaojun Wan, and Nan Duan. Enhancing large language models in coding through multi-perspective self-consistency. arXiv preprint arXiv:2309.17272 2023.
[57] Marcus J Min, Yangruibo Ding, Luca Buratti, Saurabh Pujar, Gail Kaiser, Suman Jana, and Baishakhi Ray. Beyond accuracy: Evaluating self-cone coff-consistency of code llms. In The Twelfth International Conference on Learning Representations, 2023.
[58) Kexun Zhang, Danqing Wang, Jingtao Xia, William Yang Wang. and Lei Li. Algo: Synthe- sizing algorithmic programs with generated oracle verifiers. Advances in Neural Information Processing Systems, 36, 2024.
[59] Harold Neil Gabow. Implementation of algorithms for maximum matching on nonbipartite graphs. Stanford University, 1974.
[60] Yanyan Jiang and Chang Xu. Needle: Detecting code plagiarism student submissions. In Proceedings of ACM Turing Celebration Conference -China pages 27-32, 2018
[61] Li Yujian and Liu Bo. A normalized levenshtein distance metric. IEEE transactions on pattern analysis and machine intelligence, 191))10 2007.
[62] Gonzalo Navarro. A guided tour to approximate string matching. ACM computing surveys (CSUR), 33(1):31-88, 2001.
[63] Tom Kenter and Maarten De Rijke. Short text similarity with word embeddings. In Proceedings the the 24th ACM international on conference on information and knowledge management, pages 1421-1420, 2015.
of
[64] Omid Shahmirzadi, Adam Lugowski, and Kenneth Younge. Text similarity in vector space models: a comparative study. In 2019 18th IEEE international conference on machine learning and applications (ICMLA), pages 659-666. IEEE, 2019.
13

---

[65] Felix Hill, Kyunghyun Cho, Sebastien Jean, Coline Devin, and Yoshua Bengio. Embedding word similarity with neural machine translation. arXiv preprint arXiv:1412.6444. 2014.
[66] Raj Dabre, Chenhui Chu, and Anoop Kunchukuttan. A survey of multilingual neural machine translation. ACM Computing Surveys (CSUR), 53(5):1-38, 2020.
[67] Felix Stahlberg. Neural machine translation: A review. Journal of Artificial Intelligence Research, 69:343-418 2020.
[68] Jacob Devlin, Ming-Wai Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv preprint 2Xiv:1810004805. 2018.
[69] Albert Q Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, et al. Mistral 7b, arXiv preprint 2r.00223100066255, 2023.
[70] DeepSeck-AL. Deepseek-v2. A strong, economical, and efficient mixture-of expeeetsss language model, 2024.
[71] Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, 1lge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023.
[72] Sanjiv K Bhatia et al. Adaptive k-means clustering. In FLAIRS, pages 695-699, 2004.
[73] Dominique Unruh. Scala/lsabelle: A library for accessing Isabelle from Scala. https://
wtwpaa/..a..aaiiiiuuuuuuuuuuuu/a untuh/ watah//scaaa--saaalll 2023. Accessed: 2024-01-30.
[74] Jasmin Christian Blanchette and Lawrence Paulson. Hammering away. A User's
Guide Sledgehanmnrr for Isabelle/HOL. url: http://isabelle. in. tum, de/dist/lsabelle2013 2/doc/stedechmmmer pdf. 2013.
14

---

A Boarder Impact
The paper focuses on the formalization of mathematical theorems through large langauge models. There are many potential societal consequences of our work, and we firmly believe that the majority of these impacts are positive and none which we feel must be specifically highlighted here.
B Limitations of this work
Though achieving a considerable improvement in the autoformalization task, we also find some remaining challenges either rooted in current LLMs, ATPs, semantic embedding or evaluation metries:
LLMs lack the knowledge of formal library. As shown in Figure 2 even with sufficiently large k the L.MSs may still not generate one correct formalization for some problems due to not knowing the existing functions or definitions in formal library for the concepts, which necessitate the need for advanced retrieval mechanism or more translation pairs with finetuning.
Autoformalization is more than translation. Except for the exact mapping from natural language concepts to existing formal language functions, some math problems require the combination or the variants of certain standard definitions or functions in the formal library, which further necessitate LLMs to be capable of some basic reasoning or modeling. This again exceeds the capability of current LLMs, indicated by Table 4
ATPs are not strong enough for automation. According to McCarthy's 's classical idea M. an automatic process to evaluate the correctness of formalization can be to prove the formalization with ATPs. proved, it is with high possibility the formalization correct. However, As shown in Table 1 current ATPs are far from the capability to prove the math problems of the high school level. Furthermore, ATPs are even incapable to generate the proof of symbolic equivalence for some problems, which is often much easier than the proof of the original problems.
Embeddings may neglect the nuances in natural language. When using embeddings check semantic consistency, we assume embeddings can reflect the differences between the informalized statement and the original. However, there are many nuances in math statements that even a single notation change can result in totally different semantics. Current embeddings may not differentiate the minor but significant change.
Evaluation still requires the grounding effort of humans. Even with an ideal ATP and an ideal embedding mapping, the evaluation of the formalization still requires the finalization of humans. As shown in Example 13 from any perspective (either symbolically or semantically), the formalization can be marked correct. But from the perspective of humans, the formalization oversimplifies the problem or models the problem based on an abstraction level uncommon for humans. Therefore, human preferences are still essential for evaluating the formalizations.
C Two examples of variable matching
In Example I we show how to standardize the formal statement whose proof goal is represented as the numerical equality. We introduce a new variable a, transforming two formal statements into
(xr 2/3 Ay 6Aa x y 4) (a 0) and (a 2/3 A b 6 A a Next, by viewing x. a, as auxiliary variables, the symbolic equivalence (a: = 2/3 4) (a 0). 4) and (a 0) (a 0) can be easily proved.
6
* - 4) = (a 2/3 A
A
In Example 2 since the proof goal is not numerical inequality, we have to build the bipartite graph with nodes (n. a, b, c. c.d, e, y, 2, u. v). The edge weights are computed by string edit distance and we can derive the final variable mapping a + x, b ++ y, c ++ 2, d <> u, 6 < v. using the maximum bipartite matching. Finally, we finish the standardization by refreshing the variable notations.
D Performance curves of various combination strategies
We provide performance curves of linear-comb and quad-comb in Figure 7 Compared with log-comb, we observe that linear-comb and quad-comb have smaller effective range of a. Therefore, we select the log-comb strategy and fix 0.5 in subsequent experiments.
15

---

Example 1: An Illustrative Example of Variahle Matching
Prompt:
Natural language version: "Find the product of 0. overliine and 6. The answer is 4".
Translate the natural language version an Isabelle version.
GPT-4 output (No.2):
Standardized GPT-4 output (No.2):
theorem
theorem
fixes y real
fixes y alpha real
assumes "x 2/3"
assumes "x 2/3"
and "y 6"
and "y 6"
shows "x = 4"
and "alpha = * 4"
shows "alpha 0"
GPT-4 output (No.3):
Standardized GPT-4 output (No.3):
theorem
theorem
fixes b real assumes "a 2/3"
fixes b alpha real assumes "a 2/3"
and "b 6" shows
and "b 6" "alpha
shovs "alpha 0"
Example 2: An Illustrative Example of Variable Matching
Prompt:
Natural language version: "Prove that 4 raised to the power of the sum of five positive integers divisible by 2". Translate the natural language version to an Isabelle version.
GPT-4 output (No.1):
Standardized GPT-4 output (No.1):
theorem
theorem
fires assumes "n a + b + c
d :: nat
fires v1 v3 v5
assumes "n
v1 v2 + v3 + v4 + v5"
shows "2 dvd (n))
shows "2 dvd (4"(n))
CPT-4outpuu (No.2):
Standardized GPT-4 output (No.2):
theorem
theorem
fires x y z u v :: nat
fixes v1 v2 v3
v4 v5 :: nat shous "2 dvd
shows "2 dvd
(4 (x y + v)
(4 (v1 + v2 v3 v4 v5))"
E Some motivation examples
We demonstrate some typical errors when using GPT-4 to formalize the mathematical statement. In particular, Example 3 illustrates that GPT-4's hallucination leads to the generation of a non-existent concept (reflection innctiion. matrix). Example
4 GPT-4 formalizes the condition "r, s, and t be the 0. " by using Vieta's formulas, but the formulation incorrect (r * t- = 8) and a condition (r s + t t * 8) is ignored. As to Example 5 GPT-4 should determine whether to powr -. In Isabelle language, is only applicable to natural number exponents, but it is a real number the example.
roots of the equation 4 59z² + 32.r 32
We also highlight some cases (i.e., Example t) Example 13 when reviewing the autoformalization results, e.g., incorrect formalization oracle, incorrect label, strange failure in checking symbolic equivalence, and which shed light on the following messages:
16

---

300umay (60)
46.5
46.5
180
46.0
46.0
45.5
0.0
0.2
0.4
0.5
0.8
1.0
0.0
0.2
0.4
0.6
0.8
1.0
Various valuess of
Various values of
Figure 7: Performance curves of linear- (left) and quad- (right) comb across various values of a. The formalization results are generated by GPT-4. The results show that both combination strategies successfully improve autoformalization accuracy, while the effective range of quad-comb is smaller.
The difficulty of human labeling. We find people even experts are prone to flaws in writing or labeling formalizations. As shown Example humans may overlook the potential correct candidate while our framework can discover this via symbolic equivalence. As shown in Example [ the oracle in miniF2F wrong because when n equals 0, f n 0 which makes one assumption of the oracle false. Example [8 also shows another error in miniF2F oracles. In fact, the miniF2F dataset has been revised and checked by groups of experts 19 TO Therefore, it challenging guarantee the correctness of formalized statements without the scrutinized validations of experts or any assistance from frameworks like ours.
The difficulty of symbol grounding. The symbol grounding problem hard not only for LLMs but also for humans. As shown in Example and Example T0, humans would simply regard ^ and powr or log and In as identical while their underlying symbolic implementations are much different. The most interesting case is Example 11 where spaces around 4 will make the original Isabelle system behave differently with the type inference, leading to a failure of proving equivalence.
The (over) simpliiiiiiiiiiinnnn with reasoning. We find that LLMs tend to make one or more steps' reasoning during autoformalization, which would simplify and misalign with the original statement. As shown in Example [2 LLM may implicitly consolidate assumptions. And for concepts not frequently touched formal language (e.g., geometry), LLM may directly oversimplify the problem arithmetic, shown in Example 13
F Prompt examples for autoformalizations
We set up instructions and eight gold examples with both symbolic and semantic correctness to improve the generation performance GPT-4. Our detailed prompts are shown in Prompt I and
Prompt 1: Autoformalization Prompt
As a mathematician familiar with Isabelle, your task is translate the natural language problem into an Isabelle language version. \n'n Natural language version:An instruction / An'n Translate the natural language version an Isabelle version:In
Prompt 2: Informalization Prompt
As a mathematician familiar with Isabelle, your task to the Isabelle language problem back natural language version. Anln Isabelle language version:an iistrrcctoon] Annn Translate the Isabelle language problem back to a natural langauge version:ln
17

---

Example 3: mathd precalculus 1033
Prompt:
1
Natural language version: "Let R be the matrix for reflecting over the vector
Find
del R. " Translate the natural language version an lsabelle version.
GPT-4 output:
theorem
fixes :: "real 2
assumes ho "R reflection,matrix (vector [1, 5])"
shous "determinant R -1"
Cause: GPT-4 introduces non-existent concept (reflection matrix).
Example 4: mathd intermediate 745
Prompt:
Natural language version: "Let s, and be the roots of the equation -52=-922+32 32 Find the value of f(r) + f(s) f(t), where f(x) 4x 59x2". Translate the natural language version to an Isabelle version.
GPT-4
theorem
fixes x r t :: real
and f :: "real \<Rightarrov> real" 32"
assumes ho "r and "r "[<forall> x. fx-
59/4"
powr x powr 2"
shows "f(r) + f(s) + f(t) = -376"
Cause: GPT-4 ignores condition (r
8) when using Vieta's formulas.
Example 5: aime 1984 p5
Prompt:
Natural language version: "Determine the value of ab if logsa + log, and logs + logua² = 7. Show that it is 512.". Translate the natural language version to an Isabelle version.
GPT-4output..
theorem
fixes b :: real
assumes h0 "log 8 a log (b>2)
and h1 "log 8 b log 4 (a*2) = 7"
shows "a
512"
Cause: GPT-4 incorrectly uses to real numbers
18

---

Example 6: mathd algebra 2471
Prompt:
Natural language version: "For how many positive integers a x² + 4z + 4 between and 50? The final answer is 4.". Translate the natural language version Isabelle version.
GPT-4 output (No.1):
theorem
fixes nat and f "nat \<iightarrow> nat assumes ho "Asforall> and : "Y<forall> x. (10 \<le> <<nnd> \<ee> 50) (A x) shows "card (x. x} 4"
x + 4+x 4"
output (No.2):
theorem
fixes x :: nat and f :: "nat \<iightarrow> nat assumes ho "Asforall> x. f x + x 4"
and h1 "I<forall> x. 10 \<le> xx
<<nnd> \<le> 50 <<ongrightarrow> (V<exists>
n)
shows "card fx. 10 \<le> f \<and> f \<le> 50} 4"
Cause: GPT-4 outputs are symbolically equivalent, but human expert only labeled No.1 as correct, and incorrectly overlook No.2.
Example 7: imo 1977 p6
Prompt:
Natural language version: "Let fn) be function f N N Prove that if f(n + ff())) for each positive integer n, then f(n) = n." Translate the natural language version to Isabelle version.
GPT-4 output (No.1):
theorem
fixes :: "nat \<Rightarrow> nat"
assumes ho "\sforall> n o. f (n + 1) > f (f n)"
shows "f =
Oracle:
theorem
fixes :: "nat \<Rightarrov> nat" assumes "\<forall> n. (f n) f (n + 1)" and "\<forall> shows "\<forall> n. f =
f >0"
Cause: the provided oracle incorrect
19

---

Example 8: mathd 1485
Prompt:
Natural language version: "Find the value of that satisfies natural language version to Isabelle version.
Translate the
3z-1 2+1
GPT-4 output (No.1):
theorem
fires :: real
assumes h0 "3
<<noteq>
and h1 : "x 1 <<ooteq> 0"
and h2 "1 / (3 x 1) / (x 1)"
shows "x = 5"
Oracle:
theorem
fixes x :: real
assumes h0 "
(1 (3 1)) (2 / (x + 1))
shows
5"
Cause:
implicit condition of division: dividend not equal to zero
Example 9: aime 1984 p5
Prompt:
Natural language version: "Determine the value of ab if logsa + log, 5 and logs +
logaa² = Show that it is 512.". Translate the natural language version to an Isabelle version.
GPT-4 output (No.1):
theorem
fires b real
assumes h0 "log a log (b powr 2) and h1 "log 8 + log 4 (a powr 2) = 7
shows "a * b 512"
GPT-4 output (No.2):
theorem
fixes b :: real
assumes h0 "log 8 a log (b-2) = 5"
and h1 "log 8 log 4 (a* 7" shows
512"
Cause: fail to prove equivalence powr with
20

---

Example 10: aime 1984 p5
Prompt:
Natural language version: "Determine the value ab if logsa + logab² = 5 and logsb + logıa² Show that it is 512.". Translate the natural language version Isabelle version.
GPT-4 output (No.1):
theorem
fixes b real
assumes h0 "log 8 log (b pour 2) 5"
and : "log b log (a powr 2)
shows "a
512"
Oracle:
theorem
fixes b ::real assumes h0: "(1n a) / (1n 8) (1n (b)2)) / (1n 4) 5"
and h1: "(in b) / (1n 8) + (1n (a)2)) / (1n 4) 7"
shous "a * 512"
Cause: fail to prove equivalence powr with and log with In
Example 11: numbertheory 2dvd4expn
Prompt:
Natural language version: "Show that for any positive integer n, 2 divides 4 Translate the natural language version Isabelle version.
GPT-4 output (No.1):
theorem fixes nat shows "2 dvd (47m)
GPT-4 output (No.2):
theorem
fixes nat
shows "2 dvd (4 n)"
Checking the equivalence of GPT-4 outputs (by simp):
theorem fixes var_0
avd ((4: : var_ shows "{(var_0). [(var_0) (2 dvd ((4: nat) var_0))}
Cause: the symbolic equivalence trivial for human, but cannot be proved by ATP. The data types two "4" cannot be inferred be identical.
21

---

Example 12: mathd algebra 392
Prompt:
Natural language version: "The sum of the squares of three consecutive positive even numbers is 12296. Find the product of the three numbers divided by Show that it is 32736.". Translate the natural language version to an Isabelle version.
GPT-4 (No.1):
theorem fixes n :: real assumes h0 "n > 0"
and h1 "n mod 0"
and "n powr
(n pour
(n pour 12296" 32736"
shows "(n (n 2)
4))
GPT-4 output (No.2):
theorem fixes :: real
assumes h0 "n 0"
and h1 "(2 * n) pour 2 + (2 * n 2) powr 2
+ (2 4) pour 2 12296"
shows "(
(2 2) (2 4)) 8 32736*
Cause: fail to prove the equivalence with mod and 2 n
Example 13: mathd geometry 710
Prompt:
Natural language version: "For triangle ABC, points D and E are the midpoints of sides AB and AC, respectively. Side BC measures inches. What the measure of segment DE in inches?
(..0(2225....5)(2.55--11- label(" Abb, label(" B" (0,10))), label("C" (IO, D"oel("""(("" ((2........))).)) label(" E" 12,);-)),SE) [/asy] The final answer is 3.". Translate the natural language version to an Isabelle version.
[asy] draw((55--5) (1003))(0.100)
GPT-4 output (No.1):
theorem
fires B D "real*real" and dist :: "(real#real) \<Rightarrov> (real#real)
\<Rightarrow> real"
assumes ho "dist B c 6" and "D midpoint B"
and : "g midpoint C" shows "dist D E 3"
GPT-u (No.2):
theorem
fixes BC :: real
assumes h0 "BC 6" and h1 : "DE BC / 2"
shows "DE 3"
Cause: fail formalize geometry problems
22

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification:
The abstract and introduction clearly state our claims.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results
be expected to generalize other settings.
is fine to include aspirational goals as motivation as long is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification:
The limitation thoroughly discussed in Appendix
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification. asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low images are taken in low lighting. Or speech-to-text system might be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach address problems of privacy and faimess.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory Assumptions and Proofs
Question:
For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [NA]
23

---

Justification: [NA]
Guidelines: N/A
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental Result Reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: Details of data generation are discussed in Section 4.1 and Appendix
We
will public the code and data for the reproducibility.
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome deseribe the particular way they provide for reproducibility, In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
24

---

Answer: [Yes]
Justification: We provide the code for our data generation framework, as well as a small part of the generated data, in the supplementary material.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurlPS code and data submission guidelines (https://nips.. cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for a new open-source benchmark).
The instructions should contain the exact command and environment needed run reproduce the results. See the NeurlPS code and data submission guidelines (https /nipss.cc/pulli//guu guwdes/ddee/eee Coc//ooooeeesiseeeeeee hwtpbbbmsssiooooooooiooo for more details.
The authors should provide instructions on data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information possible in supplemental material (appended to the paper) recommended, but including URLs to data and code is permitted.
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: The method does not involve training process, and inference details are in Section 4.1 and Appendix
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment Statistical Significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [No]
Justification: We cannot provide statistical significance of the experiments due to the extensive evaluation cost.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results accompanied by error bars, confi- dence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
25

---

The assumptions made should be given (e.g.. Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out of range (e.g. negative emrr rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments Compute Resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification:
The details of computer resources are in the supplementary material.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code Of Ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics
Answer: [Yes]
Justification:
We have carefully reviewed the NeurlPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g.. if there is a special consid- eration due to laws or regulations their jurisdiction).
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: Social impacts are discussed in Appendix A
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
26

---

The conference expects that many papers will be foundational research and not tied particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms monitor how system learns from feedback over time, improving the efficiency and accessibility of MI..
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
The paper does not pose such risks.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Lieenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper. properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: Code packages and datasets are properly cited.
Guidelines:
The answer NA means that the paper does not existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (c.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswi thcode. com com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
27

---

If this information is not available online, the authors are encouraged to reach out to the asset's 's creators.
13. New Assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification: The paper does not release new assets up now.
Guidelines:
The answer NA means that the paper does not release new assets,
Researchers should communicate the details of the dataset/code/moodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According the NeurIPS Code of Ethies, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
28


Reviews:
[{"review_id": "84TgkC3zje", "reviewer": "Reviewer_37Eh", "summary": "The paper presents a novel framework aimed at enhancing the accuracy of autoformalization in mathematics using LLMs. It addresses the challenge of translating natural language mathematical statements into formal language by introducing a two-pronged approach based on symbolic equivalence and semantic consistency. Symbolic equivalence leverages automated theorem provers to ensure logical homogeneity among autoformalization candidates, while semantic consistency evaluates the preservation of the original statement's meaning by comparing embeddings of the re-informalized text and the original. The framework scores and selects the best result from multiple autoformalization candidates, significantly improving accuracy across various LLMs and datasets like MATH and miniF2F. The extensive experiments demonstrate the synergistic effect of the two consistency methods, achieving relative improvements in autoformalization accuracy and reducing the need for manual verification.", "questions": "I only have a few questions as below.\n1. According to Table 1, It seems to me that semantic consistency is not working alone. It has to be used with Symbolic Equivalence. Could you provide more insights into why this is the case? On the other hand, the default settings of semantic consistency use representation from BERT and cosine similarity. Did you try other alternative methods to compute semantic consistency? I am not sure if the bottleneck is the idea of semantic consistency or the method used.\n2. I am wondering if the proposed method also works for \"low-resource autoformalization\". The community is switching from Lean 3 to Lean 4, but existing LLMs are not performing well on Lean 4 as they have not been pretrained on enough Lean 4 corpus (also because of the limited availability).", "limitations": "The authors adequately addressed the limitations", "rating": 7, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. Clear Presentation and Structure: The paper is well-organized, with a nice logical flow. I really like the figures and tables in the paper.\n2. Open Source: The authors submit the implementation of the proposed methods, which is beneficial for the research community.\n3. Innovative Framework: Introduces a new approach that combines symbolic equivalence and semantic consistency to improve the accuracy of autoformalization. Symbolic equivalence and semantic consistency are mutually complementary, with their combination further enhancing performance.\n4. Comprehensive Evaluation: The authors conduct extensive experiments on two mathematical datasets, MATH and miniF2F, demonstrating the efficacy of the proposed methods.\n5. Wide Applicability: The proposed framework is effective across various model sizes and is not limited to a specific LLM, indicating broad applicability.", "weaknesses": "This paper makes a valuable contribution to the field of formal mathematics. While I'm new to autoformalization and not an expert in this area, I believe the paper is well-written and presents a strong argument. However, due to my limited experience, my confidence level is relatively low as I might have missed some key points.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Dear Reviewer 37Eh:**\n\nThank you for the insightful feedback on our paper. We appreciate the time and effort you have put into reviewing our work, and we are grateful for encouraging comments such as clear presentation, comprehensive evaluation, and wide applicability. We have carefully read your review and addressed your concerns as follows.\n\n**[Question #1.1] Illustration of the semantic consistency**\n\nThe performance of semantic consistency relies on the informalization process, which is relatively sensitive to the category and difficulty of the problem (see Table 2 and Table 4). While semantic consistency can work well for certain problems, this sensitivity can lead to inconsistent performance when used alone. On the other hand, symbolic equivalence provides a more stable performance by computing the score based on the size of the derived equivalence class, as seen in Figure 6. When combined, semantic consistency and symbolic equivalence complement each other effectively. Semantic consistency helps identify the optimal version among multiple large symbolic equivalence classes, thereby enhancing overall performance.\n\n**[Question #1.2] Alternative methods to compute semantic consistency**\n\nWe appreciate your suggestion to explore alternative methods. As suggested, we use e5-Mistral [1] as an alternative to BERT for our embedding model. The results are detailed below. We can observe that the new embedding model does not make a significant impact on the results. This observation suggests that the quality of informalization is more critical for semantic consistency than the specific embedding model used.\n\n| MATH |  |  |  | miniF2F |  |  |  |\n| --- | --- | --- | --- | --- | --- | --- | --- |\n| SemCo(BERT) | SemCo(e5-Mistral) | Log-comb (BERT) | Log-comb (e5-Mistral) | SemCo(BERT) | SemCo(e5-Mistral) | Log-comb (BERT) | Log-comb (e5-Mistral) |\n| 39.5 | 40.5 | 45.3 | 46.7 | 34.9 | 34.4 | 43.6 | 42.6 |\n\n**[Question #2] Low-resource autoformalization**\n\nAlthough we have not yet adapted our framework to LEAN (this is planned for future work). However, the results from Table 1 and Figure 5 demonstrate that our framework remains effective even with models exhibiting low autoformalization performance (e.g., a significant improvement from 18.1% to 42.6% and from 7.5% to 18.0% for Mistral 7B on MATH and MiniF2F, respectively). Therefore, the efficacy of our framework could be expected even if the low-resource degrades the model performance.\n\n[1] https://huggingface.co/intfloat/e5-mistral-7b-instruct", "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": "noZiKqZQkv", "reviewer": "Reviewer_zk1U", "summary": "This paper introduces two methods metrics, symbolic equivalence and semantic consistency, to determine the equivalence relation between formal statements. They design novel technical solutions to measure each method and show that this improves autoformalization by allowing self-consistency-based clustering.", "questions": "How are the numbers supporting Figure 2 obtained? How many datapoints from MATH and miniF2F did you evaluate?", "limitations": "In the conclusions, the authors did mention the things they wish to leave for future work, but it feels somewhat vague. It would be good if the authors can be more concrete and lay out future ideas they'd like to try or would like the community to carry out.", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "1. The paper addresses an important and novel problem of improving autoformalization with more test-time compute.\n2. The methods used are very intuitive and easy to understand.\n3. The evaluation is sound and shows good performance gain.\n4. The writing is clear and easy to follow.", "weaknesses": "Since the authors investigated 5 models of different sizes, I wish they investigated the models' performances with the same amount of test-time compute. I.e., given the same amount of FLOP (as measured by cost, since Codex and GPT-4 did not reveal their parameter count), which model is preferred. This helps the reader understand which model they should choose for their workload.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Dear Reviewer zk1U**\n\nThank you for the insightful feedback on our paper. We appreciate the time and effort you have put into reviewing our work, and we are grateful for the recognition of the importance of our research problem and encouraging comments such as clear writing, easy-to-understand, and good performance. We have carefully read your review and addressed your concerns as follows.\n\n**[Question #1] Autoformalization cost of different LLMs**\n\nThank you for the suggestion. To assess the autoformalization cost of various LLMs, we calculate the number of output tokens generated per problem and present the results in the following. Considering the pricing for LLM generation, CodeX offers superior cost-effectiveness, since it not only achieves comparable performance with GPT-4 but also incurs a cost that is less than one-fifth of GPT-4's expense. We will include these results in the revision. \n\n| MATH | #Tokens | 1@k | miniF2F | #Tokens | 1@k |\n| --- | --- | --- | --- | --- | --- |\n| Mistral-7B | 2234.7 | 42.6 | Mistral-7B | 2049.7 | 18.0 |\n| Llemma-34B | 2036.9 | 45.2 | Llemma-34B | 1660.5 | 35.0 |\n| DeepSeek-v2 | 1848.9 | 46.9 | DeepSeek-v2 | 1698.1 | 29.9 |\n| CodeX | 1655.9 | 49.4 | CodeX | 1475.8 | 39.1 |\n| GPT-4 | 1446.4 | 45.3 | GPT-4 | 1360.3 | 43.6 |\n\n**[Question #2] Data sizes used in Figure 1 and evaluation**\n\nFor the MATH dataset, we randomly selected a subset of 400 problems. As to the miniF2F dataset, we use the whole 488 problems. Figure 1 is obtained under the same setting. More details regarding the experimental setup are included in Section 4.1.\n\n**[Limitation] Vague future work**\n\nWe appreciate your suggestion. The future work along with the proposed framework may lie in (1) adapting the proposed framework to the LEAN prover; (2) incorporating better large language models such as ProofGPT [1] and MMA [2] to further improve the performance of the framework; (3) generating more high-quality aligned informal and formal data using our framework; (4) generalizing our framework to proof autoformalization. We will update our paper to further specify these future directions.\n\n[1] ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics\n\n[2] Multilingual Mathematical Autoformalization", "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": "tLLjBmjxNI", "reviewer": "Reviewer_LZ2a", "summary": "This paper targets the task of autoformalization for mathematics, which inputs an informal theorem statement (in English) and outputs a formal theorem statement (inside an interactive theorem prover). Prior work has used LLMs in-context to produce autoformalizations. The work is motivated by a disparity between top-1 accuracy and top-k accuracy when sampling formalizations from LLMs. The proposed method works atop any generative model of formalized statements. Their approach is to refine the k samples to a final choice via a voting mechanism. The approach is twofold - first a symbolic equivalence method uses automated theorem provers (ATPs) to check for equivalence between two formalized statements. The k-samples are then clustered by equivalence, and then they perform semantic consistency: measuring the embedding similarity between the original informal statement and the informalized formal statement. They indicate improvements over the baselines.", "questions": "1. The BERT model is used for measuring embedding similarity. How do the results change if using better models? BERT is quite outdated at this point.\n\n2. Can you provide analysis as to why the log-combination is better than the other two?\n\n3. On line 308 you indicate that on average about 2 symbolic equivalences are proven for k = 10 samples, this is lower than I had expected. What is the average cluster size per problem? Is it often the case that the models output candidates which are not symbolically equivalent (or at least, cannot be proven to be)? Does the chosen formalization end up coming from a larger cluster, even with semantic consistency being used?\n\n4. In algorithm 1 you mentioned you standardize candidates $\\Psi_i, \\Psi_j$. What is the protocol for performing this operation? Do all hypotheses go in P_i, P_j?\n\nTypos:\n1. On line 164 you mentioned that prior works commonly assign scores based on cluster size. Could you include a reference?\n2. On line 166 you mentioned the self-consistency is the similarity between the autoformalized version and its informalization. Did you mean the informalized version and the informal statement?\nLine 34: Cover -> Recover?\nLine 261: wining -> winning\nLine 301: autoformalizaiton -> autoformalization\nLine 578: \"Some motivation examples -> \"Some motivational examples\" or \"Motivating examples\"", "limitations": "I believe the authors have adequately addressed the potential limitations of their work in the limitations section in the appendix.", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The idea to compare formalization candidates via symbolic equivalence is interesting. It is a nice strategy to impose additional structure on the k-autoformalization samples. The use of the semantic consistency is a natural extension of the distilled backpropogation idea presented in (https://arxiv.org/abs/2302.12433). While measuring alignment with the informal statement is not automatable, the symbolic equivalence is a nice intermediate which I believe will be further explored in the future.\n\n2. The results indicate that their approach is effective. As the approach can be placed atop any autoformalization strategy sampling > 1 candidates from a generative model, the idea is generally applicable and should be useful for all such future work.", "weaknesses": "1. The semantic consistency alone does not appear to perform much better, I wonder if this is due to the choice of BERT for the embeddings. Perhaps you can use a newer model to judge its efficacy?\n\n2. The formulae for combining the semantic consistency score do not seem to have any motivation for the particular choice of $f(x) = x, x^2, \\log x$. Can the authors explain the rationale for these choices?\n\n3. The definition of $\\tau$-semantic consistency is not used elsewhere. In particular, it is unclear the purpose of the incorporation of $\\tau$ as it is not mentioned again.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Dear Reviewer LZ2a**\n\nThank you for the insightful feedback on our paper.  We appreciate the time and effort you have put into reviewing our work, and we are grateful for encouraging comments such as interesting idea, effective results, and general applicability. We have carefully read your review and addressed your concerns as follows.\n\n**[Weakness #1 & Question #1] Newer model for the semantic consistency**\n\nThanks for the comment. As suggested, we use e5-Mistral [1] instead of the BERT as a new embedding model. The results are shown as follows. It appears that the embedding model update makes a minimal impact on performance. This may due to that the effectiveness of informalization may be more critical than the embedding model for the semantic consistency.\n\n| MATH |  |  |  | miniF2F |  |  |  |\n| --- | --- | --- | --- | --- | --- | --- | --- |\n| SemCo(BERT) | SemCo(e5-Mistral) | Log-comb (BERT) | Log-comb (e5-Mistral) | SemCo(BERT) | SemCo(e5-Mistral) | Log-comb (BERT) | Log-comb (e5-Mistral) |\n| 39.5 | 40.5 | 45.3 | 46.7 | 34.9 | 34.4 | 43.6 | 42.6 |\n\n**[Weakness #1 & Question #2] The rationale of combination strategy**\n\nThe choice of combination strategy (linear, quadratic, or logarithmic) is determined empirically. Curves of three combination strategies are shown in Figure 4 and Figure 7, and we can observe that the log-combination is the most stable. A potential reason for this result may due to that the log transformation numerically imposes a heavier penalty on candidates with lower scores, thereby reducing their likelihood of being selected. We will present a comprehensive analysis about combination strategy in our revision.\n\n**[Weakness #3] The definition of $\\tau$-semantic consistency**\n\nThe definition of $\\tau$-semantic consistency is included for the completeness and serves as a counterpart to the symbolic equivalence. In the implementation, we directly use the embedding similarity as the score of semantic consistency.\n\n**[Question #3.1] What is the average cluster size per problem?**\n\nWe apologize for the confusion. In the paper (line 308), “2.13 vs. 2.33” is computed by the average size of symbolic equivalence classes across ALL problems, i.e., $\\sum$ sizes of all classes on all problems / $\\sum$ Number of classes on all problems. For example, given two problems and their symbolic class sizes are 10 and 1 (i.e., all problem are symbolically equivalent and none problem are symbolically equivalent). Then the average size is calculated by (10 + 10 $\\times$ 1) / (1 + 10). Following your suggestion, we list the average and maximum cluster size per problem (using GPT-4 outputs) as follows. We will clarify this and include the results in the revision.\n\n| Dataset | MATH | miniF2F |\n| --- | --- | --- |\n| Average cluster size per problem | 3.19 | 4.41 |\n| Max cluster size per problem | 4.89 | 6.11 |\n\n**[Question #3.2] Is it often the case that the models output candidates which are not symbolically equivalent?**\n\nFrom the above results, the model frequently produces candidates that are symbolically equivalent.\n\n**[Question #3.3] Does the chosen formalization end up coming from a larger cluster, even with semantic consistency being used?**\n\nYes. Generally, the efficacy of log-combination is derived from that (1) the symbolic equivalence determines multiple large clusters, and then (2) the semantic consistency distinguishes the best one from them. \n\n**[Question #4] The protocol for performing standardization**\n\nThe standardization is employed to align variables and it does put all hypothesis into $P_i$ and $P_j$. Elaborately, given two formal statements, if their conclusions are in the form of the numerical relation, the standardization introduces new variables $\\alpha$, and identifies other variable as auxiliary variables. For other cases, the standardization conduct the bipartite matching for the alignment.\n\n**[Typos #1]**\n\nThanks for the comments. We will include Self-Consistency [2], CodeT [3], and Multi-Perspective Self-Consistency [4], as references.\n\n**[Typos #2]**\n\nYes, the self-consistency in the context refers to the similarity between the informalized version and the informal statement.\n\n [1] https://huggingface.co/intfloat/e5-mistral-7b-instruct\n\n [2] Self-Consistency Improves Chain of Thought Reasoning in Language Models, ICLR 2023\n\n [3] CodeT: Code Generation with Generated Tests, ICLR 2023\n\n [4] Enhancing Large Language Models in Coding Through Multi-Perspective Self-Consistency, ACL 2024", "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": "SDCtpWji6q", "reviewer": "Reviewer_GLbW", "summary": "This paper designs two self-consistency methods for formalizing mathematical statements in natural language into Isabelle --- symbolic equivalence and semantic consistency. In particular, symbolic equivalence measures whether the formalized statements are equivalent (judged by the Isabelle’s built-in automated theorem provers), and semantic consistency measures the similarity of the natural language translation of the formalized statement and its original statement (In other words, semantic consistency measures whether the formalized statement keeps the semantic meaning.) Tested with various base models, this paper shows that the combination of the two proposed methods improves the success rate of the autoformalization process.", "questions": "-\tDefinition 1 looks unnecessarily complicated to me. For two theorems A and B, does the symbolic equivalence just mean that A and B are equivalent (which can be checked by the Isabelle solve_direct tool)?\n-\tThe variable misalignment example is confusing to me. In particular, do the authors suggest that the No. 2 and No.3 outputs in Figure 1 should be equivalent? It seems to me that in output No. 3, the variables x and y are untyped but x, y in output No. 2 have type real. In addition, it is even unclear to me whether output No. 3 is provable.\n-\tIs the phenomenon in Figure 2 true for models finetuned for autoformalization such as MMA? In addition, does SymEq/SemCo still improve the performance over MMA models?", "limitations": "The authors adequately addressed the limitations and potential negative societal impact.", "rating": 5, "confidence": 4, "soundness": 2, "presentation": 4, "contribution": 2, "strengths": "-\tThis paper studies an interesting topic, self-consistency for autoformalization, which is non-trivial because the target is not unique. To the best of my knowledge, this is the first paper to study the self-consistency methods for autoformalization.\n-\tFigure 2 shows that self-consistency methods for autoformalization have great potential because the pass@k accuracy keeps increasing with more trails.", "weaknesses": "-\tThe major weakness of this paper is the scope of the autoformalization --- the symbolic equivalence method only applies to the formalization of theorem statements instead of their proofs. Autoformalization of theorem statements is an arguably less significant problem since it cannot be used to verify any informal proofs.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "**Dear Reviewer GLbW**\n\nThank you for your review and detailed feedback. In the following, please let us address the concerns and questions you've pointed out.\n\n**[Weakness #1] The scope of our framework and the significance of statement autoformalization**\n\nFirst, we would like to clarify that, the symbolic equivalence could be adapted to the proof autoformalization. Formally speaking, a formal proof is nothing but a sequence of formal subgoals logically connected (e.g., see Figure 2 in DSP [1]). Since there is no clear difference between the autoformalization for the final goal and the intermediate subgoals, the symbolic equivalence should be still effective in proof autoformalization. We leave the exploration of this direction as the future work.\n\nNext, while we do recognize the importance of automatic verification of informal proofs and regard it as our future work, we respectfully disagree with the comment that “Autoformalization of theorem statements is an arguably less significant problem since it cannot be used to verify any informal proofs”. Elaborately, automatic verification of informal proofs can be achieved by autoformalizing each subgoals in the informal proof, and the validity of the formal proof can be verified with a proof assistant such as Isabelle or Lean. Hence, we do believe the statement autoformalization capability is the foundation for verifying informal proofs.\n\nMoreover, technically, proof autoformalization requires not only the informal statement and proof as input but also the formal statement [1, 2]. Therefore, having a correct formal statement for the informal statement is a crucial precondition for the success of proof autoformalization.\n\nFinally, for theorem proving, proof autoformalization is not necessary. For example, the recent AlphaProof project [3] by Google DeepMind uses statement autoformalization to generate approximately 100 million problems and trains its solver network using the AlphaZero algorithm. \n\n[1] Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. ICLR 2023\n\n[2] Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization. ICLR 2024\n\n[3] https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/\n\n**[Question #1] Compared with solve_direct tactic**\n\nIt is quite hard to formally define the equivalence between two theorems, and hence we try to define the symbolic equivalence as a metric of the consistency between two formal statements. Continue the example shown in Figure 1, given a formal statement,`solve_direct` can successfully detect its duplicate version, but cannot detect its variant although it is still a correct formalization. \n\n```bash\ntheorem first_statement : \nfixes a b :: real\nassumes \"a = 2/3\"\nand \"b = 6\"\nshows \"a * b = 4\"\n  using assms(1) assms(2) by force\n\ntheorem second_statement : \nfixes x y :: real\nassumes \"x = 2/3\"\nand \"y = 6\"\nshows \"x * y = 4\"\n  solve_direct\n  \n(* solve_direct: the current goal can be solved directly with\n  Scratch.first_statement: ?a = 2 / 3 ⟹ ?b = 6 ⟹ ?a * ?b = 4 *)\n  \ntheorem first_statement : \nfixes a b :: real\nassumes \"a = 2/3\"\nand \"b = 6\"\nshows \"a * b = 4\"\n  using assms(1) assms(2) by force\n\ntheorem second_statement : \nfixes y :: real\nassumes  \"y = 6\"\nshows \"(2 / 3) * y = 4\"\n  solve_direct\n\n(* No proof found *)\n```\n\nEmpirically, we also replace the symbolic equivalence with `solve_direct` tactic and conduct a comparison experiment using GPT-4 autoformalization results. The 1@k results shown in the following indicate that the symbolic equivalence still outperforms `solve_direct` either when solely used or combined with the semantic consistency. \n\n| Dataset | solve_direct | SymEq | Log-comb (solve_direct + SemCo) | Log-comb (SymEq + SemCo) |\n| --- | --- | --- | --- | --- |\n| MATH | 37.5 | 42.0 | 42.2 | 45.3 |\n| miniF2F | 34.6 | 41.1 | 39.1 | 43.6 |\n\n**[Question #2] A mistake in Figure 1**\n\nWe apologize for the mistake made in Figure 1. The No.3 output in Figure 1 is provable and it should be \n\n```bash\ntheorem\nfixes x y :: real\nassumes \"x = 2/3\"\nand \"y = 6\"\nshows \"x * y = 4\"\n```\n\n**[Question #3]  Is the proposed methods still effective on MMA fine-tuned models?**\n\nThanks for the comment. We trained a Mistral 7B model using the Isabelle data in MMA, and evaluate our framework using this model on 60 MATH problems. The pass@k (k=1,2,3,10) are 23.3%, 31.6%, 35%, 46.6%, respectively, indicating the curve in Figure 1 is still effective for this model. In addition, the n@k results are provided as follows, and we can observe that our framework also works well. \n\n| 1@k |  |  |  |\n| --- | --- | --- | --- |\n| Baseline | SymEq | SemCo | Log-comb |\n| 23.3 | 26.6 | 23.3 | 26.6 |\n\n| 2@k |  |  |  |\n| --- | --- | --- | --- |\n| Baseline | SymEq | SemCo | Log-comb |\n| 31.6 | 35.0 | 33.3 | 36.6 |\n\n| 3@k |  |  |  |\n| --- | --- | --- | --- |\n| Baseline | SymEq | SemCo | Log-comb |\n| 35.0 | 36.6 | 35.0 | 38.3 |", "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:
We thank all the reviewers for their valuable and insightful comments, which help improve our paper accordingly. Here, we summarize our responses to the major issues raised by the reviewers.

Reviewer **37Eh** and **LZ2a** request a further discussion about the performance of semantic consistency. First, we have experimented with a more state-of-the-art embedding model (i.e., e5-Mistral [1]) and find the limited effect of using different embedding models (detailed results in the response to reviewer **37Eh** and **LZ2a)**. Moreover, as indicated by Table 2 and Table 4, it appears that the performance of semantic consistency is more affected by the performance of informalization.

Reviewer **LZ2a** and **GLbW** suggest further clarification on the technical details of semantic consistency and symbolic equivalence. First, we clarify more details about the semantic consistency, including the combination strategy, and the definition of $\tau$-semantic consistency (details in the response to reviewer **LZ2a**). We also have detailed examples to explain the rationale and the benefit behind the definition of symbolic equivalence (details in the response to reviewer  **GLbW**).

Reviewer **37Eh** and **GLbW** request an analysis of our framework on other settings. First, the results of Mistral 7B from Table 1 and Figure 5 indicate the effectiveness of our methods even when the model achieves low autoformalization performance (details in the response to reviewer  **37Eh**). We also included an experiment on the Mistral 7B model fine-tuned on the MMA dataset, confirming the efficacy of the proposed framework (detailed results in the response to reviewer **GLbW**).

Reviewer **zk1U** requests a cost comparison on different models. Based on the number of output tokens generated per problem with different models, it suggests that CodeX offers superior cost-effectiveness (results in the response to reviewer **zk1U**)

Reviewer **zk1U** and **GLbW** figure out typos in the text and Figure 1. We really appreciate their efforts and will revise our paper accordingly with more careful proofreading.

Meta-review: This paper presents a method for improving autoformalization of natural language statements through a modification of self-consistency. Specifically, the paper uses symbolic equivalence checking to marginalize over different formalizations of the statement like standard answer match in self-consistency. Semantic consistency then examines whether a re-informalization of these statements is equivalent with the original. Results show that symbolic equivalence checking is very helpful and a log combination with semantic consistency helps a bit on MATH and miniF2F.

The reviewers generally found the paper to present a nice idea with reasonably strong results. It's well-written.  One weakness is the fact that semantic consistency doesn't work all that well and parts of its implementation are a bit ad hoc. Moreover, the symbolic equivalence checking is a natural extension of the well-studied self-consistency method to this setting.  Nevertheless, the paper does a good job fleshing this out and conducting experiments with it.
Decision: Accept (poster)