정당화: 최소 증명과 핀포인팅

📍 현재 위치: I부 · 증명, 충실성, 신뢰 — 1장. 4권의 솔직한 평결은 미분 가능한 논리가 사들이는 것이 신뢰가 아니라 학습이라고 인정했습니다. 이 권은 신뢰의 최소 단위, 곧 확인 가능한 이유를, 우리가 가진 가장 명확한 토대인 2권의 기호 추론기 위에 세우는 것으로 시작합니다.

2권의 EL 완성 알고리즘은 성립하는가라는 질문에 답합니다: 고정점(fixpoint)을 돌리고 포화된 표를 읽으면, 학계 TBox(terminological box, 용어 상자: 온톨로지의 개념 수준 공리들)는 Professor ⊑ Researcher를 함의합니다(모든 교수는 연구자입니다; 기호 ⊑는 개념 포섭(subsumption)이며, 2권의 주력 도구입니다). 5권은 그보다 더 많은 것을 요구하는 데서 시작합니다. 2권의 거대한 임상 온톨로지 SNOMED CT(체계화된 의학 용어 임상 명명법, Systematized Nomenclature of Medicine, Clinical Terms)의 뜻밖의 포섭을 마주한 임상의, 온톨로지가 방금 어떤 개념을 충족 불가능하다고 분류해 버린 엔지니어, 신경-기호 시스템이 주장하는 도출을 감사하는 심사자, 이들 모두는 왜를 묻지만 수백 개의 항목이 담긴 고정점 표는 그 누구에게도 도움이 되지 않습니다. 이들에게 필요한 것은 정당화(justification)입니다: 결론에 책임이 있는 정확하고 최소적인 공리 집합으로, 읽을 수 있을 만큼 작고, 그 자체로 함의를 강제할 만큼 강하며, 구성원을 어느 하나라도 제거하면 무너질 만큼 빈틈이 없습니다. 이 장은 그 대상을 정확하게 정의하고, 그것을 위한 두 가지 알고리즘을 구축하며(확장-축소로 정당화 하나를 찾고, 모델 기반 진단(model-based diagnosis)에서 내려온 적중 집합 트리로 정당화 전부를 찾습니다 [1]), 둘 다 2권의 추론기를 봉인된 블랙박스로 두고 그에 맞서 실행한 다음, 렌즈를 뒤집습니다: 원치 않는 함의의 정당화들은 보수(repair)가 반드시 건드려야 할 공리들을 정확히 지목합니다. 모든 주장은 실행 가능하며, 우리의 14개 공리 세계에서는 그 열거가 가능한 16,384개의 부분 온톨로지 전체에 대해 정확히 검사됩니다.

쉽게 말하면

열네 개의 문서로 이루어진 사건 기록에 판결이 얹혀 있다고 상상해 보십시오. 판사는 기록 전체를 다시 읽고 싶어 하지 않습니다. 판사가 원하는 것은 그래도 판결을 강제하는 최소한의 증거물 집합, 즉 그중 단 하나라도 빼면 판결이 더 이상 따라 나오지 않게 되는 집합입니다. 그 최소 증거물 집합이 바로 정당화입니다. 하나의 사건에는 서로 독립된 결정적 증거 뭉치가 여럿 있을 수 있습니다: 각각 단독으로 유죄를 입증하는, 서로 다른 세 문서짜리 묶음 두 개처럼 말입니다. 그리고 여러분이 변호인이라면 그 쌍대성은 정확합니다: 판결을 뒤집으려면 모든 묶음 하나하나에서 적어도 한 문서의 신빙성을 무너뜨려야 하는데, 온전히 남은 묶음이 하나라도 있으면 그것만으로도 유죄가 성립하기 때문입니다. 묶음 하나를 찾는 것, 그것들을 전부 찾는 것, 그리고 공격할 문서의 가장 값싼 집합을 고르는 것, 이 셋이 이 장의 세 가지 알고리즘입니다.

이 장에서 다루는 내용

정당화, 정의와 대조: 온톨로지의 최소 함의 부분집합이란 무엇이며, 왜 그것이 증거의 옳은 단위인지, 그리고 그것이 1권과 2권이 이미 만들어 내는 도출과 grandAdvisor 예제 위에서 어떻게 다른지를 다룹니다.
블랙박스 오라클 규율: 이 장 어디서든 쓰이는 유일한 원시 연산은 "이 공리 부분집합이 결론을 함의하는가?"이며, 이는 2권의 정규화-완비를 그 부분집합 위에서 다시 실행하여 구현됩니다. 블랙박스 핀포인팅이 어떤 추론기에도 통하는 이유와, 글래스박스 방법이 그 대신 무엇을 사 오는지를 다룹니다.
확장-축소로 찾는 정당화 하나: 축소 루프, 그것이 유지하는 불변량, 단 한 번의 삭제 패스가 최소 집합을 산출한다는 증명, 그리고 단일 삭제 인증을 커밋된 출력과 함께 다룹니다.
Reiter의 적중 집합 트리로 찾는 정당화 전부: 그 트리를 형식화하기 전에 먼저 해독하고, 완전성 논증을 남김없이 전개하며, 가지치기 규칙과 $2^{14}$ 개 공리 부분집합 전체에 대한 무차별 대입과의 정확한 일치 검사를 다룹니다.
디버깅으로서의 핀포인팅: TenuredStudent ⊑ ⊥의 정당화를 공리 하나하나 짚어 읽고, 보수가 정확히 정당화 모임의 적중 집합이라는 정리, 그리고 최소 보수에 천장을 씌우는 NP-난해성을 다룹니다.
정직한 규모의 장부: EL에서조차 지수적으로 많은 정당화가 존재할 수 있으며, 이 분야가 쥔 지렛대들(모듈, 글래스박스 추적, 증명 기반 열거) 각각을 정확한 한 단락씩으로 다룹니다.

도출에서 증거로

1권의 전방 연쇄기와 2권의 완성 알고리즘은 둘 다 도출(derivation)을 만들어 냅니다: 결론에 이르러 끝나는 규칙 발동들의 수열입니다. 도출은 어떤 함의가 성립한다는 완벽하게 훌륭한 증인이지만, 두 가지 이유로 증거의 단위로서는 빈약합니다. 첫째, 도출은 규칙의 적용, 즉 특정한 하나의 절차가 남긴 흔적을 이름 붙일 뿐입니다; 건전성을 갖춘 다른 추론기라면 같은 사실에 대해 다른 도출을 내놓을 것이므로, 도출은 지식 못지않게 알고리즘에 대해서도 말해 줍니다. 둘째, 더 나쁘게도, 도출의 그 무엇도 최소적이지 않습니다: 1권의 전방 연쇄기는 지식 베이스 전체를 포화시키므로, grandAdvisor(alice, carol)을 담은 폐쇄(closure)에는 그 사실과 아무 관련도 없는 모든 동료 관계 사실과 인용의 이행적 폐쇄 전체까지도 함께 담기게 됩니다.

