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

arXiv: https://arxiv.org/abs/2507.07399 · HTML: https://mlsanity.com/paper/2507.07399/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 35 references that are in the map.
- First posted on arXiv 10 Jul 2025.

## Builds on (most cited first, 19 of 19)

- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Towards a Mathematics Formalisation Assistant using Large Language Models](https://mlsanity.com/paper/2211.07524/) (2022)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Evaluating Token-Level and Passage-Level Dense Retrieval Models for Math Information Retrieval](https://mlsanity.com/paper/2203.11163/) (2022)

## Built on by (most cited first, 12 of 12)

- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation](https://mlsanity.com/paper/2608.10916/) (2026)
- [FormalRx: Rectify and eXamine Semantic Failures in Autoformalization](https://mlsanity.com/paper/2607.04655/) (2026)
- [Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees](https://mlsanity.com/paper/2604.19000/) (2026)
- [Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization](https://mlsanity.com/paper/2604.23135/) (2026)
- [The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization](https://mlsanity.com/paper/2606.28013/) (2026)
- [Quizzing the Translation: A Prover-Grounded Evaluation Metric for NLrightarrowFOL](https://mlsanity.com/paper/2609.33612/) (2026)
- [Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization](https://mlsanity.com/paper/2609.39228/) (2026)
- [Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation](https://mlsanity.com/paper/2610.10604/) (2026)
- [claimcheck: Measuring and Improving Specification Faithfulness](https://mlsanity.com/paper/2610.17358/) (2026)
- [Aligning Faithfulness for Theory-Scale Autoformalization](https://mlsanity.com/paper/2610.18498/) (2026)
- [Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization](https://mlsanity.com/paper/2610.20573/) (2026)

## Abstract (arXiv)

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.