2025-11-17T10:22:13.148614

A Modal Logic for Temporal and Jurisdictional Classifier Models

Di Florio, Dong, Rotolo
Logic-based models can be used to build verification tools for machine learning classifiers employed in the legal field. ML classifiers predict the outcomes of new cases based on previous ones, thereby performing a form of case-based reasoning (CBR). In this paper, we introduce a modal logic of classifiers designed to formally capture legal CBR. We incorporate principles for resolving conflicts between precedents, by introducing into the logic the temporal dimension of cases and the hierarchy of courts within the legal system.
academic

A Modal Logic for Temporal and Jurisdictional Classifier Models

基本信息

  • 论文ID: 2510.13691
  • 标题: A Modal Logic for Temporal and Jurisdictional Classifier Models
  • 作者: Cecilia Di Florio (University of Bologna, University of Luxembourg), Huimin Dong (TU WIEN), Antonino Rotolo (University of Bologna)
  • 分类: cs.AI
  • 发表时间: 2025年10月15日 (arXiv预印本)
  • 论文链接: https://arxiv.org/abs/2510.13691

摘要

Logic-based models can be used to build verification tools for machine learning classifiers employed in the legal field. ML classifiers predict the outcomes of new cases based on previous ones, thereby performing a form of case-based reasoning (CBR). In this paper, we introduce a modal logic of classifiers designed to formally capture legal CBR. We incorporate principles for resolving conflicts between precedents, by introducing into the logic the temporal dimension of cases and the hierarchy of courts within the legal system.

研究背景与动机

问题背景

  1. 法律AI的验证需求: 机器学习分类器在法律领域的应用日益广泛，但其预测结果的规范正确性、准确性和鲁棒性无法保证，法官对此表示担忧
  2. 先例约束问题: 在普通法系统中，分类器必须满足先例约束(precedential constraint)，遵循"遵循先例"(stare decisis)原则
  3. 先例冲突: 现实法律系统中存在先例冲突，而现有的Horty模型假设案例库一致性，无法处理冲突先例

研究动机

法律案例推理本质上是一种基于案例的推理(CBR)，机器学习分类器通过历史案例预测新案例结果。然而，现有模型无法处理先例冲突，需要引入时间维度和法院层级关系来解决这一问题。

现有方法局限性

  • Horty的reason模型和result模型假设案例库一致性
  • 无法处理现实中存在的先例冲突情况
  • 缺乏时间和层级维度的形式化建模

核心贡献

  1. 扩展BCL框架: 在二元输入分类器逻辑(BCL)基础上，引入时间和层级算子，构建时间管辖分类器模型(TJCM)
  2. 形式化先例概念: 严格定义了先例、潜在约束先例和约束先例的概念
  3. 异常处理机制: 建模了两种先例异常情况——被推翻(overruled)和错误决定(per incuriam)
  4. 冲突解决原则: 形式化了基于时间-层级的先例冲突解决原则
  5. 完备性证明: 提供了TJCL逻辑系统的公理化和完备性证明

方法详解

任务定义

输入: 新的法律案例，包含事实因子、所属法院、案例名称 输出: 预测判决结果(支持原告=1，支持被告=0，未决定=?) 约束: 必须遵循先例约束和时间-层级原则

核心概念建模

1. 管辖权结构(Jurisdiction)

定义1: 管辖权 Jur = (Courts, H, B)
- Courts: 法院集合
- H ⊆ Courts × Courts: 层级关系(传递、非自反)
- B ⊆ Courts × Courts: 约束关系

2. 时间管辖分类器模型(TJCM)

定义2: TJCM = (S, f, Jur, ≤T, R)
- S ⊆ 2^Atm0: 状态集合(每个状态包含唯一法院)
- f: S → Val: 决策函数，Val = {1, 0, ?}
- ≤T: S上的全预序(时间关系)
- R ⊆ S × S: 相关性关系

3. 模态逻辑语言

定义3: L(Atm)语法
φ ::= p | t(o) | H(c,c) | B(c,c) | ¬φ | φ ∧ φ | □φ | [≤T]φ | R∀φ

先例分类体系

1. 支持先例(Supporting Precedents)

定义6: Π(s', s, o) ⟺ f(s') = o ∧ s' ∈ R(s) ∧ s' <T s

2. 潜在约束先例(Potentially Binding Precedents)

定义8: β(s', s, o) ⟺ Π(s', s, o) ∧ c'Bc
其中c' ∈ s' ∩ Courts, c ∈ s ∩ Courts

3. 异常处理机制

推翻权力(Overruling Power):

