Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning

• URL: http://arxiv.org/abs/2606.16118v2
• Date: Fri, 19 Jun 2026 01:41:59 GMT
• Title: Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning
• Abstract summary: Large Language Models (LLMs) achieve strong performance on reasoning tasks, but whether this reflects faithful logical inference or approximation remains unclear.<n>We study this question by comparing three paradigms, including pure LLM classification, LLM-based Reasoning, and solver-based Formal Reasoning.<n>Our re-annotation reveals a systematic and measurable gap between pragmatic legal interpretation and strict formal entailment.
• Score: 2.1108097398435337
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) achieve strong performance on reasoning tasks, but whether this reflects faithful logical inference or heuristic approximation remains unclear. We study this question in legal entailment by comparing three paradigms, including pure LLM classification, LLM-based Formal Reasoning, and solver-based Formal Reasoning using the Z3 SMT solver, on a re-annotated subset of ContractNLI across five LLMs. Our re-annotation reveals a systematic and measurable gap between pragmatic legal interpretation and strict formal entailment, where a substantial proportion of legally sound inferences are not formally grounded without additional unstated assumptions. While introducing formal structure improves accuracy, with LLM-based Formal Reasoning achieving the highest benchmark performance, we show that this gain does not imply faithful reasoning. We identify three recurring failure modes: scope laundering, where LLMs report solver-inconsistent classifications without executing the underlying formal reasoning, producing conclusions that appear logically grounded but are not; implicit constraint blindness, where LLMs overlook logical constraints present in formal representations; and program synthesis failures, where LLMs generate incorrect Z3 code despite structured prompting. Critically, scope laundering persists across all models, raising serious concerns about the faithfulness of LLM-based formal reasoning as a proxy for symbolic execution. These results reveal a fundamental gap between benchmark accuracy and logical faithfulness.

Related papers

• CausalFlip: A Benchmark for LLM Causal Judgment Beyond Semantic Matching [50.65932158912512]
  We propose a new causal reasoning benchmark, CausalFlip, to encourage the development of new large language models.<n>CaulFlip consists of causal judgment questions built over event triples that could form different confounder, chain, and collider relations.<n>We evaluate LLMs under multiple training paradigms, including answer-only training, explicit Chain-of-Thought supervision, and a proposed internalized causal reasoning approach.
  arXiv  Detail & Related papers  (2026-02-23T18:06:15Z)
• Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
  Large Language Models (LLMs) are increasingly deployed in real-world fact-checking systems.<n>We present FactArena, a fully automated arena-style evaluation framework.<n>Our analyses reveal significant discrepancies between static claim-verification accuracy and end-to-end fact-checking competence.
  arXiv  Detail & Related papers  (2026-01-06T02:51:56Z)
• Towards Trustworthy Legal AI through LLM Agents and Formal Reasoning [11.842866992683158]
  Existing LLM-based systems excel at surface-level text analysis but lack the guarantees required for principled rationality.<n>We introduce L4M, a novel framework that combines LLM agents with SMT-solver-backed jurisprudence.<n>We show that our system surpasses advanced LLMs including GPT-o4-mini, DeepSeek-V3, and Claude 4 as well as state-of-the-art Legal AI proofs.
  arXiv  Detail & Related papers  (2025-11-26T04:05:06Z)
• HALF: Harm-Aware LLM Fairness Evaluation Aligned with Deployment [52.374772443536045]
  HALF (Harm-Aware LLM Fairness) is a framework that assesses model bias in realistic applications and weighs the outcomes by harm severity.<n>We show that HALF exposes a clear gap between previous benchmarking success and deployment readiness.
  arXiv  Detail & Related papers  (2025-10-14T07:13:26Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  Large Language Models (LLMs) have demonstrated strong generalization across a wide range of tasks.<n>Recent studies have shifted attention from explicit chain-of-thought prompting toward implicit reasoning.<n>This survey introduces a taxonomy centered on execution paradigms, shifting the focus from representational forms to computational strategies.
  arXiv  Detail & Related papers  (2025-09-02T14:16:02Z)
• CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
  We propose that guiding models to perform a systematic and comprehensive reasoning process allows models to execute much finer-grained and accurate entailment decisions.<n>We define a 3-step reasoning process, consisting of (i) claim decomposition, (ii) sub-claim attribution and entailment classification, and (iii) aggregated classification, showing that such guided reasoning indeed yields improved hallucination detection.
  arXiv  Detail & Related papers  (2025-06-05T17:02:52Z)
• Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations [13.485604499678262]
  Natural language explanations play a fundamental role in Natural Language Inference (NLI)<n>Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations.<n>This paper investigates strategies to alleviate semantic loss during autoformalisation.
  arXiv  Detail & Related papers  (2025-05-30T06:38:39Z)
• Investigating the Robustness of Deductive Reasoning with Large Language Models [10.713787991104923]
  Large Language Models (LLMs) have been shown to achieve impressive results for many reasoning-based NLP tasks.<n>It remains unclear to which extent LLMs, in both informal and autoformalisation methods, are robust on logical deduction tasks.
  arXiv  Detail & Related papers  (2025-02-04T17:16:51Z)
• RuleArena: A Benchmark for Rule-Guided Reasoning with LLMs in Real-World Scenarios [58.90106984375913]
  RuleArena is a novel and challenging benchmark designed to evaluate the ability of large language models (LLMs) to follow complex, real-world rules in reasoning.<n> Covering three practical domains -- airline baggage fees, NBA transactions, and tax regulations -- RuleArena assesses LLMs' proficiency in handling intricate natural language instructions.
  arXiv  Detail & Related papers  (2024-12-12T06:08:46Z)
• Evaluating the Correctness of Inference Patterns Used by LLMs for Judgment [53.17596274334017]
  We evaluate the correctness of the detailed inference patterns of an LLM behind its seemingly correct outputs.<n>Experiments show that even when the language generation results appear correct, a significant portion of the inference patterns used by the LLM for the legal judgment may represent misleading or irrelevant logic.
  arXiv  Detail & Related papers  (2024-10-06T08:33:39Z)
• Aligning with Logic: Measuring, Evaluating and Improving Logical Preference Consistency in Large Language Models [31.558429029429863]
  Large Language Models (LLMs) are expected to be predictable and trustworthy to support reliable decision-making systems.<n>This work examines logical preference consistency as a foundational requirement for building more dependable LLM systems.<n>We show that improving consistency leads to better performance in LLM-driven logic-based algorithms.
  arXiv  Detail & Related papers  (2024-10-03T04:34:04Z)
• Towards Logically Sound Natural Language Reasoning with Logic-Enhanced Language Model Agents [3.5083201638203154]
  Logic-Enhanced Language Model Agents (LELMA) is a framework that integrates large language models with formal logic.<n>LeLMA employs autoformalization to translate reasoning into logic representations, which are then used to assess logical validity.<n>LeLMA achieves high accuracy in error detection and improves reasoning correctness via self-refinement.
  arXiv  Detail & Related papers  (2024-08-28T18:25:35Z)
• Assessing the Reasoning Capabilities of LLMs in the context of Evidence-based Claim Verification [22.92500697622486]
  We propose a framework designed to break down any claim paired with evidence into atomic reasoning types.<n>We use this framework to create RECV, the first claim verification benchmark, incorporating real-world claims.<n>We evaluate three state-of-the-art proprietary LLMs under multiple prompt settings.
  arXiv  Detail & Related papers  (2024-02-16T14:52:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.