EL 추론기: ELK와 CEL

📍 현재 위치: 5부 · 실전 추론기 — 15장. 확실한 답은 준동형사상(homomorphism)에 의해 체이스로부터 신뢰할 수 있는 답을 읽어내며, 널로 증언된 튜플들을 걸러 냈습니다; 이제 우리는 손으로 만든 기계 장치를 떠나 실제로 배포되어 있는 추론기들 — ELK와 CEL — 을 만나며, 이들은 우리 3부의 완성 알고리즘을 산업 규모로 실행하고, 우리는 우리 자신이 처음부터 만든 버전을 그중 하나와 맞세워 시험합니다.

3부는 여섯 개의 완성 규칙(completion rule)이 건전하고(sound) 완전하며(complete) 종료함(terminating)을 증명했고, 4부는 그와 똑같은 고정점(fixpoint) 기계 장치를 데이터로그(Datalog)와 체이스(chase) 안으로 밀어 넣었습니다. 이 모든 것 위에는 정당한 질문 하나가 걸려 있습니다: 이 가운데 진짜인 것이 있을까요? 실제로 배포된 시스템이 TBox를 정규화하고 두 개의 표를 고정점까지 포화시켜서 정말로 온톨로지를 분류할까요 — 아니면 그것은 그저 교과서가 지어낸 가르침용 이야기일 뿐일까요? 이 장은 그 질문에 솔직하게 답합니다. 실제로 배포되어 있는 두 개의 추론기, ELK와 CEL은 바로 그 완성 알고리즘(completion algorithm)이며, 속도를 위해 공학적으로 만들어져, 수십만 개의 개념을 담은 의료 어휘를 몇 초 만에 분류합니다. 동반 코드는 ELK를 함께 담을 수 없으므로, 자신이 처음부터 만든 완성 알고리즘을 다른 방식으로 검증합니다: 완전히 다른 종류의 추론기인 HermiT를 상대로, 모든 항목에서 서로 일치하는지를 확인하는 것입니다.

쉽게 말하면

여러분이 교과서를 보고서, 도서관의 책들을 주제 계층에 따라 분류하는 자신만의 기계를 직접 만들었다고 상상해 보십시오 — 그리고 그것이 열 권짜리 서가 위에서는 흠잡을 데 없이 작동합니다. 진짜 시험은 그 똑같은 아이디어가 수십만 권을 소장한 국립 도서관 앞에서도 살아남는지입니다. ELK와 CEL은 바로 그 국립 도서관을 위해 만들어진 그 아이디어입니다: 3부의 바로 그 완성 알고리즘이되, 병원의 의료 어휘 전체를 몇 초 만에 분류할 수 있도록 다듬어진 것입니다. 그리고 여기서는 그들의 엔진을 함께 담을 수 없으므로, 우리는 다른 방식으로 우리 자신의 버전을 점검합니다 — 완전히 다른 종류의 추론기인 HermiT와 나란히 그것을 실행해 보고, 둘이 단 하나의 항목까지도 빠짐없이 일치한다는 것을 확인합니다.

이 장에서 다루는 내용

알고리즘에서 제품으로 — ELK와 CEL은 완성/귀결 기반(completion / consequence-based) 방법 위에 구축된 실제 추론기입니다; CEL이 생명과학 온톨로지를 위해 먼저 나왔고, 둘 다 EL이 의도적으로 짊어진 빈곤함을 실세계의 속도로 현금화합니다.
EL 추론기를 빠르게 만드는 것 — 규칙 색인화(rule indexing), 동시성(concurrency), 그리고 오직 자라나기만 하는 표들: 역추적이 없으므로 분류는 최악의 경우에도 다항식적이고 실제로는 거의 선형적입니다.
어디서 실행되는가 — SNOMED CT와 Gene Ontology, 수십만 개의 개념이 일상적으로 분류됩니다; OWL 2 EL 프로파일이 실제로 배포되어 있는 사례입니다.
우리가 실행할 수 있는 교차 검증 — owlready2는 ELK가 아니라 HermiT를 함께 배포하므로, reasoners.py는 학계 세계(academic world)를 다시 만들고 sync_reasoner를 통해 HermiT를 구동합니다.
커밋된 결과 — 처음부터 만든 완성 알고리즘의 포섭 관계 8개, HermiT도 8개, 두 충족 불가능한 개념도 동일하게 일치하며, AGREEMENT CONFIRMED입니다.
HermiT가 공정한 오라클인 이유 — HermiT는 OWL 2 DL에 대해 완전하며, 그 논리는 EL의 진(眞)초집합이므로 처음부터 만든 추론기의 어떤 버그도 드러낼 것입니다; ELK라면 동일한 EL 분류를 내놓았을 것입니다.

