귀결 기반 추론: PTIME 분류

📍 현재 위치: 3부 · EL 완성 알고리즘 — 11장. 건전성과 완전성은 여섯 규칙이 신뢰할 수 있는 결정 절차임을 증명했습니다; 이제 우리는 그 규칙들이 구현하는 추론의 양식에 이름을 붙이고, 왜 그것 — 테이블로 탐색이 아니라 — 이 EL에게 다항 시간 분류를 안겨 주는지 살펴봅니다.

우리는 완성 알고리즘을 만들고, 그것이 두 개의 표를 포화시키는 것을 지켜보았으며, 그것이 건전하고 완전함을 증명했습니다. 우리가 한 발 물러나 알아차리지 못했던 것은, 그것이 주류와는 단 하나의 거부로 구별되는 추론기들의 가족 전체에 속한다는 사실입니다: 그것은 결코 추측하지 않습니다. 그것은 결코 결론이 거짓이라고 가정하고서 무엇이 깨지는지 살펴보지 않으며, 결코 분기를 열고 역추적하지 않습니다. 그것은 그저 아무것도 새로 나타나지 않을 때까지 사실을 앞으로 갈아 나갈 뿐입니다. 그 거부에는 이름이 있습니다, 귀결 기반 추론(consequence-based reasoning)이며, 이는 문체상의 특이함이 아닙니다 — 이것은 분류를 잠재적으로 지수적인 탐색에서 보장된 다항 시간 계산으로 바꾸어 놓는 단 하나의 설계 결정입니다.

쉽게 말하면

같은 사건을 맡은 두 명의 형사를 상상해 보십시오. 첫 번째 형사는 모순에 의해 일합니다: 그녀는 용의자가 무죄라고 가정하고, 갈라지는 모든 알리바이를 끝까지 뒤쫓다가, 이야기가 무너지는 순간 역추적합니다 — 무죄일 수 있는 모든 가능한 이야기가 결국 모순으로 끝난다면, 유죄가 증명됩니다. 두 번째 형사는 애초에 어떤 가설도 세우지 않습니다. 그녀는 증거가 강제하는 사실들만을 게시판에 압정으로 고정하고, 그다음 그 사실들이 강제하는 사실들을 고정하며, 한 차례의 온전한 순회가 단 한 장의 새 카드도 더하지 못할 때까지 게시판을 계속 훑습니다. 게시판이 더 이상 자라지 않을 때 압정으로 고정되어 있는 것이 무엇이든 그것이 진실입니다. EL 추론은 두 번째 형사이며 — 이 장은 그녀가 결코 추측할 필요가 없는 이유, 그리고 그것이 어떻게 그녀를 빠르게 만드는지에 관한 이야기입니다.

이 장에서 다루는 내용

• 대조되는 두 패러다임 — 반박에 의한 모델 구축(경우 분할과 역추적이 있는 테이블로 방법)과 귀결 기반 포화(전방, 단조, 역추적 없음)를 트레이드오프 표 안에 나란히 놓고 비교합니다.
• EL에 경우 분할이 없는 이유 — 논리합을 제거하면 "이것을 시도하거나 또는 저것을 시도하는" 모든 선택이 사라지므로, 고정점까지의 단조로운 한 차례 순회로 충분합니다; 이것이 바로 다항 시간 상한의 정확한 원천입니다.
• 완성 연산자는 하나의 $T_P$입니다 — 포화 루프는 포섭 원자 위에서 작동하는 즉시 귀결 연산자이며, 그 최소 고정점이 곧 분류이고, 1권의 전방 연쇄와 동일한 모양을 하고 있습니다.
• 추적을 파동으로 읽기 — 학계 세계의 포화 $(23,0) \to (34,7) \to (39,7) \to (39,7)$을 폐쇄가 순회마다 채워지는 과정으로 읽고, 한 차례 온전한 순회가 아무것도 더하지 못하는 바로 그 순간 고정점이 검출됩니다.
• 그것이 규모를 감당하는 이유 — 귀결 기반 분류야말로 ELK가 SNOMED CT를 분류할 수 있게 해 주는 바로 그것이며, 추론기 장의 예고편입니다.
• 아직 풀리지 않은 부분 — EL은 혼(Horn)이므로 한 번의 포화로 충분합니다; 혼을 벗어나면 귀결 기반 방법은 영리하고 통제된 형태의 분할을 다시 도입해야 하며, 포섭 대신 규칙에 적용된 동일한 전방 포화 아이디어가 바로 데이터로그(Datalog)이자 4부로 들어가는 문입니다.

