Pith. sign in

REVIEW 5 major objections 5 minor 1 cited by

Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization

T0 review · 5 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read GTED, a generalized tree edit distance over operator trees, claims the top accuracy and human-agreement scores for evaluating autoformalized statements on the miniF2F and ProofNet benchmarks.

desk verdict The metric is a sensible lightweight idea, but the headline comparison is built on test-set threshold selection and the exact transformation set is underspecified, so the reported superiority is not yet established. read the letter →

arxiv 2507.07399 v2 pith:FKJSF4BX submitted 2025-07-10 cs.LG cs.AI

Yuntian Liu , Tao Zhu , Xiaoyang Liu , Yu Chen , Zhaoxuan Liu , Qingfeng Guo , Jiashuo Zhang , Kangjie Bao
show 1 more author
Tao Luo
This is my paper
classification cs.LGcs.AI MSC 68T5005C05
keywords autoformalizationtreeeditdistanceoperatortreesevaluationmetricLeanformallanguagesemanticsimilarityhumanagreementKappacoefficient
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

GTED is proposed as an automated evaluation metric for statement autoformalization—the task of translating natural-language math statements into formal languages like Lean. It works by standardizing each formal statement with the Lean language server, parsing it into an operator tree, and measuring a generalized tree edit distance that can treat semantics-preserving steps such as α-conversion (renaming bound variables) as allowed transformations. Against six baselines on human-judged subsets of miniF2F and ProofNet, GTED reports the highest accuracy (70.73%) and Kappa (0.438) on miniF2F and the joint-highest accuracy (69.89%) on ProofNet. The paper argues that GTED is both more faithful to human judgment and computationally lighter than LLM-based or theorem-prover-based evaluation. A sympathetic reader would take the central claim to be that structural edit distance on operator trees is a reliable proxy for semantic equivalence of formal statements.

What carries the argument

The load-bearing object is the operator tree (OPT), a rooted tree in which internal nodes are Lean operators with placeholder parameter slots (underscores) and leaves are variables or constants. The argument is carried by a generalized tree edit distance: a special tree transformation is a pair of trees $(T_1, T_2)$, and a generalized tree transformation collects all special transformations that are local or co-local depictions of one another; the distance is the minimum total cost of composing such transformations to convert one OPT into another. In the implementation, the allowed set $H$ includes α-conversion as a legal, cost-bearing transformation, and the raw distance is normalized by the larger tree size and thresholded to produce a binary correctness label. The classical Zhang–Shasha tree edit distance is recovered as a special case, which anchors the claim that GTED is a strict generalization rather than an ad hoc new heuristic.

What would settle it

Rescore the compiled predictions behind Table 1 with thresholds selected on only half of the human-judged miniF2F statements and then applied to the other half; if GTED's accuracy or Kappa on the held-out half is no longer the highest among the baselines, the paper's central claim of superior faithfulness is falsified.

Watch

Extended reading notes

Core claim

The central claim is that a structural edit distance computed on operator trees generalizes the classical tree edit distance into a faithful automated evaluation metric for statement autoformalization. Given a predicted formal statement and a ground-truth statement in Lean, GTED normalizes both through the Lean language server (theorem rewriting and variable expansion), parses them into operator trees, and computes the distance under a set of allowed transformations that includes α-conversion—renaming bound variables—as a semantics-preserving step. On human-judged subsets of miniF2F (205 statements) and ProofNet (93 statements), the paper reports that GTED achieves the highest accuracy (70.73%) and Kappa (0.438) on miniF2F and the joint-highest accuracy (69.89%) on ProofNet. The authors conclude that GTED offers a balanced, computationally lightweight, and more faithful alternative to string-similarity, grammar-checking, LLM-voting, and theorem-prover-based evaluations.

Load-bearing premise

The 205 and 93 human expert judgments used as gold labels are reliable and unbiased, and the decision threshold chosen on the same test sets to maximize Kappa does not inflate GTED's standing relative to the baselines.

Editorial extensions