알고리즘에서 제품으로: ELK와 CEL

el_completion.py에 담긴 알고리즘의 모양을 떠올려 보십시오. 모든 공리를 네 가지 정규형(normal form) 중 하나로 정규화합니다 — NF1: $A \sqsubseteq B$ ; NF2: $A_1 \sqcap A_2 \sqsubseteq B$ ; NF3: $A \sqsubseteq \exists r.B$ ; NF4: $\exists r.B \sqsubseteq A$ — 그런 다음 두 개의 표를 포화(saturate)시킵니다 — $A$ 가 포섭된다고(subsumed) 알려진 개념들인 $S(A)$ 와, $A$ 가 $r$ -후속자로 $B$ 를 가진다고 알려진 쌍 $(A, B)$ 들인 $R(r)$ 을 — 아무것도 바뀌지 않을 때까지 규칙을 발동시켜서, 그런 다음 $A \sqsubseteq B$ 를 " $B \in S(A)$ "로 읽어냅니다. 이 모듈 자신의 독스트링(docstring)은 그 루프가 무엇인지를 이렇게 명명합니다: "그저 단조 연산자(monotone operator)의 고정점(fixpoint)일 뿐이며 — 1권의 전방 연쇄(forward-chaining) $T_P$ 와 똑같은 모양이되, 이제는 포섭 사실 위에서 벌어지는 것"이라고(el_completion.py 32–33번째 줄). 이것은 가르치기 위해 지어낸 장난감 패턴이 아닙니다. 그것은 두 개의 실제 추론기의 엔진입니다.

CEL은 손위 세대입니다 — 생명과학 온톨로지를 위해 특별히 만들어진 다항 시간(polynomial-time) 추론기입니다 [1]. 그것은 특화된 EL 분류기가, 당대의 범용 추론기들이 숨 막혀 하던 그 용어 체계를 다룰 수 있음을 보여 준 최초의 시스템이었습니다. ELK — "그 놀라운 ELK"("the incredible ELK")라고도 불리는 — 는 현대의 후계자입니다: OWL 2 EL 프로파일을 위한 귀결 기반(consequence-based) 추론기로(OWL은 웹 온톨로지 언어(Web Ontology Language)입니다), 색인화되어 있고 동시적이며, SNOMED CT를 몇 초 만에 분류하도록 공학적으로 만들어졌습니다 [2]. 둘 다 3부의 귀결 기반 추론(consequence-based reasoning) 장이 이름 붙인 그 가족에 속합니다: 그것들은 귀결을 앞으로 도출하며 포화시킬 뿐, 결코 반박을 찾아 탐색하지 않습니다. 이는 정반대의 방식으로 포섭을 판정하는 HermiT와 뚜렷하게 대조됩니다 — HermiT는 반례 모델(counter-model)을 구축하려 시도하다가 어떤 갈래가 충돌할(clash) 때마다 역추적(backtrack)합니다.

추론기	판정하는 논리	방법	강점을 보이는 곳
CEL	EL+ / EL++	귀결 기반 완성(consequence-based completion)	최초의 다항 시간 생명과학 분류기(SNOMED CT, Gene Ontology) [1]
ELK	OWL 2 EL	귀결 기반, 색인화되고 동시적	SNOMED CT를 몇 초 만에 분류 [2]
HermiT	OWL 2 DL (SROIQ ⊇ EL)	하이퍼테이블로(hypertableau) — 역추적을 동반한 모델 탐색	논리 전체에 대한 완전한 오라클 [3]

