PaperlayerView exact revision on arXiv

Source-linked AI summary

LGMT: A Tool for Testing the Logical Reasoning Reliability of LLMs

Zenghui Zhou, Xiaoke Fang, Zheng Zheng

arXiv:2610.32627v1cs.AI

TL;DR

Static benchmarks evaluate logical queries independently and can miss contradictions across equivalent formulations. LGMT uses first-order-logic metamorphic relations to compare model predictions across equivalent cases without ground-truth labels. Across six LLMs, it reports inconsistency rates from 20.84% to 29.44%.

  • Problem

    Static reference-based benchmarks score queries independently, leaving contradictions across equivalent formulations unmeasured.

    Source: §I · p. 1

  • Method

    LGMT transforms premise-conclusion cases into logically equivalent follow-ups and checks whether three-valued entailment predictions agree, without ground-truth labels.

    Source: §I · p. 1, §II · p. 1

  • Results

    MVRs ranged from 20.84% (Claude 4.5 Sonnet) to 29.44% (DeepSeek Reasoner) across the evaluated models.

    Source: §V · p. 4

  • Takeaways & Limitations

    LGMT enables practitioners to audit LLM reasoning consistency through CLI or Web Studio reports without ground-truth labels.

    Source: §VI · p. 4

    The current engine targets FOL entailment, and realizing rewritten statements still relies on an LLM.

    Source: §VI · p. 4

Abstract

from arXiv · show

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.

I. INTRODUCTION

Static benchmarks score queries independently, so they miss contradictions across equivalent formulations. LGMT addresses this gap with an end-to-end tool for logic-grounded metamorphic testing, extensible to custom relations and bundled with a benchmark.

I. INTRODUCTION

  • Static reference-based benchmarks score queries independently and therefore miss self-contradictions across logically equivalent formulations.Such contradictions matter when LLMs derive conclusions from domain rules, policies, and constraints in software systems.Source: §I · p. 1
  • Metamorphic testing checks relations among multiple executions without ground-truth labels, exposing defects when equivalent follow-up cases receive different answers.An MR transforms a source test case into a follow-up test case.Source: §I · p. 1
  • Practical deployment requires formal-structure rewriting, selective natural-language realization, reliable paired execution across heterogeneous APIs, and case-level diagnosis of aggregate violations.Existing reasoning test generators and NLP-oriented metamorphic-testing frameworks address only isolated stages; the introduction identifies no extensible end-to-end tool among them.Source: §I · p. 1
  • LGMT provides an open-source, extensible tool for evaluating models through OpenAI-compatible endpoints and registering custom Python MRs verified for equivalence by Z3.QA teams can supply domain rules in natural language or NL+FOL pairs.Source: §I · p. 1
  • The end-to-end implementation keeps cases in paired NL and FOL forms, rewrites FOL with 20 built-in MRs, realizes changed statements, queries both cases, and reports disagreements with evidence.The CLI and Web Studio support custom MRs; an offline mock mode requires no API key.Source: §I · p. 1
  • The bundled benchmark comprises 3,091 metamorphic groups derived from FOLIO, LogicNLI, and ProVerQA, and reports results for six LLMs; the full empirical study is in companion paper.Source: §I · p. 1

II. BACKGROUND AND RELATED TOOLS

LGMT applies metamorphic testing to entailment by transforming cases into logically equivalent forms and checking whether model predictions agree. It combines FOL-based transformations with natural-language evaluation, unlike adjacent tools that address different parts of the problem.

II. BACKGROUND AND RELATED TOOLS

  • LGMT's 20 metamorphic relations rewrite three-valued entailment cases into logically equivalent forms, with matching predictions expected across each pair.The relations span formula equivalence, symbol renaming, premise restructuring, and conclusion rewriting.Source: §II · p. 1
  • Prior tools synthesize tests from fixed templates, evaluate translation-plus-solver pipelines, lack built-in FOL support, or use transformations not guaranteed to preserve semantics.The passage contrasts these approaches with LGMT's Z3-checked FOL syntax-tree rewrites and selective realization of modified statements into natural language.Source: §II · pp. 1–2
  • The workflow turns source test cases into paired queries by applying one of 20 MRs, realizing only changed statements in natural language, then querying and comparing both cases.The tool includes a 3,091-case benchmark and targets OpenAI-compatible models.Source: Figure 1 · p. 2

III. LGMT: ARCHITECTURE AND IMPLEMENTATION

LGMT separates formal logic transformations from natural-language evaluation in a staged workflow. A dual-format case passes through decoupled stages that users can run together or invoke individually.

III. LGMT: ARCHITECTURE AND IMPLEMENTATION

  • The architecture traces a test case through five stages to address the engineering tasks of the tool.The design discussion summarizes foundations from the companion study while detailing LGMT's design, extensibility, and runtime mechanisms.Source: §III · p. 2

A. Architecture and Case Representation

  • Each record is represented as a dual TestCase pairing natural-language text with FOL formulas, separating formal structure from surface phrasing.Text-only input is translated into formulas and NLTK-validated; FOL-only input is copied as text.Source: A. Architecture and Case Representation · p. 2
  • The pipeline rewrites FOL syntax trees, realizes modified formulas as text, queries the model on both cases, then checks prediction consistency and compiles an HTML report.Its stages communicate through JSONL files and can run end-to-end or as individual commands.Source: A. Architecture and Case Representation · p. 2

