ASSESS：面向语句相似性的语义与结构评估框架

尽管在语句自动形式化方面取得了显著进展，但仍缺乏能够评估形式翻译质量的自动化评估指标。现有指标往往无法在语义和结构信息之间取得平衡：基于字符串的方法忽略了语义，而基于证明的方法在证明失败时无法提供分级的相似度。为此，我们提出ASSESS（A Semantic and Structural Evaluation Framework for Statement Similarity），通过将形式语句转换为运算树来捕捉语法结构，并利用我们新创新的TransTED（Transformation Tree Edit Distance）相似度度量，结合语义变换来计算实值相似度得分。为进行严格的验证，我们present了EPLA（Evaluating Provability and Likeness for Autoformalization），一个由1,247个专家标注的形式语句对基准数据集，独立标注了语义可证性和结构相似性。实验在EPLA基准上表明，TransTED相似度超过了现有方法，实现了状态最佳准确率和Kappa分数。基准数据集、代码及详细实验结果已发布于https://github.com/XiaoyangLiu-sjtu/ASSESS。