Assessing the Sensitivity and Alignment of FOL Closeness Metrics

📄 arXiv: 2501.08613v3 📥 PDF

作者: Ramya Keerthy Thatikonda, Wray Buntine, Ehsan Shareghi

分类: cs.CL

发布日期: 2025-01-15 (更新: 2025-09-05)

备注: EMNLP 2025

💡 一句话要点

评估一阶逻辑相似度指标的敏感性和对齐性，提升逻辑推理评估质量

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 一阶逻辑 逻辑推理 评估指标 大型语言模型 敏感性分析

📋 核心要点

  1. 现有工具增强型大型语言模型在解决逻辑推理问题时，缺乏可靠的评估指标来比较生成和真值一阶逻辑公式。
  2. 该论文通过对一阶逻辑公式进行扰动，并与大型语言模型的判断进行比较，来评估现有指标的敏感性和鲁棒性。
  3. 实验结果表明，现有指标存在过敏感或对特定扰动不敏感的问题，组合多个指标可以提高评估的鲁棒性和敏感性。

📝 摘要（中文）

本文全面研究了现有自然语言、一阶逻辑和图相似度指标在捕获采样一阶逻辑公式与其对应真值公式之间差异的敏感性。同时，衡量了基于指标的公式排序与强大的大型语言模型（LLM）判断之间的对齐性。为此，首先对真值一阶逻辑公式应用基于操作符和文本的扰动，以评估指标的敏感性。然后，通过将指标与LLM的判断进行比较来评估指标的鲁棒性。实验结果表明，n-gram指标BLEU对文本扰动过于敏感；操作符扰动会影响语义图指标Smatch++对结构变化的捕捉，以及一阶逻辑指标对特定操作符变化的捕捉。BertScore与LLM的判断更一致，证明了语义评估的重要性。此外，研究表明，与使用单个指标相比，组合多个指标可以提高鲁棒性和敏感性。

🔬 方法详解

问题定义：论文旨在解决缺乏可靠的评估指标来比较生成的一阶逻辑（FOL）公式和ground-truth公式的问题。现有方法，如BLEU、Smatch++等，在评估FOL公式的正确性时存在局限性，无法准确反映公式之间的语义差异，并且对某些类型的扰动过于敏感或不敏感。这使得难以有效验证LLM生成的FOL公式的质量。

核心思路：论文的核心思路是通过系统性地评估现有评估指标对FOL公式中不同类型扰动的敏感性和鲁棒性，来确定哪些指标能够更好地捕捉FOL公式之间的语义差异。同时，通过将指标的评估结果与LLM的判断进行比较，来衡量指标与人类判断的对齐性。最终，探索组合多个指标以提高评估性能的可能性。

技术框架：论文的技术框架主要包括以下几个步骤：1) 对ground-truth FOL公式应用基于操作符和文本的扰动，生成一系列perturbed FOL公式。2) 使用现有的自然语言、FOL和图相似度指标（如BLEU、Smatch++、BertScore等）来计算perturbed FOL公式与ground-truth公式之间的相似度。3) 使用LLM作为裁判，对perturbed FOL公式的质量进行排序。4) 将指标的排序结果与LLM的排序结果进行比较，评估指标的对齐性。5) 分析指标对不同类型扰动的敏感性，并探索组合多个指标以提高评估性能。

关键创新：论文的关键创新在于：1) 系统性地评估了现有评估指标对FOL公式的敏感性和鲁棒性，揭示了现有指标的局限性。2) 提出了使用LLM作为裁判来评估指标对齐性的方法，为评估FOL公式的质量提供了一种新的思路。3) 探索了组合多个指标以提高评估性能的可能性，并验证了组合指标的有效性。

关键设计：论文的关键设计包括：1) 扰动策略的设计，包括基于操作符和文本的扰动，以模拟LLM生成FOL公式时可能出现的错误。2) 评估指标的选择，包括自然语言、FOL和图相似度指标，以覆盖不同类型的评估方法。3) LLM裁判的设计，包括选择合适的LLM模型和prompt，以确保LLM能够准确评估FOL公式的质量。4) 对齐性评估方法的设计，包括使用Spearman相关系数来衡量指标排序与LLM排序之间的相关性。

📊 实验亮点

实验结果表明，BLEU对文本扰动过于敏感，Smatch++对结构变化敏感，BertScore与LLM判断更一致。组合多个指标可以提高评估的鲁棒性和敏感性。这些发现为选择合适的FOL公式评估指标提供了重要参考，并为进一步研究FOL公式评估方法奠定了基础。

🎯 应用场景

该研究成果可应用于提升工具增强型大型语言模型在逻辑推理任务中的性能。通过选择更合适的评估指标或组合多个指标，可以更准确地评估LLM生成的FOL公式的质量，从而指导LLM的训练和优化。此外，该研究还可以应用于其他需要评估逻辑公式相似度的场景，例如知识图谱推理、程序验证等。

📄 摘要（原文）

The recent successful paradigm of solving logical reasoning problems with tool-augmented large language models (LLMs) leverages translation of natural language (NL) statements into First-Order Logic~(FOL) and external theorem provers. However, the correctness of FOL statements, comprising operators and text, often go unverified due to the lack of a reliable evaluation metric for comparing generated and ground-truth FOLs. In this paper, we conduct a comprehensive study on the sensitivity of existing NL-, FOL-, and graph-based metrics to capture differences between a sampled FOL and its corresponding ground-truth. We then measure the alignment between a metric-based ranking of FOL outputs and a strong LLM as-a-judge. To do this, we first apply operator and text-based perturbations to ground-truth FOL statements to assess metric sensitivity. We then evaluate metric robustness by comparing the metrics against LLMs judgment. Our empirical findings highlight a clear oversensitivity in the n-gram metric BLEU for text perturbations. The operator perturbation affects the semantic graph metric Smatch++ for structural changes, and the FOL metric for specific operator changes. We observe a closer alignment between BertScore and LLM judgement, proving the importance of semantic evaluation. Additionally, we show that combining metrics enhances both robustness and sensitivity compared to using individual metrics.