본문으로 건너뛰기

솔직한 평결: 기호가 보장하는 것

📍 현재 위치: 7부 · 평결 — 22장. 개방 세계와 비일관성은 추론기가 알려지지 않은 사실을 거짓이 아니라 그저 증명되지 않은 것으로 취급하는 방식과, 단 하나의 모순이 어떻게 모든 함의를 오염시킬 수 있는지를 보여 주었습니다; 이제 우리는 이 모든 기호적 기계 장치가 정확히 무엇을 사 주고 — 무엇을 사 주지 않는지 — 를 낱낱이 헤아리며 이 권을 마무리합니다.

이 장은 새로운 기계 장치를 전혀 더하지 않습니다. 이 장은 이 권 전체를 감사(audit)합니다. 스물한 개의 장에 걸쳐 여러분은 온톨로지를 만들었고, TBox(용어 상자(terminological box), 스키마의 개념 및 역할 공리)를 정규화했으며, EL 완성(EL completion) 알고리즘을 실행했고, 이를 데이터로그(Datalog)로 다시 표현했으며, 존재 규칙(existential rule)을 체이스하여 확실한 답에 이르렀고, 사실에 유래(provenance)와 신뢰도(confidence)를 주석으로 달았습니다. 솔직한 평결은 짧으며, 두 개의 절반으로 이루어져 있습니다: 기호가 진정으로 보장하는 것들의 열과, 기호가 보장할 수 없는 것들의 열입니다. 이 평결을 그저 주장된 것이 아니라 솔직한 것으로 만드는 것은, 아래의 모든 숫자가 여러분이 직접 실행해 볼 수 있는 커밋된 코드의 한 줄이라는 점입니다 — 이 장은 그 하나하나의 배후에 있는 파일과 줄 번호를 명시합니다.

쉽게 말하면

여러분의 장부에 서명해 줄 꼼꼼한 감사관을 고용한다고 상상해 보십시오. 그는 오직 장부가 실제로 말하는 것만을 인증하고, 모든 수치 배후의 정확한 영수증을 보여 주며, 영수증이 없을 때는 숫자를 지어내기를 거부합니다 — "아마 괜찮을 것"이라는 말은 결코 하지 않고, 오직 "확인됨" 아니면 "확인 안 됨"만을 말합니다. 그 추측을 거부하는 태도야말로 그의 커다란 강점이자 단단한 한계입니다: 여러분은 그가 찍어 주는 모든 도장을 신뢰할 수 있지만, 영리한 추측이 도움이 되었을 자리에서는 빈칸을 받아 들게 될 것입니다. 기호적 추론이 바로 그 감사관입니다. 이 장은 우리가 그 도장이 얼마만큼의 가치가 있는지를 저울질하는 순간입니다.

이 장에서 다루는 내용​

  • 평결, 담백하게 말하면 — 기호는 여러분이 신뢰하고 설명할 수 있는 정확성을, 반드시 적어 두고 일관되게 유지해야 하는 지식 위에서 사 줍니다.
  • 무엇이 진정으로 견고한가 — HermiT와 일치하는 건전하고 완전하며 다항 시간인 EL 분류; 체이스 위에서 계산되는 확실한 답; 사실이 어디서 왔는지와 그것을 얼마나 확신하는지를 기록하는 유래와 신뢰도 — 각각의 배후에는 하나의 동반 모듈이 있습니다.
  • 손이 닿지 않는 채로 남는 것 — 누락되거나 잡음 섞인 사실에 대한 부서지기 쉬움, 데이터로부터의 학습 부재, 보정되지 않고 손으로 설정된 신뢰도, 그리고 존재 한정이 등장하는 순간의 결정 불가능한 종료입니다.
  • 네 가지 되풀이되는 긴장 — 표현력 대 다루기 쉬움, 개방 세계 대 폐쇄 세계, 완전함 대 확장 가능함, 정확함 대 견고함: 3권과 그 이후가 반드시 조화시켜야 할 축들입니다.
  • 증거를 실행 가능하게 만들기 — validate.py 안의 13개 검사로 이루어진 원장(ledger)으로, 주장마다 한 행씩이며, 그 종료 코드(exit code)가 이 권이 주장하는 모든 것에 대한 평결입니다.
  • 솔직한 조언 — 어떤 과제든 그 명료한 기호적 버전을 먼저 모델링하십시오, 그래야 학습된 근사가 무엇을 반환해야 하는지를 언제나 알 수 있습니다.

