Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911115797069824 |
|---|---|
| author | Liu, Yuntian Zhu, Tao Liu, Xiaoyang Chen, Yu Liu, Zhaoxuan Guo, Qingfeng Zhang, Jiashuo Bao, Kangjie Luo, Tao |
| author_facet | Liu, Yuntian Zhu, Tao Liu, Xiaoyang Chen, Yu Liu, Zhaoxuan Guo, Qingfeng Zhang, Jiashuo Bao, Kangjie Luo, Tao |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_07399 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization Liu, Yuntian Zhu, Tao Liu, Xiaoyang Chen, Yu Liu, Zhaoxuan Guo, Qingfeng Zhang, Jiashuo Bao, Kangjie Luo, Tao Machine Learning Artificial Intelligence 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. |
| title | Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization |
| topic | Machine Learning Artificial Intelligence |
| url | https://arxiv.org/abs/2507.07399 |