连接法律解释与形式逻辑：忠实性、假设与人工智能法律推理的未来

# 弥合法学解释与形式逻辑：忠实性、假设与AI法律推理的未来
来源：https://arxiv.org/html/2605.14049
Leilani H. Gilpin 加州大学圣克鲁兹分校 [email protected]

###### 摘要

大型语言模型在法律实践中的日益普及既带来了巨大希望，也带来了严重风险。法律专业人士有望从能够大规模推理合同、起草文档和分析来源的AI中受益，但法律工作的高风险性要求当前AI系统无法提供的严谨程度。核心问题不仅仅是LLM会虚构事实和引用；而是它们系统性地得出超出原文实际支持的推论，将充满假设的结论呈现为基于逻辑的结果。本提案提出了一种神经符号方法，将大型语言模型的表达能力与形式验证的严谨性相结合，旨在使AI辅助的法律推理既具备能力又值得信赖，从而在不牺牲法律实践所要求的问责性的前提下，减轻人工验证的负担。

弥合法学解释与形式逻辑：忠实性、假设与AI法律推理的未来

Olivia Peiyu Wang 加州大学圣克鲁兹分校 [email protected]
Leilani H. Gilpin 加州大学圣克鲁兹分校 [email protected]

## 1 问题陈述：两种正确性

法律专业人士和AI研究者都追求在法律文本上进行可信、可验证的推理，但通过根本不同的框架来实现。法律解释依赖于背景知识和语境推理，而形式逻辑要求所有推论都明确基于文本。

这些框架不是不同严谨程度的问题，而是不同的推理模式。一个法律上合理的结论可能在形式上是无效的，因为该规范在合同中无处体现。这种差距在法律AI研究中很大程度上是隐形的，因为大多数系统要么通过语言模型训练模仿法律解释，要么通过符号方法强制形式有效性，而没有承认两者经常出现分歧。我们认为，将这种差距显式化、可衡量化、可处理化，是法律AI中最重要的开放问题之一。

## 2 研究贡献：衡量差距

### 数据集与重新标注。