포섭을 판정하는 두 가지 방법

분류기의 임무는 함의(entailment)를 판정하는 것입니다: TBox $\mathcal{T}$가 $A \sqsubseteq B$를 강제하는가, 즉 $\mathcal{T} \models A \sqsubseteq B$라고 적히는 이것은, 공리를 따르는 모든 해석이 모든 $A$를 $B$ 안에도 넣는다는 뜻일까요? 이 질문에 답하는 근본적으로 서로 다른 두 가지 알고리즘 전략이 있으며, 그 둘을 구별하는 것이 바로 이 장의 요점입니다.

첫 번째는 고전적인 테이블로(tableau) 방법 뒤에 있는 전략인 반박에 의한 모델 구축(model-building by refutation)입니다. $\mathcal{T} \models A \sqsubseteq B$를 판정하기 위해, 그것은 목표가 거짓이라고 가정합니다 — $A$이면서 $B$는 아닌 개체 하나를 상정하고 — 그런 다음 그 개체를 포함하는, 완전하고 일관된 $\mathcal{T}$의 모델을 구축하려 시도합니다. 그 모델을 완성하려는 모든 시도가 모순(충돌(clash), 즉 $\bot$의 도출)으로 무너진다면, 그런 개체는 존재할 수 없으며 포섭 관계가 성립합니다. 이 방법의 엔진은 탐색(search)이며, 그 탐색이 분기하는 이유는 논리합(disjunction) 때문입니다. $X \sqsubseteq Y \sqcup Z$ 형태의 공리("$\sqcup$"는 또는입니다)는 선택을 강제합니다: 모델 구축자는 그 개체를 $Y$로 만들어 보아야 하고, 그 갈래 전체가 충돌한다면 역추적(backtrack)하여 대신 $Z$를 시도해야 합니다. 논리합 하나하나가 분기를 곱셈으로 늘리며, 최악의 경우 선택의 트리는 지수적으로 커집니다. 앞 장에서 우리가 신뢰했던 오라클인 HermiT가 정확히 그런 추론기입니다 — OWL 2 DL 뒤에 있는 완전한 SROIQ 논리 위에서 작동하는 하이퍼테이블로 계산법이며 — 그 거대한 논리를 판정하는 능력은 바로 그 분기하는 탐색으로 대가를 치르고 얻어진 것입니다.

두 번째 전략은 귀결 기반 추론(consequence-based reasoning) [1]입니다. 그것은 결코 반례 모델을 상정하지 않으며 결코 분기하지 않습니다. 그것은 공리를 단언된 귀결로 삼아 출발하여, 함의된 귀결 — 진정으로 따라 나오는 포섭 관계와 역할 엣지 — 만을 오직 추가하는 추론 규칙을 반복해서 적용하며, 규칙의 온전한 한 순회가 아무것도 더하지 못할 때까지 계속합니다. 그러면 답은 폐쇄로부터 곧바로 읽어낼 수 있습니다: $A \sqsubseteq B$는 정확히 $B$가 $S(A)$에 들어왔을 때 성립합니다. 반박해야 할 가설도, 열어야 할 분기도, 역추적하면서 버려야 할 상태도 없습니다. 이는 바로 지난 두 장의 완성 알고리즘이 해 오던 일이며, 우리는 다만 그 패러다임에 아직 이름을 붙이지 않았을 뿐입니다.

