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

📄 arXiv: 2606.16118v1 📥 PDF

作者: Olivia Peiyu Wang, Sanna Wong-Toropainen, Daneshvar Amrollahi, Ryan Bai, Tashvi Bansal, Arush Garg, Leilani H. Gilpin

分类: cs.AI, cs.CL, cs.LO

发布日期: 2026-06-15

备注: 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

💡 一句话要点

探讨大型语言模型在法律推理中的局限性及信度问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 法律推理 形式推理 逻辑信度 SMT求解器 推理失败模式 合同分析

📋 核心要点

  1. 现有大型语言模型在法律推理中的表现虽佳，但其推理过程的忠实性仍存在疑问，尤其是在形式化推理方面。
  2. 论文通过对比不同推理方法，提出了基于LLM的形式推理，旨在提高法律推理的准确性和可靠性。
  3. 实验结果表明，尽管引入形式结构提高了准确性，但仍存在范围洗涤等问题，影响了推理的信度。

📝 摘要（中文）

大型语言模型（LLMs）在推理任务中表现出色，但其是否反映了忠实的逻辑推理或启发式近似仍不明确。本文通过比较纯LLM分类、基于LLM的形式推理和使用Z3 SMT求解器的推理，研究法律蕴涵中的这一问题。重新标注的ContractNLI子集显示，实用法律解释与严格形式蕴涵之间存在系统性差距，许多合法推理未在没有额外假设的情况下得到形式化支持。尽管引入形式结构提高了准确性，但这种提升并不意味着推理的忠实性。我们识别出三种常见的失败模式，尤其是“范围洗涤”现象，表明LLMs在未执行底层形式推理的情况下报告不一致的分类，导致看似逻辑严谨的结论实际上并非如此。这些结果揭示了基准准确性与逻辑忠实性之间的根本差距。

🔬 方法详解

问题定义：本文旨在探讨大型语言模型在法律推理中的信度问题，尤其是其推理结果是否能忠实反映逻辑推理，而现有方法在形式化推理上存在明显不足。

核心思路：通过比较纯LLM分类、基于LLM的形式推理和求解器驱动的推理，论文提出了一种新的评估框架，旨在揭示LLMs在法律推理中的潜在缺陷。

技术框架：研究采用了三种推理方法，分别是纯LLM分类、LLM形式推理和Z3 SMT求解器推理，利用重新标注的ContractNLI数据集进行评估，分析不同方法的性能和信度。

关键创新：论文的创新在于系统性地识别和分析了LLMs在法律推理中的三种失败模式，尤其是范围洗涤现象，揭示了推理结果的表面逻辑与实际逻辑之间的差距。

关键设计：在实验中，采用了多种LLM模型进行对比，设置了不同的推理任务和评估标准，特别关注了模型在执行形式推理时的表现和潜在的逻辑约束遗漏。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

实验结果显示，基于LLM的形式推理在准确性上达到了最高基准性能，但仍存在范围洗涤等问题，影响了推理的信度。具体而言，所有模型均表现出范围洗涤现象，表明其推理结果并不总是忠实于逻辑推理。

🎯 应用场景

该研究的潜在应用领域包括法律文书自动化分析、智能合约审核及法律咨询等。通过提高法律推理的准确性和可靠性，可以为法律行业提供更高效的工具，推动法律技术的发展与应用。

📄 摘要（原文）

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.