LGMT: A Tool for Testing the Logical Reasoning Reliability of LLMs
作者: Zenghui Zhou, Xiaoke Fang, Zheng Zheng
分类: cs.AI
发布日期: 2026-10-23
🔗 代码/项目: GITHUB
💡 一句话要点
提出LGMT工具以解决LLMs推理一致性检测问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 逻辑推理 大型语言模型 推理一致性 变形关系 开源工具
📋 核心要点
- 现有方法在评估LLMs推理时存在局限，无法有效检测模型在等价问题表述中的不一致性。
- LGMT工具通过生成逻辑等价的后续用例，利用变形关系检测推理一致性，提供了一种新的评估方式。
- 在对六种LLMs的实验中，LGMT揭示了20.84%到29.44%的不一致率，显示出其有效性和实用性。
📝 摘要（中文）
大型语言模型（LLMs）在现代软件系统中越来越多地作为推理组件，但当同一问题以等价形式重新表述时，模型可能会自相矛盾。现有的静态基准测试无法揭示这种不一致性。为了解决这一局限性，本文提出了LGMT，一个开源工具，通过基于一阶逻辑的变形关系检测推理不一致性。LGMT从前提-结论形式的源测试用例出发，生成逻辑等价的后续用例，并检查模型的蕴含预测是否在这对用例中一致，而无需真实标签。该工具提供20种内置变形关系，支持通过Z3定理证明器验证的自定义关系，并可通过CLI或网页工作室运行，包括无需API密钥的离线模拟模式。在对六种广泛使用的LLMs进行的3091个变形组的基准测试中，LGMT揭示的不一致率在20.84%到29.44%之间。LGMT已在GitHub上公开发布。
🔬 方法详解
问题定义：本文旨在解决大型语言模型在逻辑推理中可能出现的自相矛盾问题。现有的静态基准测试方法无法有效揭示模型在不同表述下的推理一致性，导致潜在的逻辑错误未被发现。
核心思路：LGMT工具的核心思路是通过生成逻辑等价的后续测试用例，利用变形关系来检测模型的推理一致性。这种设计使得模型在不同表述下的推理结果可以进行比较，从而揭示潜在的不一致性。
技术框架：LGMT的整体架构包括源测试用例生成、逻辑等价性验证和推理一致性检查三个主要模块。用户提供前提-结论形式的测试用例，工具自动生成后续用例并进行一致性检测。
关键创新：LGMT的主要创新在于引入了20种内置的变形关系，并支持用户自定义关系的验证。这种方法与传统的静态基准测试方法本质上不同，因为它能够动态生成测试用例并进行一致性检查。
关键设计：LGMT使用Z3定理证明器来验证自定义变形关系的有效性，确保生成的后续用例在逻辑上是等价的。此外，工具提供CLI和网页工作室两种运行方式，方便用户使用。
🖼️ 关键图片
📊 实验亮点
在对六种广泛使用的LLMs进行的实验中，LGMT揭示的不一致率在20.84%到29.44%之间，显示出其在检测推理一致性方面的有效性。这一结果表明，LGMT能够有效识别模型在逻辑推理中的潜在问题，为模型的改进提供了重要依据。
🎯 应用场景
LGMT工具的潜在应用领域包括自然语言处理、智能问答系统和自动推理等。通过检测LLMs的推理一致性，开发者可以提高模型的可靠性和准确性，从而在实际应用中减少逻辑错误的发生，提升用户体验。未来，该工具还可以扩展到其他类型的模型和推理任务中。
📄 摘要（原文）
Large Language Models (LLMs) increasingly serve as reasoning components in modern software systems, yet a model that answers a logical query correctly can contradict itself when the same problem is restated in an equivalent form. Static benchmarks evaluate queries in isolation and therefore fail to expose such inconsistencies. To address this limitation, we present LGMT, an open-source tool that detects reasoning inconsistencies through metamorphic relations grounded in first-order logic. Given a source test case in premise-conclusion form, LGMT generates logically equivalent follow-up cases and checks whether the model's entailment predictions agree across the pair, without ground-truth labels. The tool provides 20 built-in metamorphic relations, supports custom ones verified by the Z3 theorem prover, and runs from a CLI or a web studio, including an offline mock mode requiring no API key. Across six widely used LLMs on a bundled benchmark of 3,091 metamorphic groups, LGMT reveals inconsistency rates ranging from 20.84% to 29.44%. LGMT is publicly available on GitHub at https://github.com/MaxwelsDonc/lgmt-tool, with a demonstration video at https://youtu.be/gou4opptu1U.