QMFOL: Benchmarking Large Language Model Reasoning via Quantifiable Monadic First-Order Logic Test Case Generation

📄 arXiv: 2606.20227v1 📥 PDF

作者: Xinyi Zheng, Ling Shi, Tianlong Yu, Yongxin Zhao, Lorenz Goette, Kailong Wang

分类: cs.AI, cs.SE

发布日期: 2026-06-18

💡 一句话要点

提出QMFOL以解决现有推理基准评估不足的问题

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

关键词: 逻辑推理 大型语言模型 基准评估 自动化生成 语义一致性

📋 核心要点

  1. 现有推理基准缺乏对逻辑复杂性的细粒度控制，难以平衡语义多样性与逻辑一致性。
  2. QMFOL框架通过自动生成单子一阶逻辑推理任务，实现逻辑复杂性的可量化和可控性。
  3. 实验结果显示，模型在逻辑复杂性增加时性能下降，且对语义变化敏感，提供了更精确的推理能力评估。

📝 摘要（中文）

大型语言模型（LLMs）在推理方面取得了显著进展，尤其是在演绎推理领域，这对高风险决策至关重要。随着模型的不断改进，评估基准也应随之演变。然而，现有基准在逻辑复杂性控制和语义多样性与逻辑一致性之间的平衡方面存在不足。为了解决这些问题，本文提出了QMFOL，一个自动化框架，用于生成具有可量化和可控复杂性的单子一阶逻辑推理任务。该框架通过构建形式逻辑结构，确保逻辑一致性，并基于此构建了包含2880个实例的QMFOLBench基准。对六个大型推理模型和两个LLMs的评估表明，随着逻辑复杂性的增加，模型性能下降，计算开销增加。

🔬 方法详解

问题定义：本文旨在解决现有推理基准在逻辑复杂性控制和语义多样性与逻辑一致性之间的不足，导致评估结果不够准确的问题。

核心思路：QMFOL框架通过构建形式逻辑结构，利用合取和析取模式，实现对推理深度、宽度、标签类型和干扰项的精确控制，确保逻辑一致性。

技术框架：该框架包括任务生成、自然语言转换和逻辑一致性验证三个主要模块。首先生成逻辑任务，然后通过大型语言模型转换为自然语言，最后通过外部证明器进行逻辑一致性验证。

关键创新：QMFOL的主要创新在于其自动化生成逻辑推理任务的能力，能够量化和控制复杂性，与现有方法相比，提供了更高的灵活性和准确性。

关键设计：在设计中，使用了合取和析取模式来构建逻辑结构，确保了推理任务的多样性和一致性，同时设置了960种配置以覆盖不同的逻辑和语义维度。实验中还通过回路验证确保了生成任务的逻辑一致性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，随着逻辑复杂性的增加，模型性能显著下降，计算开销也随之增加。模型在True标签任务上的表现优于False或Unknown标签任务，显示出对语义变化的敏感性。这些发现为推理能力的评估提供了重要的实证依据。

🎯 应用场景

QMFOL框架的潜在应用领域包括自然语言处理、智能问答系统和决策支持系统等。通过提供更精确的推理能力评估，该研究有助于推动大型语言模型在高风险决策场景中的应用，提升其可靠性和有效性。

📄 摘要（原文）

Large Language Models (LLMs) have made significant progress in reasoning, particularly in deductive reasoning, which is crucial for high-stakes decision-making. As models improve, evaluation benchmarks should evolve to keep pace. However, existing benchmarks lack fine-grained control over logical complexity and struggle to balance semantic diversity with logical consistency. To address these issues, we propose QMFOL, an automated framework for generating monadic first-order logic reasoning tasks with quantifiable and controllable complexity. It constructs formal logical structures using conjunction and disjunction patterns, enabling precise control over reasoning depth, width, label types, and distractors. These structures are then translated into natural language via LLMs, with logical consistency ensured through round-trip verification using an external prover. Based on our framework, we build QMFOLBench, a benchmark comprising 2880 instances with 960 configurations across diverse logical and semantic dimensions. Evaluations on six large reasoning models (LRMs) and two LLMs show that performance degrades and computational overhead increases with rising logical complexity. Models perform better on True-labeled tasks than on False or Unknown ones, and exhibit sensitivity to semantic variation. Overall, QMFOL offers a scalable and reliable approach for constructing deductive reasoning benchmarks with controllable complexity, enabling more precise evaluation of reasoning capabilities in modern language models.