B. Pluggable MR Engine with Z3-Backed Checks

LGMT's MR engine rewrites formal syntax trees so untouched statements remain unchanged. Custom relations are registered only after Z3 checks their equivalence on canonical FOL samples.

B. Pluggable MR Engine with Z3-Backed Checks

  • The built-in MR Engine parses FOL formulas into syntax trees and applies tree-level rewrites, leaving untouched premises verbatim and recording altered statements.Examples include De Morgan transformations, predicate or constant renaming, premise reordering, and conclusion double negation.Source: B. Pluggable MR Engine with Z3-Backed… · p. 2
  • Custom MR registration applies a candidate relation to five canonical FOL samples and asks Z3 to confirm equivalence, rejecting it if any applicable sample fails or none applies.This check runs before any model API call.Source: B. Pluggable MR Engine with Z3-Backed… · p. 2

C. Selective Realization and Fidelity Auditing

LGMT limits semantic drift by realizing only statements modified by a metamorphic relation, then independently audits whether those translations preserve the intended formulas.

Selective Realization

  • LGMT tags only modified statements for realization, avoiding whole-case LLM retranslation that risks paraphrasing unchanged premises and introducing semantic drift.The constrained prompt forbids simplification, quantifier reordering, or extra deductions, while unchanged sentences remain verbatim.Source: C. Selective Realization and Fidelity… · pp. 2–3

Diagnostic Report

  • The violation card pairs a four-column FOL/NL diff with reasoning traces to localize where and why predictions diverge.Source: Figure 2 · p. 3

Fidelity Auditing

D. Paired Inference and Diagnostic Reporting

LGMT runs paired model queries, measures consistency and related reliability outcomes, and presents violations through a drill-down HTML report.

Paired Inference

  • The runner queries source and follow-up cases concurrently under four prompting presets, validates outputs, and supports checkpoint resumption.Malformed JSON is repaired; unparseable responses are marked invalid so they cannot skew metrics.Source: D. Paired Inference and Diagnostic… · p. 3

Analysis and Metrics

Diagnostic Reporting

E. Implementation, Packaging, and Web Studio

LGMT packages an extensible testing tool for cross-platform use, with offline workflows and built-in checks for its metamorphic relations.

Packaging and Interfaces

Offline Mock

Verification

IV. TOOL USAGE AND WORKFLOWS

LGMT supports offline demonstrations and real-model benchmarking through progressive workflows, with reports that can inform model-upgrade gates.

Workflow 1: Offline Tour

  • The CLI and Web Studio organize use into three progressive workflows, beginning with an offline tour that requires no API key or network.The demo evaluates 40 bundled groups in under 30 seconds; the full demo exercises all 3,091 groups offline.Source: §IV · p. 3

Workflow 2: Pre-Deployment Benchmarking

  • For real-model benchmarking, teams can use any OpenAI-compatible endpoint and run separate commands to query the model and generate an HTML report.Source: §IV · pp. 3–4

Validation

  • All six evaluated models exceed 20% MVR on the 3,091-group benchmark under zero-shot CoT.Source: Table I · p. 4

Workflow 2: Pre-Deployment Benchmarking

  • CI/CD jobs can use the report to gate model upgrades when MVR or HDR exceeds a chosen threshold.Source: §IV · p. 4

V. VALIDATION

LGMT was evaluated on a 3,091-group benchmark across six LLMs and four prompting strategies. The results show substantial inconsistency across models and identify structural operations where failures are most common.

V. VALIDATION

  • The evaluation covers 3,091 metamorphic groups from FOLIO (2,673), LogicNLI (93), and ProverQA (325), tested across six LLMs and four prompting strategies.Table I summarizes Zero-shot CoT results; the complete study is reported in a companion paper.Source: §V · p. 4
  • 20.84%–29.44% MVRs across evaluated models show substantial reasoning inconsistency, while consistency requirements reduce accuracy and expose HDRs missed by single-query evaluation.Accstatic ranges from 65.38%–73.53%, Acccons from 52.38%–60.97%, and HDRs from 12.56%–16.50%.Source: §V · p. 4
  • 33.78% for conclusion rewriting (MR-C) and 33.06% for symbol renaming (MR-S) are the highest aggregate MVRs, while premise restructuring (MR-P) is lowest at 16.33%.Source: §V · p. 4

VI. CONCLUSION

LGMT operationalizes logic-grounded metamorphic testing as an end-to-end workflow for auditing LLM reasoning consistency without ground-truth labels. It supports CLI and Web Studio use, while current statement realization relies on an LLM and the engine targets FOL entailment.

VI. CONCLUSION

  • LGMT combines FOL syntax-tree rewrites and Z3-verified custom MRs with selective realization, reasoning-aware inference, and drill-down HTML reports.The workflow can be run from the CLI or Web Studio without ground-truth labels.Source: §VI · p. 4
  • Statement realization still relies on an LLM, and the current engine targets FOL entailment; composed MRs and broader formalisms are proposed as next steps.Source: §VI · p. 4
  • The tool, documentation, and benchmark are publicly available on GitHub.Source: §VI · p. 4
Loading 2610.32627v1…