그 예를 자세히 들여다보십시오, 이미 그 안에 개념 전체가 들어 있으니까요. 1권의 kb.py에서 사실 grandAdvisor(alice, carol)은 정확히 세 개의 진술로부터 도출됩니다: 두 사실 advises(alice, bob)과 advises(bob, carol), 그리고 규칙 하나 grandAdvisor(X, Z) :- advises(X, Y), advises(Y, Z)입니다. 그 세 원소 집합이 바로 증거입니다. 그것은 그 자체로 결론을 함의하며, 셋 중 어느 하나(지도 사실 둘 중 하나, 또는 규칙)라도 빼면 더 이상 그것을 함의하지 않는 지식 베이스가 남습니다. 이 예제에서 도출과 증거 집합이 일치하는 것은 예제가 아주 작기 때문일 뿐입니다; 일반화되는 개념은 증거 집합, 그리고 그것을 설득력 있게 만드는 성질, 즉 그것을 더 이상 줄일 수 없다는 성질입니다.

이제 정의를 쓰되, 쓰기 전에 먼저 풀어서 해독합니다. $O$ 를 온톨로지(ontology), 즉 공리들의 유한 집합이라고 합시다; 이 장에서 $O$ 는 2권의 학계 TBox이며, 그 크기, 즉 $O$ 가 담은 공리의 개수를 $\lvert O \rvert$ 라고 쓰면 그 값은 $14$ 입니다. $\alpha$ 를 후보 귀결이라고 합시다. 여기서는 언제나 이름 붙은 두 개념 사이의 포섭이며, $A \sqsubseteq B$ ("모든 $A$ 는 $B$ 이다")라고 씁니다. 기호 $\models$ 는 의미론적 함의(semantic entailment)입니다: $O \models \alpha$ 는 $O$ 의 모든 공리를 충족하는 모든 해석이 $\alpha$ 도 충족한다는 뜻입니다. 기호 $\subseteq$ 는 집합 포함(set inclusion)이고, $\subsetneq$ 는 진부분(proper) 포함, 즉 전체 집합이 아닌 부분집합이며, 한정 기호 $\forall$ 는 "모든 ~에 대하여"라고 읽고, 기호에 그은 사선은 부정을 뜻하므로 $\not\models$ 는 "함의하지 않는다"라고 읽습니다. 그러면:

J \text{ is a justification for } O \models \alpha \quad\text{iff}\quad J \subseteq O, \qquad J \models \alpha, \qquad \text{and} \qquad \forall\, J' \subsetneq J:\; J' \not\models \alpha .

이 세 개의 연언지(conjunct)는 이렇게 읽힙니다: $J$ 는 실제로 온톨로지 안에 있는 공리만을 사용하고; $J$ 는 그 자체로 결론을 강제하며; $J$ 의 어떤 진부분집합도 여전히 그것을 강제하지는 못합니다. 문헌은 $J$ 를 MinA(최소 공리 집합, minimal axiom set)라고도 부르며, $\alpha$ 가 어떤 개념이 충족 불가능하다고 말하는 특수한 경우( $A \sqsubseteq \bot$ , 여기서 $\bot$ 은 공허 개념입니다)에는 MUPS(최소 충족 불가능성 보존 하위 TBox, minimal unsatisfiability-preserving sub-TBox)라고 부릅니다; 이 대상에 이름을 붙이고 그것이 섬기는 디버깅 문제를 제기한 지점이 바로 공리 핀포인팅(axiom pinpointing)이 시작된 곳입니다 [2]. 이 정의가 언급하지 않는 것에 주목하십시오: 규칙도, 증명 트리도, 그 어떤 추론기도 없습니다. 정당화는 오직 온톨로지와 결론만의 성질이며, 바로 그 점이 정당화를 설명을 위한 옳은 단위로(사람이 작은 공리 집합을 감사할 수 있으므로), 디버깅을 위한 옳은 단위로(원치 않는 결론의 정당화들이 결함의 위치를 좁혀 주므로), 그리고 이 권의 나머지 전체를 위한 옳은 단위로(충실성 프로브는 대조할 정답, 즉 "진짜 이유"를 필요로 하는데, 이것이 바로 그것이므로) 만들어 줍니다.

정의의 한 가지 귀결을 지금 유도해야 합니다, 뒤이은 세 개의 논증이 그것에 기대기 때문입니다. EL에서의 함의는, 이 시리즈의 다른 모든 서술 논리에서와 마찬가지로 단조적(monotone)입니다: 공리를 더한다고 해서 귀결이 사라지는 일은 결코 없습니다. 정확히 말하면, $J \subseteq J'$ 이고 $J \models \alpha$ 이면 $J' \models \alpha$ 입니다. 증명은 의미론 한 문장으로 끝납니다: $J'$ 의 모든 공리를 충족하는 어떤 해석이든 특히 $J$ 의 모든 공리도 충족합니다( $J$ 의 원소는 모두 $J'$ 에 들어 있으므로); 따라서 $J \models \alpha$ 이므로 $\alpha$ 도 충족합니다. 단조성에는 우리가 끊임없이 쓰게 될 대우 명제가 있습니다: 더 큰 집합이 함의에 실패한다면, 그것의 모든 부분집합도 마찬가지로 실패합니다.

단조성은 곧바로 이 장에서 가장 값싼 정리인 단일 삭제 인증(drop-any-one certificate)을 사 옵니다. $J \models \alpha$ 이고, $J$ 안의 모든 공리 $i \in J$ 에 대해(기호 $\in$ 는 "~의 원소이다"라고 읽습니다) 단일 삭제 집합 $J \setminus \{i\}$ ( $J$ 에서 공리 $i$ 를 제거한 집합)가 $\alpha$ 를 함의하는 데 실패한다고 합시다. 그러면 $J$ 는 단일 삭제로 얻은 부분집합들뿐 아니라 모든 진부분집합에 대해 최소적입니다. 그 이유는 이렇습니다: 어떤 $J' \subsetneq J$ 가 $\alpha$ 를 함의한다고 가정해 봅시다. $J'$ 는 진부분집합이므로 적어도 하나의 공리 $i \in J \setminus J'$ 를 빠뜨리며, 따라서 $J' \subseteq J \setminus \{i\}$ 입니다. $J' \models \alpha$ 에 단조성을 적용하면 $J \setminus \{i\} \models \alpha$ 가 강제되는데, 이는 공리별 검사와 모순됩니다. 그러므로 $\lvert J \rvert$ 번의 오라클 검사가 $2^{\lvert J \rvert}$ 개의 모든 부분집합에 맞서 최소성을 인증합니다. 이것이 바로 companion 코드가 자신이 반환하는 모든 정당화에 대해 실행하는 감사입니다.

하나의 대상, 세 가지 쓰임: 최소 증거로서의 정당화(왼쪽), 그중 하나를 찾는 확장-축소 탐색(가운데), 그리고 그 전부를 찾아 보수의 값을 매기는 적중 집합 트리(오른쪽). 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

오라클 규율: 하나의 원시 연산, 어떤 추론기든