평결, 담백하게 말하면​

전체 발견을 한 줄로 요약하면 이렇습니다: 기호는 여러분이 신뢰하고 설명할 수 있는 정확성을, 반드시 적어 두고 일관되게 유지해야 하는 지식 위에서 사 줍니다 [1]. 이를 두 개의 절로 풀어 보면 둘 다 핵심을 떠받치고 있습니다. 신뢰하고 설명할 수 있는 정확성은 보상입니다: EL 추론기가 Professor ⊑ Person이라고 말할 때, 그것은 강한 직감이 아니라 하나의 정리(theorem)이며, 온톨로지의 모든 모델에서 참이고, 여러분에게 그 도출 과정을 건네줄 수 있습니다. 반드시 적어 두고 일관되게 유지해야 하는 지식은 대가입니다: 추론기는 오직 누군가가 작성한 공리 위에서만 추론하며, 그 공리 가운데 두 개가 모순되는 순간, 고전적 함의는 모든 것을 도출하는 것으로 붕괴합니다. 기호는 세계를 읽지 않습니다; 기호는 여러분이 만든 세계의 모델을 읽습니다. 이 권에서 견고한 모든 것은 그 거래 안에서 살아가며, 손이 닿지 않는 모든 것은 그 바깥에서 살아갑니다.

보증 원장(guarantee ledger)을 하나의 공유된 학계 온톨로지 위에 마주 보는 두 개의 열로 그린 다이어그램입니다. 왼쪽 열은 기호가 보장하는 것이라는 제목이 붙어 있으며, 초록색 도장이 찍힌 네 개의 행을 담고 있습니다: 건전하고 완전한 분류는 Professor가 Person에 포섭된다는 것을 포함한 여덟 개의 포섭 관계를 HermiT 배지에 맞춰 보여 주고; 다항 시간 결정 가능성은 스물셋에서 서른아홉까지 이어지는 세 라운드짜리 포화 상승으로 표시되며; 감사 가능한 증명은 grand-advising의 작은 역할 사슬 도출로 보여지고; 체이스 위에서의 확실한 답은 두 개의 상수 alice와 bob이 유지되는 동안 발명된 널 하나가 지워지는 모습으로 나타납니다. 오른쪽 열은 손이 닿지 않는 채로 남는 것이라는 제목이 붙어 있으며, 호박색 도장이 찍힌 네 개의 행을 담고 있습니다: 누락된 사실은 어깨를 으쓱하는 몸짓과 함께 기권함, 견고하지 않음이라는 이름표가 붙고; 줄이 그어진 학습 곡선에는 학습 없음이라는 이름표가 붙으며; 손으로 돌린 신뢰도 다이얼은 영점 팔을 가리키며 보정되지 않음이라는 이름표가 붙고; 끝없이 솟아오르는 발명된 지도교수들의 탑에는 종료성 결정 불가능이라는 이름표가 붙습니다. 두 열 아래로는 표현력 대 다루기 쉬움, 개방 세계 대 폐쇄 세계, 완전함 대 확장 가능함, 그리고 정확함 대 견고함이라는 이름표가 붙은 네 개의 수평 슬라이더 축이 지나갑니다. 하단의 도장에는 기호적 동반자, 열셋 중 열셋 역량 검사 통과라고 적혀 있고, 점선 화살표가 오른쪽 열에서 3권이라는 이름표가 붙은 벡터들의 부드러운 구름을 향해 뻗어 있습니다. 권 말미의 원장: 왼쪽 열은 각각 초록색 역량 검사로 인증된 보장들이고, 오른쪽 열은 기호가 내놓을 수 없는 것들이며, 그 아래에는 네 개의 긴장 슬라이더가 있고, 점선 화살표는 열려 있는 오른쪽 열을 신경망 기둥에 건네줍니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

무엇이 진정으로 견고한가​

이 권에 담긴 세 가지 결과는 수사가 아닙니다; 그것들은 기계적이고 재현 가능하며, 각각은 통과하거나 빌드를 붉게 물들이는 검사로 지켜집니다.

