提出新框架评估形式化语句相似性，兼顾语义与结构。
ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity
- 将形式化语句转为操作符树，用新度量法计算相似性。
- 在1247对专家标注数据上表现最优，准确率与一致性评分领先。
- 适合形式化推理、自动证明方向的研究者使用。
尽管声明自动形式化取得显著进展，但自动化评估指标仍存在关键缺口，难以有效评估形式化质量。现有方法或忽略语义（字符串匹配），或在证明失败时无法提供分级相似性评分。为此，我们提出ASSESS（Statement Similarity的语义与结构评估框架），通过将形式化语句转换为操作符树，并结合语义变换，引入新型TransTED（Transformation Tree Edit Distance）相似性度量，实现真实值相似性评分。为严谨验证，我们构建EPLA（评估自动形式化的可证明性与相似性）基准，包含1,247对来自miniF2F和ProofNet的专家标注形式化语句对，分别标注了语义可证明性与结构相似性。在EPLA上的实验表明，TransTED相似性超越现有方法，达到最先进的准确率与Kappa评分。代码、数据集及详细结果已开源：https://github.com/XiaoyangLiu-sjtu/ASSESS。
原文摘要 · Abstract (English)
Despite significant strides in statement autoformalization, a critical gap remains in the development of automated evaluation metrics capable of assessing formal translation quality. Existing metrics often fail to balance semantic and structural information: string-based methods neglect semantics, whereas proof-based approaches offer no graded similarity when proofs fail. To address these issues, we introduce ASSESS (A Semantic and Structural Evaluation Framework for Statement Similarity), which captures syntactic structure by transforming formal statements into operator trees and computes a real-valued similarity score using our novel TransTED (Transformation Tree Edit Distance) Similarity metric by incorporating semantic transformations. For rigorous validation, we present EPLA (Evaluating Provability and Likeness for Autoformalization), a benchmark comprising 1,247 expert-annotated formal statement pairs derived from miniF2F and ProofNet, distinctively labeled for both semantic provability and structural likeness. Experiments on the EPLA benchmark demonstrate that TransTED Similarity surpasses existing methods, achieving state-of-the-art accuracy and Kappa score. The benchmark dataset, code, and detailed experimental results are available at https://github.com/XiaoyangLiu-sjtu/ASSESS.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。