측면	모델 구축 / 반박 (테이블로)	귀결 기반 (포화)
핵심 동작	목표가 거짓이라고 가정하고 반례 모델 구축을 시도	아무것도 가정하지 않고 함의된 귀결을 앞으로 도출
비결정성	논리합에 대한 경우 분할, 역추적 동반	없음 — 단조로운 한 차례 순회, 역추적 없음
상태	후보 모델을 구축했다가 버림	하나의 포화된 집합을 키워 나가며 결코 버리지 않음
답을 읽는 법	모델이 존재하지 않음 ⟹ 함의됨	$B \in S(A)$ ⟹ 함의됨
가장 잘 맞는 곳	$\sqcup$, $\neg$를 갖춘 표현력 있는 DL (ALC, SROIQ)	$\sqcup$가 없는 혼 DL (EL, EL++)
최악의 비용	지수적 탐색 트리	다항식적 포화 (EL: 3차)
본보기	HermiT (하이퍼테이블로)	ELK, CEL (완성)

같은 질문에 대한 두 개의 답: 테이블로 방법은 지수적으로 자랄 수 있는 탐색 트리를 분기하고 역추적하며 나아가는 반면, 귀결 기반 포화는 하나의 단조로운 계단을 올라 고정점에 이릅니다 — EL이 저렴한 오른쪽 방법을 쓸 수 있는 이유는 그것이 분기할 논리합을 전혀 갖고 있지 않기 때문입니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

PTIME의 원천: 논리합도 경우 분할도 없음

완전한 OWL 2 DL은 그럴 수 없는데 EL은 어떻게 이 저렴한 전략으로 벗어날 수 있을까요? 답은 단 하나의 빠진 구성자에 있습니다. EL 계열은 정확히 논리곱 $\sqcap$과 존재 제한(existential restriction) $\exists r.C$만을 유지합니다; 논리합 $\sqcup$도 부정 $\neg$도 없습니다("없음"의 유일한 맛으로 허용되는 것은 바닥 개념 $\bot$뿐이며, 이는 분기하지 않는 단일 규칙으로 처리됩니다). 따라서 모든 공리는 선택된 귀결이 아니라 언제나 강제된 귀결 하나만을 가집니다. CR3가 $\text{Professor} \sqsubseteq \exists\text{advises}.\text{Student}$를 볼 때, 추가할 엣지는 정확히 하나뿐입니다; 추론기가 "$Y$로 만들 것인가 또는 $Z$로 만들 것인가"를 저울질하며 잘못된 추측을 되돌릴 준비를 해야 하는 순간은 결코 오지 않습니다. 유일한 분기의 원천을 제거하면 탐색 트리는 하나의 줄기로 무너집니다 — 고정점까지 반복되는 하나의 단조로운 순회입니다.

이것은 부드러운 관찰이 아닙니다; 이것이 복잡도 이야기의 전부입니다. 논리적으로 말하면 EL은 혼(Horn) 서술 논리입니다: 그 공리들은 혼 절(Horn clause)로 번역되며, 그 머리는 논리합을 전혀 지니지 않는데, 이것이 바로 1권이 즉시 귀결 연산자를 단조로 만드는 조건으로 짚어냈던 것과 정확히 같은 조건입니다. 고정점에서 나온 하중을 떠받치는 경고를 떠올려 보십시오: $T_P$가 단조인 것은 규칙 몸체가 양의 논리곱이기 때문입니다 — 사실을 더하는 것은 더 많은 규칙을 충족시킬 수 있을 뿐 결코 더 적게 충족시키지 않으며 — "몸체에 부정이 하나 들어 있었더라면 … 사실 집합을 키우는 것이 그 조건을 꺼버려 이전에는 유도 가능했던 머리를 파괴할 수 있었을 것이고, 그러면 단조성이 깨지고 그와 함께 위의 모든 보장도 깨졌을 것입니다." 논리합은 그 거울상의 방식으로 그것을 깨뜨립니다: 논리합으로 이루어진 결론은 추가할 단 하나의 사실이 아니라 사실들 사이의 선택이며, 선택은 탐색을 요구합니다. EL은 둘 중 어느 것도 담지 않도록 설계되었으므로, 그 귀결 연산자는 단조로 남고 그 폐쇄는 결정적으로 남습니다.