분류는 건전하고, 완전하며, 다항식적입니다 — 그리고 HermiT와 일치합니다​

서술 논리의 핵심 보장은 분류(classification)입니다: 공리가 강제하는 모든 포섭 관계 A⊑BA \sqsubseteq B("AA가 BB에 포섭된다", 즉 모든 AA는 필연적으로 BB이기도 하다고 읽습니다)를 계산해 내는 것입니다. 학계 온톨로지에 대해 el_completion.py에 있는, 처음부터 작성된 완성기(completer)는 포섭 쌍들의 집합 cl(T)\mathrm{cl}(\mathcal{T})를 반환하며, 그 보장은 하나의 "필요충분조건"입니다:

(A,B)∈cl(T)⟺T⊨A⊑B.(A, B) \in \mathrm{cl}(\mathcal{T}) \quad\Longleftrightarrow\quad \mathcal{T} \models A \sqsubseteq B.

왼쪽에서 오른쪽으로 가는 방향이 건전성(soundness)입니다 — 도출된 모든 포섭 관계가 실제로 모든 모델에서 성립한다는 것입니다. 오른쪽에서 왼쪽으로 가는 방향이 완전성(completeness)입니다 — 함의되는 모든 포섭 관계가 도출되며, 그 무엇도 놓치지 않는다는 것입니다. 검사 2(validate.py 51–63번째 줄)는 정확한 답 집합을, 즉 표제가 되는 ("Professor", "Person")을 포함한 여덟 개의 쌍을 못 박아 두므로, 건전성이나 완전성이 깨지는 날 바로 그 단언이 실패합니다. 그리고 이 분류기는 손수 만든 것이기 때문에, 이 권은 독립적인 오라클(oracle)에 대해서도 그것을 검증합니다: reasoners.py는 owlready2 안에 동일한 온톨로지를 다시 구축하고 HermiT(완전한 OWL 2 DL 추론기)를 실행하는데, 이는 8개의 포섭 관계 전부와 두 개의 충족 불가능한 개념 모두에 대해 일치합니다.

이 보장의 나머지 절반은 다루기 쉬움(tractability)입니다. EL — 논리곱 ⊓과 존재 한정 ∃만을 정확히 유지하는 경량 서술 논리 — 은 분류가 온톨로지 크기에 대해 PTIME(다항 시간, polynomial time)으로 실행되도록 설계되었습니다 [2]. 그 이유는 완성 과정 안에서 직접 눈에 보입니다: 포화된 포섭자 관계 SS는 최대 ∣NC∣2|N_C|^2개의 쌍을 담을 수 있고 역할 관계 RR은 최대 ∣NR∣⋅∣NC∣2|N_R| \cdot |N_C|^2개를 담을 수 있으므로(NCN_C는 개념 이름, NRN_R은 역할 이름입니다), 그 단조로운 상승은 멈춰야만 하기 전까지 오직 다항식 개수만큼의 사실만 더할 수 있습니다. 검사 5(validate.py 83–90번째 줄)는 정확히 그 모양 — 안정된 라운드까지의 단조 성장 — 을 인증합니다:

    rounds = res["rounds"]
    for (s0, r0), (s1, r1) in zip(rounds, rounds[1:]):
        assert s1 >= s0 and r1 >= r0, rounds       # monotone growth
    assert rounds[-1] == rounds[-2], rounds        # last round added nothing
    assert rounds[0] == (23, 0) and rounds[-1] == (39, 7), rounds

학계 세계 위에서 그 상승은 세 라운드 만에 (23,0)(23, 0)에서 (39,7)(39, 7)로 안정됩니다 — 7장의 클레이니 상승(Kleene climb)의 고정점이, 이제는 규칙 베이스 대신 온톨로지를 포화시키고 있는 것입니다. 건전성, 완전성, 그리고 다항식 상한, 이 셋이 한꺼번에 성립하는 것 — 그것이 바로 어떤 순수 신경망 모델도 현재로서는 자신의 출력에 대해 할 수 없는 보장입니다.

체이스는 확실한 답을 계산합니다​

개방 세계 아래에서의 질의 응답은 그 자신의 보장을 가집니다. 논리곱 질의(conjunctive query) Q(xˉ)Q(\bar x)가 주어졌을 때, 확실한 답(certain answers)이란 온톨로지의 모든 모델에서 참인 튜플입니다:

cert(Q,O)  =  { aˉ:O⊨Q(aˉ) }  =  { aˉ:aˉ∈QI for every model I }.\mathrm{cert}(Q, \mathcal{O}) \;=\; \{\, \bar a : \mathcal{O} \models Q(\bar a) \,\} \;=\; \{\, \bar a : \bar a \in Q^{\mathcal{I}} \text{ for every model } \mathcal{I} \,\}.

20장의 체이스(chase)는 이를 계산 가능하게 만듭니다: 그것은 존재 규칙(튜플 생성 종속성, tuple-generating dependencies, TGD)을 포화될 때까지 발동시켜, 준동형사상(homomorphism)으로 다른 모든 모델에 사상되는 단 하나의 보편 모델(universal model) UU를 만들어 냅니다. 그러면 튜플 aˉ\bar a는, 모든 상수를 고정하는 h(xˉ)=aˉh(\bar x) = \bar a를 만족하는 QQ의 몸체로부터 UU로의 준동형사상 hh가 존재할 때 정확히 확실한 답이 됩니다. 결정적으로, 발명된 널은 결코 확실한 답이 될 수 없는데, 왜냐하면 다른 모델이라면 다른 증인을 선택했을 수도 있기 때문입니다. 검사 9(validate.py 129–135번째 줄)는 이를 어떤 여지도 없이 진술합니다:

@check("certain answers are computed by homomorphism over the chase")
def _certain_answers():
    r = chase.chase(chase.CHASE_INSTANCE, chase.TERMINATING_TGDS, restricted=True)
    body, avars = chase.Q_ADVISES_STUDENT
    ca = chase.certain_answers(body, avars, r["instance"])
    assert ca == {("alice",), ("bob",)}, ca      # both professors, only constants
    assert chase.query_holds(body, r["instance"])

"누가 학생을 지도하는가?"에 대한 확실한 답은 alice와 bob입니다 — 둘 다 이름 붙은 상수이며, 발명된 지도교수는 전혀 없습니다 — 그리고 주석은 정확히 그 이유를 말해 줍니다: 오직 상수만이 모든-모델 검사에서 살아남는다는 것입니다.

유래와 주석은 사실이 어디서 왔는지, 그리고 얼마나 확신하는지를 추적합니다​

세 번째 견고한 결과는, 기호적 도출이 진리와 함께 메타데이터를 실어 나를 수 있다는 것입니다. annotated.py는 서로 다른 반환(semiring)을 통해 동일한 도달가능성 사실을 다시 계산하며, 검사 11(validate.py 147–156번째 줄)은 사실 reach(p3,p1)이 유래 다항식(provenance polynomial) t + r·s를 지닌다는 것을 인증합니다 — 이는 그것이 단일 엣지 tt 하나로 또는 두 엣지 rr과 ss가 함께 성립함을 뜻하며 — Which, Why, 불(Boolean) 유래가 모두 일치합니다. 신뢰도도 같은 궤도를 따릅니다: 구간 [0,1][0, 1] 위에서 논리곱은 만남(meet) =min⁡= \min이고 논리합은 이음(join) =max⁡= \max이므로, 어떤 사실의 신뢰도는 도출 경로들에 걸쳐 각 경로에서 가장 약한 엣지 중 최선의 값입니다. 검사 12(validate.py 159–165번째 줄)는 이를 못 박습니다:

    # max over paths of min over edges: max(0.5, min(0.9, 0.8)) = 0.8
    assert ann.provenance_of(fact, ann.CONFIDENCE) == 0.8
    assert ann.conf_meet(0.9, 0.8, 0.5) == 0.5    # conjunction ⊓
    assert ann.conf_join(0.9, 0.8, 0.5) == 0.9    # disjunction ⊔

여러분은 어떤 결론이 어디서 왔는지에 대한 감사 가능한 기록과, 각 입력이 얼마나 확실했는지에 대한 원칙 있는 결합을 손에 넣습니다 — 신뢰와 추적 가능성(traceability)의 원재료입니다.

손이 닿지 않는 채로 남는 것​

이제 다른 쪽 열입니다. 각각의 간극은 어떤 강점의 그림자입니다.

