Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategy

📄 arXiv: 2511.11816v1 📥 PDF

作者: Andrea Brunello, Luca Geatti, Michele Mignani, Angelo Montanari, Nicola Saccomanno

分类: cs.AI, cs.CL, cs.LO

发布日期: 2025-11-14

备注: Full version of the paper accepted for publication at The 40th Annual AAAI Conference on Artificial Intelligence (AAAI 2026)

💡 一句话要点

提出NL-FOL翻译新基准，揭示LLM在逻辑理解上的真正能力

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

关键词: 自然语言处理 一阶逻辑 大型语言模型 NL-FOL翻译 逻辑推理

📋 核心要点

  1. 现有NL-FOL翻译数据集存在局限性，可能低估了LLM的真实逻辑理解能力。
  2. 提出一种新的评估协议，旨在区分LLM的逻辑理解与模式识别能力。
  3. 实验表明，对话型LLM在新的基准测试中表现出强大的NL-FOL翻译能力。

📝 摘要（中文）

一阶逻辑(FOL)因其表达性和明确性，是表示自然语言(NL)概念的强大形式体系，可用于指定和验证系统属性。将FOL翻译成易读的英语相对简单，但反向问题，即NL到FOL的翻译(NL-FOL翻译)，对人类和机器来说都是一个长期存在的挑战。虽然大型语言模型(LLM)的出现带来了突破的希望，但最近的文献对它们执行NL-FOL翻译的能力提供了相互矛盾的结果。本文做出了三方面的贡献。首先，我们批判性地检查了现有的用于评估NL-FOL翻译性能的数据集和协议，揭示了可能导致LLM实际能力被错误表示的关键局限性。其次，为了克服这些缺点，我们提出了一种新的评估协议，该协议明确旨在区分真正的语义层面的逻辑理解与肤浅的模式识别、记忆和数据集污染。第三，使用这种新方法，我们表明，最先进的、面向对话的LLM表现出强大的NL-FOL翻译技能和对句子级逻辑的真正掌握，而以嵌入为中心的模型表现明显更差。

🔬 方法详解

问题定义：论文旨在解决自然语言到一阶逻辑（NL-FOL）翻译任务中，现有评估方法无法准确衡量大型语言模型（LLM）逻辑理解能力的问题。现有数据集和评估协议存在过度依赖模式识别、记忆和数据集污染等问题，导致对LLM能力的误判。现有方法的痛点在于无法区分LLM是真正理解了语义逻辑，还是仅仅在进行表面上的模式匹配。

核心思路：论文的核心思路是设计一种新的评估协议，该协议能够有效区分LLM的逻辑理解能力和模式识别能力。通过精心设计的测试用例，排除LLM通过记忆或简单模式匹配来完成翻译的可能性，从而更准确地评估其真正的逻辑推理能力。

技术框架：论文主要关注评估协议的设计，而非提出新的模型架构。整体流程包括：1）分析现有NL-FOL数据集的局限性；2）设计新的评估协议，包括测试用例的生成策略和评估指标；3）使用新的评估协议评估现有LLM的性能；4）分析实验结果，揭示LLM在NL-FOL翻译中的优势和不足。

关键创新：论文最重要的技术创新点在于提出了一个更严格、更可靠的NL-FOL翻译评估基准。该基准通过精心设计的测试用例，减少了数据集污染和模式识别的影响，从而能够更准确地评估LLM的逻辑理解能力。与现有方法的本质区别在于，新基准更侧重于考察LLM是否真正理解了自然语言的语义，并将其正确地转化为一阶逻辑表达式。

关键设计：论文的关键设计在于测试用例的生成策略。具体细节未知，但可以推测，新的测试用例可能包含以下特点：1）包含复杂的逻辑结构，例如嵌套的量词和逻辑连接词；2）避免使用常见的短语和表达方式，以减少LLM通过记忆来完成翻译的可能性；3）包含多种不同的表达方式，但逻辑含义相同，以考察LLM的语义理解能力；4）评估指标可能包括翻译的准确率、逻辑等价性等。

🖼️ 关键图片

fig_0

📊 实验亮点

实验结果表明，使用新的评估协议，面向对话的LLM表现出强大的NL-FOL翻译能力，表明它们在句子级逻辑方面具有真正的理解能力。相比之下，以嵌入为中心的模型表现明显更差，突显了新评估协议区分逻辑理解和模式识别的能力。具体的性能数据和提升幅度未知。

🎯 应用场景

该研究成果可应用于自然语言处理、知识表示与推理、智能系统验证等领域。更准确的NL-FOL翻译能力有助于构建更智能的对话系统、自动定理证明器和形式化验证工具。未来，该研究可以促进人机交互的自然性和可靠性，并推动人工智能在复杂问题求解中的应用。

📄 摘要（原文）

Due to its expressiveness and unambiguous nature, First-Order Logic (FOL) is a powerful formalism for representing concepts expressed in natural language (NL). This is useful, e.g., for specifying and verifying desired system properties. While translating FOL into human-readable English is relatively straightforward, the inverse problem, converting NL to FOL (NL-FOL translation), has remained a longstanding challenge, for both humans and machines. Although the emergence of Large Language Models (LLMs) promised a breakthrough, recent literature provides contrasting results on their ability to perform NL-FOL translation. In this work, we provide a threefold contribution. First, we critically examine existing datasets and protocols for evaluating NL-FOL translation performance, revealing key limitations that may cause a misrepresentation of LLMs' actual capabilities. Second, to overcome these shortcomings, we propose a novel evaluation protocol explicitly designed to distinguish genuine semantic-level logical understanding from superficial pattern recognition, memorization, and dataset contamination. Third, using this new approach, we show that state-of-the-art, dialogue-oriented LLMs demonstrate strong NL-FOL translation skills and a genuine grasp of sentence-level logic, whereas embedding-centric models perform markedly worse.