두 EL 추론기 모두 EL 계열 장이 마련해 둔 그 거래로 속도를 사들입니다: EL은 의도적으로 빈곤합니다. 그것은 오직 논리곱(conjunction) ⊓와 존재 제한(existential restriction) ∃만을 남겨 두고, 전칭 제한(universal restriction) ∀, 부정(negation) ¬, 논리합(disjunction) ⊔은 포기합니다. 바로 그 빈곤함이 포섭을 다항 시간에 결정 가능하게 만드는 정확한 이유이며 — ELK와 CEL은 바로 그 보장을 현금화하는 시스템들입니다.

하나의 온톨로지 위에서 만나는 두 추론 문화: 귀결 기반 EL 계열(CEL, ELK)은 S와 R을 단조롭게 키워 고정점에 이르고 SNOMED CT 규모로 확장되는 반면, HermiT는 모델을 탐색하며 역추적합니다 — 그럼에도 학계 세계 위에서 둘 다 동일한 8개의 포섭 관계와 동일한 2개의 충족 불가능한 개념에 이릅니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

EL 추론기를 빠르게 만드는 것

세 가지 공학적 사실이, 모두 처음부터 만든 코드 안에서 눈에 보이는 채로, ELK와 CEL이 빠른 이유를 설명해 줍니다.

표는 오직 자라나기만 하므로, 역추적이 없습니다. 포화(saturation)는 결코 줄어들지 않는, 도출된 사실 집합들의 오름 사슬을 쌓아 올립니다,

D_0 \;\subseteq\; D_1 \;\subseteq\; D_2 \;\subseteq\; \cdots \;\subseteq\; D_k \;=\; D_{k+1},

가능한 $(A, B)$ 사실들의 유한한 전체 공간에 의해 상한이 걸려 있으므로, 이 사슬은 반드시 안정됩니다. 모든 추가는 그것이 진정으로 새로울 때에만 셈해지도록 지켜지고 있습니다 — 역할 엣지를 기록하는 헬퍼 함수는 그 쌍이 이전에 없었을 때에만 True를 반환합니다(el_completion.py 198–203번째 줄):

    def add_r(r, pair):
        R.setdefault(r, set())
        if pair not in R[r]:
            R[r].add(pair)
            return True
        return False

그 무엇도 철회되지 않으므로, 되돌려야 할 잘못된 추측이 없습니다. 이것이 바로 HermiT와 같은 테이블로(tableau) 추론기와의 결정적인 차이입니다 — HermiT는 개체 하나를 상정하고, 전파하고, 충돌(clash)에 부딪히면 다른 갈래를 시도하기 위해 역추적합니다. 귀결 기반 EL 추론기에는 갈래가 없습니다: 그것은 오직 단조롭게 갈아 나가 하나의 고정점에 이를 뿐입니다.

규칙 색인화(rule indexing) — 각 규칙은 자신이 발동할 수 있는 것만을 훑습니다. 루프가 실행되기 전에 공리들은 모양별로 나뉘어 담기므로, 정규형 NF4( $\exists r.B \sqsubseteq A$ )에 맞는 규칙은 NF1 공리( $A \sqsubseteq B$ )를 아예 들여다보지도 않습니다(el_completion.py 191–196번째 줄):

    nf1 = [a for a in normalized if a[0] == "nf1"]
    nf2 = [a for a in normalized if a[0] == "nf2"]
    nf3 = [a for a in normalized if a[0] == "nf3"]
    nf4 = [a for a in normalized if a[0] == "nf4"]
    chains = [a for a in normalized if a[0] == "chain"]
    rsubs = [a for a in normalized if a[0] == "rsub"]

우리 것은 장난감 버전입니다; ELK는 산업적 강도로 똑같은 일을 하며, 수백만 개의 공리를 색인화하여 각 추론이 오직 발동할 가능성이 있는 소수의 공리만을 참조하도록 합니다 [2].

동시성(concurrency). 각 개념의 포화 작업은 대체로 분리 가능한 단위입니다 — 그것이 도출한 역할 후속자는 모든 단위가 전체를 다시 도출하는 대신 단위들 사이에서 전달됩니다 — 그리고 ELK는 정확히 이 점을 활용하여 작업을 코어들에 분할하고 대규모 온톨로지를 병렬로 분류합니다 [2].

