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

arXiv: https://arxiv.org/abs/2606.16118 · HTML: https://mlsanity.com/paper/2606.16118/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 27 of its 46 references that are in the map.
- First posted on arXiv 15 Jun 2026.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)

## Builds on (most cited first, 27 of 27)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Qwen2 Technical Report](https://mlsanity.com/paper/2407.10671/) (2024)
- [gpt-oss-120b & gpt-oss-20b Model Card](https://mlsanity.com/paper/2508.10925/) (2025)
- [Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting](https://mlsanity.com/paper/2305.04388/) (2023)
- [DeepSeek-V3.2: Pushing the Frontier of Open Large Language Models](https://mlsanity.com/paper/2512.02556/) (2025)
- [Reasoning Models Don't Always Say What They Think](https://mlsanity.com/paper/2505.05410/) (2025)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [Large Legal Fictions: Profiling Legal Hallucinations in Large Language Models](https://mlsanity.com/paper/2401.01301/) (2024)
- [ContractNLI: A Dataset for Document-level Natural Language Inference for Contracts](https://mlsanity.com/paper/2110.01799/) (2021)
- [Faithful Reasoning Using Large Language Models](https://mlsanity.com/paper/2208.14271/) (2022)
- [Faithful Logical Reasoning via Symbolic Chain-of-Thought](https://mlsanity.com/paper/2405.18357/) (2024)
- [A Dataset for Statutory Reasoning in Tax Law Entailment and Question Answering](https://mlsanity.com/paper/2005.05257/) (2020)
- [Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation](https://mlsanity.com/paper/2305.15541/) (2023)
- [Towards Robust Legal Reasoning: Harnessing Logical LLMs in Law](https://mlsanity.com/paper/2502.17638/) (2025)
- [Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning](https://mlsanity.com/paper/2410.08047/) (2024)
- [Catala: A Programming Language for the Law](https://mlsanity.com/paper/2103.03198/) (2021)
- [Factoring Statutory Reasoning as Language Understanding Challenges](https://mlsanity.com/paper/2105.07903/) (2021)
- [Can ChatGPT Perform Reasoning Using the IRAC Method in Analyzing Legal Scenarios Like a Lawyer?](https://mlsanity.com/paper/2310.14880/) (2023)
- [VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning](https://mlsanity.com/paper/2601.20055/) (2026)
- [Faithful Autoformalization via Roundtrip Verification and Repair](https://mlsanity.com/paper/2604.25031/) (2026)
- [Leveraging LLMs for Hypothetical Deduction in Logical Inference: A Neuro-Symbolic Approach](https://mlsanity.com/paper/2410.21779/) (2024)
- [ProSLM : A Prolog Synergized Language Model for explainable Domain Specific Knowledge Based Question Answering](https://mlsanity.com/paper/2409.11589/) (2024)
- [Language Models and Logic Programs for Trustworthy Tax Reasoning](https://mlsanity.com/paper/2508.21051/) (2025)
- [Neuro-Symbolic Compliance: Integrating LLMs and SMT Solvers for Automated Financial Legal Analysis](https://mlsanity.com/paper/2601.06181/) (2026)
- [Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)](https://mlsanity.com/paper/2509.20421/) (2025)

## Built on by (most cited first, 3 of 3)

- [Time as Structure: Temporal Dependency Graphs for Verifiable Deadline Computation over Legal Documents](https://mlsanity.com/paper/2608.15270/) (2026)
- [SoK: Formal Methods for Fact-Checking and Information Integrity](https://mlsanity.com/paper/2609.23239/) (2026)
- [Cited but Not Consulted: A Counterfactual Audit of Legal Chain-of-Thought Faithfulness](https://mlsanity.com/paper/2610.12361/) (2026)

## Abstract (arXiv)

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.