LGMT: Detecting Consistency Gaps in LLM Logical Reasoning with Metamorphic Relations

Large language models are increasingly used as reasoning components in software systems, but a model that answers a logic question correctly may contradict itself when the same question is paraphrased into an equivalent form. Static benchmarks evaluate each query in isolation and therefore cannot expose this kind of inconsistency. To address this blind spot, the open-source tool LGMT detects reasoning inconsistencies through metamorphic relations grounded in first-order logic, offering a new angle on evaluating LLM reliability.

Why static benchmarks fall short

Traditional benchmarks typically give a model a fixed set of logic problems and measure how many it answers correctly. The implicit assumption is that if a model can produce correct answers across a large number of problems, it has reliable reasoning ability. But reasoning components in the real world face continuous, varied input—the same premise may appear in different wording, and the same conclusion may be probed in a different way.

The authors of LGMT point out that a model may give the correct answer to a given logical query yet give the opposite answer after an equivalent rewrite. This self-contradiction cannot be captured by isolated evaluation, because each query looks either "right" or "wrong," while the real question is whether the model's understanding of logical structure is stable. In other words, static benchmarks measure single-point accuracy but cannot measure reasoning consistency.

LGMT's core mechanism: metamorphic relations and first-order logic

LGMT's approach comes from metamorphic testing in software testing. Its workflow is: given a source test case in premise-conclusion form, the tool generates logically equivalent follow-up cases, then checks whether the model's entailment predictions for the pair are consistent—all without requiring ground-truth labels.

Specifically, LGMT ships with 20 built-in metamorphic relations grounded in first-order logic, such as swapping the order of premises, substituting equivalent propositions, and adjusting quantifier structure. The tool also supports user-defined metamorphic relations and verifies their logical correctness with the Z3 theorem prover, ensuring that the generated equivalent cases are formally sound.

The cleverness of this design is that it sidesteps annotation costs: there is no need to manually judge whether the model's answer is right or wrong—you only need to see whether the model gives consistent entailment judgments for two logically equivalent questions. Inconsistency itself is a warning signal worth heeding.

Metamorphic Testing is a software testing method for checking program correctness without relying on expected outputs. The basic idea is to identify necessary relationships that should hold between inputs (i.e., metamorphic relations)—for example, "if input x satisfies property P, then after applying some transformation f to it, the output should satisfy a predictable change." In the LLM setting, the source query and the rewritten query are logically equivalent, so the model's entailment judgments for the two should be consistent; if they are not, a reasoning defect is exposed. This method is particularly well suited to domains that lack benchmark answers or where manual annotation is expensive.

First-Order Logic (FOL) is a formal system that introduces quantifiers (∀, ∃) and predicate and function symbols on top of propositional logic, capable of expressing structured statements such as "all objects have a certain property" or "there exists an object satisfying a certain condition." The premises and conclusions in logic reasoning problems can usually be formalized as FOL formulas, and equivalence transformations (such as swapping conjuncts, reordering quantifiers, and substituting predicates) must also be strictly defined under FOL semantics. LGMT designs its metamorphic relations on an FOL basis precisely to ensure that the generated follow-up cases are equivalent to the source case in the model-theoretic sense, rather than merely superficially similar.

The Z3 theorem prover is a high-performance SMT (Satisfiability Modulo Theories) solver developed by Microsoft Research, supporting first-order logic, arithmetic, arrays, bit-vectors, and many other theories. It can be used to determine whether a set of logical formulas is satisfiable, or to verify whether two formulas are equivalent (i.e., check whether their negation is unsatisfiable). In LGMT, Z3 is used to formally verify user-defined metamorphic relations: only relations proven to be logically valid are used to generate equivalent cases, thereby avoiding false positives of model inconsistency caused by flawed relation design.

Empirical data: consistency rates above 20% across six mainstream models

LGMT comes with a benchmark containing 3,091 metamorphic groups and was tested on six widely used LLMs. The results show inconsistency rates ranging from 20.84% to 29.44%. In other words, on these models, roughly one in every four to five logically equivalent question pairs produced a contradictory answer.

This number is worth noting. It does not mean the models "cannot reason"; rather, it shows that their grasp of logical structure is not stable enough—change the surface expression of the same logical skeleton and the conclusion may flip. For developers embedding LLMs as reasoning components in production systems, this instability translates directly into risk in downstream decisions.

Tool form: CLI, Web Studio, and offline mode

LGMT is released as open source on GitHub and offers two ways to use it: a command-line interface and Web Studio. Web Studio is suited to interactively viewing metamorphic groups and model responses, while the CLI is convenient for integration into automated testing pipelines.

One practical detail is the offline mock mode—it runs without an API key, letting researchers and developers familiarize themselves with the tool's workflow and debug custom metamorphic relations without model access. For teams wanting to quickly evaluate this approach, it lowers the barrier to entry.

Implications for LLM reliability evaluation

LGMT's value lies not only in being a testing tool but also in proposing an evaluation dimension: a model's stability under logically equivalent transformations. As LLMs are increasingly used as reasoning components, consistency metrics like this—beyond single-point accuracy—are likely to become a standard item in reliability evaluation.

Of course, metamorphic testing has its limits—it detects how a model performs under preset equivalence relations, and the design quality of those relations affects detection coverage. LGMT partially mitigates this by using Z3 to verify custom relations, but how to systematically cover various kinds of logical transformations remains a question users need to consider.

Project URL: https://github.com/MaxwelsDonc/lgmt-tool , demo video: https://youtu.be/gou4opptu1U .

One-line Summary

Open-source tool LGMT uses metamorphic relations to detect LLM reasoning inconsistencies, with inconsistency rates above 20% across six models.

Paragraph Summary

LGMT is an open-source tool designed to address the problem that static benchmarks cannot capture reasoning inconsistencies in large language models. Traditional benchmarks evaluate each query in isolation and look only at single-point accuracy, but a model may give opposite answers to logically equivalent questions. Drawing on metamorphic testing from software testing, LGMT builds in 20 metamorphic relations based on first-order logic (such as swapping premise order and adjusting quantifiers), generates logically equivalent follow-up cases for a source case, and checks the consistency of the model's entailment judgments without requiring ground-truth labels. The tool supports verifying custom relations with Z3 and provides a benchmark containing 3,091 metamorphic groups. Testing on six mainstream LLMs shows inconsistency rates between 20.84% and 29.44%. LGMT is released in two forms, CLI and Web Studio, and supports an offline mock mode, lowering the barrier to use.