现代语言模型（LMs）展现出了强大的演绎推理（deductive reasoning）能力，然而标准化评估往往只关注推理结果的正确性，而忽视了类人推理中的一个关键方面——效率。 在真实世界的推理场景中，绝大部分可用信息都是无关的，而高效的演绎推理需要能够识别并忽略这些干扰信息。 我们提出了一个基于逻辑编程（logic programming）视角的框架，用于评估语言模型的推理效率。该框架引入了一种简洁的方法，用于将语言模型生成的自然语言证明（natural language proofs）与通过执行逻辑程序所得的最短证明（shortest proofs）进行对齐。模型的效率通过衡量其在推理过程中避免不必要推理步骤的能力来量化。 在实证研究中，我们构建了一个数学文字题（math word problems）数据集，并在其中注入不同数量、不同语义重叠程度的无关公理（irrelevant axioms）。结果表明，当前的语言模型在此类条件下的推理准确率显著下降——即使这些干扰最小且与领域语义一致——并且其生成的证明中经常出现绕行于无关推理的冗余步骤。