그 보상은 확실한 복잡도의 분리입니다. 논리합과 부정을 더해 ALC를 얻으면 일반 TBox에 대한 개념 충족 가능성(concept satisfiability)은 ExpTime-완전이 됩니다 — 최악의 경우 증명 가능하게 지수적입니다. 이와 대조적으로 EL 포섭은 TBox 크기에 대해 다항 시간에, 실제로는 3차 시간 $O(n^3)$에 결정 가능하며, 이 PTIME 상한이야말로 완성 알고리즘이 안겨 주는 핵심 결과입니다 [2]. 같은 질문 — $A \sqsubseteq B$가 따라 나오는가? — 이지만, 그것을 제기하는 언어가 정직한 알고리즘이 탐색을 하는지 아니면 그저 포화만 하면 되는지를 결정합니다.

완성 연산자: 포섭 원자 위의 $T_P$

완성을 귀결 기반으로 보는 순간, 1권과의 혈연 관계는 비유이기를 멈추고 항등식이 됩니다. 전방 연쇄는 근거 원자(ground atom)들의 집합을 받아 즉시 귀결 연산자(immediate-consequence operator) $T_P$ — "몸체가 성립하는 모든 규칙을 발동시키고, 머리들을 추가하라" — 를 적용하여, 기초 사실들로부터 프로그램의 의미 그 자체인 최소 고정점까지 상승했습니다. 완성도 정확히 똑같은 일을 하며, 다만 그 "원자"가 포섭 사실이라는 점만 다릅니다. 여섯 규칙 CR1–CR4와 바닥 규칙, 역할 사슬 규칙의 한 차례 전체 순회를, 상태 $X = (S, R)$에 작용하는 단일 연산자 $T$로 묶어 봅시다:

$$T(S, R) \;=\; (S, R)\ \text{enlarged by one simultaneous firing of every completion rule.}$$

어떤 규칙도 결코 항목을 삭제하지 않으므로 — 각 규칙은 오직 S[A].add(...)나 add_r(...)만을 호출할 뿐입니다 — 이 연산자는 단조(monotone)입니다: 더 큰 상태는 오직 더 큰 상태만을 만들어 낼 수 있습니다, $X \subseteq X' \Rightarrow T(X) \subseteq T(X')$. 그것이 바로 1권의 크나스터–타르스키(Knaster–Tarski)와 클레이니 상승(Kleene climb)이 요구하는 단 하나의 성질이며, 그래서 분류는 씨앗 상태 $X_0 = \big(\{A \mapsto \{A, \top\}\},\ \varnothing\big)$로부터 도달한 최소 고정점에 지나지 않습니다:

$$\mathrm{lfp}(T) \;=\; \bigcup_{k \ge 0} T^k(X_0), \qquad A \sqsubseteq B \iff B \in S(A)\ \text{at}\ \mathrm{lfp}(T).$$

동반 파일은 이 항등식을 독스트링(docstring)에서 있는 그대로 진술합니다(el_completion.py, 32–33번째 줄):

    The whole thing is just a **fixpoint of a monotone operator** — the very same
    shape as the forward-chaining T_P of Volume 1, now over subsumption facts.

그리하여 1권이 계속 되돌아올 것이라고 약속했던 네 가지 구성 — 전방 연쇄, 데이터로그 평가, 추이 폐쇄(transitive closure), 그리고 서술 논리 완성 — 은 여기서 하나의 구성이 네 번째 가면을 쓴 것으로 드러납니다. 포섭자 원장 $S$는 사실 집합이고; 완성 규칙은 프로그램 $P$이며; $T$는 $T_P$이고; 분류는 $\mathrm{lfp}(T_P)$입니다. 여러분이 그 상승에 대해 한 번 증명했던 모든 것이 통째로 옮겨 옵니다.

