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

• URL: http://arxiv.org/abs/2507.07399v2
• Date: Fri, 22 Aug 2025 13:20:21 GMT
• Title: Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization
• Authors: Yuntian Liu, Tao Zhu, Xiaoyang Liu, Yu Chen, Zhaoxuan Liu, Qingfeng Guo, Jiashuo Zhang, Kangjie Bao, Tao Luo,
• Abstract summary: GTED is an evaluation framework that standardizes formal statements and converts them into operator trees.<n>It determines the semantic similarity using the eponymous GTED metric.<n>GTED consistently ranks as a top-performing metric, achieving the highest accuracy and Kappa on miniF2F and the joint-highest accuracy on ProofNet.
• Score: 11.26658223467498
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Table-BiEval: A Self-Supervised, Dual-Track Framework for Decoupling Structure and Content in LLM Evaluation [11.450834626205676]
  Table-BiEval is a novel approach based on a human-free, self-supervised evaluation framework.<n>It calculates Content Semantic Accuracy and Normalized Tree Edit Distance to decouple structure from content.<n>Results reveal substantial variability, highlighting that mid-sized models can surprisingly outperform larger counterparts in structural efficiency.
  arXiv  Detail & Related papers  (2026-01-09T07:38:27Z)
• ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity [9.337443482551356]
  We introduce ASSESS (A Semantic and Structural Evaluation Framework for Statement Similarity), which comprehensively integrates semantic and structural information to provide a continuous similarity score.<n>For rigorous validation, we present EPLA, a new benchmark of 524 expert-annotated formal statement pairs derived from miniF2F and ProofNet.<n>Experiments on EPLA demonstrate that TransTED Similarity outperforms existing methods, achieving state-of-the-art accuracy and the highest Kappa coefficient.
  arXiv  Detail & Related papers  (2025-09-26T12:02:58Z)
