건전성과 완전성: 규칙이 충분한 이유

📍 현재 위치: 3부 · EL 완성 알고리즘 — 10장. 완비 규칙은 우리에게 여섯 개의 발동 규칙 — CR1–CR4, 바닥 규칙 CR⊥, 역할 사슬 규칙 CRχ — 을 건네주었고, 그것들이 학계 세계 위에서 두 표 $S$와 $R$을 고정점까지 키워 나가는 것을 지켜보았습니다. 이제 우리는 영리한 루프를 추론기로 바꾸어 놓는 질문을 던집니다: 그 규칙들은 정말로 따라 나오는 포섭 관계만을, 더도 덜도 아니게 정확히 도출할까요?

완성 알고리즘은 이미 만들어졌고, 실제로 실행됩니다. 그러나 "실행되고 답이 맞아 보인다"는 것은 희망이지 보증이 아닙니다 — 통과하는 예제 하나는 다음 온톨로지에 대해 아무것도 증명해 주지 않습니다. 이 장은 그 희망을 증명으로 대체합니다. 우리는 어떤 규칙 집합이든 결정 절차(decision procedure)라고 불리기 전에 반드시 갖추어야 할 세 가지 성질에 이름을 붙이고, EL 완성이 그 셋을 모두 갖추었음을 논증한 다음, 논문 증명이 결코 할 수 없는 한 가지 일을 합니다: 처음부터 만든 추론기를 제품용 추론기 옆에서 실행하여, 둘이 항목 하나하나까지 일치하는 모습을 지켜보는 것입니다.

쉽게 말하면

다리가 개통되기 전에 그것을 인증해 줄 검사관을 고용한다고 상상해 보십시오. 최종 도장을 신뢰하기 전에 여러분에게는 세 가지 별개의 약속이 필요합니다. 첫째, 검사관은 결코 멀쩡한 케이블을 불량이라고 낙인찍지 않습니다 — 멀쩡한 다리를 폐쇄하는 거짓 경보가 없습니다. 둘째, 검사관은 결코 닳아 해진 케이블을 그냥 지나치지 않습니다 — 놓치는 것이 없습니다. 셋째, 검사는 개통일까지 실제로 끝이 납니다 — 다리 위를 영원히 서성이는 대신 말입니다. 이 셋이 한꺼번에 갖추어져야만 그 보고서에 따라 행동할 가치가 생깁니다: 늑대가 왔다고 거짓말하거나, 결함을 지나치거나, 다시는 내려오지 않는 검사관은 쓸모가 없습니다. 추론기가 바로 그 검사관이고, 클래스 위계가 그 보고서이며, 이 장은 우리의 검사관이 그 세 가지 미덕을 모두 갖추었다는 논증입니다 — 게다가 첫 번째 검사관을 검증하는 두 번째의 독립된 검사관까지 딸려 있습니다.

이 장에서 다루는 내용

• 세 가지 성질, 하나의 결정 절차 — 건전성(거짓 양성이 없음), 완전성(거짓 음성이 없음), 종료(언제나 멈춤); 이 셋이 함께여야만 표에서 함의를 읽어낼 자격이 생깁니다.
• CR4에 대해 직접 해 보는 건전성 증명 — 모든 규칙은 서술 논리 의미론에 대한 단 하나의 표시된 함의로 보여지듯이, 모든 모델에서 참을 보존합니다.
• 표준 모델에 의한 완전성 — 포화된 $S$와 $R$은 그 자체로 TBox의 한 모델이며, 규칙이 도출하지 못한 모든 포섭 관계를 반증합니다 — 그래서 함의된 것은 무엇이든 반드시 도출되었어야 합니다.
• 종료와 다항식 상한 — $S$와 $R$은 오직 자라나기만 하며, 이름과 쌍의 개수로 고정된 상한 안에 머무르므로, 고정점은 다항식 개수만큼의 단계 안에 도달합니다.
• 실증적 교차 검증 — reasoners.py는 classify()를 HermiT와 맞세우며, 둘 다 8개의 포섭 관계와 동일한 2개의 충족 불가능한 개념에 이릅니다.
• 독립된 오라클이 중요한 이유 — HermiT는 EL의 진(眞)초집합 위에서 작동하는 완전한 OWL 2 DL 추론기이므로, 그것의 일치는 처음부터 만든 코드가 얻을 수 있는 가장 강력한 외부 검사입니다.

세 가지 성질, 하나의 결정 절차