포화를 귀결의 파동으로 읽기

이것이 클레이니 상승이기 때문에, 우리는 그것이 오르는 모습을 지켜볼 수 있습니다. complete 함수는 각 순회를 계측하여, 매 라운드가 끝난 뒤 $S$와 $R$의 총 크기를 기록함으로써 독자가 귀결이 퍼져 나가는 모습을 볼 수 있게 합니다(el_completion.py, 205–213번째 줄):

    def sizes():
        s = sum(len(v) for v in S.values())
        r = sum(len(v) for v in R.values())
        return s, r

    rounds = [sizes()]
    changed = True
    while changed:
        changed = False

종료 검사 while changed는 고정점 조건 $T(X) = X$를 실행 가능하게 만든 것입니다: changed가 한 차례 전체 순회 동안 False로 남는 것은 정확히 어떤 규칙도 아무것도 추가할 수 없을 때이며, 이는 정확히 상태가 자기 자신으로 사상될 때입니다. 이 모듈을 학계 세계에 대해 실행하면 그 상승 과정이 출력됩니다 — 이는 python3 el_completion.py의 실제 커밋된 출력입니다:

saturation reached a fixpoint in 3 rounds
  round : |S| |R|  (derived subsumers, derived role pairs)
      0 :  23   0
      1 :  34   7
      2 :  39   7
      3 :  39   7

두 열을 발맞추어 오르는 두 개의 상승 사슬로 읽으십시오, 1권의 [23, 41, 47, 47] 사실 개수 파동의 직계 쌍둥이입니다. 각 파동은 $T$의 한 번 적용이 새로 확정하는 것을 기록하므로, 크기가 오르는 것을 지켜보는 것은 폐쇄가 순회마다 채워지는 것을 지켜보는 것입니다:

라운드	$\lvert S\rvert$	$\lvert R\rvert$	새 포섭자	새 엣지	이 파동이 뜻하는 것
0	23	0	—	—	씨앗: 각 개념은 오직 자기 자신과 ⊤만을 압니다
1	34	7	+11	+7	바쁜 한 차례 순회 — CR1–CR⊥ 연쇄: 위계, 7개 역할 엣지 전부, 충족 불가능한 두 개념 모두가 붙잡힙니다
2	39	7	+5	+0	CR1이 Researcher ⊑ Person을 1라운드에서 Researcher를 얻은 다섯 하위 클래스에 끌어올립니다
3	39	7	+0	+0	전선이 더 이상 나아가지 않습니다 — 고정점이 인증됩니다