누락되거나 잡음 섞인 사실에 대한 부서지기 쉬움. 개방 세계 가정(open-world assumption)은 견고함이 아닙니다; 그것은 원칙에 입각한 기권(abstention)입니다. advises(bob, carol)을 지워 보십시오, 그러면 추론기는 "아마도 여전히 지도하고 있을 것"이라는 식으로 우아하게 성능이 저하되지 않습니다 — 그것은 그저 그것을 필요로 했던 무엇이든 함의하기를 멈추고, 아무 오류도 보고하지 않습니다. TenuredStudent를 채우는 잘못된 단언 하나를 더해 보십시오, 그러면 Professor ⊓ Student ⊑ ⊥이기 때문에 모델은 비일관적이 되고 고전적 함의는 모든 것을 도출합니다. 기호는 여러분이 적어 둔 지식에 대해서는 정확하지만, 여러분이 잘못 적은 지식에 대해서는 침묵하거나 — 혹은 파국적입니다.

학습 없음. 이 권의 그 무엇도 데이터로부터 공리를 귀납하지 않습니다. 모든 포섭 관계, 역할 사슬, 서로소 관계는 손으로 작성된 것입니다; 완성기는 오직 그것들의 귀결을 펼쳐낼 뿐입니다. 추론기는 지도교수가 지도 학생과 공동 저술하는 경향이 있다는 것을 알아채고 그 규칙을 제안할 수 없습니다 — 그것은 오직 여러분이 이미 작성해 둔 규칙만을 검사할 수 있습니다.

신뢰도는 손으로 설정된 것이지, 보정된 것이 아닙니다. 위의 0.8은 [0,1][0, 1] 격자(lattice) 위에서 이루어진 진짜 산술이지만, 입력값 0.9, 0.8, 0.5는 관측된 빈도에 맞춰진 것이 아니라 온톨로지에 직접 입력된 것입니다. 결합 방식은 원칙에 입각해 있지만, 사전값(prior)은 그저 규정된 것입니다. 기호적 신뢰도는 "이 숫자들이 주어졌을 때 그것들이 어떻게 결합되는가"에는 답하지만, "이 숫자들이 올바른 것인가"에는 결코 답하지 않습니다.

종료성은 일반적으로 결정 불가능합니다. 존재 한정이 자신의 출력을 다시 자신의 입력으로 되먹일 수 있게 되는 순간, 체이스는 영원히 실행될 수 있습니다. 검사 10(validate.py 138–143번째 줄)은 모든 연구자에게 새로운 지도교수를 발명하고, 그런 다음 그 지도교수에게도 새로운 지도교수를 발명하여 결코 멈추지 않는 규칙을 붙잡아 냅니다 — 이 하니스(harness)는 오직 50회 발동 상한으로만 그것을 유계로 만듭니다. 임의의 TGD 집합이 종료하는 체이스를 가지는지, 그리고 어떤 질의가 함의되는지는 일반적으로 결정 불가능합니다; 결정 가능한 부분집합들(약한 비순환, 가드된, 끈적한)은 표현력을 포기함으로써 그 보장을 되사 옵니다.

이 시리즈 전체가 되돌아오는 네 가지 긴장​

이 간극들은 서로 무관한 네 가지 불평이 아닙니다; 그것들은 네 개의 축이며, 앞으로 등장할 모든 방법은 그 위에 위치를 부여받을 수 있습니다 [3]. 각 축은 이 권이 실제로 출력하는 하나의 숫자에 닻을 내리고 있습니다.

긴장이 권이 보여 준 극반대편 극그 거래의 대가를 치르는 것
표현력 대 다루기 쉬움EL++: ⊓, ∃, ⊥, 역할 사슬 — PTIME, 3라운드 고정점SROIQ / OWL 2 DL — 최악의 경우 이중 지수OWL 프로파일 [2]
개방 세계 대 폐쇄 세계체이스 위에서의 확실한 답 (alice, bob만)데이터로그 최소 모델, 파도 [23, 41, 47, 47]그 과제가 실제로 원하는 가정이 무엇인지
완전함 대 확장 가능함완성이 모델 전체에 도달함, 39개의 sco 원자실제 온톨로지 위에서는 폐포(closure)가 폭발할 수 있음다항식적으로 유지되도록 설계된 EL 추론기(ELK)
정확함 대 견고함8개의 포섭 관계, 정확히 맞거나, 아니면 침묵함언제나 답하지만 근사할 뿐인 벡터3권, 신경망 기둥