먼저 어휘를 고정해 둡시다. TBox $\mathcal{T}$는 스키마 공리들의 집합이며(우리의 학계 세계는 그중 14개를 가지고 있습니다); 포섭(subsumption) $A \sqsubseteq B$는 "모든 $A$는 $B$이다"로 읽습니다. 분류기가 답하는 질문은 함의(entailment)이며, $\mathcal{T} \models A \sqsubseteq B$로 쓰고 "TBox가 $A \sqsubseteq B$를 함의한다"로 읽습니다: 이는 $\mathcal{T}$를 따르는 모든 해석(interpretation)에서 그 포섭 관계가 성립한다는 뜻입니다 — 공리들과 양립하면서도 어떤 $A$가 $B$이기를 실패하는 가능 세계는 존재하지 않습니다. 완성은 이 의미론적 질문에 순전히 구문적인 조치로 답합니다: 표 $S$가 더는 자라지 않을 때까지 규칙을 발동시킨 다음, $B \in S(A)$일 때 정확히 그때에만 $A \sqsubseteq B$를 보고합니다. 그 읽어내기는 단 한 줄입니다 — return sup in S.get(sub, set())(el_completion.py 324번째 줄).

그 구문적 검사가 의미론적 함의를 의미하려면, 세 가지 성질이 나란히 맞아떨어져야 합니다. 이들에 정확히 이름을 붙이는 것이 이 학문 분야 전체입니다:

성질	평이한 뜻	이것이 없으면 무엇이 깨지는가	EL 완성이 이를 확보하는 방법
건전성(Soundness)	오직 함의된 포섭 관계만을 도출함 — 거짓 양성이 없음	추론기가 거짓을 "증명"하며, 모든 답이 의심스러워짐	모든 규칙이 모든 모델에서 보존하는 불변량 [1]
완전성(Completeness)	모든 함의된 포섭 관계를 도출함 — 거짓 음성이 없음	추론기가 실제 귀결을 놓치고, 침묵이 더는 "따라 나오지 않는다"를 뜻하지 않게 됨	$\mathcal{T}$를 충족시키면서 도출되지 않은 모든 포섭 관계를 반증하는 표준 모델 [2]
종료(Termination)	포화 루프가 언제나 멈춤	$S$에서 답을 읽어낼 수 있는 순간이 결코 오지 않음 — "끝났다"가 결코 도착하지 않기 때문	$S$와 $R$이 다항식 상한 안에서 단조롭게 자람

이 셋이 모두 함께여야만 결정 절차라는 문구를 얻습니다: 어떤 입력에 대해서든 멈추어 올바른 예/아니오 답을 내놓는 알고리즘 말입니다. 건전성과 완전성은 정확성의 절반이며, 하나의 깔끔한 쌍조건문(biconditional)으로 무너져 내립니다,

$$B \in S(A) \quad\Longleftrightarrow\quad \mathcal{T} \models A \sqsubseteq B,$$

여기서 왼쪽에서 오른쪽 방향($\Longrightarrow$, "함의한다"로 읽습니다)이 건전성이고, 오른쪽에서 왼쪽 방향($\Longleftarrow$)이 완전성입니다. 이를 정직하게 유지해 주는 단서가 하나 있습니다: 이 쌍조건문은 충족 가능한(satisfiable) 이름 $A$, 즉 $\bot \notin S(A)$인 이름에 대해서만 읽으십시오. $A$가 충족 불가능할 때($\bot \in S(A)$), 오른쪽은 공허하게(vacuously) 참입니다 — 공집합인 개념은 무엇의 부분집합도 되므로 ex falso에 의해 $\mathcal{T} \models A \sqsubseteq B$는 모든 $B$에 대해 성립합니다 — 그러나 알고리즘은 모든 이름으로 $S(A)$를 범람시키지 않습니다; 그 대신 $A$를 충족 불가능하다고 따로 보고하며, 이는 바닥 규칙의 별개 임무입니다. 종료는 세 번째 다리입니다: 이것은 왼쪽이 실제로 계산되는 순간이 반드시 온다는 것을 보장합니다. 추론기 자신의 독스트링(docstring)이 그 목표를 그대로 진술합니다 — "The algorithm is sound and complete for EL++ subsumption, and runs in time polynomial in the size of the TBox"(el_completion.py 38–39번째 줄). 그 "EL++"를 학계 세계가 실제로 사용하는 구성자들 — 논리곱, 존재 한정, ⊥, 역할 사슬, 즉 여기 여섯 규칙이 결정하는 다루기 쉬운(tractable) 핵심 — 에 견주어 읽으십시오; 완전한 EL++는 여기에 더해 명목 개념(nominal)과 구체 도메인(concrete domain)도 인정하는데, 이 온톨로지는 그 자신의 완비 규칙을 전혀 발동시키지 않습니다. 이 장의 나머지는 그 문장이 참인 이유입니다.