1라운드는 하나의 바쁜 순회이며, 규칙들이 항상 같은 순서 — CR1, 그다음 CR2, CR3, CR4, 바닥 규칙, 그리고 역할 사슬 — 로 발동하기 때문에, 서로 의존하는 추론의 사슬 전체가 그 안에서 확정될 수 있습니다. CR1은 단언된 위계를 설치합니다; CR3는 7개의 역할 엣지 전부를 한 번에 깔아 놓습니다; 그런 다음 CR4는 그 갓 생긴 advises 엣지들을 통해 Researcher를 다시 도출합니다(공리 $\exists\text{advises}.\top \sqsubseteq \text{Researcher}$가 CR3가 방금 만든 엣지 위에서 발동합니다) — 이는 직접적인 Professor ⊑ Researcher 공리에 대한 교차 검증이자, TenuredStudentAdvisor가 Researcher를 얻는 유일한 경로입니다; CR2는 TenuredStudent가 Professor와 Student를 모두 지니고 있음을 붙잡아 $\bot$을 찍습니다; 그리고 바닥 규칙은 곧바로 그 $\bot$을 advises를 따라 거꾸로 기어가게 하여 TenuredStudentAdvisor를 단죄합니다. 11개의 새 포섭자와 7개의 엣지 하나하나가 모두 1라운드의 귀결입니다. 2라운드는 정확히 다섯 개의 포섭자를 추가할 뿐 엣지는 추가하지 않으며, 그 다섯 모두가 하나의 규칙에서 나온 같은 사실 — Person — 입니다: 공리 Researcher ⊑ Person에 대한 CR1입니다. 그 공리는 순회 안에서 자신의 차례가 왔을 때 이미 Researcher를 지니고 있던 개념들에 대해서만 1라운드에서 발동할 수 있었는데, 그것은 오직 Researcher 자신뿐이었습니다. 나머지 다섯 개 — Professor, Student, Dean, TenuredStudent, TenuredStudentAdvisor — 는 1라운드의 다른 곳에서 Researcher를 얻었고, 그 순회의 CR1이 그것을 끌어올리기에는 너무 늦었으므로, 이들의 Person은 한 파동 뒤처져 도착합니다 — 정확히 1권에서 person(alice)가 researcher(alice)보다 한 파동 늦게 도착했던 것과 같습니다. 3라운드는 모든 규칙을 한 번 더 발동시키지만 아무것도 추가하지 못하며($39 = 39$, $7 = 7$), 그 아무 일도 없는 순회가 바로 엔진이 스스로 끝났음을 증명하는 순회입니다. 이것이 말하지 않는 것에 주목하십시오: 라운드 계수기는 순회의 수를 한정할 뿐, 증명 깊이를 한정하지 않습니다. 한 차례의 순회가 여러 개의 의존적인 발동을 연쇄시킬 수 있기 때문에 — TenuredStudentAdvisor의 $\bot$ 하나만 해도 1라운드 안에서 CR1 → CR2 → CR3 → 바닥 규칙을 타고 왔습니다 — 하나의 파동은 새로 확정된 귀결의 수에 대한 상한일 뿐, 추론 홉의 수를 세는 것이 아닙니다. 더 깊은 온톨로지라면 더 많은 순회가 필요하겠지만, 원장 자체가 다항식적 상한을 넘어 자랄 수 없기 때문에 순회의 수는 다항식적으로 유계인 채로 남습니다.

왜 귀결 기반 추론은 규모를 감당하는가

트레이드오프 표의 마지막 두 행이 바로 이 패러다임이 장난감이기를 멈추고 생물의학을 실제로 돌리기 시작하는 지점입니다. 탐색 트리가 없으므로, 전체 작업량은 폐쇄의 크기 — 규칙이 언젠가 추가할 수 있는 항목의 수 — 에 비례하며, EL은 그 폐쇄가 다항식적으로 유지됨을 보장합니다: $n$개의 개념 이름이 있을 때, $S$는 최대 $n^2$개의 포섭자 항목을 담고 각 $R(r)$은 최대 $n^2$개의 쌍을 담으므로, 생산적인 순회마다 적어도 하나의 항목을 추가하는 단조 루프는 다항식 개수의 순회 안에서 반드시 멈춰야 합니다. 아무리 적대적으로 모델링하더라도 EL 분류를 지수적으로 폭발시킬 수는 없는데, 알고리즘 어디에도 폭발할 지수적 대상이 애초에 존재하지 않기 때문입니다.

바로 그 보장을 추론기 ELK가 현금화합니다 [3]. ELK는 바로 이 완성 규칙들 위에 구축된 귀결 기반 분류기이며, 수십만 개의 개념을 지닌 임상 온톨로지인 SNOMED CT를 몇 초 만에 분류하는데, 그 이유는 포화가 아름답게 병렬화되기 때문입니다: 규칙이 오직 추가만 할 뿐 결코 충돌하지 않으므로, 서로 다른 개념들의 포섭자 집합을 동시에 키워 나갈 수 있습니다. 그만큼 거대한 온톨로지의 반례 모델을 억지로 탐색해야 하는 테이블로 추론기라면 익사하고 말겠지만, 귀결 기반 추론기는 그저 더 높은 계단을 오를 뿐입니다. 이것이 바로 OWL 2 EL 프로파일이 애초에 존재하는 실용적인 이유이며, ELK와 CEL 그리고 그 동류가 교과서적인 루프가 아니라 실제 운영 시스템으로 연구되는 앞으로의 추론기 장으로 이어지는 맥락입니다.

