评估一阶逻辑相似度度量的敏感性与对齐性

最近，使用工具增强的大型语言模型（LLM）解决逻辑推理问题的成功范式，依赖于将自然语言（NL）陈述翻译成一阶逻辑（FOL）并调用外部定理证明器。然而，由于缺乏可靠的评估指标来比较生成的FOL与标准答案FOL，包含运算符和文本的FOL语句的正确性往往无法得到验证。在本文中，我们对现有的基于自然语言、FOL和图的度量在捕捉采样FOL与其对应标准答案之间差异的敏感性进行了全面研究。然后，我们衡量了基于度量的FOL排序与强大的LLM作为评判者之间的对齐程度。为此，我们对标准答案FOL语句应用了基于运算符和基于文本的扰动，以评估度量的敏感性。我们通过将度量与LLM的判断进行比较来评估度量的鲁棒性。我们的实证结果突显了n-gram度量BLEU对文本扰动的过度敏感性。运算符扰动主要影响语义图度量Smatch++，而FOL度量则对特定的运算符变化敏感。我们观察到BertScore与LLM判断之间具有更紧密的对齐，这表明了语义评估的重要性。此外，我们展示了组合度量相比单独使用度量，能同时提高鲁棒性和敏感性。