arXiv 2606.161182026-06-23cs.AIcs.CLcs.LO

了解你的局限：LLM在法律推理中作为求解器和自动形式化工具的忠实性

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

UC Santa Cruz（加州大学圣克鲁兹分校）；Univ. Helsinki（赫尔辛基大学）；CodeX, Stanford（斯坦福大学CodeX中心）；Stanford University（斯坦福大学）；Canyon Crest Academy（峡谷峰学院）；Monta Vista High School（蒙塔维斯塔高中）；Los Altos High School（洛斯阿尔托斯高中）

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

备注：: 10 pages, submitted to COLM 2026 (under review, average score of 6.25 across 4 reviewers) and accepted by the AI4Law and AI4Math workshops at ICML. This is the version where we already addressed most of the reviews from the COLM & AI4Law &; AI4Math reviewers

阅读 PDF

arXiv 页面 ↗HTML 原文 ↗

AI总结：

研究LLM在法律推理中是否忠实执行逻辑推理，发现LLM基于形式推理的高性能掩盖了范围清洗等不忠实模式，揭示基准准确性与逻辑忠实性之间的根本差距。

摘要：

大型语言模型（LLM）在推理任务上表现强劲，但这是否反映了忠实的逻辑推理还是启发式近似仍不清楚。我们在法律蕴含中通过比较三种范式——纯LLM分类、基于LLM的形式推理以及使用Z3 SMT求解器的基于求解器的形式推理——在重新标注的ContractNLI子集上对五个LLM进行了研究。我们的重新标注揭示了实用法律解释与严格形式蕴含之间存在系统性的、可测量的差距，其中相当大比例的法律上合理的推理在没有额外未声明假设的情况下缺乏形式基础。虽然引入形式结构提高了准确性，基于LLM的形式推理达到了最高的基准性能，但我们表明这种提升并不意味着忠实推理。我们识别出三种反复出现的失败模式：范围清洗（LLM报告与求解器不一致的分类而不执行底层形式推理，产生看似逻辑上合理但实际并非如此的结论）、隐式约束盲区（LLM忽略形式表示中存在的逻辑约束）以及程序合成失败（尽管有结构化提示，LLM仍生成错误的Z3代码）。关键的是，范围清洗在所有模型中持续存在，这引发了对基于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.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。