이 권 안의 어떤 방법도 이 네 가지 모두에서 이기지 못합니다. 그것은 이 권의 결함이 아니라, 문제 자체의 모양이며, 신경-기호 분야가 존재하는 이유입니다.

증거를 실행 가능하게 만들기​

2권 전체에서 인용되는 모든 숫자는 validate.py가 지키고 있으며, 이는 단 하나의 규율 위에 세워져 있습니다: 요구사항이 곧 테스트다. 각 주장은 하나의 역량 검사(competency check)입니다 — 학계 온톨로지 위에서의 단순한 단언이며, 작은 데코레이터(validate.py 28–33번째 줄)에 의해 등록됩니다 — 그리고 이 프로세스의 종료 코드가 곧 평결입니다. main 루프(189–204번째 줄)는 모든 검사를 실행하고, 전부 성립할 때만 0을 반환합니다:

    total = len(CHECKS)
    print(f"\nsymbolic companion: {passed}/{total} competency checks passed")
    return 0 if passed == total else 1

핵심 주장마다 하나씩, 모두 열세 개의 검사가 있습니다. 다음은 전체 원장이며, 각 행은 그것을 실행하는 파일과 줄에 결부되어 있습니다:

#역량 검사있는 곳인증하는 것
1TBox가 네 개의 EL 정규형(+ 역할 사슬)으로 정규화됨validate.py 36-4714개의 공리가 16개의 정규형 공리가 됨, 2개의 새 이름; 형태별로 nf1×6, nf2×2, nf3×3, nf4×4, chain×1
2EL 완성이 위계를 올바르게 분류함validate.py 51-63Professor ⊑ Person을 포함한 8개의 포섭 관계
3바닥 규칙이 충족 불가능한 개념을 탐지함validate.py 66-74TenuredStudent, TenuredStudentAdvisor ⊑ ⊥; 나머지 8개 개념은 충족 가능함
4역할 사슬 규칙이 grand-advising을 도출함validate.py 77-80(Dean, Student) 쌍이 grandAdvisor에 있음
5포화가 단조적이며 안정된 고정점에 도달함validate.py 83-90라운드가 (23, 0)에서 (39, 7)까지 성장함; 마지막 라운드는 아무것도 더하지 않음
6데이터로그가 1권의 모델을 재현함validate.py 94-104파도 [23, 41, 47, 47]; 연구자 5명, grandAdvisor 3개, citesTransitively 3개, colleague 8개
7EL-as-Datalog가 완성과 일치함validate.py 107-11539개의 sco + 7개의 rel 원자; el_completion과 동일한 포섭 관계
8제한된 체이스가 무심한 체이스보다 나음validate.py 119-126제한된 체이스는 널 3개 / 3단계, 무심한 체이스는 널 5개 / 5단계
9체이스 위에서 준동형사상에 의한 확실한 답validate.py 129-135확실한 답은 alice와 bob — 상수만
10종료하지 않는 체이스가 발산함validate.py 138-143결코 종료하지 않음; 단계 상한에서 널 50개
11reach(p3,p1)의 유래 다항식은 t + r·s임validate.py 147-156다항식 t + r·s; which / why / 불(Boolean)이 일치함
12주석/퍼지 신뢰도가 [0,1] 격자에 의해 결합됨validate.py 159-165max(0.5, min(0.9, 0.8)) = 0.8; 만남(meet) 0.5, 이음(join) 0.9
13앨런의 13개 구간 관계가 분류되고 합성됨validate.py 169-18613개의 관계; meets ∘ meets는 before를 낳음; before ∘ before의 역은 13개 전부를 낳음

하니스를 실행하면 전체 원장과 그 최종 결론이 출력됩니다:

PASS  TBox normalizes to the four EL normal forms (+ role chains)
PASS  EL completion classifies the concept hierarchy correctly
PASS  the bottom rule detects the unsatisfiable concepts
PASS  the role-chain rule derives grand-advising
PASS  saturation is monotone and reaches a stable fixpoint
PASS  Datalog reproduces the Volume 1 academic-world model
PASS  EL-as-Datalog agrees with the from-scratch completion
PASS  restricted chase terminates with fewer nulls than the oblivious chase
PASS  certain answers are computed by homomorphism over the chase
PASS  the non-terminating chase diverges (bounded by a step cap)
PASS  the provenance polynomial of reach(p3,p1) is t + r·s
PASS  annotated/fuzzy confidence combines by the [0,1] lattice
PASS  Allen's 13 interval relations classify and compose correctly

