Модальная логика для моделей временных и юрисдикционных классификаторов

Основная информация

• ID статьи: 2510.13691
• Название: A Modal Logic for Temporal and Jurisdictional Classifier Models
• Авторы: Cecilia Di Florio (Болонский университет, Люксембургский университет), Huimin Dong (TU WIEN), Antonino Rotolo (Болонский университет)
• Категория: cs.AI
• Дата публикации: 15 октября 2025 г. (препринт arXiv)
• Ссылка на статью: https://arxiv.org/abs/2510.13691

Аннотация

Логические модели могут использоваться для создания инструментов верификации классификаторов машинного обучения, применяемых в юридической сфере. Классификаторы ML предсказывают исходы новых дел на основе предыдущих, выполняя таким образом форму рассуждений на основе прецедентов (CBR). В данной статье мы представляем модальную логику классификаторов, разработанную для формального описания юридического CBR. Мы включаем принципы разрешения конфликтов между прецедентами, вводя в логику временное измерение дел и иерархию судов в правовой системе.

Исследовательский контекст и мотивация

Проблемный фон

1. Потребность в верификации юридического AI: Применение классификаторов машинного обучения в юридической сфере становится всё более распространённым, однако нормативная корректность, точность и устойчивость их предсказаний не гарантированы, что вызывает озабоченность судей
2. Проблема прецедентных ограничений: В системах общего права классификаторы должны удовлетворять прецедентным ограничениям (precedential constraint), следуя принципу "следовать прецеденту" (stare decisis)
3. Конфликты прецедентов: В реальных правовых системах существуют конфликты между прецедентами, тогда как существующие модели Horty предполагают согласованность базы прецедентов и не могут обрабатывать конфликтующие прецеденты

Исследовательская мотивация

Юридическое рассуждение на основе прецедентов по сути является формой рассуждения на основе прецедентов (CBR), когда классификаторы машинного обучения предсказывают результаты новых дел на основе исторических прецедентов. Однако существующие модели не могут обрабатывать конфликты между прецедентами и требуют введения временного измерения и отношений иерархии судов для решения этой проблемы.

Ограничения существующих подходов

• Модели reason и result Horty предполагают согласованность базы прецедентов
• Неспособны обрабатывать реальные конфликты между прецедентами
• Отсутствует формализованное моделирование временного и иерархического измерений

Основные вклады

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)} если s ≠ s*
    {f(s') | s' ∈ BestTH(β̄s*)} иначе
}

Экспериментальная установка

Тематическое исследование

В статье используется тематическое исследование дел о коммерческих секретах, включающее четыре фактора:

• Поддерживающие истца: 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 и логики. Несмотря на некоторые недостатки в эмпирической верификации, строгость и инновационность её теоретического фреймворка придают ей значительную академическую ценность и практический потенциал.