If this is right

  • GTED gives a continuous similarity score in $[0,1]$ rather than a binary verdict, so downstream systems can rank or filter autoformalizations by closeness.
  • Because GTED shows a threshold-stable performance plateau, deployers do not need to locate a narrow optimal threshold as they would for BLEU.
  • GTED avoids the low recall of Identity Match and the low precision of Typecheck, and it outperforms prover-based metrics that miss many valid formalizations because of limited automated theorem proving capability.
  • With only the renaming half of α-conversion implemented, GTED already treats variable renaming as semantics-preserving; a fully scope-aware implementation would handle shadowed binders more accurately.
  • The lightweight cost of GTED relative to LLM majority voting makes it usable for large-scale evaluation and model selection during autoformalizer training.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A practical payoff not fully stated in the paper: because GTED's threshold curve is flat, a deployment could fix one threshold across datasets and still track human judgment, whereas BLEU would need per-dataset calibration.
  • Because the tree representation keeps a placeholder for every operator slot, GTED could be paired with a theorem prover to verify equivalence of subtrees, which is far easier than proving whole-statement equivalence; this would turn the metric into a hybrid structural-plus-logical evaluator.
  • The paper's own admission that GTED is semantically naive—it penalizes $x + y$ versus $y + x$—suggests that, despite the name, the metric measures syntactic-structural closeness rather than true logical equivalence; an independent user should treat the reported numbers as agreement with human judges on this test suite, not as a measure of mathematical meaning.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 5 minor

Summary. The paper proposes GTED (Generalized Tree Edit Distance), a metric for evaluating statement autoformalization by standardizing Lean expressions into operator trees and computing a tree-edit-distance-based similarity score. The three-stage pipeline consists of syntax standardization via the Lean Language Server, operator tree construction, and a generalized tree edit distance with a thresholded similarity mapping. Experiments on miniF2F and ProofNet compare GTED against baseline metrics using a human-judged gold standard, reporting the highest accuracy and Kappa on miniF2F and joint-highest accuracy on ProofNet. The paper also discusses α-conversion as an example semantic transformation and notes limitations including incomplete scope-awareness and future semantic rewrite rules.

Significance. The idea of using operator trees and a generalized tree edit distance for autoformalization evaluation is novel and potentially useful. The paper provides code and experimental results, which supports community reuse and further study. If the methodological issues are addressed, GTED could become a lightweight, semantics-sensitive alternative to proof-based metrics. However, the current empirical validation does not establish the headline claims because continuous metrics' decision thresholds are selected on the same test set used for scoring, and the metric's transformation set and cost function are not precisely specified. The evidence is therefore insufficient to support the paper's claim that GTED is a 'faithful' evaluation metric.

major comments (5)
  1. [Section 4.2, Table 1] GTED and BLEU are reported at their per-metric best thresholds on the same human-judged test set; the text states 'Table 1 reports their highest Kappa scores across all thresholds.' Because θ is chosen post-hoc on the test set to maximize agreement with the gold labels, the reported accuracy and Kappa are optimistically biased, and the comparison with threshold-free baselines (Identity, Typecheck, Definitional Equality, BEq) is unfair. The central claim that GTED outperforms these baselines is therefore not established. A valid protocol must select θ on a hold-out validation set or via cross-validation before scoring the test set, or present the full threshold curves with a fixed, pre-specified threshold.
  2. [Section 3.3, Eq. (4) and following] The transformation set H and cost function L are never specified for the experiments. The text only says 'In practice, H is likely to include' certain transformations, without listing the actual transformations used or their costs. Since dGTED depends on H and L, the metric is under-specified and the experiments cannot be reproduced. Moreover, the statement that 'legal' transformations are chosen 'for better alignment with human intuition' suggests the metric has been tuned to the human labels, which risks circularity in the evaluation.
  3. [Section 3.3, Eq. (4)] The indicator function is inverted. For identical trees, dGTED = 0, so the similarity term equals 1, and for any θ < 1 the indicator returns 1, yet the text says this indicates the trees differ. This is the opposite of the intended semantics. Please correct the formula or the prose, and clarify that the threshold is applied to the similarity score with 1 meaning 'same' or 'correct' and 0 meaning 'different'.
  4. [Section 4.1, Human Evaluation] The gold standard uses only 205 (miniF2F) and 93 (ProofNet) judgments from four experts, but no inter-annotator agreement is reported. The paper's claim that GTED is a 'faithful' metric rests on a small, possibly noisy gold standard. Without agreement statistics or a description of how disagreements were resolved, the reliability of the human labels is unknown, and the ranking of metrics based on these labels is fragile, especially for the GTED/BLEU comparison where thresholds are chosen to maximize agreement with these labels.
  5. [Section 4.1, Implementation Details] The α-conversion implementation is acknowledged to be incomplete: 'Due to the time constraints of the present work, we have provisionally deferred the implementation of the scope-aware aspect.' Since α-conversion is presented as the primary semantic-preserving transformation, the implemented GTED cannot correctly rename bound variables within nested binders. This directly undercuts the claim that GTED captures semantic equivalence and means the experiments are run on a partial version of the proposed metric.