이 장의 모든 것은 블랙박스 공리 핀포인팅(black-box axiom pinpointing)입니다: 추론기는 결코 열리지도, 계측되지도, 스스로를 설명하도록 신뢰받지도 않습니다. 아래의 어떤 알고리즘이든 호출할 수 있는 유일한 원시 연산은 함의 오라클(entailment oracle)이며, 이는 하나의 모양을 한 하나의 함수입니다: 공리 부분집합과 후보 포섭이 주어졌을 때, 그 부분집합이 그것을 함의하는가? companion 코드는 주어진 공리들 정확히 그 위에서 2권의 처음부터 작성한 EL 기계 장치를 다시 실행하여 이 오라클을 구현합니다: normalize는 그것들을 네 가지 정규형으로 다시 쓰고(el_completion.py 69–154번째 줄), complete는 완성 규칙 CR1–CR4, 바닥 규칙, 역할 사슬 규칙으로 포섭자 표 $S$ 를 포화시키며(el_completion.py 177–261번째 줄), 답은 포화된 $S$ 에서 읽어 냅니다. 그 장부 정리까지 갖춘 래퍼는 다음과 같습니다(justifications.py 100–129번째 줄):

STATS = {"saturations": 0, "oracle_calls": 0}
_SAT_CACHE: dict = {}   # frozenset of axiom ids -> saturated subsumer map S


def _saturate(ids: frozenset):
    """The saturated subsumer map S of the sub-TBox {axiom ids}: Volume 2's
    normalize + complete run on exactly those axioms (memoized per subset)."""
    if ids not in _SAT_CACHE:
        normalized, _fresh = elc.normalize([AXIOMS[i - 1] for i in sorted(ids)])
        S, _R = elc.complete(normalized)
        _SAT_CACHE[ids] = S
        STATS["saturations"] += 1
    return _SAT_CACHE[ids]

def is_entailed(ids, sub: str, sup: str) -> bool:
    """The oracle every algorithm below is built on: does the axiom SUBSET
    ``ids`` (1-based ids into AXIOMS) entail ``sub ⊑ sup``?"""
    STATS["oracle_calls"] += 1
    return _entailed_by(_saturate(frozenset(ids)), sub, sup)

래퍼의 두 가지 세부 사항이 결정적인 무게를 지닙니다. 첫째, _entailed_by(justifications.py 115–122번째 줄)는 "상위 개념이 $S(\text{sub})$ 안에 있는가"를 넘어서는 의미론적 조항 하나를 더합니다: $\bot \in S(\text{sub})$ 이면 그 개념은 충족 불가능하고, 그 외연은 모든 모델에서 공집합이며, 공집합은 모든 것의 부분집합이므로, 충족 불가능한 개념은 모든 개념에 포섭됩니다. 그 조항이 없다면 $A \sqsubseteq \bot$ 질의에 대한 핀포인팅은 소리 없이 의미론과 어긋날 것입니다. 둘째, 메모이제이션 캐시 _SAT_CACHE는 포화(saturation)의 횟수를 오라클 호출의 횟수와 따로 셉니다: 아래의 알고리즘들은 같은 부분집합에 대해 자주 다시 묻게 되며, 커밋된 실행은 실제로는 단 90번의 포화만으로 232번의 함의 호출에 답합니다. 각 포화는 다항 시간 절차를 한 번 온전히 실행하는 것이므로, 오라클 호출은 값싸기는 하지만 공짜는 아니며, 이 장의 모든 알고리즘은 오라클 호출 수로 값이 매겨질 것입니다.

왜 굳이 블랙박스를 고집할까요? 그것이 도구 전체를 추론기로부터 독립적으로 만들어 주기 때문입니다. 여기서 오라클은 마침 2권의 처음부터 작성한 완성 엔진이지만, 그것은 ELK든, HermiT든, Konclude든, 그 논리에 대해 건전하고 완전한 어떤 결정 절차든 될 수 있으며, 핀포인팅 코드는 단 한 줄도 바뀌지 않을 것입니다. 그 이식성이야말로 블랙박스 탐색을 OWL DL(Web Ontology Language, 웹 온톨로지 언어의 서술 논리 프로파일)에 대한 정당화를 찾는 실용적인 경로로 만들어 준 이유입니다. OWL DL의 추론기들은 거대하고, 고도로 최적화되어 있으며, 스스로를 설명하도록 지어지지 않았기 때문입니다 [3]. 그 대안은 글래스박스 핀포인팅(glass-box pinpointing)입니다: 추론기를 열어 모든 추론이 자신이 사용한 공리를 기록하는 라벨을 지니게 만들어서, 결론이 나타날 때 그것이 핀포인팅 논리식(pinpointing formula), 즉 공리 변수들에 대한 단조 불리언 논리식을 걸치고 도착하도록 하는 것입니다. 이 논리식을 최소로 충족시키는 진리값 배정이 정확히 정당화들입니다 [4]. 글래스박스 방법은 오라클 호출마다가 아니라 추론 중 단 한 번만 값을 치르지만, 각 추론기 안에 새로 공학적으로 지어져야 하고 그 추론기의 최적화를 뒤틀 수도 있습니다. 그 거래는 규모를 다루는 절에서 다시 돌아올 것입니다; 여기서는 일부러 블랙박스에 머무릅니다. 5권이 이후 여섯 개 부에 걸쳐 시스템을 불투명한 오라클로 다루는 데 시간을 쓸 것이며, 이 장이 바로 그 규율을 가장 순수한 형태로 보여 주기 때문입니다.

정당화 하나: 확장과 축소

첫 번째 알고리즘은 정당화 하나를 찾으며, 두 개의 루프로 이루어져 있습니다. 확장(expand): 고정된 순서로 공리를 더해 가며 지지 집합(support set)을 키우다가, 오라클이 처음으로 함의한다고 말하는 순간 멈춥니다; 그 앞부분(prefix)은 함의 집합이지만, 보통은 최소성과는 거리가 멉니다. 축소(contract): 지지 집합을 공리 하나씩 훑습니다; 그 공리를 잠정적으로 삭제하고, 함의가 살아남는지 오라클에 묻고, 살아남으면 삭제를 확정하고 그렇지 않으면 되돌립니다. 축소 패스는 공리 핀포인팅의 창시 논문이 제기한 디버깅 문제를 섬깁니다 [2]; 삭제 루프 자체는, 확장-축소 탐색 안에 담긴 채로(원 논문은 두 단계를 expand와 shrink라고 부릅니다), 블랙박스 정당화 추출을 실용적으로 만든 바로 그것입니다 [3]. 커밋된 두 루프는 다음과 같습니다(justifications.py 150–155번째 줄과 158–162번째 줄; 그 사이와 뒤의 로그 장부 정리는 생략했습니다):

    # -- Expand ------------------------------------------------------------
    support: list = []
    for i in sorted(ids):
        support.append(i)
        if is_entailed(support, sub, sup):
            break

    # -- Contract (deletion-based) ------------------------------------------
    just = set(support)
    for i in list(support):
        if is_entailed(just - {i}, sub, sup):
            just.discard(i)

