The Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning

root-parent1 pts0 comments

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

-->

Computer Science > Artificial Intelligence

arXiv:2606.16118 (cs)

[Submitted on 15 Jun 2026]

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

Authors:Olivia Peiyu Wang, Sanna Wong-Toropainen, Daneshvar Amrollahi, Ryan Bai, Tashvi Bansal, Arush Garg, Leilani H. Gilpin<br>View a PDF of the paper titled Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning, by Olivia Peiyu Wang and 6 other authors

View PDF<br>HTML (experimental)

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.

Comments:<br>10 pages, submitted to COLM 2026 (under review, average score of 6.25 across 4 reviewers) and accepted by the AI4Law workshop at ICML. This is the version where we already addressed most of the reviews from the COLM reviewers

Subjects:

Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Logic in Computer Science (cs.LO)

Cite as:<br>arXiv:2606.16118 [cs.AI]

(or<br>arXiv:2606.16118v1 [cs.AI] for this version)

https://doi.org/10.48550/arXiv.2606.16118

Focus to learn more

arXiv-issued DOI via DataCite (pending registration)

Submission history<br>From: Olivia Peiyu Wang [view email]<br>[v1]<br>Mon, 15 Jun 2026 02:14:49 UTC (596 KB)

Full-text links:<br>Access Paper:

View a PDF of the paper titled Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning, by Olivia Peiyu Wang and 6 other authors<br>View PDF<br>HTML (experimental)<br>TeX Source

view license

Current browse context:

cs.AI

next >

new<br>recent<br>| 2026-06

Change to browse by:

cs<br>cs.CL<br>cs.LO

References & Citations

NASA ADS<br>Google Scholar

Semantic Scholar

export BibTeX citation<br>Loading...

BibTeX formatted citation

&times;

loading...

Data provided by:

Bookmark

Bibliographic Tools

Bibliographic and Citation Tools

Bibliographic Explorer Toggle

Bibliographic Explorer (What is the Explorer?)

Connected Papers Toggle

Connected Papers (What is Connected Papers?)

Litmaps Toggle

Litmaps (What is Litmaps?)

scite.ai Toggle

scite Smart Citations (What are Smart Citations?)

Code, Data, Media

Code, Data and Media Associated with this Article

alphaXiv Toggle

alphaXiv (What is alphaXiv?)

Links to Code Toggle

CatalyzeX Code Finder for Papers (What is CatalyzeX?)

DagsHub Toggle

DagsHub (What is DagsHub?)

GotitPub Toggle

Gotit.pub (What is GotitPub?)

Huggingface Toggle

Hugging Face (What is Huggingface?)

ScienceCast Toggle

ScienceCast (What is ScienceCast?)

Demos

Demos

Replicate Toggle

Replicate (What is Replicate?)

Spaces Toggle

Hugging Face Spaces (What is Spaces?)

Spaces Toggle

TXYZ.AI (What is TXYZ.AI?)

Related Papers

Recommenders and Search Tools

Link to Influence Flower

Influence Flower (What are Influence Flowers?)

Core recommender toggle

CORE Recommender (What is CORE?)

Author

Venue

Institution

Topic

About arXivLabs

arXivLabs: experimental projects with community collaborators

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for...

toggle reasoning llms formal faithfulness legal

Related Articles