최악의 비용은 건전성과 완전성 장이 세워 둔 바로 그 방식으로 유계입니다. 개념 이름들을 $N$ 으로, 역할들을 $N_R$ 로 적으면,

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

그러므로 두 표는 오직 다항식적 크기까지만 자랄 수 있으며, 따라서 포화는 다항식 개수만큼의 생산적인 순회 뒤에 멈춥니다 — 바로 PTIME(다항 시간, polynomial-time) 보장입니다. 실제 온톨로지에서는 완성된 관계가 희소한 채로 남으며, ELK의 실측 동작은 입력 크기에 대해 거의 선형적입니다 [2].

어디서 실행되는가: SNOMED CT와 Gene Ontology

OWL 2 EL 프로파일이 애초에 존재하는 이유는 하나의 배포 사례입니다. SNOMED CT(체계화된 의학 용어 임상 명명법, Systematized Nomenclature of Medicine, Clinical Terms)는 수십만 개의 임상 개념을 가지고 있으며, ELK나 CEL 같은 추론기가 그 전체를 몇 초 만에 분류할 수 있도록 바로 그 목적으로 OWL 2 EL에 가까운 파편(fragment)으로 저작되어 있습니다. Gene Ontology도 생물학 쪽에서 같은 이야기를 들려줍니다. 이것이 바로 OWL 2 EL의 배포 사례입니다: 이 프로파일은 반대 방향이 아니라, 이 귀결 기반 분류기들이 규모에서 무엇을 해낼 수 있는지를 중심으로 표준화되었습니다 [2][1].

그리고 바닥 규칙(bottom rule)이 수행하는 모델링 버그 점검은, 이 추론기들이 실제 용어 체계 위에서 실행하는 바로 그 점검입니다. 어떤 클래스가 실수로 서로소인 두 클래스의 하위 클래스로 만들어지면, 그것은 충족 불가능(unsatisfiable)하다고 표시됩니다 — 일부러 과잉 제약을 걸어 둔 TenuredStudent가 $\text{Professor} \sqcap \text{Student} \sqsubseteq \bot$ 아래에서 Professor이면서 동시에 Student로 선언될 때 촉발하는 것과 똑같은 실패입니다. 그리고 TenuredStudentAdvisor도 함께 끌려 내려갑니다: 그것은 반드시 TenuredStudent — 이제는 그 자신이 ⊥인 — 를 지도해야 하므로, 바닥 규칙이 advises 엣지를 따라 ⊥를 거꾸로 전파하여, 그것 역시 충족 불가능하다고 표시됩니다. 수십만 개의 개념을 가진 어휘 위에서, 이것은 편집자를 위한 화재경보기입니다: 추론기는 모순을 조용히 분류해 버리는 대신 문제가 되는 클래스의 이름을 짚어 줍니다.

우리가 실제로 실행할 수 있는 교차 검증

우리는 ELK를 순수 파이썬(pure-Python) 동반 코드 안에 함께 담을 수 없으므로, 검증은 owlready2가 실제로 함께 배포하는 추론기를 사용합니다. reasoners.py가 설명하듯이, "owlready2는 HermiT(완전한 OWL 2 DL 추론기)와 Pellet을 함께 배포합니다; EL에 특화된 ELK는 담고 있지 않으므로, 우리는 sync_reasoner를 통해 HermiT를 구동합니다 — EL의 진(眞)초집합이므로, 여기서의 일치는 가능한 가장 강력한 검사입니다"(reasoners.py 11–13번째 줄). 이 모듈은 동일한 학계 세계(academic-world) 온톨로지 — 이름 붙은 개념 10개, 역할 6개, TBox 공리 14개 — 를 owlready2의 파이썬 구문으로 공리 하나하나 그대로 다시 만듭니다(reasoners.py 45–51번째 줄):

    world = get_ontology("http://nesy-guide.org/academic.owl")
    with world:
        # Concept names (declared so the hierarchy is explicit).
        class Person(Thing): pass
        class Researcher(Person): pass          # (3) Researcher ⊑ Person
        class Professor(Researcher): pass       # (1) Professor ⊑ Researcher
        class Student(Researcher): pass         # (2) Student ⊑ Researcher

