LGMT：用蜕变关系检测大模型逻辑推理的一致性漏洞

大语言模型正越来越多地充当软件系统中的推理组件，但一个能正确回答逻辑问题的模型，在同一个问题被等价改写后却可能自相矛盾。静态基准测试孤立地评估每个查询，因此无法暴露这类不一致。针对这一盲区，开源工具 LGMT 通过基于一阶逻辑的蜕变关系来检测推理不一致性，为 LLM 的可靠性评估提供了一个新的视角。

为什么静态基准不够用

传统基准测试通常给模型一组固定的逻辑题，看它答对多少。这种方法的隐含假设是：如果模型能在大量题目上给出正确答案，就说明它具备了可靠的推理能力。但现实中的推理组件面临的是连续、多变的输入——同一个前提可能以不同措辞出现，同一个结论可能被换一种方式追问。

LGMT 的作者指出，一个模型可能在某个逻辑查询上给出正确答案，却在等价改写后给出相反答案。这种自相矛盾无法被孤立评估捕捉，因为每个查询看起来都是“答对了”或“答错了”，而真正的问题在于模型对逻辑结构的理解是否稳定。换句话说，静态基准测的是单点准确率，却测不出推理的一致性。

LGMT 的核心机制：蜕变关系与一阶逻辑

LGMT 的思路来自软件测试中的蜕变测试（metamorphic testing）。它的工作流程是：给定一个前提-结论形式的源测试用例，工具会生成逻辑等价的后续用例，然后检查模型对这对用例的蕴涵预测是否一致——整个过程不需要真实标签。

具体来说，LGMT 内置了 20 种蜕变关系，这些关系建立在一阶逻辑的基础上，例如交换前提顺序、对等价命题做替换、调整量词结构等。工具还支持用户自定义蜕变关系，并通过 Z3 定理证明器验证这些关系的逻辑正确性，确保生成的等价用例在形式上是可靠的。

这种设计的巧妙之处在于绕开了标注成本：不需要人工判断模型答案的对错，只需要看模型对逻辑等价的两个问题是否给出一致的蕴涵判断。不一致本身就是值得警惕的信号。

蜕变测试（Metamorphic Testing） 是一种在不依赖预期输出的前提下检验程序正确性的软件测试方法。其基本思想是：识别输入之间应当保持的必然关系（即蜕变关系），例如“若输入 x 满足性质 P，则对其做某种变换 f 后，输出应满足可预测的变化”。在 LLM 场景中，源查询与改写查询在逻辑上等价，因此模型对两者的蕴涵判断理应一致；若不一致，就暴露了推理缺陷。这种方法特别适合缺乏基准答案或人工标注成本高昂的领域。

一阶逻辑（First-Order Logic, FOL） 是在命题逻辑基础上引入量词（∀、∃）和谓词、函数符号的形式系统，能够表达“所有对象都具有某性质”或“存在满足某条件的对象”这类结构化陈述。逻辑推理题中的前提与结论通常可形式化为 FOL 公式，而等价变换（如交换合取项、量词换序、谓词替换）也需在 FOL 语义下严格定义。LGMT 以 FOL 为基础设计蜕变关系，正是为了保证生成的后续用例与源用例在模型论意义上等价，而非仅表面相似。

Z3 定理证明器 是由微软研究院开发的高性能 SMT（可满足性模理论）求解器，支持一阶逻辑、算术、数组、位向量等多种理论。它可用于判定一组逻辑公式是否可满足，或验证两个公式是否等价（即检查其否定是否不可满足）。在 LGMT 中，Z3 被用来形式化验证用户自定义的蜕变关系：只有被证明为逻辑有效的关系，才会被用于生成等价用例，从而避免因关系设计错误而误判模型不一致。

实测数据：六款主流模型的一致性率在 20% 以上

LGMT 附带了一个包含 3,091 个蜕变组的基准，并在六款广泛使用的 LLM 上进行了测试。结果显示，不一致率范围在 20.84% 到 29.44% 之间。也就是说，在这些模型上，大约每四到五个逻辑等价的问题对中，就有一个出现了答案矛盾。

这个数字值得关注。它并不意味着模型“不会推理”，而是说明模型对逻辑结构的把握不够稳定——同样的逻辑骨架换一层表达，结论就可能翻转。对于把 LLM 当作推理组件嵌入生产系统的开发者来说，这种不稳定性会直接转化为下游决策的风险。

工具形态：CLI、Web Studio 与离线模式

LGMT 以开源形式发布在 GitHub 上，提供两种使用方式：命令行界面和 Web Studio。Web Studio 适合交互式地查看蜕变组和模型响应，CLI 则便于集成到自动化测试流程中。

一个实用的细节是离线 mock 模式——不需要 API key 就能运行，这让研究者和开发者可以在没有模型访问权限的情况下先熟悉工具流程、调试自定义蜕变关系。对于想快速评估这一方法的团队来说，降低了上手门槛。

对 LLM 可靠性评估的启示

LGMT 的价值不只在于一个测试工具，更在于它提出了一个评估维度：模型对逻辑等价变换的稳定性。随着 LLM 被越来越多地用作推理组件，单点准确率之外的这类一致性指标，很可能成为可靠性评估的常规项目。

当然，蜕变测试也有其边界——它检测的是模型在预设等价关系下的表现，等价关系本身的设计质量会影响检测覆盖面。LGMT 用 Z3 验证自定义关系，部分缓解了这个问题，但如何系统性地覆盖各类逻辑变换，仍是使用者需要思考的。

项目地址：https://github.com/MaxwelsDonc/lgmt-tool ，演示视频：https://youtu.be/gou4opptu1U 。