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

시간 및 관할권 분류기 모델을 위한 양상 논리

기본 정보

  • 논문 ID: 2510.13691
  • 제목: A Modal Logic for Temporal and Jurisdictional Classifier Models
  • 저자: Cecilia Di Florio (볼로냐 대학교, 룩셈부르크 공과대학교), Huimin Dong (TU WIEN), Antonino Rotolo (볼로냐 대학교)
  • 분류: cs.AI
  • 발표 시간: 2025년 10월 15일 (arXiv 프리프린트)
  • 논문 링크: https://arxiv.org/abs/2510.13691

초록

논리 기반 모델은 법률 분야에 적용되는 기계학습 분류기의 검증 도구를 구축하는 데 사용될 수 있습니다. ML 분류기는 이전 사건들을 기반으로 새로운 사건의 결과를 예측하며, 이는 사건 기반 추론(CBR)의 한 형태를 수행합니다. 본 논문에서는 법률 CBR을 형식적으로 포착하도록 설계된 분류기의 양상 논리를 소개합니다. 우리는 선례 간의 충돌을 해결하기 위한 원칙을 통합하며, 사건의 시간 차원과 법률 체계 내 법원의 계층 구조를 논리에 도입합니다.

연구 배경 및 동기

문제 배경

  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 등 (2022, 2023): 분류기 체계의 논리 프레임워크
  • Ashley (1990): 법률 논증 모델링
  • Blackburn 등 (2001): 양상 논리 이론 기초
  • MacCormick & Summers (1997): 선례 해석의 비교 연구

종합 평가: 이는 법률 AI와 논리학의 교차 분야에서 중요한 기여를 한 이론성이 강한 우수 논문입니다. 실증 검증 측면에서 다소 부족하지만, 이론 프레임워크의 엄밀성과 혁신성으로 인해 중요한 학술적 가치와 실용적 잠재력을 지니고 있습니다.