더 까다로운 두 개의 EL++ 공리 — 분리성(disjointness)과 역할 사슬(role chain) — 은 owlready2의 구성 요소에 하나씩 그대로 대응됩니다(reasoners.py 72–75번째 줄):

        # (6) Professor ⊓ Student ⊑ ⊥  (disjointness)
        AllDisjoint([Professor, Student])
        # (7) advises ∘ advises ⊑ grandAdvisor
        grandAdvisor.property_chain.append(PropertyChain([advises, advises]))

그런 다음 reasoner_classification은 HermiT를 실행하고, 처음부터 만든 코드가 보고하는 것과 정확히 같은 두 가지 — 이름 붙은 개념들 사이의 포섭 관계와 충족 불가능한 개념 — 을 똑같은 방식으로 걸러서 읽어내므로, 두 답을 곧바로 비교할 수 있습니다(reasoners.py 98–103번째 줄):

    with world:
        sync_reasoner(world, infer_property_values=False, debug=0)

    named = set(onto.CONCEPTS)
    unsat = {c.name for c in world.inconsistent_classes()
             if c.name in named}

커밋된 결과: 일치 확인됨

실행해 보면, 두 개의 독립적인 코드 경로 — 하나는 교과서 규칙을 그대로 따라 만든 것이고, 하나는 십 년 동안 다져진 엔진입니다 — 가 동일한 분류에 이릅니다. 다음은 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개의 포섭 관계는 단순한 개수가 아닙니다; 그것들은 처음부터 만든 추론기가 스스로 출력하는 구체적인 계층입니다(python3 el_completion.py):

classification: 8 subsumptions between named concepts
  Dean ⊑ Person
  Dean ⊑ Professor
  Dean ⊑ Researcher
  Professor ⊑ Person
  Professor ⊑ Researcher
  Researcher ⊑ Person
  Student ⊑ Person
  Student ⊑ Researcher

unsatisfiable concepts (2): ['TenuredStudent', 'TenuredStudentAdvisor']

그 여덟 개 하나하나 — Dean에 관한 세 개의 포섭 관계, Professor에 관한 두 개의 포섭 관계, Researcher ⊑ Person, 그리고 Student에 관한 두 개의 포섭 관계 — 가 모두 HermiT에 의해 확인되며, 두 엔진 모두 동일한 두 개의 충족 불가능한 개념에 표시를 답니다. 이를 강제하는 단언(assertion)은 어떠한 어긋남도 용납하지 않습니다: 그것은 두 결과 집합을 있는 그대로 비교하며, 불일치가 있다면 그 대칭 차집합을 출력할 것입니다(reasoners.py 150–151번째 줄):

    assert subs_agree, ("subsumption mismatch", r_subs ^ el_subs)
    assert unsat_agree, ("unsat mismatch", r_unsat ^ el_unsat)

그것은 결코 발동하지 않습니다. 두 개의 엔진, 두 개의 방법, 하나의 분류입니다.

HermiT가 공정한 오라클인 이유

일치는 그 증인만큼만 강력하며, 여기서는 HermiT가 가장 강력하게 구할 수 있는 증인입니다. 그것은 완전한 OWL 2 DL 추론기입니다 [3]: 그 결정 절차 — 하이퍼테이블로 계산법(hypertableau calculus) — 는 OWL 2 DL 배후의 완전한 SROIQ 서술 논리를 위해 만들어져 있으며, 이는 완성 알고리즘이 다루는 그 자그마한 EL 파편의 진(眞) 초집합(superset)입니다. 여기서 두 가지 귀결이 따라 나옵니다.

첫째, HermiT는 같은 맹점을 공유할 수도 있는, 우리 자신의 아이디어를 그대로 베낀 두 번째 사본이 아닙니다. 그것은 완전히 다른 방법 — 귀결을 도출하는 대신 모델을 탐색하는 방법 — 으로, 그것도 훨씬 더 큰 논리 위에서 포섭을 판정하므로, 처음부터 만든 추론기의 어떤 버그든 불일치로 드러날 것인데, 그런 일은 일어나지 않습니다. 어떤 구현과, 그것과 독립적이면서 더 강력한 추론기가 모든 항목에서 일치할 때, 둘 다가 똑같은 방식으로 틀렸을 잔여 가능성은 외부 검증이 줄 수 있는 것 중 가장 작은 축에 듭니다.