symbolic companion: 13/13 competency checks passed

그 마지막 줄 — symbolic companion: 13/13 competency checks passed — 이 바로 이 권의 진짜 평결입니다. 이는 이 스물두 개의 장에 걸친 주장들이 신뢰에 의존해 주장된 것이 아니라 실행 가능하다는 것을 뜻하며, 그중 하나라도 참이기를 멈추는 날 main은 1을 반환하고 빌드는 붉게 물듭니다.

신경-기호 시스템을 구축하기 위한 정직한 조언​

이 권에서 하나의 작업 습관만을 가져간다면, 이것을 가져가십시오: 학습된 버전에 손을 뻗기 전에 과제의 명료한 기호적 버전을 먼저 모델링하십시오. 그 이유는 순수주의가 아니라 실용적인 것입니다. 일단 여러분이 건전하고 완전한 답이 무엇인지 — 정확한 8개의 포섭 관계, 두 개의 상수 alice와 bob, 유래 t + r·s — 를 진술할 수 있게 되면, 여러분은 신경망 근사를 견주어 잴 수 있는 정답(ground truth)을 손에 쥐게 됩니다. 그러면 여러분은 임베딩이 무엇을 반환해야 하는지를 정확히 말할 수 있고, 그것이 얼마나 벗어나는지 볼 수 있으며, 운 좋은 추측과 학습된 진실을 구별할 수 있습니다. 그 단계를 건너뛰면, 유창한 모델은 견주어 확인할 그 무엇도 없이 확신에 찬 답을 여러분에게 건네줄 것입니다. 기호적 모델은 학습이 대체하는 옛 방식이 아닙니다; 그것은 학습이 근사하려고 애쓰는 명세(specification)입니다.

아직 풀리지 않은 부분​

솔직한 미해결 질문은 이 두 열이 어떤 거래도 없이 병합될 수 있는가입니다. 이 분야가 시도해 온 모든 부분적 결합은 한 속성의 대가를 다른 속성으로 치르는 것처럼 보입니다: 학습기를 온톨로지를 존중하도록 제약하면 흔히 확장 가능성이나, 그것을 학습 가능하게 만들었던 매끄러운 기울기(gradient)를 잃게 됩니다; 추론기가 잡음을 용인하도록 허용하면 흔히 그 도장을 신뢰할 만한 것으로 만들었던 보장을 잃게 됩니다 [3]. 2권은 그 거래가 불가피하다고 말해 줄 수 없습니다 — 그리고 그렇다고 단언하는 것은 잘못일 것입니다. 2권은 오직, 엄밀하게 그리고 하나의 공유된 온톨로지 위에서, 기호적 보장이 필요하지만 충분하지는 않다는 것만을 확립합니다: 증명 가능하고 감사 가능한 진리라는 개념이 전혀 없는 시스템은 정작 중요한 곳에서 신뢰받을 수 없기에 필요하며; 바로 그 동일한 시스템이 누락된 사실에 대해 기권하고, 아무것도 학습하지 않으며, 언제나 멈출 수는 없기에 충분하지 않습니다. 어떤 하나의 시스템이 증명이 존재하는 곳에서는 정확하고, 그렇지 않은 곳에서는 견고하며, 완전함과 확장 가능함을 동시에 갖출 수 있는지는 진정으로 열려 있습니다 — 이는 남은 권들이 굴복하기 위해서가 아니라 공략하기 위해 존재하는 질문입니다.

왜 중요한가​