왜 단 한 번의 패스로 충분할까요? 루프는 하나의 불변량(invariant)을 유지합니다: 어느 시점에서든 작업 집합 just는 $\alpha$ 를 함의합니다. 이는 진입 시점에 성립하고(확장이 처음으로 함의하는 앞부분에서 멈추었으므로), 확정된 모든 삭제는 오라클로 확인되었으므로 종료 시점에도 성립합니다: 결과는 함의합니다. 최소성은 더 미묘한 절반입니다, 루프가 각 공리를 단 한 번, 최종 결과가 아니라 그 순간의 작업 집합이 무엇이었든 그것에 맞서서만 검사하기 때문입니다. 단조성이 이 틈을 메워 줍니다. 반환된 집합을 $R$ 이라 쓰고 임의의 공리 $i \in R$ 을 잡읍시다. 루프가 $i$ 를 검사했을 때 그 작업 집합 $W$ 는 $W \supseteq R$ 을 만족했으며(상위집합 기호 $\supseteq$ 는 $W$ 가 $R$ 의 모든 원소를 담고 있다는 뜻으로, 집합은 루프가 진행됨에 따라 줄어들기만 하고 $R$ 안의 모든 것은 끝까지 살아남았으므로 성립합니다), 검사는 실패했습니다: $W \setminus \{i\} \not\models \alpha$ 이며, 이것이 $i$ 가 유지된 이유입니다. 이제 $R \setminus \{i\} \subseteq W \setminus \{i\}$ 이고, 단조성의 대우(함의하지 않는 집합은 함의하는 부분집합을 갖지 않는다)로부터 $R \setminus \{i\} \not\models \alpha$ 가 나옵니다. 이것이 바로 모든 $i \in R$ 에 대한 단일 삭제 조건이며, 첫 절의 인증 정리가 이를 완전한 최소성으로 격상시킵니다: $R$ 은 정당화입니다. companion 코드는 이 논증을 그저 신뢰하고 마는 것이 아니라, 반환하기 전에 공리당 오라클 호출 한 번씩으로 그 인증을 명시적으로 다시 실행합니다(justifications.py 168–173번째 줄):

    # -- The minimality audit (per axiom, against the oracle) ----------------
    assert is_entailed(result, sub, sup), "contraction destroyed the entailment"
    for i in sorted(result):
        assert not is_entailed(result - {i}, sub, sup), (
            f"not minimal: axiom ({i}) is redundant in {fmt_just(result)}")

질의 Dean ⊑ Researcher에 대한 커밋된 추적은 모든 결정을 보여 줍니다:

[2] ONE justification by expand-contract — query: Dean ⊑ Researcher
  expand   : support grows in axiom order; axioms 1..8 first entail the query (support size 8)
  contract : (1) dropped  (2) dropped  (3) dropped  (4) KEPT  (5) KEPT  (6) dropped  (7) dropped  (8) KEPT
  MinA     : {4, 5, 8}
  audit    : dropping any single axiom of the MinA breaks the entailment (asserted, per axiom, for every query)

축소 과정을 하나의 이야기처럼 읽어 봅시다. 지지 집합은 공리 1부터 8까지, 즉 처음으로 함의하는 앞부분입니다. 공리 1(Professor ⊑ Researcher)을 삭제해도 함의는 살아남는데, 두 번째 경로가 존재하기 때문입니다: Dean ⊑ Professor, Professor ⊑ ∃advises.Student, 그리고 ∃advises.⊤ ⊑ Researcher가 여전히 사슬을 이루어 결론에 이릅니다. 공리 2, 3, 6, 7은 애초에 아무 상관이 없었다는 더 단순한 이유로 탈락합니다. 공리 4, 5, 8은 각각 제거되면 함의를 깨뜨리므로 각각 유지되며, 그 결과가 세 공리짜리 우회로 {4, 5, 8}입니다. 이 알고리즘의 답이 삭제 순서에 따라 달라진다는 점에 주목하십시오: 만약 루프가 공리 1보다 공리 4를 먼저 시도했다면, 대신 두 공리짜리 정당화 {1, 8}을 찾았을 것입니다. 확장-축소는 어떤 정당화 하나를 약속할 뿐, 결코 정준적이거나 가장 작은 것을 약속하지는 않습니다.

비용 계산은 깔끔합니다. $n = \lvert O \rvert$ 를 온톨로지의 크기라 합시다. 확장은 많아야 $n$ 번의 오라클 호출을 하고(앞부분마다 한 번씩), 축소는 정확히 $\lvert \text{support} \rvert \le n$ 번을 호출하며, 감사는 $1 + \lvert R \rvert$ 번을 더 호출하므로, 정당화 하나의 비용은 초기 함의 검사까지 포함해 많아야 $2n + \lvert R \rvert + 2$ 번의 오라클 호출입니다. 이 횟수는 $n$ 에 대해 선형으로 자라며, 증가율을 나타내는 빅오(big-O) 표기법으로 $O(n)$ 이라고 씁니다(온톨로지를 가리키는 글자 $O$ 와의, 표준적이지만 아쉬운 충돌입니다). 그 각각의 호출은 다항 시간 포화입니다. 하나의 이유를 찾는 일은 진정으로 값쌉니다. 전부를 찾는 일에서 비로소 구조가, 그리고 비용이 나타납니다.

정당화 전부: Reiter의 적중 집합 트리

왜 정당화 하나로는 충분하지 않을까요? 커밋된 실행은 온톨로지 자체로 답합니다. 함의 Professor ⊑ Researcher는 두 개의 정당화를 가집니다: 직접 공리 {1}, 그리고 우회로 {4, 5}(교수는 어떤 학생을 지도하고, 무언가를 지도하는 것은 무엇이든 연구자입니다). 이 중복은 실제 사실이지 이 장을 위해 꾸며낸 것이 아닙니다: 2권의 ontology.py는 공리 5에 대한 주석에서 완성 규칙이 4와 5로부터 공리 1을 다시 도출한다는 것을 짚습니다. 정당화에 근거해 행동하려는 이에게 이 사실이 주는 결과는 즉각적입니다: 공리 1을 삭제해도 함의는 다른 이유에 떠받쳐져 여전히 성립합니다. 설명은 때로 이유 하나만 보여 주는 것으로 충분할 수 있지만, 디버깅은 그럴 수 없습니다. 정당화 하나를 죽이면서 다른 하나는 살려 두는 보수는 아무것도 고친 것이 없기 때문입니다. 우리에게는 완전한 집합이 필요합니다.

