跳转至

Are Language Models Efficient Reasoners? A Perspective from Logic Programming

会议: NeurIPS 2025 arXiv: 2510.25626 代码: GitHub 领域: LLM推理 / 形式化评估 关键词: reasoning efficiency, logic programming, irrelevant information, proof length, deductive reasoning

一句话总结

从逻辑编程角度提出评估 LLM 推理效率（而非仅正确性）的框架——通过 verbalized logic program 将自然语言证明映射到逻辑程序证明，发现当前 LLM 在含无关公理的数学题中不仅准确率下降，且推理过程严重低效（超过一半的推理步骤是不必要的）。

研究背景与动机

  1. 领域现状：LLM 推理评估主要关注最终答案的正确性，忽略了推理过程的效率。近期推理模型（如 o1、DeepSeek-R1）经常生成远超必要的推理步骤。
  2. 现有痛点：(1) 用 token 数量度量效率混淆了"不必要的推理步骤"和"冗长的自然语言表述"两个来源；(2) 缺乏形式化框架定义"高效推理"；(3) 现有数据集（GSM8k-IC 等）仅添加一条无关信息，无法系统评估。
  3. 核心矛盾：现实推理中大量可用信息是无关的，高效推理需要识别并忽略干扰；但 LLM 缺乏系统性地区分相关/无关信息的能力。
  4. 本文要解决什么？ (1) 定义并度量推理效率；(2) 系统评估 LLM 面对无关信息时的准确性和效率。
  5. 切入角度：逻辑编程提供了干净的形式化框架——每个推理步骤对应超图中的一条边，最短证明是最高效的。通过 verbalized logic program 将自然语言证明映射回逻辑推导步骤。
  6. 核心idea一句话：用 verbalized logic program 桥接自然语言推理和形式化推导，以最短证明为参照度量 LLM 的推理效率。

方法详解

整体框架

(1) 构建 verbalized GSM logic program：从 GSM 风格数学题生成逻辑程序，每个定理关联自然语言描述；(2) 注入无关公理：添加与目标定理不同程度语义重叠的无关信息；(3) 评估：将 LLM 生成的 CoT 证明映射回逻辑程序的定理，与最短证明对比。

关键设计

  1. Verbalized Logic Program:
  2. 做什么：为逻辑程序中的每个定理关联一组自然语言字符串，实现形式化推理和自然语言推理的双向映射
  3. 核心思路：构建包含公理（已知事实）、推理规则（如加法、乘法）和目标定理的带类型逻辑程序，每个元素都有对应的自然语言模板

  4. 设计动机：区分"不必要的推理步骤"和"冗长表述"——只度量前者

  5. 系统化的无关信息注入:

  6. 做什么：在 GSM 问题中添加可控数量的无关公理，且控制无关公理与目标问题的语义重叠度
  7. 核心思路：三种重叠类型——(1) 主体重叠（涉及相同人物如 "Ryan"）；(2) 对象重叠（涉及相同物品如 "cats"）；(3) 双重重叠（同时涉及相同人物和物品）

  8. 设计动机：现有数据集只添加一条无关信息，本框架可添加任意数量、可控重叠度的无关信息

  9. 效率度量:

  10. 做什么：将 LLM 的 CoT 步骤映射到逻辑程序的定理，计算"非必要定理比例"
  11. 核心思路：对于正确回答的问题，统计 LLM 生成的证明中有多少定理不在最短证明路径上
  12. 设计动机：最短证明是效率的理论下界，偏离量直接度量低效程度

实验关键数据

准确率下降（加入无关公理）

模型 无无关公理 1个无关 3个无关 5个无关
GPT-4o ~95% ~88% ~78% ~70%
o1-mini ~97% ~92% ~85% ~78%
Llama-3.1-70B ~85% ~75% ~60% ~50%

推理效率（正确答案中的不必要定理比例）

条件 不必要定理比例
50% 公理无关 >50% 的 LLM 推理步骤也是不必要的
高语义重叠 不必要比例更高（LLM 被相似信息吸引）
无无关公理 ~5-10%（少量冗余推理）

关键发现

  • 即使只添加一条同领域的无关信息，所有 LLM 的准确率都有可观下降
  • 准确率下降不能仅归因于输入变长——等长但无干扰的控制组表现显著更好
  • LLM 在正确回答的问题中也频繁使用无关信息进行推理，说明效率问题比准确率问题更普遍
  • 语义重叠越高，LLM 越倾向于使用无关信息——这暗示 LLM 的搜索过程依赖某种"语义相似性启发式"

亮点与洞察

  • 效率 vs 正确性：首次将"推理效率"从"推理正确性"中分离出来作为独立评估维度
  • 逻辑编程的桥接作用：verbalized logic program 优雅地连接了自然语言推理和形式化推理，使自动评估成为可能
  • LLM 的"语义吸引"现象：LLM 倾向于使用语义相似的信息进行推理，即使这些信息是无关的——这揭示了基于 attention 的信息检索机制的固有局限性

局限性 / 可改进方向

  • 仅限数学应用题：GSM 风格问题的逻辑结构相对简单，更复杂的推理（如多跳、反事实）未覆盖
  • 自然语言→逻辑映射的准确性：映射过程可能引入噪声
  • 未评估推理模型的最新版本（如 o3）

相关工作与启发

  • vs Shi et al. (2023) GSM-IC: 仅添加一条无关信息；本文系统化多条、可控重叠度的注入
  • vs 推理效率优化（han et al. 2025）: 它们用 token 数作为效率指标；本文用形式化的不必要推理步骤

评分

  • 新颖性: ⭐⭐⭐⭐⭐ 首个从逻辑编程角度评估 LLM 推理效率的框架
  • 实验充分度: ⭐⭐⭐⭐ 多模型 + 系统化的无关信息变体 + 效率和准确率双重评估
  • 写作质量: ⭐⭐⭐⭐⭐ 形式化定义严谨，实验设计精巧
  • 价值: ⭐⭐⭐⭐⭐ 对理解和改进 LLM 推理质量有重要学术价值