提出新评估指标GTED，更准确衡量自然语言转形式化表达的效果。
Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization
- 将形式化语句转为操作符树，用广义树编辑距离计算语义相似度
- 在miniF2F和ProofNet上均达顶尖准确率，Kappa值最高
- 轻量高效，适合自动化评估，推动形式化研究发展
陈述自动形式化（statement autoformalization）指将自然语言陈述自动翻译为形式语言，已成为研究热点，但稳健的自动化评估指标仍十分有限。现有方法常缺乏语义理解能力，计算成本高，且受限于自动定理证明技术进展。为此，我们提出GTED（Generalized Tree Edit Distance），一种新评估框架：先标准化形式化陈述并转化为操作符树，再通过广义树编辑距离度量语义相似性。在miniF2F与ProofNet两个基准上，GTED始终表现优异，在miniF2F上取得最高准确率与Kappa值，在ProofNet上达到联合最高准确率。其强大性能为社区提供了计算轻量、更忠实的自动化评估工具。代码与实验结果见https://github.com/XiaoyangLiu-sjtu/GTED。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。