정당화 전부를 찾는 고전적 경로는 Reiter의 적중 집합 트리(hitting-set tree, HST)이며, 모델 기반 진단(model-based diagnosis)에서 들여와 [1] 온톨로지에 맞게 각색된 것입니다 [3]. 형식화하기 전에 먼저 그 발상을 해독해 봅시다. 우리는 이미 정당화 하나 $J$ 를 찾았습니다. 다른 정당화 $J^{*}$ 는 어디에 숨어 있을 수 있을까요? $J^{*} \ne J$ 이고 둘 다 최소적이므로 어느 하나가 다른 하나를 포함할 수는 없으며, 따라서 $J^{*}$ 는 $J$ 의 공리 중 적어도 하나를 빠뜨려야 합니다. 그러므로: $J$ 안의 각 공리 $i \in J$ 에 대해, 온톨로지에서 $i$ 를 삭제하고 나머지를 탐색합니다. 다른 어떤 정당화든 이 삭제들 중 적어도 하나에서는 살아남을 것이고, 그 가지에서 발견될 것입니다. 이를 재귀적으로 반복하면 탐색 공간은 하나의 트리가 됩니다: 각 노드는 그 경로상의 삭제들을 뺀 온톨로지의 정당화로 라벨이 붙고; 각 간선은 부모 라벨의 공리 하나를 삭제하며; 닫힌 잎(closed leaf)은 남은 공리들이 더 이상 함의하지 않는 노드로, 그 경로의 삭제 집합이 모든 정당화를 적중시켰다는 뜻입니다. 커밋된 핵심부는 다음과 같습니다(justifications.py 195–219번째 줄):

    root = single_justification(ids, sub, sup)
    if root is None:
        return set(), 0
    justs: list = [root]          # discovery order (kept for determinism)
    expanded: set = set()         # hitting sets (paths) already handled
    nodes = 1
    queue: list = [(root, frozenset())]   # (node label, deletions so far)
    while queue:
        label, deleted = queue.pop(0)     # FIFO: breadth-first, deterministic
        for i in sorted(label):
            path = deleted | {i}
            if path in expanded:          # early path termination
                continue
            expanded.add(path)
            nodes += 1
            reuse = next((j for j in justs if not (j & path)), None)
            if reuse is not None:         # node-label reuse: no oracle work
                queue.append((reuse, path))
                continue
            j = single_justification(ids - path, sub, sup)
            if j is None:
                continue                  # closed leaf: path hits every MinA
            justs.append(j)
            queue.append((j, path))
    return set(justs), nodes

이제 완전성 논증을 남김없이 전개합니다, 이것이 이 구성 전체가 딛고 선 정리이기 때문입니다. $J^{*}$ 를 $O \models \alpha$ 의 임의의 정당화라 합시다. 주장: 트리의 어떤 노드는 정확히 $J^{*}$ 로 라벨이 붙습니다. 다음과 같이 고른 경로를 따라가 봅시다. 뿌리에서 시작하는데, 그 삭제 집합은 $D = \emptyset$ (공집합)이며, $J^{*}$ 와 서로소(disjoint)입니다. 라벨 $J$ 와 삭제 집합 $D$ 가 $D \cap J^{*} = \emptyset$ 을 만족하는 임의의 노드에서(교집합 기호 $\cap$ 은 공통 원소들을 모으며, 서로소라는 것은 이 경로에서 $J^{*}$ 의 어떤 공리도 삭제되지 않았다는 뜻입니다): $J = J^{*}$ 이면 끝입니다. 그렇지 않다면 $J \ne J^{*}$ 이며, 최소성은 양방향으로 작동합니다: $J \subsetneq J^{*}$ 이면 $J^{*}$ 의 최소성과 모순되고, $J \supsetneq J^{*}$ 이면 $J$ 의 최소성과 모순되므로, 어느 하나가 다른 하나를 포함할 수 없고 차집합 $J \setminus J^{*}$ 는 공집합이 아닙니다. $i \in J \setminus J^{*}$ 를 하나 골라 $i$ 를 삭제하는 간선을 따라갑니다. 자식 노드의 삭제 집합 $D \cup \{i\}$ (합집합 기호 $\cup$ 은 두 집합의 원소를 한데 모읍니다)는 여전히 $J^{*}$ 와 서로소입니다( $J^{*}$ 바깥에서 $i$ 를 골랐으므로), 따라서 남은 온톨로지 $O \setminus (D \cup \{i\})$ 는 여전히 $J^{*}$ 전체를 담고 있고, 단조성에 의해 $\alpha$ 를 함의하며, 그러므로 그 자식 노드는 닫히지 않고 어떤 정당화로 라벨이 붙습니다. 이를 반복합니다. 각 단계는 유한집합 $O \setminus J^{*}$ 에서 뽑은 공리 하나만큼 $D$ 를 키우므로, 많아야 $\lvert O \rvert - \lvert J^{*} \rvert$ 번의 단계 뒤에는 그 걸음이 반드시 멈추어야 하며, 멈추는 유일한 경우는 $J = J^{*}$ 일 때뿐입니다. 모든 정당화가 어떤 노드에 라벨을 붙이며, 트리는 그 전부를 찾아냅니다. 탐색 전체의 종료성도 같은 유한성에서 나옵니다: 모든 경로의 삭제 집합은 유한한 온톨로지 안에서 엄격히 커지기만 하기 때문입니다.

코드 안의 두 가지 최적화는 장식이 아닙니다; 이들은 Reiter의 트리와 함께 도입되어 온톨로지 각색판에도 그대로 남은, 하중을 떠받치는 가지치기입니다 [1][3]. 이른 경로 종료(early path termination): 같은 공리 집합을 삭제하는 두 경로는 동일한 부분 문제로 이어지므로(순서가 아니라 집합만이 중요합니다), 이미 확장된 삭제 집합은 두 번 다시 확장되지 않습니다; 이것이 expanded 검사입니다. 노드-라벨 재사용(node-label reuse): 이미 찾아낸 어떤 정당화 $J$ 가 현재 경로의 삭제들과 서로소라면, $J$ 는 남은 온톨로지 안에서 온전히 살아남아 여전히 함의하며, 그곳에서도 여전히 최소적입니다(최소성은 아래로 상속됩니다: 더 작은 온톨로지 안에서 함의하는 $J$ 의 진부분집합이 있다면, 단조성에 의해 그것은 $O$ 안에서도 함의할 것이므로, 이는 $O$ 안에서의 $J$ 의 최소성과 모순됩니다). 그러므로 $J$ 는 오라클 작업을 전혀 들이지 않고도 그 노드에 라벨을 붙일 수 있습니다; 이것이 reuse 줄입니다.

커밋된 열거와 트리의 크기는 다음과 같습니다:

질의	찾아낸 MinA	탐색한 HST 노드	무차별 대입과 일치?
Professor ⊑ Researcher	2개 : `{1}`, `{4, 5}`	4	정확히 일치
Dean ⊑ Researcher	3개 : `{1, 8}`, `{5, 9}`, `{4, 5, 8}`	13	정확히 일치
TenuredStudent ⊑ ⊥	1개 : `{6, 10, 11}`	4	정확히 일치
TenuredStudentAdvisor ⊑ ⊥	1개 : `{6, 10, 11, 12}`	5	정확히 일치
Student ⊑ Professor	함의되지 않음: 없음	0	—

Dean ⊑ Researcher는 천천히 읽을 가치가 있습니다, 그 세 정당화가 시사하는 방식으로 겹치기 때문입니다. {1, 8}은 상속 경로입니다: 학장은 교수이고, 교수는 연구자입니다. {5, 9}는 순수한 역할 경로입니다: 학장은 어떤 교수를 지도하고, 무엇이든 지도하는 것은 연구자가 되게 합니다. {4, 5, 8}은 위에서 확장-축소가 찾아낸 혼합 경로입니다: 학장은 교수이고, 교수는 어떤 학생을 지도하며, 지도하는 것은 연구자가 되게 합니다. {4, 5, 8}이 첫 번째 정당화와 공리 8을 공유하고 두 번째 정당화와 공리 5를 공유하면서도 그 자체로는 최소적임에 주목하십시오: 그것의 어떤 진부분집합도 함의하지 않습니다. 정당화들은 반사슬(antichain)을 이룹니다(최소성으로부터 곧바로 따라 나오듯, 어느 하나가 다른 하나를 포함하지 않습니다), 하지만 자유롭게 겹칠 수 있으며, 바로 그 겹침이 보수를 하나-고르기 문제가 아니라 적중 집합 문제로 만드는 것입니다.