아직 풀리지 않은 부분

정직한 경계는 위의 모든 것을 작동하게 만든 바로 그 특징입니다: EL은 혼(Horn)이므로, 하나의 단조로운 포화로 충분합니다. 혼을 벗어나는 순간 — 온톨로지가 "모든 유전자는 코딩이거나 또는 비코딩이다"와 같은 진정한 논리합을 담는 순간 — 그 말끔한 그림은 금이 갑니다. 순전히 전방으로만 나아가는, 역추적 없는 순회는 더 이상 완전할 수 없는데, 논리합으로 이루어진 귀결은 추가할 하나의 사실이 아니라 분기하는 의무이며, 완전성은 추론기가 두 갈래를 모두 고려하기를 요구하기 때문입니다. 열려 있는 공학적 질문은, 완전성을 유지하기에 딱 필요한 만큼의 경우 분할만을 허용하면서 역추적 없는 속도를 얼마나 유지할 수 있는가입니다. 귀결 기반 패러다임은, 순진한 테이블로가 하듯 모든 논리합에 대해 성급하게 분기하는 대신, 논리합으로 이루어진 귀결을 도출하고 어떤 추론이 진정으로 선택을 강제할 때에만 분할함으로써 정확히 혼을 넘어서까지 밀어붙여져 왔습니다 [1] — 이는 훨씬 더 표현력이 풍부한 논리에 대해서도 포화의 효율성 대부분을 되찾아 주는 혼종 방식이지만, 그 최악의 경우는 다시 한번 지수적입니다. 감당할 수 있는 경계선이 정확히 어디에 있는지는 여전히 활발한 연구의 경계이지, 정해진 선이 아닙니다.

이 장을 떠나는 두 번째 실마리도 있는데, 뻔히 보이는 곳에 숨어 있습니다. 서술 논리의 어휘를 벗겨내고 나면 남는 것 — 사실 집합에 씨앗을 뿌리고, 오직 추가만 하는 단조 규칙을 발동시키며, 최소 고정점까지 포화시키는 것 — 은 그 사실이 포섭 관계인지 임의의 관계인지 개의치 않는 범용 엔진입니다. 근거 데이터(ground data) 위의 사용자 작성 규칙에 적용하면, 그 동일한 엔진이 바로 데이터로그(Datalog)입니다: 1권의 즉시 귀결 연산자 $T_P$가 이제 질의 언어와 산업용 런타임을 갖춘 것입니다. 귀결 기반 분류와 데이터로그 평가는 하나의 아이디어가 지닌 두 가지 적용일 뿐이며, 이것이 바로 다음 부가 여러분이 방금 배운 모든 것을 재사용할 수 있는 정확한 이유입니다.

왜 중요한가

신경-기호 AI에게 이 장의 교훈은, 상징적 추론기가 무엇을 계산하는지 못지않게 어떻게 계산하는지가 중요하다는 것입니다. 귀결 기반 추론기는 단지 올바른 것이 아니라, 한 방향으로 나아가는 구성에 의해 올바르며, 이는 미분 가능한 추론 레이어가 작동하는 것과 같은 방향입니다. 4권이 명료한 "$B$가 $S(A)$ 안에 있는가?"라는 질문을 유연한(soft) 점수로 대체하고 매끄럽고 단조로운 갱신을 수렴할 때까지 반복할 때, 그것은 정확히 이 포화 — 고정점을 향한 전방 상승이며, 결코 역추적하는 탐색이 아닌 것 — 를 모방하고 있는 것입니다. 학습과 가장 자연스럽게 혼성화되는 패러다임은 전방으로만 나아가고, 단조로우며, 탐색이 없는 패러다임인데, 고정점은 그것을 통과해 미분할 수 있지만 역추적하는 탐색 트리는 그럴 수 없기 때문입니다. 따라서 귀결 기반 추론은 단지 EL이 빠른 이유일 뿐만 아니라, EL 방식의 추론이 상징적 추론기가 취할 수 있는 가장 신경망 친화적인 형태인 이유이며, 학습된 온톨로지 추론의 어떤 근사치든 반드시 견주어 측정되어야 할 명료한 목표이기도 합니다.