둘째, ELK는 정확성 질문에 대해서는 군더더기입니다. 정확히 동일한 EL 분류를 내놓을 것이기 때문입니다: 그것은 우리 코드가 모방하는 것과 똑같은 귀결 기반 방법으로 똑같은 EL 파편을 판정합니다. 그러므로 더 무겁고 더 일반적인 HermiT를 상대로 검사하는 것은 의도적인 선택입니다 — 초집합 오라클(superset oracle)의 일치는 같은 파편을 다루는 도구의 일치보다 더 강한 증거인데, 그 초집합 오라클은 원리상 EL이 보는 것보다 더 많은 것을 찾아낼 수도 있었는데도 정확히 똑같은 것을 찾아냈기 때문입니다. 이것이 바로 동반 코드의 장 지도(chapter map)가 soundness-completeness에 대해 기록해 둔 것입니다: "HermiT와 일치함(포섭 8개, 충족 불가능 2개)."

아직 풀리지 않은 부분

EL 추론기는 전문가(specialist)이며, 그 속도는 그 좁음과 떼어 놓을 수 없습니다. 온톨로지가 EL 바깥의 무언가 — 전칭 제한 ∀r.C, 부정 ¬C, 논리합 ⊔, 혹은 진정한 카디널리티(cardinality) — 를 필요로 하는 순간, ELK와 CEL은 그것을 그저 판정할 수 없습니다. 그러면 여러분은 HermiT나 Konclude 같은 완전한 DL 추론기로 물러나 완전한 DL 추론의 최악의 경우 폭발(SROIQ 포섭은 2NEXPTIME-완전입니다)을 감수하거나, 데이터로그 모양의 부분을 RDFox 같은 규칙 엔진에 넘겨야 합니다. 어떤 지식 베이스에 대해서도 모든 상황에서 최선인 단 하나의 엔진은 없으며, "이 공리는 여전히 EL인가?"라는 프로파일의 경계는 오늘날에도 대체로 손으로 그어집니다. 정직하게 열려 있는 질문은, 온톨로지를 프로파일별로 먼저 나누는 사람 없이도, 각 질의를 그것을 판정할 수 있는 가장 저렴한 엔진으로 시스템이 자동으로 경로 지정(route)할 수 있는가입니다: EL로 충분한 곳에서는 EL의 빠른 방식으로, 어떤 공리가 진정으로 요구하는 곳에서만 완전한 DL로 말입니다.

이와 관련된 주의사항 하나는 교차 검증 그 자체에도 적용됩니다. 학계 세계 위에서의 일치는 하나의 입력에 대해 구현을 뒷받침해 줄 뿐입니다; 그것은 SNOMED CT 위에서의 일치를 보증하지 않으며, 보증할 수도 없습니다. 그 보편적인 보장을 제공하는 것은 건전성과 완전성 정리(theorem)이며 — 경험적 악수는 이 코드가 하나의 온톨로지 위에서 그 정리를 충실히 실현하고 있음을 확인해 줄 뿐, 모든 온톨로지 위에서도 그러하리라는 것을 확인해 주지는 않습니다. 테스트는 일치가 존재함을 보여 줄 뿐 결코 그 보장을 보여 주지는 않습니다; 그 간극을 메우는 것이 바로 증명입니다.

왜 중요한가