신경-기호적 내기는 이 두 열이 경쟁하는 것이 아니라 상호 보완적이라는 것입니다. 이 장은 그 내기가 아직 이겨지지 않은 이유에 대한 솔직한 진술입니다: 여러분은 그 보장들이 하나의 세계 위에서 초록색 검사를 얻어 내는 것을 보았고, 같은 세계 위에서 그 간극들이 여전히 열려 있는 채로 남는 것도 보았습니다. 그 그림을 명확히 붙잡고 있는 것 — 왼쪽에는 진짜 보장들, 오른쪽에는 진짜 한계들, 그리고 사라지지 않을 네 개의 긴장 — 이야말로 여러분이 앞으로 지니고 나아갈 수 있는 가장 유용한 것입니다. 그것은 여러분이 견고한 추측을 증명으로, 혹은 증명을 견고한 시스템으로 착각하지 않도록 지켜 주며, 진정한 신경-기호 방법이 진보로 인정받으려면 정확히 무엇을 내놓아야 하는지를 말해 줍니다: 한쪽에서 더 높은 숫자가 아니라, 양쪽 모두에서 도장을 얻어 내는 시스템입니다.

핵심 용어​

  • 평결(The verdict) — 기호는 여러분이 신뢰하고 설명할 수 있는 정확성을, 반드시 적어 두고 일관되게 유지해야 하는 지식 위에서 사 줍니다; 지능에 대해 필요하지만 충분하지는 않습니다.
  • 건전하고 완전한 분류(Sound and complete classification) — 분류기는 함의되는 포섭 관계를 모두, 그리고 오직 그것만을 도출합니다, (A,B)∈cl(T)  ⟺  T⊨A⊑B(A, B) \in \mathrm{cl}(\mathcal{T}) \iff \mathcal{T} \models A \sqsubseteq B; 여기서는 HermiT에 대해 검증되었습니다.
  • PTIME(다루기 쉬움, tractability) — EL 분류는 온톨로지 크기에 대해 다항 시간으로 실행됩니다; 학계 세계는 3라운드 만에 (23,0)(23, 0)에서 (39,7)(39, 7)로 포화됩니다.
  • 확실한 답(Certain answers) — 모든 모델에서 참인 튜플로, 체이스가 구축한 보편 모델로 질의를 준동형사상에 의해 사상함으로써 계산됩니다; 오직 상수만이 자격을 갖춥니다(alice, bob).
  • 유래 / 주석(Provenance / annotation) — 도출을 따라 함께 실려 가는 메타데이터: 다항식 t + r·s는 어떤 사실이 왜 성립하는지를 기록하며; [0,1][0, 1] 격자는 신뢰도를 만남(meet) =min⁡= \min, 이음(join) =max⁡= \max으로 결합합니다.
  • 개방 세계 기권(Open-world abstention) — 누락된 사실은 "함의되지 않음"을 낳을 뿐, 결코 "거짓"이나 "아마도"를 낳지 않습니다 — 견고함이 아니라 원칙에 입각한 침묵입니다.
  • 결정 불가능한 종료성(Undecidable termination) — 임의의 존재 규칙에 대해 체이스는 영원히 실행될 수 있고 함의는 결정 불가능합니다; 오직 제한된 부분집합만이 보장을 되찾습니다.
  • 네 가지 긴장(The four tensions) — 표현력 대 다루기 쉬움, 개방 세계 대 폐쇄 세계, 완전함 대 확장 가능함, 정확함 대 견고함: 이후의 모든 방법이 위치를 부여받는 축들입니다.
  • 역량 검사(Competency check) — 온톨로지 위에서의 실행 가능한 단언 하나; 이 권의 주장은 곧 그 테스트와 같으며, 종료 코드 — 13/13 — 가 곧 평결입니다.

이 장이 이끄는 곳​

2권은 여러분에게 보장들과 한계들, 그리고 그것들을 저울질할 하나의 세계를 건네주었습니다 — 그리고 답해지지 않은 하나의 질문도 함께: 정확한 기호와 견고한 벡터가 하나로 합쳐질 수 있을까요? 다음 권인 3권 — 신경 표현은 신경망 기둥을 발전시킵니다: 임베딩과 지식의 기하학적 표현으로, 여기서 개념은 하나의 영역이고 관계는 하나의 방향이며, 질의는 증명 대신 거리(distance)로 답해집니다. 이는 같은 지식 베이스이며, 하나의 지식과 하나의 질문을, 반대편 렌즈를 통해 바라본 것입니다 — 이 권의 보장이 필요로 하는 견고함을 지닌 기둥이자, 이 권의 도장이 채워 주도록 만들어진 그 보장의 결여를 지닌 기둥입니다.