핵심 용어

• 귀결 기반 추론(Consequence-based reasoning) — 반박해야 할 가설도 역추적도 없이, 함의된 귀결을 포화(고정점)에 이를 때까지 앞으로 도출함으로써 함의를 판정하는 것; 완성 알고리즘이 속하는 패러다임입니다.
• 모델 구축 / 반박 (테이블로)(Model-building / refutation (tableau)) — 대조되는 패러다임: 목표가 거짓이라고 가정하고, 반례 모델을 탐색하며, 모든 갈래가 충돌할 때 함의를 보고합니다; 논리합에서 분기하며 지수적 시간을 요구할 수 있습니다.
• 경우 분할 / 역추적(Case split / backtracking) — 논리합 $\sqcup$이 모델 구축자에게 강제하는 비결정적 선택과, 실패한 선택을 되돌리는 것; EL에는 논리합이 없으므로 존재하지 않습니다.
• 혼 서술 논리(Horn description logic) — 공리가 논리합이 없는 (EL과 같은) DL로, 그 즉시 귀결 연산자가 단조이며 한 번의 포화로 완전합니다.
• 즉시 귀결 연산자 $T$ / $T_P$(Immediate-consequence operator) — 상태 $(S, R)$ 위에서 모든 완성 규칙을 동시에 한 번 발동시키는 것; 단조이며, 분류는 그 최소 고정점 $\mathrm{lfp}(T)$입니다.
• 포화 파동(Saturation wave) — 한 라운드($T$의 한 번 적용) 동안의 $\lvert S\rvert$와 $\lvert R\rvert$의 성장; 순회 내부의 고정된 규칙 순서가 여러 의존적 발동을 하나의 파동 안으로 무너뜨릴 수 있으므로 이는 증명 깊이 계수기가 아니라 그 순회에서 새로 확정된 귀결에 대한 상한이며, 아무 일도 없는 파동이 고정점을 인증합니다.
• PTIME 분류(PTIME classification) — EL 포섭이 다항(3차) 시간에 판정되는 것으로, 귀결 기반 포화가 안겨 주고 테이블로 탐색은 안겨 줄 수 없는 보장입니다.
• ELK — 규칙 발동을 병렬화하여 SNOMED CT의 수십만 개 클래스를 몇 초 만에 분류하는 귀결 기반 EL 추론기입니다.

이 장이 이끄는 곳

우리는 이제 완성 알고리즘을 모든 각도에서 살펴보았습니다: 하나의 엔진으로서(여섯 규칙과 while changed 루프), 인증된 결정 절차로서(건전하고, 완전하며, 종료하는), 그리고 마지막으로 일반 패러다임의 한 사례로서(귀결 기반, 단조, PTIME) 말입니다. 이 부를 마무리하는 실마리는, 그 패러다임이 서술 논리보다 더 크다는 관찰입니다. 다음 장인 데이터로그는 바로 그 동일한 전방 포화 엔진 — 최소 고정점까지 오르는 $T_P$ 연산자 — 을 가져다가, 질의 인터페이스와 규모에서도 그 상승을 빠르게 만들도록 공학적으로 설계된 런타임을 갖춘, 근거 데이터 위의 범용 규칙 언어로 바꾸어 놓습니다. 완성 알고리즘은 온톨로지를 분류했습니다; 데이터로그는 여러분이 직접 규칙을 작성하고 그것을 똑같은 방식으로 포화시킬 수 있게 해 주며, 추론이 더 이상 개념 위계에 관한 것이 아니라 임의의 관계에 관한 것이 되는 4부를 열어젖힙니다.