결정 절차는 세 기둥 — 건전성, 완전성, 종료 — 위에 서 있으며, 이들이 함께 그 정상의 쌍조건문에 자격을 주는 한편, HermiT를 상대로 한 교차 검증은 그 전체 구조를 뒷받침하는, 밑바닥의 악수입니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

건전성: 모든 규칙이 참을 보존하다

건전성은 규칙이 결코 거짓말하지 않는다고 말합니다. 그 논증은 하나의 튼튼한 발상입니다: 모든 구문적 항목을 하나의 의미론적 사실에 묶어 두는 불변량(invariant)을 유지하고, 각 규칙이 그것을 보존하는지 확인하는 것입니다.

먼저 의미론입니다. 어떤 기호보다도 먼저 해독해 둡시다. 해석(interpretation) $\mathcal{I}$는 하나의 가능 세계입니다: 이는 개체들의 정의역(domain) $\Delta^{\mathcal{I}}$를 고정하고, 각 개념 이름 $A$를 집합 $A^{\mathcal{I}} \subseteq \Delta^{\mathcal{I}}$로 읽으며(그 외연(extension) — 그 세계에서 실제로 $A$인 것들입니다), 각 역할 $r$을 쌍들의 집합 $r^{\mathcal{I}}$로 읽습니다. 구성자들은 그 당연한 의미를 얻습니다: 논리곱은 교집합이며, $(C \sqcap D)^{\mathcal{I}} = C^{\mathcal{I}} \cap D^{\mathcal{I}}$("둘 다에 속함")이고, 존재 한정은 $(\exists r.C)^{\mathcal{I}} = \{\, x : \exists y,\ (x,y) \in r^{\mathcal{I}} \ \wedge\ y \in C^{\mathcal{I}} \,\}$("어떤 $C$와 $r$-관계를 맺는 $x$들")입니다. 해석 $\mathcal{I}$가 $\mathcal{T}$의 모델이 되는 것은 모든 공리를 충족시킬 때이며, 각 공리 $C \sqsubseteq D$는 $C^{\mathcal{I}} \subseteq D^{\mathcal{I}}$를 뜻합니다.

이제 불변량입니다. 포화가 진행되는 내내, $\mathcal{T}$의 모든 모델 $\mathcal{I}$에 대해, 우리는 다음을 유지합니다:

$$B \in S(A) \ \Rightarrow\ A^{\mathcal{I}} \subseteq B^{\mathcal{I}}, \qquad (A,B) \in R(r) \ \Rightarrow\ A^{\mathcal{I}} \subseteq (\exists r.B)^{\mathcal{I}}.$$

말로 풀면: 알고리즘이 기록하는 모든 포섭자는 모든 모델에서 실제 포섭 관계이며, 그것이 기록하는 모든 역할 엣지는 모든 모델에서 실제로 "$A$가 $B$인 $r$-후속자를 가진다"는 사실입니다. 이것이 포화가 멈추는 순간까지 살아남는다면, $B \in S(A)$는 모든 모델에서 $A^{\mathcal{I}} \subseteq B^{\mathcal{I}}$를 강제하는데 — 이는 정확히 $\mathcal{T} \models A \sqsubseteq B$입니다. 그러므로 건전성을 증명하는 것은 이 불변량이 모든 규칙 발동 이후에도 살아남는다는 것을 증명하는 것입니다.

이는 처음부터 성립합니다: $S(A)$는 단지 $A$와 $\top$만으로 씨앗이 뿌려지고(el_completion.py 187번째 줄, S = {a: {a, TOP} for a in names}), $A^{\mathcal{I}} \subseteq A^{\mathcal{I}}$와 $A^{\mathcal{I}} \subseteq \top^{\mathcal{I}} = \Delta^{\mathcal{I}}$는 둘 다 자명하게 참입니다. 귀납 단계는 각 규칙을 확인합니다. 가장 미묘한 CR4를 살펴봅시다 — 코드 네 줄과 그 주석입니다(el_completion.py 234–238번째 줄):

# CR4: (A, B) ∈ R(r), B' ∈ S(B), ∃r.B' ⊑ C  ⟹  C ∈ S(A)
for _, r, b_prime, c in nf4:
    for (A, B) in list(R.get(r, ())):
        if b_prime in S[B] and c not in S[A]:
            S[A].add(c); changed = True

