ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity
Authors: Xiaoyang Liu
Tao Zhu
Zineng Dong
Yuntian Liu
Guo qingfeng
Liu ZhaoXuan
Yu Chen
Tao Luo
Venue: ICLR 2026 Poster (2026)
Keywords: Lean 4
Evaluation Metric
Operator Trees
Autoformalization
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: Despite significant strides in statement autoformalization, a critical gap remains in the development of automated evaluation metrics capable of assessing formal translation quality. Existing metrics often fail to balance semantic and structural information: string-based methods neglect semantics, whereas proof-based approaches offer no graded similarity when proofs fail. To address these issues, we introduce ASSESS (A Semantic and Structural Evaluation Framework for Statement Similarity), which captures syntactic structure by transforming formal statements into operator trees and computes a real-valued similarity score using our novel TransTED (Transformation Tree Edit Distance) Similarity metric by incorporating semantic transformations. For rigorous validation, we present EPLA (Evaluating Provability and Likeness for Autoformalization), a benchmark comprising 1,247 expert-annotated formal statement pairs derived from miniF2F and ProofNet, distinctively labeled for both semantic provability and structural likeness. Experiments on the EPLA benchmark demonstrate that TransTED Similarity surpasses existing methods, achieving state-of-the-art accuracy and Kappa score. The benchmark dataset, code, and detailed experimental results are available at https://github.com/XiaoyangLiu-sjtu/ASSESS.

Published as a conference paper at ICLR 2026
ASSESS: A SEMANTIC AND STRUCTURAL EVALUA- TION FRAMEWORK FOR STATEMENT SIMILARITY
Xiaoyang Liu"
Tao Zhu"
Zineng Dong Tao Luo
Yuntian Liu Qingfeng Guo
Zhaoxuan Liu
Yu Chen
School of Mathematical Sciences, Shanghai Jíao Tong University
{xiaoyang 1iu, branden2004, stjudzzn, fulcrums, graceggf, liuzhaoxuan, 1c1y2462525, 1uotao41Jesjtu.ddu edu.
ABSTRACT
Despite significant strides in statement autoformalization, a critical gap remains in the development of automated evaluation metrics capable of assessing formal translation quality. Existing metrics often fail to balance semantic and structural information: string-based methods neglect semantics, whereas proof-based ap- proaches offer no graded similarity when proofs fail. To address these issues, we introduce ASSESS (A Semantic and Structural Evaluation Framework for Statement Similarity), which captures syntactic structure by transforming formal statements into operator trees and computes a real-valued similarity score us- ing our novel TransTED (Transformation Tree Edit Distance) Similarity metric by incorporating semantic transformations. For rigorous validation, we present EPLA (Eraluating Provability and Likeness for Autoformalization), a benchmark comprising 1,247 expert-annotated formal statement pairs derived from miniF2F and ProofNet, distinctively labeled for both semantic provability and structural likeness. Experiments on the EPLA benchmark demonstrate that TransTED Sim- ilarity surpasses existing methods, achieving state-of-the-art accuracy and Kappa score. The benchmark dataset, code, and detailed experimental results are avail- able htttps://gitaee com/ Xiaoyang u- SjtuAA/SSSSSSSSSSSSSSSSSS
INTRODUCTION
Formal languages such as Isabelle (Paulson 1994), HOL.Ligh (Harrison, 1996), Rocq (Barras et al.) 1997]. and Lean (de Moura et al. 2015 Moura & Ullrich 2021) have recently gained prominence within the mathematical community for their capacity to rigorously verify proofs. Nevertheless, formalizing mathematical content is labor-intensive process that demands substantial time, effort, and a profound familiarity with these specialized languages and their corresponding mathematical libraries, such as Mathlib (mathlib Community/ (220).. Consequently, the task of autoformalization (Szegedy 2020), defined translating theorem statements and proofs from natural language into their formal counterparts, has become an active area of research.
While autoformalization has advanced rapidly, methods for evaluating its output have lagged be- hind. Existing metrics, which generally function by assigning similarity score, are constrained by fundamental trade-off between capturing semantic meaning and preserving structural information. String String-based metrics such as BLEU (Papineni et al. 2002) rely on surface-level n-gram overlap, rendering them sensitive inconsequential lexical variations while remaining blind to underlying semantic content. Conversely, proof-based approaches (Li et al. 2024 Liu et al. (025a) can guar- antee semantic equivalence but are limited by prover brittleness, resulting in high false negatives and no graded feedback for unproven statements. Additionally, syntax- metrics (Jiang et al.) (023) operate merely at the level of grammatical compliance, offering negligible semantic or structural insights. Finally, the LLM-as-a-Judee (Ying et al. 2024a) approach, while powerful, introduces prohibitive costs and significant reproducibility concerns. These collective shortcomings highlight
"quual contribution.
1 "Corresponding author. Also affiliated to Institute of Natural Sciences, MOF-LSC, CMA-Shanghai, Shang- hai Jiao Tong University.

---

Published as a conference paper at ICLR 2026
critical gap: the need for an automated evaluation metric that robustly integrates semantic and structural information to assess statement similarity in a reproducible and efficient manner.
In this work, propose ASSESS (A Semantic and Structural Evaluation Framework for Statement Similarity), novel two-stage framework for evaluating formal statement pairs. The core of ASSESS is its novel metric, TransTED (Transformation Tree Edit Distance) Similarity. It is designed to capture both semantic and structural nuances, offering a reproducible solution that relies exclusively on CPU resources. In the first stage, ASSESS leverages the Lean Language Server parse each formal statement pair into their operator trees (OPTs), a representation that captures hierarchical structure more effectively than raw text. To overcome the semantic limitations of a standard Tree Edit Distance (TED) (Zhang & Shasha 1989), the second stage augments the TED with curated set of transformations. This augmentation enables TransTED Similarity to robustly measure statement similarity where purely structural or semantic methods fail.
To enable rigorous evaluation, we introduce EPLA (Evaluating Provability and Likeness for Auteformalization). We constructed this benchmark by autoformalizing informal statements from the miniF2F-test (Zheng et al. 2022) and ProofNet-test (Azerbayev et al., 2023) datasets, utilizing combination of two domain-specific and two general-purpose models. We filtered the candidate formalizations using the Lean compiler to ensure syntactic validity. The surviving instances were paired with ground-truth references and expert-annotated based semantic provability and struc- tural likeness. The benchmark contains 1, 1,247 annotated pairs in total, with 831 from EPL.A-iniFF2F and 416 from EPLA-ProofNG.
Experimental results demonstrate that TransTED Similarity consistently outperforms all baselines. establishes new state-of-the-arl by achieving 70.16% accuracy and 0.35 Kappa score on EPLA- miniF2F, alongside 67.31 % accuracy and a 0.30 Kappa score on EPPL-PrrofNNe: Compared to ex- isting approaches. our metric provides a more robust assessment than brittle proof-based methods, is more reproducible than ALM-basee judges, and surpasses the performance of n-gram-bu -rrsed met- rics. Furthermore, a detailed ablation study identifies the transformation component as the key factor in these performance gains. This confirms that our mechanism bridges the gap between semantic equivalence and structural likeness by dynamically aligning syntactically diverse yet logically iden- tical expressions.
We summarize our main contributions as follows:
1. We propose novel method that leverages the Lean Language Server to automatically parse formal statements into operator trees. This structured representation enables the direct application of TED Similarity to quantify statement similarity.
2. We introduce TransTED Similarity, which augments the traditional TED Similarity by in- corporating semantic transformations into the distance computation. This semantic-aware metric achieves state-of- of-the-ar art performance on the EPLA benchmark.
3. We present EPLA, comprehensive benchmark tailored for this evaluation task, comprising
1,247 formal statement pairs annotated by domain experts.
RELATED WORK
Autoformalization. The goal of autoformalization is to translate informal mathematics into for- mal code. Research in this area, particularly for theorem statements, has evolved significantly. While early work often relied on neural machine translation (Wang et al. [0188] Cunningham et al. [2022). the transformative impact of Large Language Models (L.LMs) has given rise three dominant strate-
gies. These include exploring the efficacy of few-shot prompting (Wu et al.) 2022; Agrawal et al.
2022 Zhou et al. 2024); improving capabilities by fine-tuning LLMs (Gao et al. 2025 Lu et al,
2024 Liu et al. 2025b Wu et al. 2025 Yu et al., 2025) on relevant parallel statements; and inte-
grating sutrivaal-augment generation (Zhang et al. 2024) to achieve enhanced performance.
Automated Evaluation. Automated evaluation in the context of autoformalization denotes met- machine-generated rics that assign guantitative scores to machine generated formal statements, with the goal of estimat- ing their similarity relative to natural- natural-language language source (Weng et al. 2025). Early efforts relied on grammatical validity (Jang et al. 2023) and string similanity (Azerbayev et al. 2023), yet these of- ten struggle with semantic understanding. While FormalAlign (Lu et al. 2025) integrates evaluation
2

---

Published as a conference paper at ICLR 2026
NL.FL Parallel Dataset
+
Formal Label
Formal Prediction
LIW
10
TED
NL Label
FL Label
[vee]
Operator Trees
No goals
TED
tree edit distance
TED-5
Search completed
Translatori Model
NLEE
Prediction
minimum
0.0
(a) EPLA Benchmark
(b) TED Similarity
(c) TransTED Similarity
Figure I: Overview of the ASSESS Framework. (a) EPLA Benchmark: This dataset is constructed
using four distinct translators generate Formal Language (FL) pairs, followed by compilation checks and human evaluation. (b) TED Similarity: A baseline metric computed by converting FL pairs into operator trees calculate the Tree Edit Distance (TED) similarity.
(c) TransTED Simi- equality. It conducts a tree search guided
larity: A novel metric that reformulates an FL pair by specific tactic commands, utilizing TED as heuristic to minimize the edit distance. The search halts upon satisfying any of the following conditions: successful proof generation (Proved), Node Limit Exceeded (NLE), or Time Limit Exceeded (TLE).
with autoformalization, its internal scoring mechanism cannot serve as a standalone metric. Simul- tancously, pross-iryyyyility (Murphy al., 2024 Li et al. 2024 Liu et al. [025a Poiroux al., 2025) between formal statements emerges as a widely accepted standard for automated evaluation, but its effectiveness is constrained by the current progress in automated theorem proving. GTED (Liu et al.] (225cc pioneered the use of operator trees for this evaluation task; however, it suffered from implementation instabilities and its transformation mechanism was confined to simple variable renaming. In contrast, our framework formalizes these concepts into a rigorous pseudometric space and introduces proof-based transformations to capture deep semantic alignment.
Operator Trees. Operator trees (OPTs) represent mathematical expressions syntax trees, with operators as internal nodes and operands as leaves (Zanibbi et al. 22002). Compared with sequence- based formula representations, OPTs explicitly capture the hierarchical structure and semantic lations within expressions, preserving operator precedence and operand dependencies (Zanibbi & Blostein 2012, Hu et al. 2013). These properties have made OPTs foundational applications in mathematical information retrieval (MIR). For instance, systems extract structural features from OPT's for similarity searching (Zhong Zanibbi 2019) or combine them with other representations for formula retrieval, as in the MCAT system (Kristianto et al.] (016). The utility of OPT's also extends to deep learning, where models like MathBERT (Peng et (021) integrate OPT structures during pretraining to enhance semantic understanding and encoders such FORTE (Wang et al. 2021 learn formula representations directly from OPT-based inputs.
3
METHODOLOGY
This section details our proposed framework, ASSESS, as illustrated in Figure I We begin by estab- lishing the theoretical foundations in Section 3.1] Subsequently, present the two metries: the basic TED Similarity in Section 3.2, followed by our primary contribution, the semantically-awe aware
aware
TED Similarity in Section 3.3
3

---

Published as a conference paper at ICLR 2026
3.1 PRELIMINARIES
Our framework quantifies statement similarity by computing the distance between their structural representations. We model these representations vertices within a weighted, undirected graph, where dissimilarity is captured by the shortest-path distance between them. To formalize this graph- based approach, we begin with the definition of a pseudometric space.
A pseudometric space is set X equipped with a function d X x X - Rzo, called pseudo- metric, that satisfies the following axioms for all v, y, X:
Identity: d(z, x)
Symmetry: d(x, v) = d(y. 2²)
Triangle inequality: d(x, 2) S d(x,u) y) + d(y,z)
Crucially, a pseudometric differs from metric in that d(x, y) does not necessarily imply y. This property is essential for our application, structurally distinct formal statements can be semantically equivalent (e.g., a + and b a).
Definition (Shortest-patth distance). Let G = (V, E, w) be an undirected. weighted graph, where V is the set of vertices, E is the set of edges, and w E - Rzo is the edge weight function. The shortest path distance d V + E20 defined as:
d(u, r) = inf Σ wr(e p is path from u to e with finitely many edges
PEP
By convention, d(v, v) = 0. This function d satisfies the required axioms, confirming that dV,
constitutes a pseudometric space.
3.2 TED SIMILARITY
Our baseline metric, TED Similarity, quantifies structural correspondence between two formal state- ments. This is achieved three steps: (1) representing each statement as a hierarchical operator tree (OPT); (2) computing the Tree Edit Distance (TED) between the OPTs; and (3) normalizing this distance to produce final similarity score.
3.2.1 OPT CONSTRUCTION
To capture the hierarchical structure of formal statements, we represent each as a labeled, ordered operator tree. We leverage the Lean Language Server parse formal statement, from which we derive the tree's topology based on the nested scopes its elements: operators become parent nodes and their arguments become ordered children. During construction, we apply additional transformations to standardize the tree structure:
Placeholder Representation: append a placeholder <SLOT> the labels of all non- leaf (operator) nodes. This explicitly marks the node's functional role, disambiguating operators from operands that might share the same name.
Parentheses Omission: Parentheses enforce operator precedence linear string repre- sentation. Since a tree's 's topology inherently encodes this hierarchy, parentheses are redun- dant structural artifacts and are omitted from the OPT.
As example, Figure 2 demonstrates the constructed OPT for the following formal statement:
theorem eq ( 2 x E Finset, range 10, (x 1) 2) $ 10 = 5) (
Finset. Ice 9, n 2) 10 5) := by sorry
3.2.2 METRIC CALCULATION
With formal statements converted to OPTs, instantiate the pseudometric space defined in Section 3.1 The set of vertices becomes the set of all possible OPTs, and the distance function the Tree Edit Distance.

---

Published as a conference paper at ICLR 2026
<SLOT>
<510T> <510T>
<LOOT> % <SLOT>
<LOTT> % <LOT>>
2
<SLOT> <SLOT>, <SLOT>
10
2 <SLOT> <SLOT>, <5LOT>
10
<5LOT>
<5LOT> <5LOT>
<SLOT>
<SLOT>
<5LOT>
<SLOT>
<5LOT>
<5LOT>
10
Figure The operator tree (OPT) of a formal statement.
Definition 2 (Tree Edit Distance). Let X be the set of all labeled, ordered operator trees (OPTs).
The Tree Edit Distance (TED), dTED X x X + +2o0 between two trees T2 E X is the minimum total cost of a sequence of operations that transforms T₁ into Tz. The standard operations and their associated non-negative costs are:
Deleting a node, connecting its children to its parent in order. Cost: Cdel-
Inserting a node, the inverse of a delete operation. Cost: Cins-
Relabelling a node by changing label. Cost: Crs--
For drEn to be valid pseudometric, the costs must satisfy Cinss ensuring symmetry.
To enable meaningful comparisons across trees of varying sizes, we define TED Similarity by nor- malizing the absolute Tree Edit Distance relative to tree size.
Definition (TED Similarity). The TED Similarity between two OPTs, Ti and T2, is:
dPED(Ti,, T2)
GinTEEDTT, (2) 1= max | [T
where [7] is the number of nodes in tree T.
This formulation assumes unit costs for all operations (Cael = Gms = Gpl = 1), a standard convention adopt (Zhang & Shashal 1989). The denominator max{/Ti], [T]}} serves normalization factor, representing the cost of deleting all nodes in the larger tree.
3.3 TRANSTED SIMILARITY
While TED Similarity effectively captures structural differences, it is syntactically rigid and penal- izes semantically equivalent expressions, such as a + and b + a. We therefore introduce TraDsTED Similarity, which integrates semantic awareness into the distance computation via transformations.
3.3. THEORETICAL FRAMEWORK
In our framework, we define a concept, transformation, to integrate semantic awareness into distance functions. We start with an example: i = implies that f(i) = f()). In other words, f(i) f() is no stronger than i j. We say that the contrast of (?) and f()) can be transformed to the contrast of and j. Generally, a weaker contrast can be transformed to a stronger one. We notice that the two sides of weak contrast contrast should be no larger than that between the transformed one. For compatibility with TED, we will define new distance between OPTs instead of expressions.
usually near in semantic. Therefore the distance between the original
5

