技术摘要：通过相关性敏感评估与求解器 grounded 推理迈向可信法律人工智能

1. 问题陈述

法律推理从根本上要求区分具有法律实质意义的变化与无关变化。在法治体系中，司法裁决必须满足形式理性：结论应由明确、普遍且逻辑连贯的规则加以证成，这些规则可追溯至 governing statutes（管辖法规）。然而，当前应用于法律任务（如问答、意见摘要、律师资格考试推理）的大语言模型（LLM）在此区分上存在关键缺陷。它们通常：

• 在无关扰动下不稳定：其决策会因法律无关属性（如人口统计特征、风格化改写、程序背景）或对抗性框架而改变。
• 对实质变化不敏感：当法定要素、心理状态或适用例外发生改变时，它们未能更新预测。
• 易受混淆：它们难以区分表面事实相似但适用条件不同的相似法规。

现有评估往往孤立地研究这些现象（例如，分别评估公平性或鲁棒性）。目前缺乏一个统一的框架，用于评估模型是否在“不应改变”的扰动下保持不变性，同时在“应改变”的扰动下正确更新。

2. 方法论

本文提出了一种双管齐下的方法：一个新的评估框架和一种新颖的推理架构。

2.1 法律相关性敏感评估

作者将可信法律推理 formulate 为法律相关性敏感评估问题。该框架将司法公平性、鲁棒性、对抗性框架和法规混淆评估统一为一个单一套件。

• 扰动分类学：评估将扰动分为两类：
  1. 标签保持（不应改变）：改变法律无关信息（如人口统计属性、释义、无关专家意见、虚构的法律权威）但保留实质事实的扰动。可信模型必须满足 $f(x) = f(\tau(x))$。
  2. 标签改变（应改变）：修改法律实质条件（如行为、心理状态、危害严重程度、法定例外）的扰动。可信模型必须满足 $f(\tau(x)) = y_{\tau}$，其中 $y_{\tau}$ 是新的法律正确标签。
• 指标：该框架测量不变性（在无关变化下的稳定性）、变化对齐（在实质变化下的正确更新）、偏差幅度和法规正确性。

2.2 LexGuard：基于求解器的对抗性多智能体框架

为解决标准 LLM 的缺陷，作者引入了LexGuard，这是一个利用形式推理将法律提议与法律核查分离的框架。

• 法律形式化：法规和司法解释被自动形式化为一个由可执行约束组成的形式法律知识库（$K$）。每条规则表示为条件约束：$ARTICLEGUARD \land CLAUSEGUARD \Rightarrow PENALTY$。这些守卫（guards）检查主体、客体、行为、意图、危害、因果关系和例外。
• 对抗性智能体：两个角色区分的 LLM 智能体（检察官和辩护律师）从同一案件叙述中独立提取结构化的事实 - 法规论证元组。
  • 检察官专注于支持责任的事实。
  • 辩护律师专注于缺失的要素、例外和替代解释。
  • 智能体在相似性簇内辩论易混淆条款，以细化候选法规。
• 以求解器为中心的裁决：
  1. 系统在 $K$ 中搜索与提议法规相对应的约束。
  2. 提取的事实被细化并与所需的法律要素进行匹配。
  3. 细化后的事实和约束被编码为 SMT（模理论可满足性）公式（$\Phi$）。
  4. SMT 求解器（Z3）检查条款守卫、子句守卫和例外守卫的可满足性。
  5. 冲突解决：如果求解器发现矛盾（例如，冲突的事实或不兼容的守卫），它将返回一个识别冲突的"unsat core"（不可满足核心），触发事实重新 grounded 或约束修复。
  6. 最终判决仅由求解器验证的法律适用性生成，过滤掉无关事实和幻觉法规。

3. 主要贡献

1. 评估框架：将可信法律推理 formulate 为法律相关性敏感问题，并通过统一的“应改变”和“不应改变”扰动套件实例化，涵盖公平性、鲁棒性、对抗性攻击和法规混淆。
2. LexGuard 架构：一个基于求解器的对抗性多智能体框架，将法规形式化为可执行约束，利用对抗性智能体提取竞争性论证，并采用 SMT 求解器验证逻辑一致性和法规满足性。
3. 实证验证：综合实验表明，现有法律 LLM 系统性地对无关变化敏感，且无法区分相关法律要素，而 LexGuard 显著提高了可靠性、公平性和鲁棒性。

4. 实验结果

作者在公共法律数据集（LeCaRDv2, LEEC）及其自定义扰动套件上评估了 LexGuard。

• 标准预测性能：LexGuard 在 LeCaRDv2 和 LEEC 上实现了通用和特定条款预测的最佳 F1 分数。增益主要由更高的精确度驱动，表明求解器有效地抑制了无关法规预测。
• 量刑准确性：LexGuard 在量刑预测中实现了最低的均方根误差（RMSE），无论是否使用“黄金”（真实）法规，同时保持了高法律有效性（经求解器验证）。
• 相关性敏感性（RQ3 & RQ4）：
  • 应改变：LexGuard 在法定要素被修改时表现出更优的预测更新能力，在“变化对齐”方面优于基线。
  • 不应改变：LexGuard 展现出对抗性框架（如虚构权威、角色劫持）和良性改写的强鲁棒性，在基线失效的情况下保持了高不变性和攻击感知 F1 分数。
• 法规混淆（RQ5）：在涉及易混淆法规簇的任务中（如盗窃与诈骗），LexGuard 实现了显著更高的“正例精确度”（88.71% 对比基线的 58.57%），以及更低的遗漏率和错误相似法规选择率。
• 消融研究：移除 Z3 推理器导致性能最大程度的下降，凸显了符号一致性检查的必要性。移除对抗性辩论模块也显著降低了准确性，证实了易混淆条款间细粒度竞争的价值。

5. 意义与主张

本文主张，法律可信度不仅需要准确性，还需要对法律实质变化的校准敏感性。

• 超越准确性：如果模型在无关扰动下不稳定或对实质变化不敏感，仅凭高准确性不足以支撑法律人工智能。可信度由区分相关变化与无关变化的能力定义。
• 可审计推理：通过将决策 grounded 于形式约束和 SMT 验证，LexGuard 生成可针对明确法规规则进行审计的符号化证成，解决了标准 LLM 的“黑箱”性质。
• 鲁棒性机制：结果表明，对对抗性攻击和无关扰动的鲁棒性不能仅通过提示工程（如思维链或少样本提示）实现，而需要通过形式求解器实现提议与验证的结构化分离。

承认的局限性：
作者指出，该框架的形式化质量取决于用于生成初始事实和规则的 LLM 的准确性。当前系统仅限于法规规则，尚未完全涵盖判例法、开放纹理规范或不断演变的法理。此外，多阶段过程引入了适度的计算开销，但每个案例的成本仍保持在实际可承受范围内。