표의 마지막 열은 장난감 세계만이 누릴 수 있는 사치이며, companion 코드는 그것을 의도적으로 씁니다. brute_force_all(justifications.py 224–253번째 줄)은 TBox의 $2^{14} = 16{,}384$ 개 부분집합 전부를 열거하여 각각을 새로 포화시키고(캐시를 우회하며, 완성 엔진 말고는 HST 실행과 아무것도 공유하지 않습니다), 함의하는 부분집합을 표시하며, 정확히 최소적인 것만을 남깁니다; 최소성은 단일 삭제 인증과 같은 단조성 논증에 의해 오직 단일 삭제 자식들만 검사하면 됩니다. 그런 다음 하니스는 네 개의 함의 모두에 대해 HST와 무차별 대입 사이의 정확한 집합 동등성을 단언합니다(justifications.py 328–331번째 줄):

    for q in QUERIES:
        assert single[q] in hst[q], f"single MinA missing from HST on {q}"
        assert hst[q] == brute[q], f"HST != brute force on {q}"
        assert hst[q] == EXPECTED[q], f"reason set changed on {q}"

그리고 커밋된 비용 줄은 이 구성 전체의 요점을 숫자로 보여 줍니다:

  oracle work for [2]+[3]: 90 saturations, 232 entailment calls (memoized); brute force: 16384 saturations

90번의 포화 대 만 육천 번: 적중 집합 트리는 네 개의 질의 전체에서 총 26개의 노드를 탐색했고, 완전탐색이 찾아낸 모든 것을 증명 가능하게 찾아냈습니다. 공리 14개에서는 완전탐색이 감당할 만한 심판이지만, SNOMED CT의 수십만 개 공리에서는 $2^{\lvert O \rvert}$ 가 더 이상 하나의 숫자가 아니며, 가지치기를 갖춘 트리야말로 그 알고리즘입니다.

디버깅으로서의 핀포인팅: 보수는 적중 집합이다

이제 렌즈를 뒤집어 봅시다. 지금까지 함의들은 원했던 것이었고 정당화들은 설명이었습니다. 학계 TBox에는 버그도 하나 담겨 있습니다. 2권에서 심어졌고 마침내 여기서 진단되는 버그입니다: TenuredStudent는 충족 불가능하며, 즉 TBox는 TenuredStudent ⊑ ⊥를 함의하므로, 그 어떤 개체도 모순 없이는 결코 tenured student가 될 수 없습니다. 원치 않는 함의의 정당화는 설명이 아니라 기소장입니다: 그것은 결함이 자리한 공리들을 정확하고 최소적으로 지목합니다. 커밋된 진단은 다음과 같습니다:

[5] pinpointing as debugging — why is TenuredStudent unsatisfiable?
  the single MinA {6, 10, 11} (Schlobach & Cornet's MUPS of the concept):
    ( 6) Professor ⊓ Student ⊑ ⊥
    (10) TenuredStudent ⊑ Professor
    (11) TenuredStudent ⊑ Student
  minimal repairs = minimal hitting sets of all MinAs (Reiter's diagnoses):
    remove ( 6) → TenuredStudent satisfiable again (verified against the oracle)
    remove (10) → TenuredStudent satisfiable again (verified against the oracle)
    remove (11) → TenuredStudent satisfiable again (verified against the oracle)

그 이야기는 세 개의 공리로 이루어져 있습니다: TenuredStudent는 교수이고, TenuredStudent는 학생이며, 교수와 학생은 서로소입니다. 핀포인팅이 하지 않은 일에 주목하십시오: 그것은 어느 공리가 틀렸는지는 말하지 않았습니다. 그것은 모델링 판단이며(아마도 서로소 공리 6이 너무 강할 것입니다), 어떤 알고리즘도 그 판단을 대신 내려 줄 수 없습니다. 알고리즘이 할 수 있는 일은 선택지를 한정하는 것입니다: 보수(repair)란 그것을 제거하면 함의가 죽는 공리 집합 $R \subseteq O$ , 즉 $O \setminus R \not\models \alpha$ 인 집합이며, 정당화들이 보수를 완전히 결정합니다.

정리(보수의 쌍대성). $R$ 이 $\alpha$ 에 대한 보수인 것은, $R$ 이 모든 정당화들의 모임에 대한 적중 집합(hitting set)인 것과 정확히 동치입니다. 즉 모든 정당화 $J$ 에 대해 $R \cap J \ne \emptyset$ 이라는 뜻이며: 보수는 각 정당화에서 적어도 하나의 공리를 제거합니다.

양쪽 방향 모두 짧으며, 둘 다 다시 단조성입니다. $R$ 이 어떤 정당화 $J$ 를 완전히 놓친다고, 즉 $R \cap J = \emptyset$ 이라고 합시다. 그러면 $J$ 의 모든 공리가 제거를 견디고 살아남으므로 $J \subseteq O \setminus R$ 이며, $J \models \alpha$ 에 단조성을 적용하면 $O \setminus R \models \alpha$ 가 나옵니다: 보수가 아닙니다. 반대로, $R$ 이 모든 정당화를 적중시킨다고 하고, 그 제거가 실패했다고, 즉 $O \setminus R \models \alpha$ 라고 상상해 봅시다. 함의하는 유한 집합은 반드시 최소 함의 부분집합을 포함합니다: 그 위에서 축소 루프를 돌려, 함의가 살아남는 동안 공리를 삭제합니다; 그 루프는 집합이 유한하고 엄격히 줄어들기만 하므로 종료되며, 정확히 단일 삭제 테스트를 통과하는 집합, 즉 정당화에서 멈춥니다. 그러므로 $O \setminus R$ 은 어떤 정당화 $J \subseteq O \setminus R$ 을 포함할 것이고, 이는 $O$ 의 정당화이기도 하며, $R \cap J = \emptyset$ 이 되어 가정과 모순됩니다. 따라서 최소 보수는 정확히 최소 적중 집합이며, 이는 어휘를 바꾼 Reiter의 원래 쌍대성입니다: 부품 대신 공리, 최소 충돌 집합 대신 정당화, 진단 대신 보수입니다 [1]. 온톨로지 디버깅은 원리로부터 나온 진단의 특수한 경우이며, 이것이 바로 이 권의 디버깅 장이 1987년의 인용으로 문을 연 이유입니다.

companion 코드는 정당화들의 합집합에 대해 가장 작은 것부터 열거하는 방식으로 최소 적중 집합을 계산하며, 이미 찾은 적중 집합을 포함하는 후보는 버립니다(justifications.py 258–272번째 줄). 그런 다음 유일하게 정직한 방식으로 그 루프를 닫습니다. 주장된 보수 각각을 다시 오라클에 넘기는 것입니다(justifications.py 340–343번째 줄):

    assert unsat_repairs == {frozenset({6}), frozenset({10}), frozenset({11})}
    for rep in sorted(unsat_repairs, key=sorted):
        assert not is_entailed(ALL - rep, "TenuredStudent", BOT), (
            f"repair {fmt_just(rep)} did not restore satisfiability")

여기서는 그 모임에 원소가 하나뿐이므로, 최소 적중 집합은 세 개의 단일원소 집합이며, 공리 하나씩을 제거하는 각 방법이 검증 가능하게 충족 가능성을 회복시킵니다. 겹치는 모임에서는 이 문제가 진짜 복잡도를 얻습니다. 정확히 말하면: 정당화들의 모임과 정수 $k$ (크기 예산)가 주어졌을 때, 크기가 많아야 $k$ 인 적중 집합이 존재하는지 결정하는 것은 NP-완전인데, 이것이 고전적인 최소 적중 집합 문제, 곧 집합 커버(set cover)와 동치인 문제이기 때문입니다(NP는 비결정적 다항 시간(nondeterministic polynomial time)으로, 예-답의 검증을 다항 시간에 할 수 있는 결정 문제들의 클래스이며, NP-완전은 그중 가장 어려운 문제들을, NP-난해는 적어도 그만큼 어렵다는 것을 뜻합니다). 따라서 최소 크기의 보수를 찾는 일은 NP-난해합니다. Reiter의 논문은 이 난해함을 분석하는 대신 비켜 갑니다: 그의 트리는 너비 우선으로 자라므로 진단은 크기가 커지는 순서로 도착하고, 작은 보수만을 원하는 탐색은 크기 예산에서 그냥 멈추면 됩니다 [1]. 그 난해성의 증명은 이 권의 범위를 넘어섭니다; companion 코드가 대신 보여 주는 것은 그 난해함이 딛고 선 쌍대성이 장난감 규모에서 정확하고 오라클로 검증된다는 사실입니다. 그리고 커밋된 실행에서 나오는 두 번째, 더 조용한 주의사항이 있습니다: 개념 TenuredStudentAdvisor 역시 MinA {6, 10, 11, 12}와 함께 충족 불가능한데, 공리 12가 그것에게 어떤 TenuredStudent를 지도하도록 강제하고 바닥 규칙이 그 역할을 따라 모순을 거꾸로 전파하기 때문입니다. 6, 10, 11 중 무엇을 제거하든 TenuredStudent를 고치는 일은 마침 이 두 번째 MinA도 적중시켜 두 개념을 한꺼번에 치유합니다; 하지만 일반적으로는 공리 전체를 삭제하는 것은 무딘 도구입니다, 하나의 공리가 여러 주장을 담고 있을 수 있고 그중 오직 하나만이 결함일 수 있기 때문입니다. 보수가 공리 6을 삭제하는 대신 약화시킬 수 있도록 정당화를 공리 수준 아래로 정련하는 것은 간결한 정당화(laconic justification)의 주제이며 [5], 이는 미해결 부분에서 다시 돌아옵니다.

규모, 정직하게

위의 모든 것은 정확하며, 그 천장도 같은 호흡으로 말해 두어야 합니다. 첫째, 열거되는 대상 자체가 거대해질 수 있습니다: EL 안에서조차, 크기가 매개변수 $n$ 에 대해 선형으로만 자라나는데도 단 하나의 함의가 $2^{n}$ 개의 정당화를 갖는 TBox 계열이 존재하므로, 어떤 알고리즘의 영리함을 쓰기도 전에 이미 정당화 전부를 열거한 결과물 자체가 지수적입니다; 그 구성은 핀포인팅을 EL 계열로 가져온 논문에 온전히 담겨 있으며, 그 논문은 주어진 크기 한도 안의 정당화가 존재하는지 묻는 것조차 NP-완전임을 함께 증명합니다 [6]. 그 증명들은 이 권의 범위를 넘어섭니다; companion 코드는 대신 그 반대의 사치를 보여 줍니다. 완전한 열거가 작고(네 개의 함의에 걸쳐 일곱 개의 MinA) 독립적으로 검사 가능한 14개 공리짜리 세계입니다. 이 분야가 그 천장에 맞서 쥔 세 가지 지렛대를 각각 한 단락씩 다룹니다:

건초더미 줄이기: 모듈. $A \sqsubseteq B$ 에 대한 정당화는 정확한 통사적 의미에서 그 함의의 서명(signature)으로부터 도달 가능한 공리만을 쓸 수 있습니다; 블랙박스 계열은 처음부터 이를 활용해, 온톨로지 전체를 취하는 대신 선택 함수를 따라 지지 집합을 확장했습니다 [3]. 이 발상의 성숙한 형태가 바로 지역성 기반 모듈 추출(locality-based module extraction)입니다: 값싼 통사적 패스 하나가 목표 함의의 모든 정당화를 담고 있음이 증명으로 보장되는 온톨로지의 부분집합을 추출하고, 이후 모든 핀포인팅은 그 모듈 안에서 실행됩니다 [7]. SNOMED 규모의 입력에서 이것은 흔히 몇 분과 영원히 끝나지 않음 사이의 차이를 만듭니다.

추론기 열기: 핀포인팅 논리식. 글래스박스 핀포인팅은 도출된 모든 귀결에, 그것이 어떻게 도출되었는지를 기록하는 공리 변수들에 대한 단조 불리언 논리식을 라벨로 붙입니다; 목표의 라벨이 바로 핀포인팅 논리식이며, 그것을 최소로 충족시키는 진리값 배정이 정확히 정당화들로서, 수백 번의 오라클 호출 대신 계측된 실행 단 한 번으로 계산됩니다 [4]. 그 대가는 실재합니다: 계측은 논리 체계마다 새로 공학적으로 지어져야 하고, 추론기의 최적화를 깨뜨릴 수 있으며, 논리식 자체가 폭발적으로 커질 수 있습니다. 이론은 그것이 언제 다루기 쉬운 채로 남는지를 정확히 한정합니다.

증명을 따라가기. 귀결 기반(consequence-based) 추론기는 각 포섭을 명시적인 규칙 적용으로 도출하므로, 모든 결론 뒤의 추론 단계들이 이미 실행 안에 존재합니다; EL 계열의 기함 추론기 ELK가 정확히 이렇게 지어져 있고 [8], 그 도구들은 그 단계들을 증명 흔적(proof trace)으로 노출하며, 증명 기반 열거(proof-driven enumeration)는 부분집합을 맹목적으로 탐색하는 대신 기록된 추론들로부터 리졸루션(resolution)으로 정당화를 캐냅니다 [9]. 이는 EL 계열 온톨로지에 대한 실용적인 중간 경로입니다: 블랙박스의 일반성은 포기되지만, 추론기는 어차피 그 증명들을 계산하려던 참이었습니다.

이 장에서 한 문장만은 반드시 챙겨 가십시오, 이 권의 나머지 전체가 그것에 기대기 때문입니다. 정당화는 "왜"에 대한 정답(ground truth)입니다: 다음 장의 충실성 프로브는 시스템이 스스로 보고하는 설명이 실제로 답을 강제하는 증거와 일치하는지를 묻고, VII부는 정확히 이 기준에 맞추어 SATORI의 어텐션 흔적을 채점합니다. 이유를 감사하는 그 뒤의 모든 것은 이런 확인 가능한 종류의 이유가 존재한다는 것을 전제합니다.

미해결 부분

정직한 공백 세 가지가 있습니다. 첫째, 규모: SNOMED CT 규모에서의 열거는 어떤 공학으로도 없앨 수 없는 이유로 최악의 경우 여전히 값비쌉니다. 답 자체가 지수적으로 길 수 있기 때문입니다; 모듈, 글래스박스 추적, 증명 채굴은 상수를 옮길 뿐, 천장을 옮기지는 못합니다. 둘째, 선택: 어떤 함의가 수십 개의 정당화를 가질 때, 사람은 어느 것을 먼저 봐야 할까요? 온톨로지 엔지니어와 비전문 사용자가 함의를 이해하고 고치는 데 실제로 무엇이 도움이 되는지에 대한 경험적 문헌은, 알고리즘보다 수십 년이나 젊고, 아직 얇습니다. 셋째, 세분성: 공리 하나가 여러 주장을 한데 묶을 수 있으므로 공리 전체는 흔히 잘못된 단위이며, 각 공리의 논리적으로 활성인 부분만을 남기는 간결한 정당화는 정준적 형태를 읽기 쉬움과 맞바꾸는데, 그 절충은 여전히 협상 중입니다 [5]. 대상 자체는 확정되었지만, 그것의 인간 인터페이스는 아직입니다.

왜 중요한가

이 장은 이 권의 주춧돌입니다, 이후의 모든 신뢰 계측 도구가 필요로 하는 단 하나의 것, 즉 수학적 정의와 알고리즘과 인증서를 갖춘 확인 가능한 이유를 만들어 내기 때문입니다. 이 시리즈는 1권 이래로 이런 분업을 향해 지어져 왔습니다: 기호 시스템은 그저 정확한 것이 아니라 감사 가능(auditable)하며, 정당화는 바로 그 감사 가능함이 무엇을 뜻하는지를 형식화한 것입니다. 독자 자신의 연구를 위해 옮겨 갈 수 있는 자산은 두 가지 규율입니다. 오라클 규율(시스템을 블랙박스로 다루고, 원시 연산 하나를 정의하고, 모든 것을 그것에 대한 호출 수로 값매김하는 것)은 오라클이 EL 추론기가 아니라 신경망 모델일 때에도 그대로 적용되며, 5권은 그 방식을 되풀이해서 적용할 것입니다. 인증서 규율(단일 삭제 감사 없이는 결코 최소 대상을 반환하지 않는 것; 적어도 한 번은 장난감 규모에서 무차별 대입에 맞서 검사해 보지 않은 열거는 결코 신뢰하지 않는 것)은 시연(demonstration)을 일화(anecdote)로부터 갈라놓는 것이며, justifications.py의 커밋된 assert들이 그 살아 있는 예입니다.

핵심 용어

정당화(justification, MinA, 최소 공리 집합): $J \models \alpha$ 이면서 $J$ 의 어떤 진부분집합도 $\alpha$ 를 함의하지 않는 부분집합 $J \subseteq O$ ; 어떤 함의에 대한 최소 증거입니다.
MUPS(최소 충족 불가능성 보존 하위 TBox, minimal unsatisfiability-preserving sub-TBox): 개념 충족 불가능성 함의 $A \sqsubseteq \bot$ 에 대한 정당화입니다.
단조성(monotonicity): EL과 그 친척 논리들에서, 공리를 더한다고 귀결이 사라지는 일은 결코 없습니다; $J \subseteq J'$ 이고 $J \models \alpha$ 이면 $J' \models \alpha$ 입니다. 단일 삭제 인증, 축소 증명, 보수의 쌍대성 뒤에 있는 보조정리입니다.
단일 삭제 인증(drop-any-one certificate): 단일 삭제가 각각 함의를 깨뜨린다는 $\lvert J \rvert$ 번의 오라클 검사로, 단조성에 의해 $2^{\lvert J \rvert}$ 개의 모든 부분집합에 맞서 최소성을 인증합니다.
확장-축소(expand-contract): 지지 집합을 처음 함의할 때까지 키운 다음, 공리를 하나씩 삭제하되 함의가 살아남는 삭제만 유지합니다; $O(\lvert O \rvert)$ 번의 오라클 호출로 정당화 하나를 반환합니다.
블랙박스 대 글래스박스 핀포인팅: 블랙박스는 오직 함의 오라클만을 사용하며 어떤 추론기와도 작동합니다; 글래스박스는 추론기를 계측하여 핀포인팅 논리식, 즉 그 최소 충족 진리값 배정이 정당화가 되는 단조 불리언 논리식을 내놓게 합니다.
적중 집합 트리(hitting-set tree, HST): 노드가 경로상에서 삭제된 공리들을 뺀 온톨로지의 정당화들이고, 각 간선이 부모 라벨의 공리 하나를 삭제하는 열거 트리입니다; 모든 정당화를 찾는 데 완전합니다.
보수/진단 쌍대성(repair/diagnosis duality): $R$ 이 함의를 제거하는 것은 $R$ 이 모든 정당화를 적중시키는 것과 동치입니다; 최소 보수는 최소 적중 집합이며, 어휘만 바꾼 Reiter의 진단입니다.
간결한 정당화(laconic justification): 각 공리의 논리적으로 활성인 부분만을 남기며 공리 수준 아래로 정련된 정당화입니다.

이 장이 이끄는 곳

이 장의 설명들은 자신의 이유에 대해 거짓말을 할 수 없는 시스템에서 뽑아낸 것이었습니다: 오라클의 답은 공리들에 의해 결정되며, 정당화는 확인 가능한 증거입니다. 5권이 다음으로 감사할 시스템들은 그렇지 않습니다. 신경망 모델은 왜냐고 물으면 하나의 이야기를 내놓지만, 그 아키텍처의 그 무엇도 그 이야기가 실제 계산과 일치한다는 것을 보장하지 않습니다. 충실성은 그 불일치를 잡아내는 프로브를 구축하며, 여기서 정의한 정당화는 그 프로브들이 맞추어 눈금이 매겨지는 금본위(gold standard)입니다: 설명은 정확히, MinA가 오라클에 대해 하는 역할을 모델에 대해 해낼 때 충실합니다.

Companion 코드: examples/frontier/justifications.py는 2권의 examples/symbolic/el_completion.py 위에서 함의 오라클을 구현하고, 공리별 최소성 감사를 갖춘 확장-축소, 두 가지 가지치기를 모두 갖춘 Reiter의 적중 집합 트리, 16,384개 공리 부분집합 전체에 대한 무차별 대입 심판, 그리고 TenuredStudent 모순에 대한 검증된 보수들을 구현합니다. 이 장의 모든 숫자를 재현하려면 python3 examples/frontier/justifications.py를 실행하십시오; 그 실행은 결정적이며 모든 주장은 assert로 지켜집니다.

이 장에서 다루는 내용​

도출에서 증거로​

오라클 규율: 하나의 원시 연산, 어떤 추론기든​

정당화 하나: 확장과 축소​

정당화 전부: Reiter의 적중 집합 트리​

디버깅으로서의 핀포인팅: 보수는 적중 집합이다​

규모, 정직하게​

미해결 부분​

왜 중요한가​

핵심 용어​

이 장이 이끄는 곳​