• SEOE: A Scalable and Reliable Semantic Evaluation Framework for Open Domain Event Detection [70.23196257213829]
  We propose a scalable and reliable Semantic-level Evaluation framework for Open domain Event detection.<n>Our proposed framework first constructs a scalable evaluation benchmark that currently includes 564 event types covering 7 major domains.<n>We then leverage large language models (LLMs) as automatic evaluation agents to compute a semantic F1-score, incorporating fine-grained definitions of semantically similar labels.
  arXiv  Detail & Related papers  (2025-03-05T09:37:05Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  We introduce QASemConsistency, a new formalism for localizing factual inconsistencies in attributable text generation.<n>We show that QASemConsistency yields factual consistency scores that correlate well with human judgments.
  arXiv  Detail & Related papers  (2024-10-09T22:53:48Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• On the Limitations of Embedding Based Methods for Measuring Functional Correctness for Code Generation [4.065344017083881]
  We analyze the ability of embedding-based metrics like CodeBERTScore to measure functional correctness and other helpful constructs like editing effort. Our results show that while they have a weak correlation with functional correctness (0.16), they are strongly correlated (0.72) with editing effort.
  arXiv  Detail & Related papers  (2024-04-26T15:54:39Z)
• Unlocking Structure Measuring: Introducing PDD, an Automatic Metric for Positional Discourse Coherence [39.065349875944634]
  We present a novel metric designed to quantify the discourse divergence between two long-form articles. Our metric aligns more closely with human preferences and GPT-4 coherence evaluation, outperforming existing evaluation methods.
  arXiv  Detail & Related papers  (2024-02-15T18:23:39Z)
• PROXYQA: An Alternative Framework for Evaluating Long-Form Text Generation with Large Language Models [72.57329554067195]
  ProxyQA is an innovative framework dedicated to assessing longtext generation. It comprises in-depth human-curated meta-questions spanning various domains, each accompanied by specific proxy-questions with pre-annotated answers. It assesses the generated content's quality through the evaluator's accuracy in addressing the proxy-questions.
  arXiv  Detail & Related papers  (2024-01-26T18:12:25Z)
• Generating Benchmarks for Factuality Evaluation of Language Models [61.69950787311278]
  We propose FACTOR: Factual Assessment via Corpus TransfORmation, a scalable approach for evaluating LM factuality. FACTOR automatically transforms a factual corpus of interest into a benchmark evaluating an LM's propensity to generate true facts from the corpus vs. similar but incorrect statements. We show that: (i) our benchmark scores increase with model size and improve when the LM is augmented with retrieval; (ii) benchmark score and perplexity do not always agree on model ranking; (iii) when perplexity and benchmark score disagree, the latter better reflects factuality in open-ended generation.
  arXiv  Detail & Related papers  (2023-07-13T17:14:38Z)
• BLEURT Has Universal Translations: An Analysis of Automatic Metrics by Minimum Risk Training [64.37683359609308]
  In this study, we analyze various mainstream and cutting-edge automatic metrics from the perspective of their guidance for training machine translation systems. We find that certain metrics exhibit robustness defects, such as the presence of universal adversarial translations in BLEURT and BARTScore. In-depth analysis suggests two main causes of these robustness deficits: distribution biases in the training datasets, and the tendency of the metric paradigm.
  arXiv  Detail & Related papers  (2023-07-06T16:59:30Z)
• INSTRUCTSCORE: Explainable Text Generation Evaluation with Finegrained Feedback [80.57617091714448]
  We present InstructScore, an explainable evaluation metric for text generation. We fine-tune a text evaluation metric based on LLaMA, producing a score for generated text and a human readable diagnostic report.
  arXiv  Detail & Related papers  (2023-05-23T17:27:22Z)
• Towards Interpretable and Efficient Automatic Reference-Based Summarization Evaluation [160.07938471250048]
  Interpretability and efficiency are two important considerations for the adoption of neural automatic metrics. We develop strong-performing automatic metrics for reference-based summarization evaluation.
  arXiv  Detail & Related papers  (2023-03-07T02:49:50Z)
• ROSCOE: A Suite of Metrics for Scoring Step-by-Step Reasoning [63.77667876176978]
  Large language models show improved downstream task interpretability when prompted to generate step-by-step reasoning to justify their final answers. These reasoning steps greatly improve model interpretability and verification, but objectively studying their correctness is difficult. We present ROS, a suite of interpretable, unsupervised automatic scores that improve and extend previous text generation evaluation metrics.
  arXiv  Detail & Related papers  (2022-12-15T15:52:39Z)
• On the Usefulness of Embeddings, Clusters and Strings for Text Generator Evaluation [86.19634542434711]
  Mauve measures an information-theoretic divergence between two probability distributions over strings. We show that Mauve was right for the wrong reasons, and that its newly proposed divergence is not necessary for its high performance. We conclude that -- by encoding syntactic- and coherence-level features of text, while ignoring surface-level features -- such cluster-based substitutes to string distributions may simply be better for evaluating state-of-the-art language generators.
  arXiv  Detail & Related papers  (2022-05-31T17:58:49Z)
• TRUE: Re-evaluating Factual Consistency Evaluation [29.888885917330327]
  We introduce TRUE: a comprehensive study of factual consistency metrics on a standardized collection of existing texts from diverse tasks. Our standardization enables an example-level meta-evaluation protocol that is more actionable and interpretable than previously reported correlations. Across diverse state-of-the-art metrics and 11 datasets we find that large-scale NLI and question generation-and-answering-based approaches achieve strong and complementary results.
  arXiv  Detail & Related papers  (2022-04-11T10:14:35Z)
• RoMe: A Robust Metric for Evaluating Natural Language Generation [7.594468763029502]
  We propose an automatic evaluation metric incorporating several core aspects of natural language understanding. Our proposed metric, RoMe, is trained on language features such as semantic similarity combined with tree edit distance and grammatical acceptability. Empirical results suggest that RoMe has a stronger correlation to human judgment over state-of-the-art metrics in evaluating system-generated sentences.
  arXiv  Detail & Related papers  (2022-03-17T09:07:39Z)
• Curious Case of Language Generation Evaluation Metrics: A Cautionary Tale [52.663117551150954]
  A few popular metrics remain as the de facto metrics to evaluate tasks such as image captioning and machine translation. This is partly due to ease of use, and partly because researchers expect to see them and know how to interpret them. In this paper, we urge the community for more careful consideration of how they automatically evaluate their models.
  arXiv  Detail & Related papers  (2020-10-26T13:57:20Z)
• GO FIGURE: A Meta Evaluation of Factuality in Summarization [131.1087461486504]
  We introduce GO FIGURE, a meta-evaluation framework for evaluating factuality evaluation metrics. Our benchmark analysis on ten factuality metrics reveals that our framework provides a robust and efficient evaluation. It also reveals that while QA metrics generally improve over standard metrics that measure factuality across domains, performance is highly dependent on the way in which questions are generated.
  arXiv  Detail & Related papers  (2020-10-24T08:30:20Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.