CR4는 세 가지 사실이 표 안에 동시에 있을 때 발동합니다 — $(A,B) \in R(r)$, $B' \in S(B)$, 그리고 공리 $\exists r.B' \sqsubseteq C$가 $\mathcal{T}$에 속함 — 그리고 $C \in S(A)$를 결론짓습니다. 그 건전성은 다음 함의이며, $\mathcal{T}$의 모든 모델 $\mathcal{I}$에서 참이고, 각 전제에는 그것을 보증하는 표 항목이 표시되어 있습니다:

$$\underbrace{A^{\mathcal{I}} \subseteq (\exists r.B)^{\mathcal{I}}}_{(A,B)\,\in\, R(r)} \ \wedge\ \underbrace{B^{\mathcal{I}} \subseteq (B')^{\mathcal{I}}}_{B'\,\in\, S(B)} \ \wedge\ \underbrace{(\exists r.B')^{\mathcal{I}} \subseteq C^{\mathcal{I}}}_{\exists r.B' \,\sqsubseteq\, C \,\in\, \mathcal{T}} \quad\Longrightarrow\quad A^{\mathcal{I}} \subseteq C^{\mathcal{I}}.$$

이를 점별로 읽으십시오 — 이것이 손으로 확인하는 방법입니다. 임의의 개체 $x \in A^{\mathcal{I}}$를 취하십시오. 첫 번째 전제는 $x \in (\exists r.B)^{\mathcal{I}}$를 놓으므로, $(x,y) \in r^{\mathcal{I}}$이고 $y \in B^{\mathcal{I}}$인 어떤 $y$가 있습니다. 두 번째 전제 $B^{\mathcal{I}} \subseteq (B')^{\mathcal{I}}$는 그 증인을 $y \in (B')^{\mathcal{I}}$로 승격시킵니다 — 그래서 $x$는 어떤 $B'$와 $r$-관계를 맺으며, 즉 $x \in (\exists r.B')^{\mathcal{I}}$입니다. 세 번째 전제는 그저 그 공리가 $\mathcal{I}$에서 성립한다는 것이며, 이는 곧 $x \in C^{\mathcal{I}}$를 내어 줍니다. $x$가 임의였으므로, $A^{\mathcal{I}} \subseteq C^{\mathcal{I}}$입니다 — 이는 새로 쓰인 $C \in S(A)$에 대해 정확히 그 불변량입니다. 동일한 하나의 모델에 대한 점별 확인이 CR1, CR2, CR3, 바닥 규칙, 역할 사슬 규칙에도 그대로 통합니다; 각각은 그저 자신이 다루는 구성자의 의미론을 사슬처럼 이을 뿐입니다. 이 불변량이 씨앗에서 성립하고 모든 발동에 의해 보존되므로, 고정점에서도 성립하며, 건전성이 따라 나옵니다 [1].

완전성: 나머지 모든 것을 반증하는 모델

완전성은 그 거울상 주장이자 더 어려운 방향입니다: $\mathcal{T} \models A \sqsubseteq B$라면 규칙이 실제로 $B$를 $S(A)$에 넣었어야 합니다. 대우(contraposition)를 취하면, 고정점에서 $B \notin S(A)$일 때마다, 그 포섭 관계는 정말로 따라 나오지 않습니다 — 어떤 $A$가 $B$가 아닌, $\mathcal{T}$의 모델이 반드시 존재해야 합니다. 완전성은 바로 그 반례 모델(countermodel)을 구축함으로써, 포화된 표 그 자체로부터 단 한 번 증명됩니다.

그 구성물이 표준 모델(canonical model) $\mathcal{I}$이며, $S$와 $R$로부터 곧바로 읽어냅니다 [2]. 각 충족 가능한 개념 이름마다(즉 $\bot \notin S(A)$인 각 $A$마다) 정의역 원소 하나 $d_A$를 취하고, 그 외연을 표로부터 정의합니다:

$$\Delta^{\mathcal{I}} = \{\, d_A : \bot \notin S(A) \,\}, \qquad A^{\mathcal{I}} = \{\, d_B : A \in S(B) \,\}, \qquad r^{\mathcal{I}} = \{\, (d_A, d_B) : (A,B) \in R(r) \,\}.$$

이것이 성립하는 데에는 두 가지 사실이 필요하며, 둘 다 포화 — 어떤 규칙도 더 이상 발동할 수 없는 상태 — 의 귀결입니다. 첫째, 표는 정직하게 읽힙니다: 구성에 의해 $d_A \in B^{\mathcal{I}}$인 것과 $B \in S(A)$인 것은 동치입니다. 둘째, $\mathcal{I}$는 $\mathcal{T}$의 진짜 모델입니다. 바로 여기서 완비 규칙들이 거꾸로 자신의 값어치를 증명합니다: 모델이 반드시 충족시켜야 하는 각 폐쇄 조건은 더 이상 발동할 수 없는 어떤 규칙과 대응합니다. $\mathcal{I}$가 공리 $\exists r.B' \sqsubseteq C$를 위반했다고 가정해 봅시다 — 어떤 $d_A$가 어떤 $B'$로 향하는 $r$-엣지를 가지고 있지만 $d_A \notin C^{\mathcal{I}}$인 경우입니다. 정의를 풀어 보면, 이는 $(A,B) \in R(r)$, $B' \in S(B)$, $C \notin S(A)$가 모두 성립한다는 뜻이며 — 그렇다면 CR4의 가드 c not in S[A]가 참이 되어 그 규칙이 여전히 발동할 것이므로, 우리가 고정점에서 멈추었다는 것과 모순됩니다. 포화란 정확히 표준 모델에 그런 틈이 없다는 진술입니다; 모든 공리 형태는 그것의 위반을 바로잡을 규칙에 의해 지켜지고 있습니다.

그 대가는 즉각적입니다. $d_A$가 실제로 $\Delta^{\mathcal{I}}$ 안에 있는, 즉 충족 가능한 어떤 이름 $A$에 대해서든 말입니다. 모든 $S(A)$가 $A$ 자신으로 씨앗이 뿌려지므로, $d_A \in A^{\mathcal{I}}$는 언제나 성립합니다. 그래서 만약 $B \notin S(A)$라면, $d_A \in A^{\mathcal{I}}$이면서도 $d_A \notin B^{\mathcal{I}}$입니다: 표준 모델은 어떤 $A$가 $B$가 아닌 증언 세계이며, 따라서 $\mathcal{T} \not\models A \sqsubseteq B$입니다. 이것이 바로 정의역이 충족 불가능한 이름들의 $d_A$를 제외하는 이유입니다: 그곳에서는 $\mathcal{T} \models A \sqsubseteq B$가 모든 $B$에 대해 공허하게 성립하므로(다시 그 ex-falso 포섭 관계입니다), 반례 모델은 존재하지도 필요하지도 않으며, 바닥 규칙이 그 이름들을 따로 보고합니다. 대우를 취하면: 충족 가능한 모든 $A$에 대해, 함의된 것은 무엇이든 도출되었습니다. 포화된 표로부터 조립된 하나의 모델이, 충족 가능한 이름들 사이에서 도출되지 않은 모든 포섭 관계를 동시에 반증합니다 — 그것이 완전성 전체를 하나의 대상으로 담아낸 것입니다.

종료와 다항식 상한

루프가 결코 멈추지 않는다면 정확성은 아무 가치도 없으므로, 종료는 세 번째 기둥입니다 — 그리고 EL의 경우에는 덤으로 복잡도 상한까지 딸려 옵니다. 포화 루프는 각 회차의 앞머리에서 changed = False로 뒤집었다가 어떤 규칙이 새로운 것을 추가할 때에만 다시 True로 돌리는, 평범한 while changed:입니다(el_completion.py 210–213번째 줄):

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

모든 규칙은 $S$나 $R$에 추가할 뿐 결코 제거하지 않습니다 — 각각은 진짜 추가일 때에만 changed = True를 설정하는 not in 검사(c not in S[A], pair not in R[r])로 지켜지고 있습니다. 그래서 표는 단조롭게(monotonically) 자라며, 고정된 상한 안에서 자랍니다. $N$을 개념 이름들의 집합, $N_R$을 역할들의 집합이라고 합시다. 각 $S(A)$는 $N$의 부분집합이고 각 $R(r)$은 $N \times N$의 부분집합이므로, 총합은 다음과 같이 상한이 정해집니다:

$$\sum_{A} |S(A)| \ \le\ |N|^2, \qquad \sum_{r} |R(r)| \ \le\ |N_R| \cdot |N|^2.$$

오직 증가하기만 하고 위로 유계인 양은 반드시 안정됩니다. 생산적인 회차마다 그 두 상한으로 유계인 총합에 최소한 하나의 원소가 추가되므로, $O(|N_R| \cdot |N|^2)$번의 회차 — 다항식 개수만큼 — 이후에는 아무것도 새로 나타나지 않고, changed는 False로 머무르며, 루프는 최소 고정점에서 종료합니다. 각 회차 자체도 다항식만큼의 작업만 합니다(이름들에 대해 공리를 훑는 작업이므로), 그래서 분류 전체는 TBox 크기에 대해 다항식적입니다 — 이는 OWL 2 EL 추론기가 수십만 개의 개념을 가진 온톨로지인 SNOMED CT와 Gene Ontology까지 규모를 키울 수 있게 해 주는 PTIME 결과입니다 [1]. 우리 학계 세계는 단 세 라운드 만에 고정점에 도달합니다; 독립 실행은 그 상승 과정을 출력하는데, $S$와 $R$의 크기는 한 회차가 아무것도 바꾸지 못하는 바로 그 순간 얼어붙습니다(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

바로 위 행을 그대로 반복하는 마지막 행 — $|S| = 39$이고 $|R| = 7$이며, 둘 다 변화 없음 — 은 종료가 눈에 보이게 된 것입니다: 3라운드는 모든 규칙을 발동시키지만 아무것도 만들어 내지 못하고, 루프는 멈춥니다. 그 평평한 부분이 $T(X) = X$의 실행 가능한 형태입니다: 단조 연산자가 상태를 자기 자신으로 사상하는 순간, 그 상승은 끝난 것입니다.

실증적 교차 검증: 처음부터 만든 것과 HermiT의 대결

증명은 종이 위의 메타 논증일 뿐입니다; 그것은 이 파이썬 코드가 그 증명을 충실히 구현했는지에 대해서는 아무것도 말해 주지 않습니다. 전사(transcription) 실수, 가드의 하나 어긋난 계산, 빠진 규칙 사례 — 이런 것들은 수학에는 결코 나타나지 않습니다. 이를 위해 우리에게는 독립된 증인이 필요합니다. 동반 파일 reasoners.py는 owlready2로 동일한 학계 세계 온톨로지를 다시 만들고, sync_reasoner를 통해 HermiT를 그 위에서 실행하며(reasoners.py 99번째 줄), 처음부터 만든 classify()를 호출하고(136번째 줄), 두 분류가 "항목 하나하나까지" 일치한다고 단언합니다(reasoners.py 139–152번째 줄):

    print("Reasoner (HermiT via owlready2) vs. from-scratch EL completion")
    print(f"  from-scratch subsumptions : {len(el_subs)}")
    print(f"  HermiT subsumptions       : {len(r_subs)}")
    print(f"  from-scratch unsatisfiable: {sorted(el_unsat)}")
    print(f"  HermiT unsatisfiable      : {sorted(r_unsat)}")

    subs_agree = r_subs == el_subs
    unsat_agree = r_unsat == el_unsat
    ...
    assert subs_agree, ("subsumption mismatch", r_subs ^ el_subs)
    assert unsat_agree, ("unsat mismatch", r_unsat ^ el_unsat)
    print("\n  AGREEMENT CONFIRMED — the from-scratch reasoner matches HermiT.")

단언 메시지 안의 ^는 대칭 차집합(symmetric difference)을 설정합니다 — 두 추론기가 어긋나는 항목들입니다 — 그래서 실패한다면 정확히 무엇이 갈라졌는지를 출력할 것입니다. 그런 일은 결코 일어나지 않습니다. 커밋된 출력(python3 reasoners.py)은 말끔한 일치입니다:

Reasoner (HermiT via owlready2) vs. from-scratch EL completion
  from-scratch subsumptions : 8
  HermiT subsumptions       : 8
  from-scratch unsatisfiable: ['TenuredStudent', 'TenuredStudentAdvisor']
  HermiT unsatisfiable      : ['TenuredStudent', 'TenuredStudentAdvisor']

  subsumptions agree : True
  unsatisfiable agree: True

  AGREEMENT CONFIRMED — the from-scratch reasoner matches HermiT.

두 추론기 모두 동일한 8개의 포섭 관계 — Dean ⊑ Person, Professor, Researcher; Professor ⊑ Person, Researcher; Researcher ⊑ Person; Student ⊑ Person, Researcher — 를 찾아내며, 둘 다 동일한 2개의 충족 불가능한 개념, 즉 바닥 규칙이 제 몫을 하게 만드는 일부러 과잉 제약된 클래스인 TenuredStudent와 TenuredStudentAdvisor에 표시를 답니다. 독립된 두 개의 코드 경로 — 하나는 교과서의 완성 규칙을 그대로 옮겨 쓴 것이고, 다른 하나는 십 년간 다져진 엔진입니다 — 가 동일한 위계에 이릅니다.

독립된 오라클이 가장 강력한 검사인 이유

일치는 그 증인만큼만 설득력이 있으며, HermiT는 구할 수 있는 가장 좋은 증인입니다. 그것은 완전한 OWL 2 DL 추론기입니다 [3] — 그 결정 절차(하이퍼테이블로 계산법)는 OWL 2 DL 배후의 완전한 SROIQ 서술 논리를 위해 공학적으로 만들어져 있으며, 이는 우리 완성 알고리즘이 다루는 그 자그마한 EL 파편의 진(眞) 초집합입니다. 그래서 HermiT는 같은 맹점을 공유할 수도 있는 동일한 발상의 두 번째 사본이 아닙니다; 그것은 훨씬 더 큰 논리 위에서 완전히 다른 방법으로 포섭을 판정하며, 그러고도 여전히 동일한 8-대-2 답에 이릅니다(reasoners.py 독스트링, 12–16번째 줄: "a strict superset of EL, so agreement here is the strongest possible check"). owlready2 배포판에는 EL 특화 추론기인 ELK가 함께 담겨 있지 않습니다; 더 무겁고 더 일반적인 HermiT를 구동하는 것은 의도적인 선택인데, 초집합 오라클의 일치가 같은 파편을 다루는 도구의 일치보다 더 강한 증거이기 때문입니다 — 같은 파편이라면 같은 실수를 숨길 수도 있었을 것입니다. 처음부터 만든 구현과 독립적이고 더 강력한 추론기가 모든 항목에서 일치할 때, 둘 다가 같은 방식으로 틀렸을 잔여 가능성은 외부 검증이 줄 수 있는 것 중 가장 작은 축에 듭니다. 증명은 규칙이 옳다고 말해 주고, 오라클은 코드가 그 규칙을 충실히 옮긴 사본이라고 말해 줍니다.

아직 풀리지 않은 부분

정직한 경계는 이렇습니다. 건전성, 완전성, 종료라는 세 부분의 정확성은 알고리즘에 관한 메타 정리이지, 알고리즘이 자기 자신에 대해 확인하는 사실이 아닙니다. 추론기는 온톨로지를 분류하지만, 내부로부터는 자신의 규칙 집합이 자신이 구현하는 (⊥와 역할 사슬을 포함한) EL 파편에 대해 완전하다는 것을 증명하지 못하고, 증명할 수도 없습니다. 그 증명은 수학과 우리가 코드에 갖는 신뢰 안에 있으며, HermiT와의 교차 검증은 구현을 뒷받침할 뿐 정리를 뒷받침하지는 않습니다: 하나의 온톨로지에서의 일치가 모든 온톨로지에서의 일치를 인증해 줄 수는 없으며, 우연히 공유된 버그나 조용히 EL 바깥으로 미끄러진 온톨로지는 여전히 둘 다를 속일 수 있습니다. "규칙이 증명 가능하게 옳다"는 것과 "기계가 이 입력에 대해 그것이 옳음을 검증했다" 사이의 그 틈이, 바로 각 답과 함께 검사 가능한 정당화를 함께 산출함으로써 그것을 메우려 하는 증명 산출(proof-producing) 혹은 인증(certifying) 추론기가 좁히려는 바로 그 이음매입니다.

그리고 눈앞에 숨어 있는 더 큰 이야기가 있습니다. 이 규칙들이 어떻게 작동하는지를 다시 돌아보십시오: 우리의 방법 전체는 귀결을 곧바로 도출하는 것이었습니다 — 단언된 공리에서 시작하여, 참을 보존하는 규칙을 발동시키고, 포화시키는 것이지, 테이블로 추론기가 하는 것처럼 부정을 가정하고 모순을 뒤쫓는 것이 아니었습니다. 그 전진하는, 모순 없는 방식에는 이름이 있습니다. 귀결 기반 추론(consequence-based reasoning)이며, 이것이 정확히 EL에게 그 다항 시간 보장을 사 주는 것입니다. 그것이 이 부(part)의 마지막 정거장입니다.

왜 중요한가

건전성과 완전성이야말로 신경-기호(neuro-symbolic) AI의 상징적인 절반이 그 취약함을 감수할 가치가 있는 온전한 이유입니다. 학습된 모델은 모든 질의에 답하지만 자신 있게 틀릴 수 있습니다; 건전하고 완전한 추론기는 더 좁은 질문에 답하지만, 그것의 "예"는 하나의 보증이고 그것의 "아니오"는 "따라 나오지 않는다"를 뜻하며, 그것으로 끝입니다. 그 확실성이야말로 신경망 근사가 반드시 그것에 견주어 측정되어야 하는 것입니다: 훗날 어떤 미분 가능한 혹은 임베딩 기반의 추론기가 그럴듯함(plausibility)에 따라 포섭 관계의 순위를 매길 때, 여기서 인증된 8개의 정확한 포섭 관계와 2개의 정확한 충족 불가능성은 그 유연한(soft) 모델이 어긋났는지를 말해 주는 정답(ground truth)입니다 — 그리고 역할을 통해 거꾸로 전파된 모순인 TenuredStudentAdvisor의 장거리 충족 불가능성은, 유연한 모델이 놓치기 쉬운 바로 그런 종류의 추론입니다. 결정 절차는 학습하는 절반이 근사하려고 애쓰는 명세이며, 정확한 답에 견주지 않고서는 어떤 근사가 좋은지 말할 수 없습니다. 그 규칙들이 충분하다는 것을, 그리고 왜 그런지를 아는 것이야말로, 완성 알고리즘을 그저 우연히 맞아 보였던 또 하나의 발견법이 아니라, 그런 잣대로 쓸 수 있게 해 주는 것입니다.

핵심 용어

• 결정 절차(Decision procedure) — 모든 입력에 대해 멈추어 올바른 예/아니오 답을 내놓는 알고리즘; 포섭에 대해서는 건전성, 완전성, 종료를 함께 요구합니다.
• 건전성(Soundness) — 함의된 포섭 관계만을 도출합니다($B \in S(A) \Rightarrow \mathcal{T} \models A \sqsubseteq B$); 모든 규칙이 모든 모델에서 보존하는 불변량으로 증명됩니다.
• 완전성(Completeness) — 함의된 모든 포섭 관계를 도출합니다(충족 가능한 $A$에 대해 $\mathcal{T} \models A \sqsubseteq B \Rightarrow B \in S(A)$); 도출되지 않은 모든 포섭 관계를 반증하는 표준 모델로 증명됩니다.
• 종료(Termination) — 포화 루프는 언제나 멈춥니다. $S$와 $R$이 $\le |N_R| \cdot |N|^2$의 다항식 상한 안에서 단조롭게 자라기 때문입니다.
• 함의 $\mathcal{T} \models A \sqsubseteq B$ — TBox의 모든 모델에서 그 포섭 관계가 성립합니다; 구문적 검사 $B \in S(A)$가 반드시 맞추어야 할 의미론적 목표입니다.
• 표준 모델(Canonical model) — 포화된 $S$와 $R$로부터 곧바로 구축되는 하나의 해석으로, $\mathcal{T}$를 충족시키면서도 규칙이 도출하지 못한 모든 것의 실패를 증언합니다.
• 오라클(HermiT) — EL의 진(眞)초집합 위에서 작동하는 완전한 OWL 2 DL 추론기로, 처음부터 만든 분류가 옳다는 독립된 증인으로 쓰입니다.
• 대칭 차집합(Symmetric difference)(파이썬의 ^ 연산자) — 두 분류가 어긋나는 항목들의 집합; 여기서는 텅 비어 있으며, 그래서 일치가 확인되는 것입니다.

이 장이 이끄는 곳

우리는 완성 알고리즘에 대한 고리를 닫았습니다: 증명 가능하게 건전하고, 완전하며, 종료하는 규칙들이, 모든 항목에서 그것들과 일치하는 제품용 추론기에 의해 뒷받침됩니다. 그러나 그것들이 어떻게 작동하는지를 다시 눈여겨보십시오 — 그것들은 결코 추측하지 않고, 결코 부정을 가정하지 않으며, 결코 테이블로를 만들어 역추적하지 않습니다. 그것들은 단언된 것에서 시작하여 아무것도 새로 나타나지 않을 때까지 귀결을 갈아 나가는, 하나의 단조로운 고정점 상승입니다. 다음 장인 귀결 기반 추론은 그 방식에 제 이름을 붙여 주고, 모순을 찾아 헤매는 대신 귀결을 곧바로 도출하는 것이 정확히 무엇 때문에 EL에게 그 다항 시간 분류를 사 주는지를 보여 줍니다 — 우리가 계속 읽어 온 바로 그 포화 흔적을, 이제는 일반적이고 강력한 추론 패러다임의 한 사례로서 보게 됩니다.