신경-기호(neuro-symbolic) AI에게, ELK는 "논리는 규모를 감당하지 못한다"는 오래된 반론에 답하는 존재 증명(existence proof)입니다. 단조 연산자를 최소 고정점까지 포화시키는 것보다 더 이국적인 그 무엇도 없이 수십만 개의 의료 개념을 몇 초 만에 분류하는 추론기는, 엄밀한 상징적 추론이 종이 위의 증명에 그치지 않고 실제 시스템 안에 자리 잡을 만큼 충분히 빠를 수 있음을 보여 줍니다. 그 엄밀하고 건전하며 완전한 분류가 바로, 학습된 혹은 신경망적 근사가 반드시 견주어 측정되어야 할 정답(ground truth)입니다: 훗날 어떤 미분 가능한 추론기가 그럴듯함(plausibility)에 따라 포섭 관계의 순위를 매길 때, 여기서 인증된 8개의 정확한 포섭 관계와 2개의 정확한 충족 불가능성이 바로 그것이 어긋났는지를 말해 주는 척도입니다. 그리고 두 엔진 사이의 악수는 이 분야 전체가 재사용하는 하나의 본보기입니다 — 빠른 전문가와 일반적인 오라클이 일치할 때, 여러분은 그 전문가를 신뢰하고 그것의 더 저렴한 비용만을 치르면 됩니다.

핵심 용어

ELK — OWL 2 EL 프로파일을 위한 귀결 기반 추론기입니다; 색인화되어 있고 동시적이며, 완성 표들을 고정점까지 포화시켜 SNOMED CT 규모의 온톨로지를 몇 초 만에 분류합니다.
CEL — ELK의 선배로, 생명과학 온톨로지를 위해 만들어진 최초의 다항 시간 추론기입니다; 동일한 귀결 기반 방법을 씁니다.
귀결 기반 추론(Consequence-based reasoning) — 역추적 없이, 귀결을 앞으로 도출하며 단조 연산자를 고정점까지 포화시키는 것; ELK, CEL, 그리고 처음부터 만든 완성 알고리즘 배후의 방법입니다.
OWL 2 EL — 다루기 쉬운(tractable) OWL 프로파일로(오직 ⊓와 ∃, 그리고 ⊥와 역할 사슬만을 가집니다), 그 다항 시간 분류를 ELK와 CEL이 구현합니다; SNOMED CT와 Gene Ontology가 실제로 배포되어 있는 사례입니다.
HermiT — SROIQ 위에서 작동하는 완전한 OWL 2 DL 추론기로(EL의 진(眞)초집합입니다), 하이퍼테이블로 모델 탐색으로 포섭을 판정합니다; 여기서는 독립적인 오라클로 쓰입니다.
초집합 오라클(Superset oracle) — 외부 증인으로 쓰이는, 더 큰 논리를 위한 추론기입니다; 검사 대상 코드와 방법도 맹점도 공유하지 않으므로, 그 일치는 같은 파편을 다루는 도구의 일치보다 더 강한 증거입니다.
단조 포화 / 역추적 없음(Monotone saturation / no backtracking) — 표 $S$ 와 $R$ 은 오직 최소 고정점까지 자라나기만 하므로, EL 추론기는 결코 추측하지 않고 결코 되돌리지 않습니다 — 이것이 바로 분류가 실제로는 거의 선형적인 이유입니다.

이 장이 이끄는 곳

이제 우리는 완성 알고리즘이 그저 증명 가능하게 옳을 뿐만 아니라 실제로 배포되어 있음을 압니다: ELK와 CEL은 그것을 SNOMED CT 규모로 실행하며, 처음부터 만든 버전은 초집합 오라클과 항목별로 일치합니다. 그러나 EL 추론기는 전문가이며, 일반적인 지식 베이스는 그 이상을 필요로 합니다 — 데이터로그 모양의 부분을 위한 규칙 엔진과, EL을 뒤로하는 공리들을 위한 완전한 DL 추론기가 그것입니다. 다음 장인 데이터로그와 DL 엔진: RDFox, HermiT, Konclude는 그런 엔진들을 살펴보며, 3부 이래로 이 권이 계속 맴돌아 온 하나의 순환 고리를 닫습니다: EL 완성을 데이터로그로 다시 표현하는 것이며, 그리하여 전문화된 추론기와 일반적인 규칙 엔진이 결국 하나의 동일한 고정점을 실행하고 있었음이 드러납니다.

이 장에서 다루는 내용​

알고리즘에서 제품으로: ELK와 CEL​

EL 추론기를 빠르게 만드는 것​

어디서 실행되는가: SNOMED CT와 Gene Ontology​

우리가 실제로 실행할 수 있는 교차 검증​

커밋된 결과: 일치 확인됨​

HermiT가 공정한 오라클인 이유​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 장이 이끄는 곳​