我们使用ContractNLI（Koreeda and Manning, 2021 (https://arxiv.org/html/2605.14049#bib.bib1)）来研究这一差距，它是少数基于真实合同语言的基准之一。其原始标注由受过法律训练的标注者完成，主要反映法律解释。我们不对此提出异议。我们在严格的形式定义下重新标注相同的示例——假设HH被前提PP蕴含，当且仅当P∧¬HP\\wedge\\neg H是不可满足的；矛盾当且仅当P∧HP\\wedge H不可满足；否则为中立。

结果令人震惊——标签发生了大量转移，主要是从“蕴含”转向“中立”。这些不是错误。有些情况下，原始结论依赖于背景法律知识或上下文假设，律师合理引用这些知识或假设，但文本中并未出现。这种主要的蕴含→\\to中立转变揭示了实用法律解释与严格形式蕴含之间的系统性差距。我们进一步构建了最小对数——对于每个分歧案例，通过显式提供缺失的假设，构造出一个在形式上被蕴含的最小修改后的假设。这种方法将一个模糊的差距转变为一个可处理、可分析的对象。

### 实验发现。

我们在五个LLM（GPT（Agarwal et al., 2025 (https://arxiv.org/html/2605.14049#bib.bib13)）、Claude（Anthropic, 2026 (https://arxiv.org/html/2605.14049#bib.bib14)）、LLaMA（AI@Meta, 2024 (https://arxiv.org/html/2605.14049#bib.bib15)）、DeepSeek（Liu et al., 2025 (https://arxiv.org/html/2605.14049#bib.bib16)）、Qwen（Yang et al., 2024 (https://arxiv.org/html/2605.14049#bib.bib17)））上评估了三种范式：纯LLM分类、基于形式逻辑表示的LLM推理、以及结合LLM形式化与SMT求解器（de Moura and Bjørner, 2008 (https://arxiv.org/html/2605.14049#bib.bib12)）的神经符号管道。形式结构提高了准确性，但准确性并不意味着忠实推理。高性能模型通过模仿法律解释（包括其隐含假设）而非形式推理来取得成功。SMT管道更为保守，在缺乏显式基础时返回中立分类，从而揭示差距而非掩盖它。

我们识别出三种反复出现的失败模式：

- **假设注入**：推理通过未陈述的推论悄然弥合差距。
- **范围洗白**：推理将非正式结论呈现为形式上有依据的。
- **隐式约束盲点**：推理忽略了形式表示中存在的约束。

所有模型中的主要错误是中立→\\to蕴含的错误分类，反映了系统的假设注入。蕴含↔\\leftrightarrow矛盾的混淆很少见，这表明挑战在于基础不足，而非逻辑不一致。

### 最小公理框架。

此外，“中立”分类不一定非得是死胡同。系统不是在得到中立分类后停止，而是计算**最小附加公理集**，使其足以将分类转变为“蕴含”或“矛盾”，并将其呈现给法律审查者，附带一个针对性问题——标准合同法或合同语境是否隐含地确立了这一假设？律师回答“是”则验证了形式逻辑无法单独捕捉的隐含规范；律师回答“否”则确认该案例确实存在规定不足。在这两种情况下，法律专业知识恰恰被应用于形式方法所限之处。最小公理集的复杂性也具有诊断意义：复杂或大量的公理意味着真正的解释困难，而少量简单的公理则表明可以自信地进行自动分类。

## 3 研究议程：弥合差距

法律解释-形式逻辑差距并非合同蕴含所独有。只要AI系统引用来源来支持法律主张，就会出现这种差距，这在LLM辅助的起草、监管分析和诉讼支持中越来越常见（Magesh et al., 2025 (https://arxiv.org/html/2605.14049#bib.bib26)；Freifeld and Scarcella, 2026 (https://arxiv.org/html/2605.14049#bib.bib25)）。先前的工作处理**虚构引用**，即不存在的参考文献，这个问题现在通过检索验证已基本可处理（Agrawal et al., 2024 (https://arxiv.org/html/2605.14049#bib.bib10)；cohan2019scicite）。更困难且影响更大的问题是**立场歪曲**——来源存在且被正确检索，但主张夸大、弱化或歪曲了来源所说的内容（United States Court of Appeals for the Sixth Circuit, 2026 (https://arxiv.org/html/2605.14049#bib.bib18)）。一个被训练成像律师一样推理的模型会常规性地从引用的来源中推断出比严格支持更多的内容，因为这就是法律解释所做的。在法律和医疗领域，50%到80%的LLM回答并未得到其引用来源的完全支持（Agrawal et al., 2024 (https://arxiv.org/html/2605.14049#bib.bib10)），但尚无形式化的检测框架来应对这种失败模式。

我们提出两项贡献来应对这一问题：

- **基准数据集**：基准数据集应包括LLM生成的法律和学术文本，在声明层面注释立场歪曲，使用我们研究贡献中的三分类框架和最小对数方法。
- **求解器参与训练**：不使用LLM判断或人类偏好作为反馈，我们将使用形式验证工具作为奖励信号，教导模型区分形式上可支持的推论和充满假设的推论。当求解器标记出基础不足的声明时，它还会计算支撑该声明所需的最小公理，直接输入到针对性的人工审查中，正好在法律解释与形式基础出现分歧的点上。

### 愿景。

长期目标是实现AI法律推理，使其在两个框架中都能透明运行。它应能在适当时进行法律解释，在需要时进行形式基础化，并能揭示连接两者的最小假设，以供针对性法律审查（Hildebrandt, 2018 (https://arxiv.org/html/2605.14049#bib.bib5)；Francesconi and Governatori, 2023 (https://arxiv.org/html/2605.14049#bib.bib9)）。我们认为，理解当前法律AI系统在何处以及为何失效，并非这一议程的限制，而是其基础。只有诚实地刻画失败模式，我们才能确定在何处可以负责任地应用AI辅助，并构建能够主动揭示解释不确定性、而非在事后要求律师验证结论的系统（Dixon Jr, 2025 (https://arxiv.org/html/2605.14049#bib.bib11)）。

## 参考文献

- S. Agarwal, L. Ahmad, J. Ai, S. Altman, A. Applebaum, E. Arbus, R. K. Arora, Y. Bai, B. Baker, H. Bao, et al. (2025). Gpt-oss-120b & gpt-oss-20b model card. *arXiv preprint arXiv:2508.10925*. 引用：§2 (https://arxiv.org/html/2605.14049#S2.SS0.SSS0.Px2.p1.1).
- A. Agrawal, M. Suzgun, L. Mackey, and A. Kalai (2024). Do language models know when they’re hallucinating references?. In *Findings of the Association for Computational Linguistics: EACL 2024*, pp. 912–928. 引用：§3 (https://arxiv.org/html/2605.14049#S3.p1.1).
- AI@Meta (2024). Llama 3 model card. 外部链接：Link (https://github.com/meta-llama/llama3/blob/main/MODEL_CARD.md) 引用：§2 (https://arxiv.org/html/2605.14049#S2.SS0.SSS0.Px2.p1.1).
- Anthropic (2026). Introducing claude sonnet 4.6. Note: Accessed: 2026 外部链接：Link (https://www.anthropic.com/news/claude-sonnet-4-6) 引用：§2 (https://arxiv.org/html/2605.14049#S2.SS0.SSS0.Px2.p1.1).
- L. M. de Moura and N. S. Bjørner (2008). Proofs and refutations, and z3.. In *LPAR Workshops*, Vol. 418, pp. 123–132. 引用：§2 (https://arxiv.org/html/2605.14049#S2.SS0.SSS0.Px2.p1.1).
- J. H. B. Dixon Jr (2025). Guidelines for judicial officers: responsible use of artificial intelligence. *The Judges’ Journal* 64(2), pp. 36–38. 引用：§3 (https://arxiv.org/html/2605.14049#S3.SS0.SSS0.Px1.p1.1).
- E. Francesconi and G. Governatori (2023). Patterns for legal compliance checking in a decidable framework of linked open data: e. francesconi, g. governatori. *Artificial Intelligence and Law* 31(3), pp. 445–464. 引用：§3 (https://arxiv.org/html/2605.14049#S3.SS0.SSS0.Px1.p1.1).
- K. Freifeld and M. Scarcella (2026). Sullivan & cromwell law firm apologizes for AI hallucinations in court filing. *Reuters*. Note: https://www.reuters.com/legal/litigation/sullivan-cromwell-law-firm-apologizes-ai-hallucinations-court-filing-2026-04-21/ Reuters. Accessed: 2026-04-29 引用：§3 (https://arxiv.org/html/2605.14049#S3.p1.1).
- M. Hildebrandt (2018). Law as computation in the era of artificial legal intelligence: speaking law to the power of statistics. *University of Toronto Law Journal* 68(supplement 1), pp. 12–35. 引用：§3 (https://arxiv.org/html/2605.14049#S3.SS0.SSS0.Px1.p1.1).
- Y. Koreeda and C. D. Manning (2021). ContractNLI: a dataset for document-level natural language inference for contracts. In *Findings of the Association for Computational Linguistics: EMNLP 2021*, pp. 1907–1919. 引用：§2 (https://arxiv.org/html/2605.14049#S2.SS0.SSS0.Px1.p1.4).
- A. Liu, A. Mei, B. Lin, B. Xue, B. Wang, B. Xu, B. Wu, B. Zhang, C. Lin, C. Dong, et al. (2025). Deepseek-v3. 2: pushing the frontier of open large language models. *arXiv preprint arXiv:2512.02556*. 引用：§2 (https://arxiv.org/html/2605.14049#S2.SS0.SSS0.Px2.p1.1).
- V. Magesh, F. Surani, M. Dahl, M. Suzgun, C. D. Manning, and D. E. Ho (2025). Hallucination-free? assessing the reliability of leading ai legal research tools. *Journal of empirical legal studies* 22(2), pp. 216–242. 引用：§3 (https://arxiv.org/html/2605.14049#S3.p1.1).
- United States Court of Appeals for the Sixth Circuit (2026). United states v. john farris, no. 25-5623 (6th cir. 2026). Note: https://law.justia.com/cases/federal/appellate-courts/ca6/25-5623/25-5623-2026-04-03.html Decided April 3, 2026 引用：§3 (https://arxiv.org/html/2605.14049#S3.p1.1).
- A. Yang, B. Yang, B. Hui, B. Zheng, B. Yu, C. Zhou, C. Li, C. Li, D. Liu, F. Huang, et al. (2024). Qwen2 technical report. *arXiv preprint arXiv:2407.10671*. 引用：§2 (https://arxiv.org/html/2605.14049#S2.SS0.SSS0.Px2.p1.1).