minor comments (5)
  1. [Section 4.1 and reference list] The model is called 'HERALD Translator' in the text but 'Herald' in the reference list (Gao et al., 2024); please standardize the capitalization.
  2. [Appendix B] The prompt templates contain '[UNUSED TOKEN 146]' and similar tokens without explanation; please clarify whether these are part of the model's tokenizer template or a typographical artifact.
  3. [Section 3.3] The prose says 'The normalization process may also fail' but does not state the conditions under which normalization fails; please add a precise description of when and why this happens.
  4. [Table 1] For Identity Match on ProofNet, Precision is reported as '0/0'; this is undefined and should be replaced with 'N/A' or a dash, with a note explaining the absence of true positives.
  5. [Figure 4] The 'Best Threshold' marker is placed at the maximum of the Kappa curve, but the curve is not labeled with numeric values; adding a small annotation with the threshold and Kappa value would improve clarity.
Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The score relies on one fitted threshold and several domain assumptions. No new physical or formal entities are postulated.

free parameters (1)
  • threshold theta per metric and dataset = not stated numerically in text (best Kappa threshold)
    For continuous metrics (GTED, BLEU), Table 1 reports the highest Kappa across all thresholds; theta is chosen on the test set. This is a fitted decision parameter.
assumptions (4)
  • domain assumption Lean Language Server standardization preserves the semantic content of formal statements while removing syntactic variation.
    Section 3.1 relies on this for both the reference and predicted statements before tree construction; if normalization changes meaning, the metric compares distorted versions.
  • ad hoc to paper Operator tree edit distance is a meaningful proxy for semantic similarity of formal statements.
    This is the core modeling assumption behind GTED; the paper admits it penalizes logically equivalent but syntactically different statements (e.g., x + y vs y + x) in Section 5, so the assumption is only partially satisfied.
  • domain assumption Human expert labels are the correct gold standard for autoformalization quality.
    Section 4.1 uses four Lean4 experts to label only compiled predictions (205 miniF2F, 93 ProofNet); no inter-annotator agreement is reported.
  • standard math Zhang-Shasha tree edit distance algorithm computes the edit distance correctly for the special case used.
    Invoked for computing TED as a special case of GTED in Section 3.3.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization." pith.science (2026). https://pith.science/paper/FKJSF4BX

@misc{pith2026250707399,
  author       = {Pith},
  title        = {Pith review of: Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FKJSF4BX}},
  note         = {Machine review of arXiv:2507.07399}
}
read the original abstract

Statement autoformalization, the automated translation of statements from natural language into formal languages, has become a subject of extensive research, yet the development of robust automated evaluation metrics remains limited. Existing evaluation methods often lack semantic understanding, face challenges with high computational costs, and are constrained by the current progress of automated theorem proving. To address these issues, we propose GTED (Generalized Tree Edit Distance), a novel evaluation framework that first standardizes formal statements and converts them into operator trees, then determines the semantic similarity using the eponymous GTED metric. Across the miniF2F and ProofNet benchmarks, GTED consistently ranks as a top-performing metric, achieving the highest accuracy and Kappa on miniF2F and the joint-highest accuracy on ProofNet. This strong overall performance provides the community with a computationally lightweight and more faithful metric for automated evaluation. The code and experimental results are available at https://github.com/XiaoyangLiu-sjtu/GTED.

Figures

Figures reproduced from arXiv: 2507.07399 by the authors.