---

Published as a conference paper at ICLR 2026
Here provide formal definition of TransTED. Let X be the set of all operator trees. We define a new pseudometric d' on X that is constrained by the following two properties:
Domination by TED: For any two trees Tı, T2 E X, the new distance is bounded by the original Tree Edit Distance: d' (Ti, 72) S (T),
Monotonicity under transformation: If a pair of formal expressions (ez,ey) can be trans- formed into a logically stronger pair (eu: ex) (i.e., if ey by implies ex ey), then the metric must satisfy d' (OPT(ez). OPT(e,)) S d (OPT(e))) OPT(e,)).
Finding the largest pscudometric d' that satisfies these conditions can formulated as a linear programming problem. The following theorem establishes that this problem has a unique optimal solution, which we define as TransTED. The full proof is provided in Appendix C
Theorem 1. Let X be an arbitrary set, b X + Rzo be a function and T is a subset of (X x)2. Consider the function space
Xx, X, f, ((x,))) F F:= (1l F--11 is pseudometric X, and (V( (u. u) E TT, $ f(
Then there exists unique maximum 3 F such that for any (x. v) E X x X,
J(x,u) = sup I (x,
SEF
3.3.2 IMPLEMENTATION
Since practical implementations constrained by finite set of transformations, algorithm computes a tractable upper bound TransTED rather than its exact theoretical value. Crucially, however, if the transformation sequence establishes semantic equivalence, the computed distance becomes exactly 0, coinciding with the true theoretical value.
Table 1: Additional Tactic Commands
Tactic command
Original Goal
Transformed Goal
apply congzArg
f =
f y
y
apply congrFun
f x
f g
apply forall_congr; intro
(a + b)
c)
T
apply Emppies_conge all all_goais (try rfl)
(a > c) = (b + d)
a b c
d or None
(fun (x : A)
=> f x)
ext
(x
A) J
x
g x
(fun (y : A)
g y)
Fw (propext and imp]
a b +
norm
cast
In the context of the Lean theorem prover, transformation be conceptualized the set of tacties that adhere to our theoretical framework (see Theorem T. For implementation, on one hand, we curated set of tactic commands, including rw?, the most related automatic tactic for searching cquivalence transformations, and additional ones selected for their practical efficacy, listed in Table On the other hand, since these tactics operate on single equalities rather than pairs of statements, we first construct equation as the initial contrast to be transformed and unified later, by connecting given pair of formal statements with an equal sign. Concrete examples are provided in Appendix
and c d should proved by rf1, or otherwise the tactic command generates two new goals, which is forbidden in our heuristic search. norm_cca cast undertakes simple type coercions.
At least one

---

Published as a conference paper at ICLR 2026
To circumvent the combinatorial explosion of applying all tactics, apply search algorithm. The algorithm performs a heuristic search through transformations. The guiding heuristic prioritizes tac- ties that reduce the TED between OPTs on the left- and right-hand sides of the equation, effectively pruning less promising branches. Searching is terminated as long as one of the following condi- tions is satisfied: The equivalence is proved, the node limit is exceeded (NLE), and the time limit is exceeded (TLE). This approach allows our method to efficiently find short-distance transforma- tion paths and the complete algorithm is detailed in Appendix [ Finally, normalize the raw TransTED distance into TransTED Similarity score, defined in an analogous way as Definition
4 EXPERIMENTS
4.1 THE EPLA BENCHMARK
We introduce EPLA (Evaluating Provability and Likeness for Autoformalization) a benchmark de- signed to transcend the limitations of current evaluation protocols. Existing benchmarks frequently rely on coarse binary labels (e.g., provable vs. umprovable), precluding nuanced assessment of metric performance. For instance, a slightly incorrect yet easily fixable translation is significantly more valuable than a completely erroneous one, yet binary metrics classify both identically as False. EPLA provides more nuanced evaluation standard to address this critical gap.
EPLA is built upon two established datasets: miniF2F-test (Zheng et al., 2022) and ProofNet-test Azerbayev et al. 2023). We utilize the specific versions of these datasets provided by Numina for miniF2F-test and DeepSeek") for ProofNet-test. To generate candidate formalizations, we translate natural language statements from the datasets into Lean 4 using four distinct models: two domain- specific models, Herald Translator (Gao et al., 2025) and Sneedel-Formalize-Ve
(Lin et al.) 2025), and two gemeral-purpose models, Gemini-2.5-Pro (Comanici et al.. 2025) and Qwen3-Max YYng et al. 2025). The prompts used for the domain-specift models are consistent with the original papers, while the prompts used for the general-purpost models are provided in Appendix F.5
Following the application of a compilation filter to retain only syntactically valid statements, a panel of seven experts with mathematical backgrounds annotated and cross-validated each pair of formal statements. The annotation methodology employs three Boolean sub-labels: Provability, repre- senting the semantic equivalence of the statements; Likeness before transformation, indicating structural similarity between the original statements; and Likeness after transformation, indicat- ing structural similarity following semantic-pres preentiriipeeeiinnggg transformations. The resulting EPLA bench- mark, detailed in Table 2 comprises 1,247 annotated instances. Further specifications regarding the benchmark's ' format and label definitions are provided in Appendix
Table 2: Statistics of the EPLA benchmark
Herald Translator Goedel- Formalizer
Gemini 2.5 Pro
Qwen3-Mat
Total
EPI.A-minF22F
198
234
175
224
831
EPLA-Proofis
89
130
62
135
416
4.2 EXPERIMENT SETTING
Baselines. We benchmark TED Similarity and TransTED Similarity against several competing baseline methods to validate the efficacy of our proposed metric. To ensure fair and consistent evaluation across these methods, we establish specific conventions for handling theorem names. For string-based approaches (e.g., Identity Match, BLEU), we standardize theorem names in both ground truth and predicted formal statements to thm. For proof-based approaches (e.g., Definitional Equality, BEq), we designate the ground truth theorem names as thm_P and the predicted theorem names as t hmm_Q. For all other methods, theorem names remain unaltered.
Identity Match: A predicted formal statement is considered correct if, after removing all whitespace, it is identical to the ground truth.
http:://huggnngghccccoddddss/sth test

---

Published as a conference paper at ICLR 2026
Table 3: Overall results of the competing baselines and our metrics. The boldface refers the highest score and the underline indicates the next best result of the metrics. Detailed results about the number of TP, TN, FP and FN are available in Appendix F.2
EPLA-minit-2
EPLA-ProofNet
Metric
Precision
Recall
Accuracy
Kappa
Precision
Recall
Accuracy
Kappa
(Baselines)
Identity Match
100.00%
8.79%
32.61%
0.05
100.00%
3.69%
43.51
0.03
BLEU
82.25%
73.94%
68.96%
0.26
72.30%
43.85%
57.21%
0.18
Majurity Voting
91.00%
31.27%
46 46.93%
66.67%
45.08%
54.57%
Definitional Equality
97.09%
32.57%
49.46%
0.19
86.21%
10.25%
46.39%
0.07
BBq
98.60%
45.77%
59.45%
0.29
98.77%
32.79%
60.34%
0.28
(Ours)
TED Similarity
84.51%
71.99%
69.56%
0.31
66.11%
81.56%
64.67%
0.23
TraD Similarity
87.97%
69.06%
70.16%
0.35
68.49%
81.97%
67.31
0.30
BLEU:
We follow the implementation in ProofNet (Azerbayev et al. 2023
Majority Voting: Following Lean Workbook (Ying et 2024a we employ DeepSeek-
V3.2-Exp (DeepSeek-AI 2025) with temperature 0.7 for 16 rounds of majority voting.
2025a): A predicted formal statement is considered correct if exxmmple: thm__ thm
Definitional Equality (Liu et al.
by rfl succeeds.
BEq (Liu 2025a): This metric assesses the mutual provability between a ground-truth formal statement thm and predicted formal statement thm Q. It employs InternI.M2. Math-Plus-20B (Ying et al.] (2024b) with an expanded set tactics to attempt proofs in both directions. The prediction is considered correct only if both proof' are successful.
The prompts employed in the Majority Voting baseline detailed in Appendix F5 Regarding tactic usage for the BEq baseline, we adopt the normal set of tactics exact, exact? have, apply, cases', constructor. ext, intro, intros, zw, use and fix the number of LLM generation attempts at k- = 16, consistent with the optimal hyperparameters reported in the original work. For TransTED Similarity, we utilize the top-5 suggestions generated by the rw? tactic each step of the search process and define the termination criteria as a maximum tree size of or a search timeout of minutes.
Implementation.
To ensure fair comparison with baselines requiring binary labels, we establish a unified evaluation protocol. First, we utilize the provability labels from EPLA as the ground-truth labels for the formal statement pairs. Second, for real-valued metrics such as BLEU, TED Similarity, and TransTED Similarity, we convert scores into binary predictions via thresholding. We report the optimal Kappa score and associated statisties, determined by sweeping
all possible decision thresholds.
All experiments were conducted on the EPLA benchmark using the Lean toolchain v4 .6.99.0rrrl The computational environment consisted of one NVIDIA A800 GPU with 80GB of memory and two Intel Xeon Silver 4216 CPUs, providing a total of 32 physical cores. With the exception of the GPU-dependent BEq baseline, all evaluations particularly lightweight, requiring only interaction with the Lean Language Server and REPL.
executed CPUs. Our proposed metric is
4.3 EXPERIMENT RESULTS
Overall Comparison. Table 3 presents a comprehensive overview of our proposed TransTED Similarity compared to various baseline metrics across the EPLA-miniF2F and EPLA-ProoINet benchmarks. Our primary evaluation focuses accuracy and the Cohen's 's Kappa, as accuracy di- rectly reflects the overall correctness of the evaluation, and Kappa (Cohen 1960) offers robust measure of agreement beyond chance. The results demonstrate that Trans TED Similarity achieves state-of-the-ane performance across both datasets. On EPLA-miniF2E, it secures the highest accu- racy (70.16%) and Kappa (0.35). It maintains this superior performance the
8

---

Published as a conference paper at ICLR 2026
BLEU
TED Similarity
TransTED Similarity
Optimal Point
EPLA-miniF2F
EPLA-ProofNet
0.7
0u 0.33)
Kappa
0.33
0.2
0.1
0.0
0.2
0.6
Threshold
Figure 3: Comparison of BLEU, TED Similarity, and TransTED Similarity across varying decision thresholds on EPLA-miniF2F and EPPLA-rrofNee.. Red stars indicate the optimal threshold config- uration for each metric. Details regarding threshold selection are provided in Appendix F.
dataset, again leading with the highest accuracy (67.31%) and Kappa (0.30). This consistent lead, particularly in the Kappa metric, highlights method's robust ability to align with ground-truth judgments, outperforming all evaluated baselines.
Comparison with Baselines. As detailed Table TransTED Similarity effectively mitigates key limitations inherent to existing baseline categories. First, while proof-based metrics like Defi nitional Equality and BEq achieve high precision, their performance is plagued by low recall. This brittleness stems from the limitations of current Automated Theorem Provers, which frequent fail to verify valid equivalences, resulting in a high rate of false negatives. Our method sidesteps this rigid dependency, yielding significantly more balanced assessment (see Appendix [ for comprehen- sive discussion). Furthermore, TransTED Similarity significantly outperforms the Majority Voting baseline, achieving superior accuracy 776 46.93% EPL.A-minF22F) and substantially higher Kappa score (0.35 vs. 0.14). Crucially, our method circumvents the primary limitations of LLM-based metrics: it GPU-independent and fully reproducible. Finally, our method overcomes a critical limitation of n-gram-based metrics like BLEU: their inability to capture the semantics of mathematical text. As illustrated in Figure 3 TransTED Similarity demonstrates significant ro- bustmess, maintaining high stability across broad spectrum of decision thresholds. Further details regarding threshold selection are provided in Appendix F.T
Ablation Study. We conduct an ablation study comparing our TransTED Similarity metric against the basic TED Similarity metric. The results, presented in Table demonstrate that this component provides sigmificant performance boost on both datasets. On EPLA-miniF2F, its inclusion creases accuracy by 0.60 percentage points, improving it from 69.56% to 70.16%, and raises the Kappa score from 0.31 to 0.35. This trend holds on APLA-ProofNet where accuracy improves by 2.64 percentage points from 64.67% to 67.31% %o, and the Kappa score increases from 0.23 to 0.30. These consistent gains substantiate our central hypothesis: by integrating semantic transformations, metric effectively discerns semantic equivalence amidst syntactic diversity. This capability en- ables TransTER Similarity to deliver a more accurate and human-aligned evaluation, succeeding where purely structural methods, such the standard TED Similarity, fall short.
Analysis of Tactic Commands. To assess the practical utility of our tactic set, conducted a detailed statistical analysis of their usage patterns during the search process. Specifically, we quantified the frequency with which each tactic command was adopted. Here, adopted tactic defined as one applied along the optimal transformation path that yields a minimum TED state. These statistics summarized in Figure with raw data in Appendix F22
High usage frequency of zw? and norm cast indicates their utility as simplification through rewriting and type-coercion normalization, and their low adoption rate is
tools for

---

Published as a conference paper at ICLR 2026
minif
04
ProofNet
42
Usage percantage (total)
Usage parcentage (adopted)
Adoption rate
Figure 4: Statistic of the usage frequencies and adoption rates of tactic commands. (A) Usage Per- centage (total): The proportion of each tactic command's successful applications out all successful applications during the entire search process. (B) Usage Percentage (adopted): The proportion of each tactic command's s adoption counts out of all adoption counts. (C) Adoption Rate: The propor- tion of cach tactic command's adoption counts out of its total application counts.
consistent with their role exploring a wide search space and handling routine transformations. Conversely, high adoption rates of apply forall porall_congr; intro and rw [propext: and_imp] illstrate their high specificity: they are applied less often, but when their preconditions decomposing universal quantifier restructuring nested implication are met, they are highly effective and frequently reside on the critical path towards simplification. Other tactics commands rarely successfully used, due to their strict application requirements and strong dependence precise type unification, limiting their general applicability.
Overall, the synergy between high-frequency, general-purpose tacties and their specialized, high- specificity counterparts forms a robust strategy. The former ensures extensive exploration of the search space, while the latter precisely resolves the intricate logical dependencies central estab- lishing semantic equivalence.
5 CONCLUSION
In this work, we addressed the critical gap in evaluating autoformalized statements, where existing metrics fail adequately balance semantic and structural information. We introduced ASSESS, novel framework whose core contribution is the TransTED Similarity metric. By augmenting the structural comparison of operator trees with set of semantic transformations, our method provides more holistic and robust measure of statement similarity. We also developed EPLA, expert- annotated benchmark for this task. Experiments conducted on EPLA demonstrate that TransTED Similarity establishes new state-of-the-arr, outperforming existing methods in both accuracy and Kappa score. This work provides the autoformalization community with more reliable, efficient, and reproducible metric.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGEMENTS
This work is sponsored by the National Key R&D Program of China Grant No. 2022YFA1008200 (T. L.). We also thank Shanghai Institute for Mathematics and Interdisciplinary Sciences (SIMIS) for their financial support. This research was funded by SIMIS under grant number SIMIS-ID-2025- ST. The authors are grateful for the resources and facilities provided by SIMIS, which were essential for the completion of this work. We appreciate the valuable assistance of Yifan Bai and Yantao Li with the human evaluation.
REPRODUCIBILITY STATEMENT
We are committed to ensuring the reproducibility of our research. To this end, we pro- vide comprehensive details of our benchmark, experimental setup, and evaluation methodol- ogy. The code, benchmark and experimental results are available at httts:///githut com/
XiaoyangLiu-s Jtu/AASESSSSSSSS
Specific details for reproducing our results can be found in the following sections of the paper:
EPLA Benchmark: The construction methodology, data sources, generation process, and the complete expert annotation scheme for our benchmark are detailed in Section 4.1
Baselines and Experiment Setting: The Lean toolchain version, implementation details and specific configurations for all baseline methods are provided Section 4.2 and Appendix
F.5
Detailed Results: In addition to the main results in Table 3 detailed per-metric perfor- mance, including the number of True Positives, True Negatives, False Positives, and False Negatives, are available in Appendix F2
REFERENCES
Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. To- wards a mathematics formalisation assistant using large language models, 2022. URL https:
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level math- ematies, 2023. URL htttts:://aaattt wttp:/iww.rr//bb/////000 12433
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Bean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, César Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq Proof Assistant Reference Manual Version 6.1. Research Report RT-0203, INRIA, May 1997. URL Projet COQ.
hal. www.sccnnennnniiic 00069968
Jacob Cohen. A coefficient of agreement for nominal scales. Educational and Psychologi- cal Measurement, 20(1):37 1960. doi: 10.1177001316446000000000 URL https:
Gheorghe Comanici, Eric Bieber, Mike Schaekermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, et al. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capa- bilities, 2025. httthttp://aaaat
org/ abs 2bbb/250006261
Garett Cunningham, Razvan Bunescu, and David Juedes. Towards autoformalization of math- ematics and code correctness: Experiments with elementary proofs. In Deborah Ferreira, Marco Valentino, Andre Freitas, Sean Welleck, and Moritz Schubotz (eds.), Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP), pp. 25-32, Abu Dhabi, United Arab Emirates (Hybrid), December 2022. Association for Computational Lin- guistics. doi: 10.18663/v1/2222.mmall. wwt.:0222.mmahpp-11. 1.4. URL mathnlp-11..
11

---

Published as a conference paper at ICLR 2026
Leonardo de Moura, Soonho Kong. Jeremy Avigad, Floris van Doom, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction CADE-25, pp. 378-3888 388, Cham, 2015. Springer International Publishing. ISBN 978-
3-319-21401-6.
DeepSeek-AI Deepseek-v3.2: Pushing the frontier of open large language models, 2025. URL https::/aaxiis wwtp:/oog/a.....ooo
Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. In The Thirteenth International Confer- ence on Learning Representations, 2025. URL https: httpp:s//opeerevieww net forum?id
Se6MgCtRhz
John Harrison. Hol light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri (eds.), Formal Methods in Computer-Aide Design, pp. 263-269, Berlin, Heidelberg, 1996. Springer
Berlin Heidelberg. ISBN 978-9- 3-540-4956773.
Xuan Hu, Liangeai Gao, Xiaoyan Lin, Zhi Tang, Xiaofan Lin, and Josef B. Baker. Wikimirs: mathematical information retrieval system for wikipedia. In Proceedings of the 13th ACM/IEEE- CS Joint Conference on Digital Libraries, JCDL '13, pp. 1 11-20, New York, NY, USA, 2013. Association for Computing Machinery, ISBN 450320077 doi: 10.1145/246699624666999
URL https: ottp:://///o....11111111111. 11tp:////1.11111116616144 2467699
Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization, 2023.
URL https:
03755
Giovanni Yoko Kristianto, Goran Topic, and Akiko Aizawa, Meat math retrieval system for ntcir- 12 mathir task. In NTCIR, 2016.
Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. Aut- oformalize mathematical statements by symbolic equivalence and semantic consistency. In The eight Anmual Conference on Neural Information Processing Systems, 2024. URL net wow.mmidduiiiiii
https:///pperewee http://eereeeeeee.e.eeerorrnnaaa
Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction, 2025. URLhttps:
T/axxiv.org/abs/
03613
Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: Towards faithful metric and dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025a. URL https:
/oppnnevvew www. http://oorummn-dddb2e222e-
Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, and Tao Luo. ATLAS: Autoformalizing theorems through lifting, augmentation, and synthesis of data. In The Thirty-ninth Annual Conference Neural Information Processing Systems, 2025b. URL.
forummiiioo 1
Yuntian Liu, Tao Zhu, Xiaoyang Liu, Yu Chen, Liu ZhaoXuan, Guo qingfeng, Jiashuo Zhang, Kangjie Bao, and Tao Luo. Generalized edit distance (GTED): faithful evaluation met- ric for statement autoformalization. In 2nd Al for Math Workshop @ ICML 2025, 2025c. URL btttps://openrese
net forum fwt.ommmmm.m4455ii.mmmm
Jinniao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. Process- driven autoformalization Ican 4, 2024. URL htt.l:ttp///// httpp//////xxaaaa/aa//a/oa orw.//iiorrr/eooo abs/ 2206 01940
Jinnqio Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, and Zhijiang Guo. For- malalign: Automated alignment evaluation for autoformalizatio.. In The Thirteenth Interna- tional Conference on Learning Representations, 2025. URL httpps//cpenreview.
forum? 3=R5Rr
12

---

Published as a conference paper at ICLR 2026
The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367-381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 978 145077977 doi: 10.1145/ 3377288.33338844 URL htt.t::////:o.. http://oo...og111111114333333333 33744/33338888333332
Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff' Sutcliffe (eds.), Automated Deduction CADE 28. pp. 625-635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5.
Logan Murphy, Kaiyu Yang. Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Auto- formalizing euclidean geometry. In Forty-first International Conference on Machine Learning, 2024.
eew. net/ / forum? d- ZbZOsGA
Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: method for automatic evaluation machine translation. In Proceedings of the 40th Annual Meeting on Association for Computational Linguistics, ACL '02. pp. 311-318, USA, 2002. Association for Computa- tional Linguistics. doi: 00.3115/107308331077133 URL https:://c...ooo:o//
1073083 10731
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer Verlag, 1994.
Shuai Peng, Ke Yuan, Liangcai Gao, and Zhi Tang. Mathbert: A pre-trained model for mathematical formula understanding, 2021. URL
00377
Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. Reliable evaluation and bench- Christos Christodoulopoulos, Tanmoy Chakraborty,
marks for statement autoformalization. Carolyn Rose, and Violet Peng (eds.). Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing. pp. 17947-17969, Suzhou, China, November 2025. Association doi: 10.18653/v http//22222mm/// main.
for Computational Linguistics. ISBN 77998889176-3338 907. URL /RLLitttp///caaaatooooorry wwg.://oooorr///oee 2020 2mm emmlp ma main. 907/
Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce Miller (eds.). Intelligent Computer Mathematics, pp. 3-20, Cham, 2020. Springer International Publishing. ISBN 978-3-030-53518.
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef (eds.), Intelligent Computer Mathematics, pp. 255-270, Cham, 2018. Springer International Publishing. ISBN 978-3-319-9881 12-4.
Zichao Wang, Andrew S Lan, and Richard G Baraniuk. Mathematical formula representation via tree embeddings. In iTextbooks@ AIED, pp. 121-133, 2021.
Ke Weng, Lun Du Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, and Tiancheng Zhang. Aut- oformalization in the era of large language models: A survey, 2025. URL httpp://arxxv.
hrq//bs/220 2505. 23466
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jam- nik, and Christian Szegedy. Autoformalization with large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Pro- cessing Systems, 2022. URL / www.opeewwweeeeeeeooeeeeeee www.rr/mmmmddtuiktedoeeo.
Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, and Xing Hu. hhepfun-formalley Unlocking the autoformalization potential of Ilms through knowledge-reasoning fusion, 2025. URL 04440
An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, Chujie Zheng, Dayiheng Liu, Fan Zhou, Fei Huang, Feng Hu, Hao Ge, Haoran Wei, Huan Lin, Jialong Tang, Jian Yang. Jianhong Tu, Jianwei Zhang, Jianxin Yang, Jiaxi Yang, Jing Zhou, Jingren Zhou, Junyang Lin, Kai Dang, Keqin Bao, Kexin Yang, Le Yu, Lianghao Deng, Mei Li, Mingfeng Xue, Mingze Li, Pei Zhang, Peng Wang. Qin Zhu, Rui Men, Ruize Gao, Shixuan L Liu, Shuang Luo, Tianhao Li, Tianyi Tang, Wenbiao Yin, Xingzhang
13

---

Published as a conference paper at ICLR 2026
Ren, Xinyu Wang, Xinyu Zhang, Xuancheng Ren, Yang Fan, Yang Su, Yichang Zhang, Yinger Zhang, Yu Wan, Yuqiong Liu, Zekun Wang, Zeyu Cui, Zhenru Zhang, Zhipeng Zhou, and Zihan Qiu. Qwen3 technical report, 2025. URL httph:httttttttttt org/ abs 2205/255... 09388
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024a. URL https::
net forum wew.uummddiwwwwww jHDb
Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong. Kuikun Liu, Ziyi Wang, Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm math: Open math large language models toward verifiable reasoning, 2024b. URL htt.htts:: wxwii.ivv.... wwx.ivvrr www.//rg/oooo.o.o. abs 2402. 06332
Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, and Weiyang Liu. For- malmath:
Benchmarking formal mathematical reasoning of large language models, 2025. URL
https: // aariiv..om org/ abs 2505. 02735
R. Zanibbi, D. Blostein, and J.R. Cordy. Recognizing mathematical expressions using tree trans- formation. IEEE Transactions on Pattern Analysis and Machine Intelligence, 24(11):1455-1467, 2002. doi: 10.1 ww.11999/AMM..202.00000
Richard Zanibbi and Dorothea Blostein. Recognition and retrieval of mathematical expressions. International Journal on Document Analysis and Recognition (IJDAR), 15(4):331-357, 2012.
Kaizhong Zhang and Dennis Shasha. Simple fast algorithms for the editing distance between trees and related problems. SIAM Journal on Computingg 18(6):1245 1262, 1989. doi: 10.1137/ 021 0218 URL https: /oii org/ 10 10w.11110021100
Lan Zhang, Xin Quan, and Andre Freitas. Consistent autoformalization for constructing math- ematical libraries. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen (eds.), Pro- ceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pp- 2020-4033, Miami, Florida, USA, November 2024. Association for Computational Linguis- tics. doi: 10. (0.118553/1/2224..co wttp///2....mmmmai....2mm
URLhttps: / waclantholooyy org/2024.
emn p- ma in. 233/
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022. /tt/
Wei Zhong and Richard Zanibbi. Structural similarity search for formulas using leaf-root paths in operator subtrees. In Leif Azzopardi, Benno Stein, Norbert Fuhr, Philipp Mayr, Claudia Hauff, and Djoerd Hiemstra Advan.ee in Information Retrieval, pp. 116 116-129, Cham, 2019.
Springer International Publishing. ISBN 978-3-030-15712-8.
Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don't trust: Verify grounding LLM quantitative reasoning with autoformalization. In The Twelfth International Conference on Learning Representations, 2024. URL https:
/ //openreview. feet//forumiidee 14ple
14

---

Published as a conference paper at ICLR 2026
A THE USE OF LARGE LANGUAGE MODELS (LLMS)
We utilized a large language model (LLM) as a general-purpont writing assistant during the prepa- ration of this manuscript. The primary role of the LLM was to polish the text written by the authors, such as improving grammar. All intellectual contributions, including the research methodology. ex- perimental results, and their interpretation, entirely the work of the authors. The LLM'ss function was strictly that of an assistive tool for improving the quality of the written presentation.
B LIMITATIONS AND FUTURE WORK
We analyzed some failure cases for understanding Tra Similarity metric's boundaries and guiding future research. We categorize the primary failure modes into two types.
Limited Tactic Commands (False Negatives). TransTED Similarity relies on curated of tactic commands (specifically zw? and 7 structural tactics). In complex cases requiring creative leaps or intermediate lemma synthesis, the heuristic search may fail to find a path, leading a low score for equivalent statements.
EPLA-miniF2F #25
NL: Let S = 2010 2011 +.. 4018. Compute the residue of S, modulo 2009. Show that is 0.
Label:
theorem mathd_ www.ertheooyy.rr.o 353 (s : N) (ho s Σ k in Finset. Iee 2010 4018,
2009 = 0 := by sorry
Prediction:
theorem my_ favorite theereeeeeemm (Finset. sum (Finset. Ice 2010 4018) id) & 2009 0 : by sorry
TED Similarity: 0.17
TransTED Similarity: 0.17
In this case, the current tactic set could not bridge the semantic gap between the variable definition s in the hypothesis and its direct usage in the conclusion. This highlights the need further optimize the configuration of tactic commands.
Struutur-St Tension (False Positives). Because TransTED Similarity includes struc- tural similarity component, it can assign high scores to statements that are structurally similar but semantically distinct (e.g., off-by-one errors or index shifts).
EPLA-ProofNet #360
NL: Prove that (Σ a,b;)) (E) jaz²) (Σ) {
4) for all real numbers a1....,
and bi...., Dn-
Label:
theorem exercise_6_> in : N) (a b Fin n + R) :
1, a b
i) 2 < (E Fin i
2) E i, bi
1) == by
sorry
Prediction:
theorem test problem (n : N) (a b Fin n + ( Fin D,
j b j) 2 (E j Fin n, (i.val + 1) (a () 2)
Fin n, (b 1) - (j.val + 1)) == by sorry
TED Similarity: 0.51
TransTED Similarity: 0.81
15

---

Published as a conference paper at ICLR 2026
The final transformed statement:
theorem node_4
4 (a N) [a_1 a_2 Fin a + R) : i Fin a, tti
2)
Σ i : Fin a, a_2 i - 2 / M1 ( 1 Pin a, (f
ti + 1) * aal
2) * +Σ -ii: Fin a, 2 j 2 (1N) + 1) = by
sorry
The label (left hand side) iterates over while the prediction (right hand side) iterates over j + 1. Although TransTED Similarity fails to provide a correct binary verification on mathematical equivalence due to structural likeness, the searching result precisely locates the semantic difference. This suggests that TransTED Similarity might be highly effective for human-in-the-loop debugging, filtering nearly-correct candidates for expert review.
Furthermore, we concede that TransTED Similarity does not guarantee 100% precision. This is fundamental characteristic of continuous metrics, which require a decision threshold and thus in- cur a precision-recal trade-off. Unlike rigorous decision metrics like BEq (which guarantee 100% precision but suffer from extremely low recall due prover brittleness), TransTED Similarity is designed as fractionalized metric. Its goal is to maximize alignment with human judgment by balancing precision and recall, rather than strictly filtering for absolute logical provability. Conse- quently, TransTED Similarity's s false positives are rarely meaningless. Instead, they are typically samples with "high semantic similarity but minor technical discrepancies," such as:
Consistency issues in variable naming type.
Differences in implicit type parameters.
The omission of single minor hypothesis.
In practical scenarios like comaan-n--thellog evaluation or dataset pre-screening these similar but not correct candidates are highly valuable. A metric that flags these as highly similar helps human experts locate and correct minor errors, whereas strict prover like BEq would simply reject them, providing no feedback.
C PROOF OF THEOREM
Here we provide the full proof of the Theorem I
Proof. OE F 0. Let f: X X
Rzo be function defined
F(z,8) = sup fI.
JEF
Since f(x,y) S b(x, y) for any f F, fa, v) S b(x, y) < co. suffices to show that
By definition of F. for any point pairs (x,8) E X x X and any neighbourhood N of [x y), there exists fa.y.N E such that
f E.
Now we check that f satisfies these properties one by one.
First, we verify that / pseudometric. Take any x, U, E X. Since for any E F, f(x,,)
i(x, x) = =sup p(x sup 0 0= 0.
fEF
feF
Similarly, for any f e F, f(z y) fly, 2), so
f(x. v) sup f(x = sup fly, fly, feF
feF
To show that the triangle inequality holds, introduce arbitrary neighbourhood N of 2)) Then
No St,2,(a, 2) S1,s,N v) Sa. f(x, F(y,z).
16

---

Published as a conference paper at ICLR 2026
Let M is an arbitrary neighbourhood of f(2, 2), we have f(x,2) f(x.v) + f(y,
Next, show that f satisfies the extra requirements the definition of J. We have shown that [(, y) S b(x,y), Now take any ((r,)) v), (u, v)) E T. Notice that for any F, ((r S f(u, Now for any neighbourhood N of f(x, 3), we have
N fz. v) S San.N(,,)) S f(u,v),
hence f(a,v) v) S F(,
D PSEUDOCODE FOR TRANSTED
This section provides the detailed pseudocode for our TransTED algorithm. The implementation consists of two primary functions: a primary wrapper TRANSTED that handles initial checks, and the core TEDAFTERTRANSSFRRME (line 13) is guided by using the Tree Edit Distance as heuristic (line 18). a proof of equivalence found, the distance is O; otherwise, if the time limit is exceeded, the algorithm returns the smallest TED found among all visited nodes (line 21).
function, which executes the heuristic search. The search
Algorithm TransTED
1: function TRANSTED(FLI,, FL2)
2: eq (FL1 FL22
3: if (oompile(eq) fails then
4: return TED(eq)
5: end if
6: return TEDAFTEETTAANSFORAATTOONGG
7:
end function
8: function TEDDAFTERTRANNFFRAATTTNNNN
9: if ComplettcdUUseeTcciicea,,, exact?) then
10: return 0
11: end
12: HeuristicSearch(
13:
start eq.
14:
stop the goal completed node limit exceeded (NLE) V time limit exceeded (TLE) search method: suggestions by rw? and some given additional tactic commands
15:
valid nodes: single goal of equality, or "completed"
17:
heuristic function
TED between the expressions trees of both sides of the equality
19:
if TLE then
20:
return smallest TED of all the visited nodes
21:
else
22:
return O
b The goal is completed within the time limit
23:
end if
24:
end function
E BENCHMARK STRUCTURE
The EPLA data format structured as a tuple: (natural language statement, ground-truth formal- ization, candidate formalization, annotation label). The annotation label is further decomposed into three Boolean sub-labels, each designed to quantify specific dimension of similarity and address distinct application scenario.
17

---

Published as a conference paper at ICLR 2026
Sub-label
Definition
Application Scenario
To evaluate if metric correctly assesses the semantic equivalence of two statements.
Whether the two statements are semantically equivalent.
Provability
To evaluate if metric reflects the editing cost required to make one statement structurally identical another.
Likeness before transformation
Whether the two (original) statements are structurally similar.
To evaluate if metric reflects the editing cost required to make one statement semantically identical another.
Whether the two statements are structurally similar after semantie-preservvnng transformations
Likeness after transformation
Due to inherent logical dependencies between sub-labels, the label space is constrained to the five valid combinations. The underlying logic governed by two key implications:
Provability = Likeness after transformation: Since provable statements are inher-
ently semantically equivalent, valid transformation path exists by definition, satisfying the likeness criterion.
Likeness after transformation: Structural simi- larity serves as strict condition: the editing cost required to demonstrate semantic equiv- alence is naturally upper-bounded by the cost required to achieve structural identity.
Likeness before transformation =
Provability
Likeness before transformation
Likeness after transformation
True
True
True
True
False
True
False
True
True
False
False
True
False
False
False
F EXPERIMENTAL DETAILS AND CASE STUDIES
This appendix supplements the main paper with comprehensive experimental details and qualitative case studies. We begin by outlining the methodology for threshold selection in Appendix F.1 fol- lowed by the detailed experimental results Appendix [22 We then provide qualitative assessment
of metric performance, presenting illustrative examples of TransTED Similarity in Appendix F33 and discussing false positives Definitional Equality and BEq in Appendix [F4, Finally, the specific prompt templates used for autoformalization and evaluation are documented in Appendix F.5
F.1 THRESHOLD SELECTION
We observe that the choice of threshold is inherently benchmark-dependdet., This dependency stems from the richness of the underlying mathematical formalism: plentiful mathematical structures = more structurally variant expressions of the same meaning * lower possible structural likeness.
For instance, the optimal TransTED Similarity threshold for EPLA-miniF2F (0.61) significantly higher than that for EPLA-ProofNG (0.38). This disparity reflects the greater structural complex- ity and variation inherent to the latter. Consequently, we recommend that practitioners calibrate thresholds according to the structural diversity of their specific domain, using the optimal values ported in this work as reference baselines. To ensure robustness, we further advise evaluating model performance across spectrum of thresholds rather than relying single static cut-off.
18

---

Published as a conference paper at ICLR 2026
F.2 DETAILED EXPERIMENTAL RESULTS
Tables and present the experimental results on the EPLA-miniF2F and EPLA-ProofNet bench- marks, respectively. For each metric, we report detailed classification breakdown (TP, TN, FP, FN) alongside computational costs, measured by total and average execution times. Additionally, Figures and analyze the tactic command counts for TransTED Similarity.
Table 6: Detailed experimental results of automated evaluation metrics EPLA-
2F
Metric
TP
IN
FP
FN
Precision
Recall
Accuracy
Kappa
Tot. Time (6)
Arg. Time (s]
[Revefirr]]
Menntty
217
32.61%
BLEU
454
119
160
82.25%
73.94%
68.95%
0.26
10,6390
0,0128
Majocity Voting
192
198
422
91.00%
31.27%
16.93%
0.14
11343.1519
13,6500
Defiaitiona Equality
200
32.57%
49,40/66
215.8885
0.25%
BEq
281
213
333
08 601
45.71%
39,4596
0.29
26133.5967
31 .484
[Ours)
Samilarity
21.99%
Trans TED Similarity
424
139
58
190
87.97%
69.00%
70.16%
0.35
42028.5440
50,5559
Table 7: Detailed experimental results of automated evaluation metrics on EPLA-ProofNet.
EPIA-ProofNel
Metric
Precisson
Aucuracy
(s)
Avg.
(Ravelines)
Idenitty Match
9
172
235
100.00%
3.695
43.515
0.03
0.1179
0,0003
BLEU
L07
131
137
72.30%
43.85%
57.21%
0.18
5.7977
0,0139
Majority Voting
L10
117
134
66.67%
45.08%
54.57%
5371.1336
12.9114
Definitional Equality
25
168
219
86.21
10.25%
46.39%
0.07
114 6867
0.2757
08.77%
14872.711
35,7518
(Ours)
TED Sumilarity
199
70
102
45
66.11%
$1.56%
64.67%
0.23
549.1361
1.3200
Stallarrty
54343.4060
LET 1/2
Adde ALLHAAL 11.2
HaU INTTALLN ALLEAA T1- OUFN) Inteereae
Figure 5: Statistic of the tactic commands in EPLA-miniF2F
19

---

Published as a conference paper at ICLR 2026
coyphh TIEIN Adde Fi JingT sLgAA
carly cong 5.20M
Mace TNNIAOOOON COALLON Th OOUN
(395))
Figure 6: Statistic of the tactic commands in EPLA-ProofNet
F.3 ILLUSTRATIVE EXAMPLES OF TRANSTED SIMILARITY
This section provides set of illustrative examples to offer qualitative understanding of TransTED Similarity's ' performance, particularly in cases where TED Similarity fails. Each example is pre- sented in consistent format, including the original natural language statement (NL), the ground- truth formalization (Label), and the model's output (Prediction). We then present the scores from both metrics, the transformation path (Proof) discovered by our method, and brief analysis.
#67
NL: If is rational (r + 0) and irrational, prove that ræ irrational.
Label:
theorem exercise_ 1b (x R) (y Q (a y # 0) : Irrational x + Irrational ( y = by sorry
Prediction:
theorem mul_ray rat tac_ttac____1 (r Q (x R) (h Irrational x) hr r + 0) Irrational (r x) : by sorry
TED Similarity: 0.238095233095233814
TransTED Similarity:
Proof given by TransTED Similarity:
example :
(V (x : R) (y Q y + Irrational Irrational (x ty
))
V (r (r: Q (x R), Irrational x - r * Irrational (fr
x) : by
rw [forall_swap)
apply forall_congr; intro
Iw I-
apply forall congr; intro
rw [forall [forall_swap] [@Rat. camm_comm] given by rw?
Comparing the label and prediction, human evaluator can easily match related variables and as- sumptions and give correct judgment that they are semantically almost identical. However, TED Similarity soon gets into trouble dealing with lots of variable renaming and structure adjustment and gives really low similarity score. Fortunately, suggestions provided by rw? together with
20

---

Published as a conference paper at ICLR 2026
additional tactics, such apply forall_ _ongr intro make it possible to complete the natural matching step by step, leading to a more accurate estimation on semantic similarity.
EPLA-miniF2F #170
NL: A line passes through the points B(7, -1) and C(-1, The equation of this line be written in the form mæ + b; compute m + b. Show that it is 5.
Label:
theorem ssthd_algebra 142 (m b R) (ho m N + -1) (h1 : -1
7) m +bb = := by sorry
Prediction:
theorem my my_favorite thecrem let B R (7, -1); let
R R := (-1, 7); V m b R (B.2 = m + A C.2
C.1 + b) + +
:= by sorry
TED Similarity: 0.0333333333 TransTED Similarity:
Proof given by TransTED Similarity:
example :
(A b : R), m m*
-1
5)
(let B = (7, -1);
let C == (-1, 7);
C.2 A (m b R), B.2 m B. 2.1 C.1 + 3- + 5)
:= by apply forall_congr, intro rw [mul_neg_one
given by rw?
apply forall_congry intro
rw (and_symm_leffs -- given by rw?
[and_symm_right, given by rw?
rw (propext and_imp]
In this example, TransTED algorithm successfully matches corresponding variables and hypotheses by applying proper tactics and theorems, and gives reliable evaluation result beyond structural likeness.
F.4
FALSE POSITIVES IN DEFINITIONAL. EQUALITY AND BEQ
This case study investigates the root cause of the false positives (FP) recorded by the Definitional Equality metric and the BEq metric, classified into three categories according to causes.
Causes
miniF2F
ProofNet
Definitional Equality FP
BEq FP
#115, #128, #402
Implicit Variable Matching
#24, #701
#378, #603, #639, #641
Over-simplifying
+
+
Header Mixing
#280
+
+
F.4.1
IMPLICIT VARIABLE MATCHING
21

---

Published as a conference paper at ICLR 2026
EPLA-miniF2F #24
NL: Expand the product (x + 1)². Show that it is x² + +
Label:
theorem ma titth_aalgbbbrr 176 (x R) 1x + 1) x x 2 == by sorry
Prediction:
theorem my- favoriioeeette theerreemt (R Type*) [CommRing R] (x R)
(x + 1) 2
2 2 + := by sorry
Definitional Equality
example mathd_algesan 176 my_favorit_thherre :- by rfl
In the Prediction, the statement was generalized by introducing an implicit type variable { Type+} with typeclass assumption [CommRing R] instead of the concrete type R, resulting a semantic difference; however, Lean will automatically instantiate CommRing instance, Definitional Equality the compiler infers these instantiations and the two declarations become definitionally equal, thus passing the verifier and producing a false positive.
== and resolve the
EPLA-miniF2F #701
NL: Expand (x (2r 6). Show that it is 2x-2-18.
Label:
theorem mathd_algebra _43 (x R) (x 3) 2 - 18 := by sorry
x
Prediction:
theorem test_proble em (R. Type*) [CommRing R] (x : R) (x 3) x 6)
x x
by sorry
Definitional Equality
example : matho aatha_algebra_433 test_problem by rfl
The emror type here is identical to that in EPLA-miniF2F #24.
EPLA-ProofNet #115
NL: Prove that (1, then Sq is an infinite group.
Label:
theorem exercise_11 1_3_________ Infinite (Equiv.Pezn) N) := by sorry
Prediction:
(Ω Type __1 [Infinite Ω] Infinite (Equiv.Ferm ?) := by sorry
theorem wwwiiite_of_ininitteee
Definitional Equality
example exercise_1_3_ = infinitte_o := by rfl
In the Prediction, the model introduced an implicit type variable { Type u_1} with type- class assumption [Infinite Q) instead the concrete type N: however, Lean can instantiate Ω N and use the existing Infinite N instance, so in Definitional Equality the compiler infers these instantiations and the two declarations become definitionally equal, thus passing the verifier and producing false positive.
22

---

Published as a conference paper at ICLR 2026
EPLA-ProofNet #128
NL: Prove that x² + 4x + 6x + 2r + 1 irreducible in Z[z].
Label:
theorem exercise_ 9_4_2c Irreducible'n (x'4 + 4+x03 + 6+X²2 + 2+X + Folynomial Z) := by sorry
Prediction:
theorem wrredbciilee_iilsonss.
Irreducible (vilsons_poly
[[x]) = by sorry
Definitional Equality
example 2x irreducible :- by rfl
In the Prediction, an undefined variable wilsons poly appeared instead of the polynomial given in the problem, resulting in semantic difference. However, Lean will automatically interpret wilsons poly as an implicit variable. Therefore, in Definitional Equality, the Lean compiler will automatically infer wilsons-poly as the polynomial X 4x +6X 2X + 1. thus passing the verification and leading to a false positive.
EPLA-ProofNet #402
NL: Let f: X - X be continuous. Show that if X [0, 1]. there is a point such that f(x) = x. (The point x called fixed point f-)
Label:
theorem exercise_24 I) (hf Continuous f) 3 (x I), f x := by sorry
TTopologicalSpace I] [Compact.ppac I]
Prediction:
theorem test_problen (f Set. (0 R) Set. Ice (0 R)
1) (hf : Continuous f) x, x x := by sorry
Definitional Equality
example : exercise_24_0 24_ test_probles :- by rfl
In the Prediction, the model explicitly uses the concrete type, the interval [0. 1], for both the domain and codomain the function f. However, the Label, the theorem is stated more abstractly for any type / equipped with needed instances. While [0, 1] can be endowed with such structure (making it a valid candidate for I), the type [0. 1] + [o, 1] is not definitionally equal to the function type 1 + for abstract /. Therefore, the definitions are not considered identical by the kernel, the rfl tactic fails, and this case is correctly identified as a negative example.
F.4.2 OVER-SIMPLIFYING
EPLA-miniF2F #378
What is the units digit of the sum of the squares of the first nine positive integers? Show that is
NL:
Label:
theorem mathd _athd__auneeeeeeeaaaaaaaa nuwbertheery_33 ( x in Finset. range 10, (x 1)
2) 8 10
by sorry
Prediction:
theorem my fwy_rvvritte_mmm my_ffaorrit__therre theorem E in Finset. range 9, (1 1)
-2) 8 10 = 5 := by sorry
23

---

Published as a conference paper at ICLR 2026
These two theorems produce exactly the same numerical result. However, the natural language de- scription specifies computing the squares of the first nine positive integers, while the Label computes the squares of the first ten positive integers. Although this does not change the final value, the mantics are different. Nevertheless, BBq reports that the two theorems are equivalent, which does match the actual situation.
EPLA-miniF2F #603
What the units digit of the of the squares of the first nine positive integers? Show that is
NL:
Label:
theorem ma mathd_ brtthd_nunbbrtheory_3 (E x in Finset. range 10, (x 1)
2) $ 10
by sorry
Prediction:
theorem test_problen : (Finset. sum (Finset. Ice 1 9) (fun => ) $ 10 = 5 == by sorry
These two theorems produce exactly the same numerical result. However, the natural language de- scription specifies computing the squares of the first nine positive integers, while the Label computes the squares of the first ten positive integers. Although this does not change final value, the se- mantics are different. Nevertheless, BEq reports that the two theorems are equivalent, which does not match the actual situation.
EPLA-miniF2F #639
NL: How many integers between 15 and 85 are divisible by 20? Show that is
Label:
theorem ma methh__numbertheory 12 Finset.cam card ginset.filter (fun => 20 x) (Finset. Ice 15 85) 4 := sorry
Prediction:
theorem test_ pessleprolemm (Finset filter (fun => 20 n) ( range B5 Finset.range 16)) card
: by sorry
Although the Label and Prediction produce the numerical result, the Label is consistent with the natural language: it additionally includes 15 and 85 in the computation. While this does affect the numerical result, not semantically equivalent the natural language. On the other hand, the Prediction is strictly equivalent to the natural language. Therefore, the Label and Prediction are not equivalent.
EPLA-miniF2F #641
NL: What the sum of the units digits of all the multiples between and 50? Show that it is 78
Label:
theorem mathd miteeddoumbbrtheory. 447 E k in Finset. filter (fun
=> x) (Finset. Ice 49), 10) 78 := by sorry
Prediction:
theorem test_proble : ( ((Finset. range 17) sum (fun => 10)) = 78 := by sorry
(3
i)
Although the computations for Label and Predict are the same, Predict additionally includes 0 and 50, whereas the natural language statement refers to the numbers between 0 and 50, excluding and 50. Therefore, Predictis ion does not match the natural language. However, BEg will consider Label and Prediction equivalent.
24

---

Published as a conference paper at ICLR 2026
F.4.3 HEADER MIXING
EPLA-ProofNet #280
NL: Show that (12) is an algebraic number.
Label: open Real open scoped BigOperators
theorem exercise_12_12 : IsAlgebraic Q (sin (Real.pi/12) : by
sorry
Prediction:
theorem my_Favorite_ IsAlgebraic (Real. (π 12))
:= by sorry
Definitional Equality
example thm_P thm_ : by rfl
In the Prediction, æ not defined, so the two theorems are not equivalent. However, if the headers merged, then becomes defined and the two theorems become equivalent. Since BEq first merges the headers and then performs mutual provability checking, BEq concludes that the two theorems are equivalent, which does not match the actual situation.
F,5 PROMPT TEMPLATES
This section presents the prompts employed during the autoformalization phase, utilizing Gemini- 2.5-Pro (Comanici al. 2025) and Qwen3-Max (Yang et al.) 2025). Subsequently, we detail (Ying et al.,
the prompts for the majority voting phase, which leverages 2024b) for back-translation and DeepSeek-V3.2-Exp (DeepSeek-A) 2025) for the NLII consistency check.
Prompt Template for Autoformalization
Please autoformalize the following problem in Lean with header. Use the following theorem names: my www.oaitt_tthoorreeee theorem. (tntormal_saatemeet)
Your code should start with "Lean4 import Mathlib
You should only output the theorem statement in Lean 4 format, ending with "by sorry You should NOT output the proof.
Prompt Template for Back-Transian Translation
[UNUSED TOKEN 146Juser
Convert the formal statement into natural language:
'' 'lean
(formal statement)
"IUNUSED_TOOENN"
[UNUSED TOKEN 146 146)assistant
25

---

Published as a conference paper at ICLR 2026
Prompt Template for NLI Check
Please check following two math problems is same or different? Please consider each statement in two problems, they are different if any statement is different. Please point out any differences you found. Please reply **same** or **different** in the final sentence with bold format.
Problem 1: (THM.1)
Problem 2: (THM 2}
26


Reviews:
[{"review_id": "e9jiEombxS", "reviewer": "Reviewer_18nk", "summary": "This paper tackles a practical problem in automated theorem proving: how to automatically evaluate whether a machine-generated formal statement correctly captures the meaning of a natural language mathematical problem. The authors propose ASSESS, a framework that tries to balance both the structural form and semantic meaning when comparing formal statements.\n\n**The approach works in two steps.** \n\nFirst, they use the Lean Language Server to parse formal statements into operator trees (OPTs), tree structures that represent the syntactic hierarchy of the statement. They apply some preprocessing like adding placeholders and removing redundant parentheses to standardize these trees. \n\nSecond, they compute a similarity score using their proposed TransTED metric, which extends the classic Tree Edit Distance algorithm by incorporating semantic transformations. These transformations are implemented as Lean tactics (like `apply congrArg`, `ext`, etc.) that can recognize when two syntactically different statements are semantically equivalent. The algorithm uses heuristic search with TED as the guiding heuristic to find the minimum achievable distance.\n\n**The paper makes three main contributions.** \n\n- First is the TransTED Similarity metric itself, which outputs a continuous score between 0 and 1 rather than a binary decision. The authors provide theoretical justification through Theorem 1, which frames the problem in terms of pseudometric spaces. \n\n- Second, they introduce EPLA, a new benchmark with 524 human-annotated statement pairs drawn from miniF2F and ProofNet. Each pair gets fine-grained labels covering both semantic correctness (provable vs unprovable) and structural similarity (like vs unlike), creating five categories in total. \n\n- Third, they show experimental results where TransTED achieves 78.82% accuracy on miniF2F and 70.86% on ProofNet, with Kappa scores of 0.46 and 0.40, beating several baselines including BLEU, LLM-based voting, and proof-based methods.\n\nThe authors argue their method offers a sweet spot. It's more semantically aware than simple string matching, more robust than brittle proof-based approaches, and more efficient and reproducible than using LLMs as judges.", "questions": "**Q1: Relationship with GTED**\n\nAs noted in the weaknesses, GTED has substantial overlap with your work. This is the most critical issue affecting our assessment:\n\n- Can you clarify whether you were aware of GTED during development?\n- Please provide detailed technical comparison showing what is genuinely new in your approach\n- Would you be willing to evaluate both methods on identical test sets for fair comparison?\n\nYour response will directly determine whether we view this as independent innovation or incremental refinement of GTED.\n\n---\n\n**Q2: Handling complex formalizations [Important - could mitigate scope limitation]**\n\nThe evaluation focuses on simple, single-statement theorems. We understand this reflects the datasets used, but it raises questions about practical applicability.\n\n- Have you conducted any experiments (even informal) with formalizations containing definitions, structures, or multi-statement developments?\n  \n- Can you discuss theoretically how the OPT construction and transformation tactics would handle such cases?\n\nEven preliminary evidence or principled discussion would help assess whether the scope limitation is fundamental or merely reflects current evaluation constraints.\n\n---\n\n**Q3: Transformation tactics design [Moderate - would strengthen contribution]**\n\nTable 1 presents seven transformation tactics. Can you provide more details like\n\n- How were these tactics selected? Systematic exploration or intuition?\n- Have you analyzed their individual contributions (ablation study)?\n- Which tactics are most frequently used or impactful?\nThis would help understand the design rationale and completeness of the transformation set.\n\n---\n\n**Q4: Statistical reliability of improvements**\n\nFor ProofNet (151 samples), the +3.31% improvement represents only about 5 additional correct predictions. Have you checked whether this difference is statistically significant? A simple test would help confirm the reliability of this improvement, though the miniF2F results (+6.70% on 373 samples) are more clearly substantial.", "limitations": "", "rating": 4, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "**Originality**\n\nThe paper makes several novel contributions. Applying operator trees to formal statement evaluation bridges mathematical information retrieval techniques to theorem proving in an unexplored way. The key innovation **augmenting Tree Edit Distance with semantic transformations via Lean tactics** elegantly addresses the challenge that semantically equivalent statements can have very different syntactic forms. The pseudometric space formulation (Theorem 1) provides theoretical grounding. The EPLA benchmark's five-category annotation scheme is notably more nuanced than existing binary evaluation datasets.\n\n**Quality**\n\nThe technical approach is sound. Leveraging the Lean Language Server for OPT construction is pragmatic engineering. The choice of transformation tactics (Table 1) reflects good mathematical intuition. The experimental evaluation covers diverse baselines (string-based, proof-based, LLM-based). The ablation study provides clear evidence that transformations contribute meaningfully (+6.70% on miniF2F). Implementation details demonstrate attention to reproducibility.\n\n**Clarity**\n\nThe paper is well-structured with logical progression from motivation through methodology to experiments. Mathematical notation is introduced systematically with helpful examples. Figure 3 effectively demonstrates TransTED's robustness to threshold selection compared to BLEU's sensitivity. Results are presented with appropriate metrics and clear tables.\n\n**Significance**\n\nThe work addresses a real bottleneck where existing evaluation methods have well-documented limitations. An efficient (CPU-only), reproducible automated metric could significantly accelerate research by enabling faster iteration without expensive human evaluation. Outperforming LLM-based majority voting while being much cheaper suggests genuine practical utility. The EPLA benchmark could become a standard evaluation resource for the community.", "weaknesses": "**1. Missing Citation of Highly Related Concurrent Work [Major - Critical for Novelty Assessment]**\n\nThe paper does not cite GTED (Liu et al., \"Generalized Tree Edit Distance: A Faithful Evaluation Metric for Statement Autoformalization\", arXiv preprint, arXiv:2507.07399v1, July 10, 2025), despite substantial overlap in core contributions. Both works use operator trees extracted via Lean Language Server, extend Tree Edit Distance with semantic transformations, and evaluate on miniF2F and ProofNet. The timeline raises concerns: GTED appeared on arXiv on July 10, 2025, while the ICLR 2026 deadline was September 24, 2025, where a 2.5-month gap that should have been sufficient for discovery and citation, especially given the direct relevance to this work.\n\nWithout proper comparison, several critical questions remain unanswered. I cannot assess whether the pseudometric formulation (Theorem 1) is substantially different from GTED's \"generalized tree transformation\" framework, or whether they are merely different mathematical presentations of the same underlying idea. The transformation sets appear different quantitatively (ASSESS: 6-7 tactics vs GTED: primarily α-conversion), but it's unclear if this represents a genuine methodological advance or simply different implementation choices. Most importantly, the reported performance differences (GTED: 70.73% accuracy on miniF2F vs ASSESS: 78.82%) cannot be properly interpreted without knowing whether they stem from algorithmic improvements or merely different evaluation datasets.\n\nIf the authors were genuinely unaware of GTED during development, this represents an unfortunate collision of independent work and should be acknowledged. However, if they were aware but chose not to cite it, this falls into more serious issues of academic integrity. Either way, the current manuscript must address this relationship. I believe the contribution lacks sufficient demonstrated novelty until the authors: (1) explicitly cite GTED and clarify their awareness timeline, (2) provide detailed technical comparison showing what is genuinely new beyond GTED, and (3) ideally, evaluate both methods on identical test sets to enable fair performance comparison.\n\nI believe this issue significantly impacts my assessment of the paper's originality and must be resolved for acceptance.\n\n---\n**2. Dataset weakness**\n\n2.1 Selection bias\n\nThe benchmark includes samples that successfully compile after translation, creating severe selection bias. Based on GTED's reported numbers using Herald translator alone, the compilation success rates are approximately 84% for miniF2F (205/244) and only 25% for ProofNet (93/371). The ProofNet success rate is particularly concerning, the evaluation excludes 75% of the original test set, precisely the cases where translation is most challenging.\n\nWhile ASSESS uses both Herald and Gemini translators (producing 373 miniF2F pairs and 151 ProofNet pairs as shown in Table 2), the underlying selection bias remains: the metric is only evaluated on cases where at least one translator produced compilable output. We have no information about how TransTED would behave on the harder cases where translation completely fails. This severely limits conclusions about the metric's general applicability.\n\n2.2 Translator bias\n\nThe benchmark relies exclusively on two translators (Herald and Gemini 2.5 Pro). Different autoformalization systems may produce systematically different output patterns, where some favoring verbose formulations, others producing compact statements, or using different Mathlib conventions. TransTED's performance might not transfer to outputs from other translation systems. Including diverse translators would strengthen claims about the metric's general applicability. This selection bias severely limits the conclusions we can draw about the metric's general applicability. The paper should explicitly discuss this limitation and its implications.\n\n2.3 Simple statement-only evaluation\n\nBoth miniF2F and ProofNet contain only simple, single-statement theorems , and typically one-line formulas expressing direct mathematical relationships. Real world formalization is substantially more complex, often involving custom definitions (def), structured types (structure, inductive), multi-statement developments with auxiliary lemmas, and nontrivial type hierarchies. \n\nFor example, a predicted formalization might define a helper function that accomplishes the same mathematical purpose as the ground truth's , but with different naming and internal structure. The current OPT-based approach, which only compares the final theorem statement in isolation, might struggle with such cases. The paper provides no discussion of this limitation. It remains unclear whether TransTED can handle complex multi-component formalizations, whether OPT construction can parse and align definitions appropriately, or whether transformation tactics generalize beyond simple theorems.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "2GyBV5lXQD", "reviewer": "Reviewer_qWzN", "summary": "This work introduces ASSESS, a two stage evaluation framework that first translates natural language formal statements using the Lean Language Server into Operator and then measures the distance between the translation and a ground truth via a new metric TransTED. TransTED is a core contribution of the paper, and it extends from Tree Edit Distance by applying transformations to Operator Trees that surface semantic similarity (making the metric less prone to structurally different but semantically equivalent parses of formal statements). To prove the effectiveness of ASSESS the authors introduce a new dataset in this work, EPLA. EPLA is the other core contribution of this paper, and consists of 524 annotated pairs of natural language proofs and their formal translations annotated by experts.\n\nThe authors show that on EPLA, their method (ASSESS) consistently outperforms traditional evaluation metrics for autoformalization (this is a meta-evaluation, their evaluation framework is better at evaluating the task of auto-formalization).  The authors take care to compare against several common approaches for evaluating autoformalization including string based approaches, model-based approaches (like DeepSeek majority voting), and proof-based approaches.  ASSESS not only achieves higher accuracy, but has clear benefits to the alternative methods (including lower computational budget and reproducibility).  The authors compare their method by using a simple \"Tree Edit Distance\" (no translations for surfacing semantic similarity) and find that it leads to significant degradations when removed, showing the efficacy of their TransTED metric.", "questions": "- Why is there no mutually provable & like* label? (I may be misunderstanding the relation between mutually provable and structurally similar under transformation)", "limitations": "", "rating": 6, "confidence": 3, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "- **A large contribution: a dataset benchmarking evaluators for autoformalization + a method for evaluations**, a lot of work has gone into this paper, and it shows. The dataset EPLA is a nice contribution to the field for researchers working on evaluating and measuring the effectiveness of auto-formalization methods.\n- **Strong main results: the leading approach behind theirs requires large amounts of compute (deepseek)**, excluding their ablated method, in order to achieve both high precision and recall when evaluating auto-formalization, their method appears to be the best as well as the most cost-effective.\n- **Well written and clear results**, the math is a bit dense, but the paper overall is quite clear and well written. The graphs and tables show the results of their experiments clearly; figures 1 and 2 also help make their contributions a bit more concrete (showcasing an overview of the ASSESS framework and an example of an Operator Tree, respectively).\n\nI lack the expertise to critically evaluate if the math theorems and proofs introduced in the paper are accurate or well-constructed, but the prose surrounding them was clear enough for me to understand and follow. Overall, this paper seems like a good contribution.", "weaknesses": "- **A lack of analysis** The method introduced does perform the best over all other evaluation methods; however, there is no discussion on the failure modes of the proposed method.  This makes it a bit difficult to understand where improvements could be made or more research is necessary (the EPLA dataset has some room left for improvement, so this may be a nice addition to the work).  *It is possible that some of this is discussed in the Appendix, and I missed it; if so, I'd still like a callout in the main body.*\n- **Lack of ablations** There is one ablation, that of removing all the translations and using \"TED\" as the metric in ASSESS, but I do wonder how much of the gain TransTED gets from having each individual translation.  It may be worrisome if most of the gain from TransTED came from only a few of the translations in Table 1, or conversely, it may be insightful to see that all the translations improved the performance of TransTED, indicating that maybe future researchers could focus on devising more of these in order to push performance on EPLA further.  I think what I'd like to see is more discussion on whether the translations introduced provide the most gain and other translations won't help that much, or if adding a whole library of translations could improve performance significantly.\n\n\n---\n\nMinor notes:\n- There's a weird artifact on lines 293 or 294 where the top of the text is slightly cut off.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "08C8ttb1M5", "reviewer": "Reviewer_nDGg", "summary": "ASSESS is a two-stage framework to evaluate similarity between formal statements by combining structure and semantics. It parses statements into Operator Trees, then scores them with TransTED Similarity—an enhanced tree edit distance that applies semantic-preserving transformations. The authors introduce EPLA, a 524-pair expert-annotated benchmark (from miniF2F and ProofNet) labeled for both semantic provability and structural likeness. On EPLA, TransTED achieves state-of-the-art accuracy and the highest Cohen’s Kappa, outperforming string-, syntax-, proof-, and LLM-judge baselines. It is CPU-only, reproducible, provides continuous similarity scores, and ablations show the transformation component drives the gains.", "questions": "Please refer to Weaknesses.", "limitations": "", "rating": 2, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The proposed TransTED metric effectively combines syntactic and semantic information, overcoming the major limitation of existing purely structural or proof-based methods.  \n- Introduces a semantically enhanced Tree Edit Distance that accounts for logical transformations, providing graded similarity instead of binary judgments.  \n- Builds the largest expert-annotated dataset for this task (524 pairs), allowing rigorous and reproducible evaluation.", "weaknesses": "- No source code is provided.\n- Why not compare with models like Kimina-Autoformalizer-7B and Goedel-Formalizer-V2-8B?  \n- Perhaps you could compare the recall accuracy with some embedding-based retrieval systems.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "veqFIlTFvn", "reviewer": "Reviewer_FqxJ", "summary": "This paper proposes a similarity score metric to assess the semantic and structural correspondence between pairs of formalized statements in autoformalization. Specifically, the proposed TransTED method leverages tree edit distance (TED) on operator trees extracted from Lean, and further augments TED through transformations based on tactics applied to equality relations between statements. To evaluate TransTED, the authors construct the EPLA dataset, which consists of autoformalized formal statements collected from MiniF2F and ProofNet. Experimental results show that TransTED achieves higher accuracy and Kappa coefficient compared to several baseline metrics on the newly constructed EPLA dataset, and demonstrates greater robustness than the BLEU score.", "questions": "How are semantic provability and structural similarity jointly used to evaluate the actual equivalence between two formal statements in the experiments? Could the authors provide a few concrete examples illustrating how these two aspects interact during evaluation?\n\nIn the example mathd_algebra_132, the labeled statements appear to perform a one-step reasoning that directly substitutes the point coordinates into the line equation. I am curious whether current LLMs also perform such autoformalization. Moreover, if an LLM conducts multiple reasoning steps during autoformalization, would it still be considered equivalent under the proposed metric?\n\nWhat is the average computation time of TED and TransTED during evaluation?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "The paper is generally easy to read and well-organized. I appreciate the formalization and clear logical flow of the methodology section. The proposed method is well motivated and intuitively explained. Experimental results show that it outperforms existing baselines by a reasonable margin in accuracy and is better aligned with manual evaluations, demonstrating its effectiveness.", "weaknesses": "The proposed evaluation metric extends the traditional TED score through several augmentations; however, in practice, the implementation primarily applies a limited set of Lean tactics to establish the equality of two formal statements, and relies on a curated subset of these tactics. When the tactics fail to prove equivalence, the method simply falls back to the standard TED computation. Thus, the approach can be viewed as augmenting or relaxing proof-based equivalence checking with TED-based similarity, rather than achieving full proof-based validation. As a result, the evaluation metric does not guarantee 100% precision, unlike BEq or identity matching.\n\nI also find some aspects of the experiments a bit unclear (see questions below). In my opinion, definitional equality should yield 100% precision—the reported misclassified examples mostly involve implicit type variables, which could reasonably be interpreted as equivalent or easily resolvable by instantiation.\n\nFinally, I would suggest avoiding the claim that “to our knowledge, this represents the largest and most comprehensive dataset dedicated to this evaluation task.” Several recent works have autoformalized and manually verified a larger number of statements than those included in EPLA, such as:\n\n[1] Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency\n\n[2] FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models\n\n[3] Improving Autoformalization Using Type Checking", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)