定义10: O(c', c) ⟺ H(c', c) ∨ (c' = c ∧ ¬cBc)

错误决定(Per Incuriam): 通过递归图结构Gs = (Vs, Es)计算，考虑：

  • 违反约束先例且无推翻权力
  • 与约束先例的时间-层级关系
  • 推翻链的完整性

最终约束先例:

定义21: s' ∈ β̄s ⟺ s' ∈ βs ∧ ¬(Incuriam(s) ∧ s ~= s') ∧ ¬Overruled(s')

冲突解决原则

时间-层级原则

定义23: BestTH(β̄s) = {s' ∈ β̄s | ∀s'' ∈ β̄s: s' ⊀ s'' ∧ ¬(s' ~= s'' ∧ s' <T s'')}

决策函数

定义25: f*(s) = {
    {f(s)} if s ≠ s*
    {f(s') | s' ∈ BestTH(β̄s*)} otherwise
}

实验设置

案例研究

论文使用贸易秘密案例进行说明，包含四个因子：

  • 支持原告: measure(安全措施), deceived(欺骗获取)
  • 支持被告: reverse(可逆向工程), disclosed(自愿披露)

法院层级

基于英格兰和威尔士民事法院系统：

  • c0: 英国最高法院(不受自身约束)
  • c1: 上诉法院(自我约束)
  • c2: 高等法院(自我约束)
  • c3, c4: 县法院(不发布约束性决定)

运行示例

6个历史案例(s1-s6)和1个新案例(s*)，展示完整的冲突解决过程。

实验结果

主要结果

通过运行示例验证了框架的有效性：

  1. 初始冲突识别: s1, s2, s3, s4都与s*相关但判决不同
  2. 管辖权过滤: 排除s5, s6(县法院判决，无约束力)
  3. 异常处理:
    • s1被s3推翻
    • s4被认定为per incuriam
  4. 最终决策: s3(最高法院，较新)胜过s2(上诉法院)，s*被强制判为0

理论结果

  • 完备性定理(命题3): TJCL相对于TJCM是完备的
  • 语义等价性(命题9): 语法和语义per incuriam定义等价
  • 正确性验证: 各模态算子的语义正确性得到证明

相关工作

法律CBR研究

  • Horty模型: reason模型和result模型，但假设一致性
  • CATO框架: 贸易秘密案例推理，提供因子结构
  • Liu等人: 建立了Horty模型与分类器模型的对应关系

时间和层级建模

  • Broughton: 结合垂直和水平约束，但处理方式不同
  • Wyner & Bench-Capon: 基于论证框架的司法推理
  • Ashley: 法律论证建模的开创性工作

模态逻辑应用

  • BCL框架: 二元分类器逻辑的基础
  • 混合逻辑: 名称算子的理论基础

结论与讨论

主要结论

  1. 成功扩展了BCL框架，引入时间和管辖权维度
  2. 形式化了复杂的法律先例关系和异常处理
  3. 提供了处理先例冲突的系统性方法
  4. 建立了完整的公理系统和完备性证明

局限性

  1. 相关性关系: 未对相关性关系施加特定属性约束
  2. 二元约束: 约束关系是二元的，未考虑上下文依赖性
  3. 计算复杂性: 未分析per incuriam计算的复杂性
  4. 实际应用: 缺乏大规模实际案例的验证

未来方向

  1. 考虑上下文依赖的约束关系
  2. 探索与论证框架的联系
  3. 开发具体的验证算法
  4. 扩展到其他法律体系

深度评价

优点

  1. 理论严谨性: 提供了完整的形式化框架，包括语法、语义和公理系统
  2. 实际相关性: 解决了法律AI中的实际问题——先例冲突
  3. 创新性: 首次在分类器逻辑中引入时间和管辖权维度
  4. 完备性: 提供了理论保证，确保了逻辑系统的健全性

不足

  1. 计算复杂性: 未分析per incuriam递归计算的复杂性
  2. 实证验证: 缺乏大规模实际数据的验证
  3. 相关性定义: 相关性关系的定义过于宽泛
  4. 跨法系适用性: 主要针对普通法系，对其他法系的适用性未充分讨论

影响力

  1. 理论贡献: 为法律AI提供了新的理论工具
  2. 实用价值: 可用于构建法律分类器的验证工具
  3. 跨学科意义: 连接了逻辑学、AI和法学三个领域
  4. 后续研究: 为相关领域提供了坚实的理论基础

适用场景

  1. 法律AI验证: 验证法律分类器的先例一致性
  2. 法律推理系统: 构建处理先例冲突的专家系统
  3. 法学研究: 形式化分析法律推理过程
  4. 司法决策支持: 辅助法官处理复杂的先例关系

参考文献

论文引用了25篇相关文献，主要包括：

  • Horty (2011): 先例理论的规则和理由
  • Liu et al. (2022, 2023): 分类器系统的逻辑框架
  • Ashley (1990): 法律论证建模
  • Blackburn et al. (2001): 模态逻辑理论基础
  • MacCormick & Summers (1997): 先例解释的比较研究

总体评价: 这是一篇理论性很强的优秀论文，在法律AI和逻辑学的交叉领域做出了重要贡献。虽然在实证验证方面有所不足，但其理论框架的严谨性和创新性使其具有重要的学术价值和实用潜力。