Figure 1
Figure 1. Illustration of GTED (Generalized Tree Edit Distance) for statement formalization. (a) Data Preparation: A translator model generates a formal language (FL) prediction from a natural language (NL) input. (b) Standardization: Both the FL prediction and the ground-truth FL label are standardized via theorem rewriting and variable expansion. (c) OPT Construction: The standardized statements are then parsed into operato… view at source ↗
Figure 2
Figure 2. Example of an operator tree for a formal statement. From a long-term perspective, the strategic design of place￾holders is crucial because it facilitates the rapid restoration of partial subtrees to their original formal sub-statements. This capability, in turn, enables mutual proof to establish the equivalence of these subtrees. Consequently, this approach seamlessly integrates proof-based evaluation directly into … view at source ↗
Figure 3
Figure 3. An example of α-conversion, the renaming of a bound variable. are sourced from Numina1 for miniF2F-test, and from DeepSeek2 for ProofNet-test. Moreover, since automated evaluation requires both ground truth and predicted formal statements, we employ HERALD Translator (Gao et al., 2024), a state-of-the-art autoformalization model, to trans￾late these datasets into their respective formal statements for subsequent eva… view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Comparison of BLEU and GTED across thresholds on miniF2F. like Majority Voting. As shown in [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: Comparison of BLEU and GTED across thresholds on ProofNet. Prompt Template for Back-Translation [UNUSED TOKEN 146]user\nConvert the formal statement into natural language:\n“‘ lean\nformal statement\n“‘[UNUSED TOKEN 145]\n[UNUSED TOKEN 146]assistant\n Prompt Template f…

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

    cs.CL 2026-07 conditional novelty 7.0 of 10

    FormalRx diagnoses Lean autoformalization failures with a 28-category SCI taxonomy and an 8B model that jointly predicts alignment, error type, location, and correction.

Reference graph

Works this paper leans on

13 extracted references · 5 canonical work pages · cited by 1 Pith paper

  1. [1]

    Towards a mathematics formalisation as- sistant using large language models

    Agrawal, A., Gadgil, S., Goyal, N., Narayanan, A., and Tadipatri, A. Towards a mathematics formalisation as- sistant using large language models. arXiv preprint arXiv:2211.07524,

    arXiv

  2. [4]

    Moura, L

    arXiv preprint arXiv:2406.01940, 2024b. Moura, L. d. and Ullrich, S. The Lean 4 theorem prover and programming language. In Automated Deduction– CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pp. 625–635. Springer,

    arXiv 2021

  3. [6]

    Rethinking and improving autoformalization: Towards a faithful met- ric and a dependency retrieval-based approach

    Liu, Q., Zheng, X., Lu, X., Cao, Q., and Yan, J. Rethinking and improving autoformalization: Towards a faithful met- ric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Repre- sentations, 2025a. Liu, X., Bao, K., Zhang, J., Liu, Y ., Chen, Y ., Liu, Y ., Jiao, Y ., and Luo, T. Atlas: Autoformalizing theo- ...

    arXiv

  4. [10]

    First experiments with neural translation of informal to formal mathematics

    Wang, Q., Kaliszyk, C., and Urban, J. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13- 17, 2018, Proceedings 11, pp. 255–270. Springer,

    work page 2018

  5. [11]

    Lean Workbook: A large-scale Lean problem set for- malized from natural language math problems

    Ying, H., Wu, Z., Geng, Y ., Wang, J., Lin, D., and Chen, K. Lean Workbook: A large-scale Lean problem set for- malized from natural language math problems. In The Thirty-eight Conference on Neural Information Process- ing Systems Datasets and Benchmarks Track, 2024a. Ying, H., Zhang, S., Li, L., Zhou, Z., Shao, Y ., Fei, Z., Ma, Y ., Hong, J., Liu, K., W...

    arXiv

  6. [13]

    Evaluating Token-Level and Passage-Level Dense Retrieval Models for Math Information Retrieval

    Zhong, W., Xie, Y ., and Lin, J. Applying structural and dense semantic matching for the arqmath lab 2022, clef. In CLEF (Working Notes), pp. 147–170, 2022a. Zhong, W., Yang, J.-H., Xie, Y ., and Lin, J. Evaluat- ing token-level and passage-level dense retrieval mod- els for math information retrieval. arXiv preprint arXiv:2203.11163, 2022b. Zhou, J. P., ...

    work page Pith review arXiv 2022

  7. [1989]

    Consistent autofor- malization for constructing mathematical libraries

    Zhang, L., Quan, X., and Freitas, A. Consistent autofor- malization for constructing mathematical libraries. In Proceedings of the 2024 Conference on Empirical Meth- ods in Natural Language Processing , pp. 4020–4033. Association for Computational Linguistics, November

    work page 2024

  8. [1994]

    Deepseek- prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition

    Ren, Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., et al. Deepseek- prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801,

    arXiv

Show all 13 references
  1. [1996]

    Q., Li, W., and Jamnik, M

    Jiang, A. Q., Li, W., and Jamnik, M. Multilingual mathemat- ical autoformalization. arXiv preprint arXiv:2311.03755,

    arXiv

  2. [2022]

    W., Radev, D., and Avigad, J

    Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E. W., Radev, D., and Avigad, J. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433,

    arXiv

  3. [2023]

    The Lean theorem prover (system description)

    De Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J. The Lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378–388. Springer,

    2015

  4. [2024]

    Deepseek-v3 technical report

    Liu, A., Feng, B., Xue, B., Wang, B., Wu, B., Lu, C., Zhao, C., Deng, C., Zhang, C., Ruan, C., et al. Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437,

    arXiv

  5. [2025]

    A promising path towards autoformaliza- tion and general artificial intelligence

    Szegedy, C. A promising path towards autoformaliza- tion and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceed- ings 13, pp. 3–20. Springer,

    2020

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.