정직한 평결: 기초가 주는 것

📍 현재 위치: 5부 · 평결 — 15장. 이전 장인 관통 예제는 alice, bob, carol, 논문 p1부터 p3까지, advises와 cites 엣지로 이루어진 하나의 작은 학계 세계가 이 책의 모든 방법을 한꺼번에 짊어지고 있는 모습을 보여주었습니다. 이제 우리는 그 장치들로부터 한 걸음 물러나, 기초 권의 끝에서 정말로 중요한 단 하나의 질문을 던집니다. 이 모든 것이 실제로 우리에게 무엇을 사주었는가?

여러분은 이미 많은 것을 밑바닥부터 만들어 왔습니다. 전방 연쇄 엔진, 목표를 거슬러 올라가며 증명을 탐색하는 증명기, 직선을 맞추는 회귀기, XOR을 깨뜨리는 신경망, 번역하는 임베딩까지 말입니다. 이 장은 새로운 도구를 더하지 않습니다. 대신 지금까지 쌓아온 것을 점검합니다. 정직한 평결은 짧으며, 세 부분으로 이루어져 있습니다. 여러분이 이제 손에 쥔 두 가지와, 아직 손에 쥐지 못한 한 가지입니다. 이 평결이 단순한 주장이 아니라 정직(honest)한 이유는, 그 안의 모든 주장이 여러분이 직접 실행할 수 있는 커밋된 코드 한 줄 한 줄이기 때문입니다. 이 장은 각 숫자 뒤에 있는 파일과 줄 번호를 명시하므로, 아래의 그 무엇도 그저 믿음으로 주장되지 않습니다.

쉽게 말하면

한 학기 동안 두 언어를 배웠다고 상상해 보십시오. 하나는 증명(proof)의 언어입니다. 모든 문장은 증명 가능하게 참이거나, 증명 가능하게 거짓이거나, 정직하게 알 수 없는 것 중 하나이며, "참"이라고 말할 때는 정확히 왜 그런지 보여줄 수 있습니다. 다른 하나는 닮음(resemblance)의 언어입니다. 이 언어는 결코 "모른다"고 말하지 않고 언제나 최선의 추측을 내놓으며, 그 추측은 섬뜩할 만큼 훌륭해집니다. 하지만 이 언어는 결코 풀이 과정을 보여주지는 못하고, 오직 자신감만을 보여줄 뿐입니다. 이제 여러분은 두 언어 모두에 유창합니다. 아직 할 수 없는 것은 이 둘을 한 호흡 안에서 동시에 말하는 하나의 대화입니다. 증명이 가능할 때는 증명하고, 그렇지 않을 때는 추측하는 것을 말입니다. 그 빠져 있는 이중언어 문장이 바로 뉴로-심볼릭 AI(neuro-symbolic AI)이며, 이 권 이후의 모든 내용은 그 문장을 쓰려는 시도입니다.

이 장에서 다루는 내용

• 평결, 있는 그대로 말하기 — 여러분은 1권을 마치며 뉴로-심볼릭 AI의 두 절반과 이를 판단할 잣대를 손에 쥐지만, 그 둘을 잇는 다리는 아직 갖지 못합니다.
• 진정으로 탄탄한 것 — 전방과 후방 양방향으로 실행되며, 정확히 47개 원자로 이루어진 고정점까지 파동 단위로 추적되는 명료하고 기계적인 증명 개념. 그리고 증명 가능하게 들어맞는 학습: 복원된 직선, XOR을 이겨내는 신경망, 참인 사실을 거짓인 사실보다 더 그럴듯하다고 순위 매기는 임베딩까지, 각각 코드와 한 줄 한 줄 대응하는 실제 숫자와 함께 제시됩니다.
• 여전히 활짝 열려 있는 것 — 정확한 증명기의 보장과 학습기의 강건함을 어느 쪽도 잃지 않은 채 잇는 일.
• 되풀이되는 세 가지 긴장 — 정확함 대 강건함, 설명 가능함 대 불투명함, 완전함 대 확장 가능함. 시리즈 전체가 계속 되돌아오는 이 세 축은 각각 코드가 실제로 출력하는 숫자에 근거합니다.
• 실행 가능해진 증거 — validate.py의 열두 가지 점검 장부. 각 주장을 파일과 줄 번호에 한 줄씩 대응시키며, 그 종료 코드가 이 권이 하는 모든 주장에 대한 평결이 됩니다.
• 어디서 시작할지 — 초보자를 위한 정직한 조언입니다. 어떤 과제든 먼저 명료한 심볼릭 버전을 배워 두면, 신경망 근사가 무엇을 반환해야 하는지 언제나 말할 수 있습니다.

평결, 있는 그대로 말하기

전체 결론을 세 개의 절로 말씀드리면 이렇습니다. 첫째, 여러분은 이제 뉴로-심볼릭 AI의 두 절반 모두를 손에 쥐고 있습니다. 이 용어는 신경망 학습을 심볼릭 추론과 결합하는 프로그램을 가리킵니다 [1]. 한쪽 절반은 정확하지만 부서지기 쉽습니다. 논리는 오직 진정으로 따라 나오는 것만을 도출하고 각 단계를 증명할 수 있지만, 질문이 자신의 규칙 밖으로 한 걸음만 벗어나도 그 즉시 침묵합니다. 다른 절반은 강건하지만 불투명합니다. 학습된 모델은 여러분이 던질 수 있는 어떤 질문에도 답하고 자신의 데이터를 넘어 일반화하지만, 확신에 차서 틀릴 수 있고 왜 그런지는 보여주지 못합니다. 둘째, 여러분은 그 둘을 판단할 잣대(yardstick)를 쥐고 있습니다. 공유된 어휘(증명(proofs), 고정점(fixpoints), 경사(gradients), 임베딩(embeddings))와, 두 절반이 정면으로 맞붙어 실행된 하나의 공유된 세계(23개의 단언된 사실이 7개 규칙 아래에서 닫혀 47개 원자로 이루어진 모델이 되는 학계 지식 베이스)가 그것입니다. 셋째 — 그리고 이것이 정직한 부분입니다 — 여러분은 아직 다리(bridge)를 쥐고 있지 않습니다. 1권의 그 무엇도 증명기의 보장을 학습기의 강건함과 이어 주지 않습니다. 두 절반이 같은 세계에 들어맞는다는 사실이야말로 그 둘 사이의 간극을 눈에 보이게 만드는 것이며, 그것을 메우는 일이 바로 남은 네 권이 존재하는 이유입니다 [2].

권의 끝에서 마주하는 저울: 정확하지만 부서지기 쉬운 심볼릭 절반과 강건하지만 불투명한 신경망 절반이 하나의 공유된 학계 세계 위에서 무게를 재고 있으며, 두 절반 사이의 다리는 아직 점선으로 된 간극일 뿐이고, 열두 가지 검사로 이루어진 장부가 양쪽 접시 위의 모든 것이 실제로 작동함을 인증합니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

진정으로 탄탄한 것

이 권 안의 두 가지 결과는 손짓으로 얼버무린 것이 아닙니다. 그것들은 기계적이고, 재현 가능하며, 코드로 지켜지고 있습니다. 이제 하나씩 살펴보며, 이번에는 그 메커니즘이 실제로 움직이는 모습을 지켜보겠습니다.

첫 번째 탄탄한 결과: 양방향으로 실행되는 증명

저울의 심볼릭 접시는 명료한 증명 개념 위에 놓여 있으며, 이 개념은 양방향으로 작동합니다. 전방으로 실행하면, 추론은 즉각귀결 연산자(immediate-consequence operator) $T_P$ — "T 아래첨자 P"라고 읽으며, 사실들의 집합을 받아 몸체가 현재 충족된 모든 규칙을 발동시키고, 입력에 더해 그 규칙들이 한 단계에서 결론짓는 모든 머리를 돌려주는 사상 — 를 반복 적용하는 것입니다. 원자들의 집합 $S$에 대해(원자(atom)란 advises(alice, bob)처럼 변수가 없는 하나의 사실입니다) 이를 풀어 쓰면 다음과 같습니다.

$$T_P(S) \;=\; S \,\cup\, \{\, \text{head} \;:\; \text{rule (head} \leftarrow \text{body) fires with its body true in } S \,\}.$$

기호 $\cup$는 집합 합집합(union, "둘 중 어느 한쪽에라도 있는 모든 것")이고, 중괄호 안의 콜론은 "다음을 만족하는"이라고 읽으며, 이 표현 전체는 정확히 forward_chain.py의 함수 t_p(42–49행)입니다. out = set(facts)가 $S$를 초기화하고, 그런 다음 조건이 맞는 각 규칙의 머리가 추가됩니다. $T_P$의 고정점(fixpoint)이란 연산자가 자기 자신으로 사상하는 집합, 즉 $T_P(S) = S$입니다. 규칙을 적용해도 이미 갖고 있던 것 외에는 아무것도 생기지 않는다는 뜻입니다. 최소 고정점(least fixpoint), 즉 $\mathrm{lfp}(T_P)$("lfp" = 최소 고정점, 그런 집합 가운데 가장 작은 것)는 프로그램의 의미이며, least_fixpoint의 루프(52–63행)는 기본 사실에서 시작해 연속된 두 라운드가 동일해질 때까지(if nxt == current: return) $T_P$를 반복 적용함으로써 그것에 도달합니다.

관통 예제 위에서 이 오름을 파동 단위로 살펴보겠습니다. 23개의 단언된 사실에서 시작하며, 아래 표의 각 행은 $T_P$의 한 번의 적용입니다. 아래 표에는 두 개의 기호가 등장합니다. ⟹는 "따라서 / 함의한다"로 읽고, ∧는 "그리고"로 읽습니다.

파동	연산자	이번 파동에서 새로 생긴 원자와 그 이유	누적 크기
0	— (단언됨)	23개의 기본 사실 (클래스 소속 5개, advises 4개, authored 4개, cites 2개, affiliated 5개, about 3개)	23
1	23에 대한 $T_P$	researcher +5 (교수 또는 학생 ⟹ researcher), grandAdvisor +3 (advises와 advises의 합성), colleague +8 (같은 기관 소속), citesTransitively +2 (기저 사례, cites 엣지당 하나)	41
2	41에 대한 $T_P$	person +5 (researcher ⟹ person), citesTransitively(p3, p1) +1 (재귀 단계: cites(p3, p2) ∧ citesTransitively(p2, p1))	47
3	47에 대한 $T_P$	새로 생기는 것 없음: $T_P(S) = S$이므로 고정점이 확인됨	47

이 누적 크기는 정확히 forward_chain.py가 출력하는 값입니다: sizes per round: [23, 41, 47, 47], 그다음 47 atoms total, 24 derived. 24개의 도출된 원자는 남김없이 researcher 5개 + person 5개 + grandAdvisor 3개 + colleague 8개 + citesTransitively 3개로 분해되며, $23 + 24 = 47$입니다.

이 추적 과정에서 두 가지 특징이야말로 단 한 번의 통과가 아니라 고정점이 필요한 이유 전체입니다. 첫째, person(alice)는 파동 2가 되어서야 나타날 수 있는데, 규칙 person(X) ← researcher(X)가 researcher(alice)를 필요로 하고, 그 자체가 파동 1에서야 비로소 도출되기 때문입니다. 결론이 또 다른 결론을 낳는 것입니다. 둘째, citesTransitively(p3, p1) 역시 파동 2를 기다리는데, 재귀 규칙 citesTransitively(A, C) ← cites(A, B), citesTransitively(B, C)가 자신의 머리를 다시 자신의 몸체로 되먹이기 때문입니다. 인용 사슬 p3 → p2 → p1의 폐쇄는 단순한 조회가 아니라 진정한 재귀입니다. 아무것도 더하지 않는 네 번째 통과(sizes[-1] == sizes[-2], 즉 47 == 47)는 엔진이 스스로 끝났음을 증명하는 것이며, 검사 _fc_stable(validate.py, 52–57행)이 정확히 그것을 못 박습니다. 이 검사는 model == fc.t_p(model, rules)를 단언하는데, 이는 곧 $T_P(S) = S$라는 명제 그 자체입니다.

다른 방향으로 실행해도 똑같은 사실들이 목표에서부터 거꾸로 도출됩니다. sld.py의 SLD 증명기는 질의에서 출발하여 "어떤 규칙이 이것을 결론지을 수 있으며, 그렇다면 그 몸체는 무엇을 필요로 하는가"를 물으며, 단순한 '예'가 아니라 감사 가능한 증명 트리(proof tree)를 돌려줍니다. grandAdvisor(alice, carol)을 물으면(sld.py, prove, 63–75행; Proof.render, 29–34행이 렌더링) 다음이 출력됩니다.

grandAdvisor(alice, carol)
  advises(alice, bob)
  advises(bob, carol)

이것을 눈으로 검토할 수 있는 하나의 도출 과정으로 읽으십시오. 목표 grandAdvisor(alice, carol)은 X = alice, Y = bob, Z = carol로 단일 규칙 grandAdvisor(X, Z) ← advises(X, Y), advises(Y, Z)에 의해 성립되며, 각 잎, 즉 advises(alice, bob)과 advises(bob, carol)은 더 이상의 증명이 필요 없는 기본 사실입니다. 두 방향을 잇는 깊은 사실은 그것들이 일치한다는 점입니다. 전방 엔진이 도출하는 모든 것을 후방 증명기 또한 증명할 수 있습니다. 검사 _fc_sld_agree(validate.py, 77–82행)는 이를 조금의 여지도 없이 단언합니다. 모델 안의 47개 원자 전부를 훑으며 각각에 대해 sld.provable(atom)을 단언합니다.

@check("forward and backward chaining agree on membership")
def _fc_sld_agree():
    facts, rules = program()
    model = fc.least_fixpoint(facts, rules)
    for atom in model:
        assert sld.provable(atom), f"SLD failed to prove derived atom {atom}"

이는 완전성(completeness)을 구체적이고 실행 가능하게 만듭니다. 전방 엔진이 도출하는 모든 원자를 후방 증명기 또한 증명할 수 있으며(모델 전체가 SLD가 증명할 수 있는 것의 부분집합입니다), 이것이 더 이상 참이 아니게 되는 날 종료 코드는 빨갛게 바뀝니다. 그 거울상인 건전성(soundness) — 증명기가 모델 안에 있는 원자만을, 가짜 없이 오직 그것만을 증명한다는 것 — 은 이 루프가 반복하는 대상이 아닙니다. 그것은 SLD 리졸루션이 확정 혼 절(definite Horn clause)에 대해 건전하다는 사실로부터 따라 나오며, 이 장은 74행의 단 하나의 부정 검사 assert not sld.provable(("advises", "alice", "carol"))로 그것을 표본 확인합니다. 이는 증명기가 올바르게 도출을 거부하는 비사실입니다.

두 번째 탄탄한 결과: 증명 가능하게 들어맞는 학습

신경망 접시는 증명 가능하게 들어맞는 학습 위에 놓여 있습니다. 이것은 "모델이 괜찮아 보였다"는 말이 아니라, 성립하거나 빌드를 실패시키거나 둘 중 하나인 단언입니다. "데이터에 함수를 맞춘다"는 것의 세 가지 얼굴이 있으며, 각각 우리가 눈으로 직접 살펴볼 수 있는 단 하나의 세계 위에서 시연됩니다.

첫 번째는 선형 회귀(linear regression)입니다. 경사 하강법(gradient descent) — 오차가 가장 가파르게 증가하는 방향을 가리키는 부분 기울기의 벡터인 경사(gradient)를 따라 파라미터를 내리막으로 살짝 밀어내는 것이므로, 그 음의 방향이 내리막을 가리킵니다 — 은 직선의 기울기를 복원해 냅니다. 파일 안의 다섯 개 점에 대해 fit_line(learning.py, 22–37행)을 실행하면 line: y = 1.990 x + 0.050 (loss 44.182 -> 0.0214)가 출력됩니다. 참된 기울기 2.0에 가까운 값이 복원되었고, 평균제곱오차 손실은 44.182에서 0.0214로, 백 배 넘게 떨어졌습니다. 검사 _learning(validate.py, 133–141행)은 assert l1 < l0 / 100과 assert abs(w - 2.0) < 0.1 두 사실을 한꺼번에 지킵니다.

두 번째는 관통 예제에 직접 뿌리내린 로지스틱 분류기(logistic classifier)입니다. 이 분류기의 두 특징은 advise_features(learning.py, 49–64행)에 의해 advises 관계에서 곧바로 읽어낸 것입니다. 각 사람에 대해, 나가는 차수(out-degree, 그 사람이 지도하는 사람 수)와 들어오는 차수(in-degree, 그 사람을 지도하는 사람 수)입니다. 교수는 레이블 1, 학생은 레이블 0을 받습니다. 코드가 만드는 정확한 표는 다음과 같습니다.

사람	나가는 차수	들어오는 차수	레이블
alice	1	0	교수 (1)
bob	2	1	교수 (1)
carol	1	1	학생 (0)
dave	0	1	학생 (0)
erin	0	1	학생 (0)

어느 한 열만으로는 두 집단을 가를 수 없습니다. carol(학생)과 alice(교수)는 나가는 차수가 똑같이 1이고, bob(교수)과 학생들은 모두 들어오는 차수가 1입니다. 분류기는 반드시 두 특징 모두에 의존해야 하며, fit_logistic(67–85행)은 교차 엔트로피 손실에 대한 경사 하강법으로 그 조합을 찾아내어 logistic: weights=[7.75, -8.59] bias=-2.76 loss=0.010을 출력하고, 다섯 사람 모두 올바르게 레이블링됩니다. 부호는 정확히 우리가 바라는 대로의 정성적 규칙을 따릅니다. 나가는 차수 가중치는 크고 양수입니다(사람을 지도하는 것은 교수라는 증거입니다). 들어오는 차수 가중치는 크고 음수입니다(지도를 받는 것은 학생이라는 증거입니다). 같은 검사 _learning이 preds == y를 단언합니다.

세 번째는 XOR, 즉 어떤 직선도 갈라놓을 수 없는 배타적 논리합 패턴(두 입력이 다르면 출력 1, 같으면 출력 0)입니다. 선형 분류기는 증명 가능하게 네 가지 경우 중 세 개를 넘겨 맞힐 수 없으며, neural.py가 이를 확인해 줍니다: linear classifier on XOR: [1, 1, 1, 1] ... correct: 2 / 4. 은닉층 하나를 더하면 — train_mlp(neural.py, 31–67행)에서 역전파로 학습되는 2-4-1 다층 퍼셉트론(multi-layer perceptron, MLP) — 네 가지 경우 모두가 맞게 나옵니다: 2-4-1 MLP on XOR: [0, 1, 1, 0] ... correct: 4 / 4 (loss 0.0003). 검사 _neural(validate.py, 145–154행)은 두 절반을 모두 명시합니다. 직선에 대해서는 assert lin_correct < 4를, 네트워크에 대해서는 assert mlp == [int(v) for v in neural.XOR_Y]를 말입니다.

    params, loss = neural.train_mlp(neural.XOR_X, neural.XOR_Y)
    mlp = [neural.predict_mlp(params, x) for x in neural.XOR_X]
    assert mlp == [int(v) for v in neural.XOR_Y], mlp   # MLP gets all four

세 번째 탄탄한 결과: 기하로서의 의미

같은 내리막 요령을 기호에 적용하면, 처음부터 만든 TransE 임베딩이 나오는데, 여기서 관계는 하나의 이동(translation)입니다. 참인 트리플(머리 $h$, 관계 $r$, 꼬리 $t$)은 $\mathbf{h} + \mathbf{r} \approx \mathbf{t}$를 만족해야 하며, 굵은 글씨는 각 개체와 관계에 배치된 두 좌표짜리 벡터이고, $\approx$는 "근사적으로 같다"로 읽습니다. 트리플의 그럴듯함은 그 근사가 얼마나 심하게 틀리는지, 즉 거리(embeddings.py, score, 79–82행)로 측정됩니다.

$$\text{score}(h, r, t) \;=\; \big\lVert\, \mathbf{h} + \mathbf{r} - \mathbf{t} \,\big\rVert \;=\; \sqrt{\textstyle\sum_{i} (h_i + r_i - t_i)^2}.$$

여기서 $\lVert \cdot \rVert$는 벡터의 유클리드 길이(Euclidean length, 좌표를 제곱하여 더한 값의 제곱근)이고, $\sum_i$는 좌표 $i = 1, 2$에 대한 합이며, $\sqrt{\cdot}$는 보통의 제곱근입니다. 낮을수록 이동이 더 잘 들어맞는다는 뜻이므로, 좋은 임베딩은 참인 트리플을 거짓인 트리플보다 아래에 둡니다. 학습 후(시드가 고정되어 재현 가능합니다), embeddings.py는 정확히 그 순서를 출력합니다.

점수가 매겨진 트리플	평균 / 값	해석
참인 트리플 (모든 이항 사실)	1.609	$\mathbf{h} + \mathbf{r} \approx \mathbf{t}$ 패턴에 잘 들어맞음
손상된 트리플 (꼬리를 바꿔치기함)	2.737	더 나쁘게 들어맞음 — 약 1.13의 뚜렷한 격차
advises(alice, bob) (실제 엣지)	0.399	낮은 점수: 기하가 이를 믿음
advises(alice, erin) (비엣지)	0.929	더 높은 점수: 기하가 이를 의심함

검사 _embeddings(validate.py, 158–165행)는 전체 격차 assert true_s < corr_s(1.609가 2.737 아래)와, 단일 엣지 순서 assert s_true < s_false(0.399가 0.929 아래)를 모두 단언합니다. 회귀, 신경망, 지식 그래프 임베딩 — 이 셋은 "데이터에 함수 맞추기"라는 하나의 발상이 지닌 세 가지 얼굴이며, 각각 우리가 눈으로 직접 살펴볼 수 있는 단 하나의 세계 위에서 시연되었고, 각각 통과하거나 빌드를 빨갛게 물들이는 단언에 의해 지켜지고 있습니다.

여전히 활짝 열려 있는 것

이제 간극을 살펴보겠습니다. 각 절반은 상대방이 결코 할 수 없는 일을 정확히 훌륭하게 해냅니다. 증명기는 자신의 논리에 대해 건전하고 완전합니다(sound and complete). 따라 나오는 것을, 오직 그것만, 모두 도출합니다. 하지만 그 밖의 모든 것에 대해서는 침묵합니다. advises(alice, erin)인지 물으면 그것은 그저 거부합니다. 그 엣지는 단언되지도 않았고 어떤 규칙으로도 도출되지 않으므로, 증명기는 침묵에 빠집니다. 검사 _sld_answers는 유사한 비사실 advises(alice, carol)을 한 줄로 표본 확인합니다. assert not sld.provable(("advises", "alice", "carol"))(validate.py, 74행)입니다. 어느 엣지에 대해서도 증명기는 "도출 불가능"이라고만 답할 뿐, 결코 "가능성이 낮다"고는 답하지 않습니다. 증명기에는 정도(degree)라는 개념이 없습니다. 임베딩은 그 거울상입니다. 결코 침묵하지 않으며, 여러분이 이름 붙일 수 있는 어떤 트리플에도 숫자를 돌려주지만, 결코 확신하지도 않습니다. 어떤 단일한 숫자든 틀릴 수 있기 때문입니다. 임베딩은 비엣지 advises(alice, erin)에 0.929점을 매기는데, 이는 실제 엣지의 0.399점보다 높으므로 순위는 옳지만, 0.929는 하나의 힌트일 뿐 평결이 아니며, 그 기하 안의 그 무엇도 그것을 보장해 주지 않습니다. 이 분야 전체가 안고 있는 아직 풀리지 않은 공학적 문제는 이 둘을 융합하는 것입니다. 증명이 존재하는 곳에서는 증명기의 보장을 지키면서, 증명이 없는 곳에서는 학습기의 강건한 추측으로 물러날 수 있는 하나의 시스템을, 그 융합이 어느 한쪽의 성질도 조용히 파괴하지 않은 채로 만들어 내는 것입니다. 1권이 이 두 극을 유별나게 선명하게 보여주는 것은, 정확히 그것이 결코 그 둘을 이어 붙였다고 흉내 내지 않기 때문입니다.

시리즈 전체가 계속 되돌아오는 세 가지 긴장

이 간극은 하나의 불일치가 아니라 세 가지이며, 그것들에 이름을 붙이는 일이 뉴로-심볼릭 AI에 대해 명료하게 생각하는 것의 절반을 차지합니다. 앞으로 나올 권들의 모든 방법은 이 세 축 위 어디에 자리 잡고 있는지로 그 위치를 찾아낼 수 있으며 [3], 각 축은 이 권이 실제로 출력하는 숫자에 근거하고 있습니다.

정확함 대 강건함. 전방 연쇄는 정확합니다. 47개 원자는 증명 가능하게 옳고 규칙에 대해 증명 가능하게 완전하며, 추적 [23, 41, 47, 47]은 폐쇄에 도달했고 그것이 안정적임이 인증되었음을 보여줍니다. 하지만 부서지기 쉽습니다. 규칙 집합 밖의 사실 하나만 있어도 아무 말도 하지 않습니다. TransE는 강건합니다. 거부 대신 그럴듯함(비엣지에 대해 0.929)으로 우아하게 성능이 떨어질 뿐입니다. 하지만 부정확합니다. 그 거리는 하나의 힌트일 뿐, 평결이 아닙니다. 여러분은 보장을 가질 수도, 우아한 실패를 가질 수도 있습니다. 이 권은 결코 둘을 동시에 갖지 못했습니다.

설명 가능함 대 불투명함. SLD 증명 트리가 곧 설명 그 자체입니다. advises(alice, bob)과 advises(bob, carol)로부터 grandAdvisor(alice, carol)을 도출하는 두 줄짜리 도출 과정은 사람이 읽고 검토할 수 있는 사슬이며, 검사 _sld_proof(validate.py, 61–66행)는 두 잎이 모두 그 안에 나타남을 단언합니다. 분류기가 교수와 학생을 가르도록 해 주는 가중치 [7.75, -8.59], 혹은 XOR을 풀어내는 은닉층 파라미터들은 겉으로 아무것도 설명하지 않습니다. 그것들은 읽을 수 있는 이유가 전혀 없는, 작동하는 답일 뿐입니다. 심볼릭 추론은 구조상 투명하며, 학습된 모델은 기본적으로 불투명합니다.

완전함 대 확장 가능함. 고정점 반복은 완전합니다. 최소 모델 전체, 즉 47개 원자 모두에 도달하며, 그것이 유도하는 개념 위계는 진정한 순서입니다. 검사 _orders는 professor ⊑ researcher ⊑ person(여기서 ⊑는 "~에 포섭된다", 즉 "~의 하위 클래스이다"로 읽습니다)을 확인하며, join("professor", "student") == "researcher"(둘의 최소 공통 상위 클래스)와 meet("professor", "student") is None(공통 하위 클래스 없음)도 함께 확인합니다. 바로 그 완전성이 실제 지식 베이스 위에서는 폭발할 수 있는 원인이며, 그곳에서는 폐쇄가 입력보다 천문학적으로 더 커질 수 있습니다. 임베딩이 수백만 개의 엣지를 가진 그래프까지 규모를 늘릴 수 있는 것은 정확히 그것이 결코 완전해지려 하지 않기 때문입니다. 그것은 근사할 뿐이며, 보장을 우아한 숫자와 맞바꿉니다. 커버리지와 비용은 서로를 잡아당깁니다.

이 책의 어떤 단일한 방법도 이 세 축 모두에서 승리하지 못합니다. 이것은 이 책의 실패가 아닙니다. 이것은 문제 자체의 모양이며, 이 분야가 존재하는 이유입니다.

실행 가능해진 증거

이 권에서 인용된 모든 숫자는 동반 프로그램 validate.py에 의해 지켜지며, 이 프로그램은 하나의 원칙 위에 세워져 있습니다: 요구사항이 곧 테스트다(requirements are tests)라는 원칙입니다. 이 책이 내세우는 각 주장은 하나의 역량 검사(competency check) — 관통 예제에 대한 하나의 평이한 단언이며, 자그마한 check 데코레이터(validate.py, 29–33행)에 의해 등록됩니다 — 이며, 이 프로세스의 종료 코드가 곧 평결입니다. main 루프(168–183행)는 모든 검사를 실행하고, 통과한 개수를 세며, 모든 검사가 성립할 때에만 0을 반환합니다.

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

검사는 모두 열두 개이며, 이 권의 핵심 주장들에 일대일로 대응합니다. 아래는 각 행이 그것을 실행하는 파일 및 줄 번호와, 그것이 인증하는 숫자나 사실에 묶인 전체 장부입니다.

#	역량 검사	위치	인증하는 것
1	전방 연쇄가 최소 고정점에 도달함	validate.py 37–49	researcher 5개, grandAdvisor 쌍 3개, citesTransitively 3개, colleague 8개 — 24개의 도출된 원자
2	전방 연쇄가 종료됨(고정점이 안정적임)	validate.py 52–57	[23, 41, 47, 47]; T_P(model) == model
3	SLD가 증명 트리로 역할 사슬 목표를 증명함	validate.py 61–66	grandAdvisor(alice, carol) 트리가 두 지도 잎을 모두 포함함
4	SLD 질의 응답이 바인딩과 일치함	validate.py 69–74	colleague(alice, Who) = [bob]; advises(alice, carol)은 증명 불가능
5	전방 연쇄와 후방 연쇄가 일치함	validate.py 77–82	47개 원자 전부가 SLD로 증명 가능함
6	명제 진리표, 타당성, SAT, 함의	validate.py 86–93	항진명제는 타당하고, 모순은 충족 불가능하며, 함의가 성립함
7	구조 위에서의 1차 논리 충족	validate.py 97–106	모든 교수는 연구자이지만, 모든 학생이 교수인 것은 아님
8	관계 합성과 이행적 폐쇄	validate.py 110–119	advises ∘ advises (지도와 지도의 합성) = 조부모 지도 쌍 3개; cites⁺ (cites의 이행적 폐쇄) = 3쌍; affiliated는 함수적임
9	개념 위계는 부분순서임	validate.py 123–129	professor ⊑ researcher ⊑ person, 올바른 합과 곱
10	선형 및 로지스틱 회귀가 들어맞음	validate.py 133–141	손실이 100배 넘게 떨어짐, 기울기가 2.0의 0.1 이내, 5명 모두 정확함
11	은닉층이 직선이 실패하는 곳에서 XOR을 학습함	validate.py 145–154	선형 모델은 4개 중 4개 미만; 2-4-1 MLP는 4개 중 4개
12	TransE가 참인 트리플을 손상된 트리플보다 위에 매김	validate.py 158–165	1.609가 2.737 아래; 0.399가 0.929 아래

이 하니스(harness)를 실행하면 전체 장부와 그 최종 결과가 출력됩니다.

PASS  forward chaining reaches the least fixpoint (derived facts)
PASS  forward chaining terminates (fixpoint is stable)
PASS  SLD proves a role-chain goal with a proof tree
PASS  SLD query answering matches the intended bindings
PASS  forward and backward chaining agree on membership
PASS  propositional truth tables, validity, satisfiability, entailment
PASS  FOL satisfaction over the running example structure
PASS  relation composition and transitive closure
PASS  the concept hierarchy is a partial order with correct joins/meets
PASS  linear and logistic regression fit the data by gradient descent
PASS  a hidden layer learns XOR where a linear model fails
PASS  TransE embeddings score true triples above corrupted ones

logic companion: 12/12 competency checks passed

마지막 줄 — logic companion: 12/12 competency checks passed — 이 바로 이 권의 진짜 평결이며, 이후의 권들이 그대로 재사용하는 것과 똑같은 "요구사항이 곧 테스트다"라는 원칙입니다. 이는 이 평결이 요약하는 열네 개 장에 걸친 주장들이 믿음으로 단언된 것이 아니라 실행 가능하다는 뜻이며, 그 가운데 하나라도 더 이상 참이 아니게 되는 날 main은 1을 반환하고 빌드는 빨간불이 켜진다는 뜻입니다.

뉴로-심볼릭 AI를 시작하는 이에게 주는 조언

이 권에서 실전에 쓸 습관을 딱 하나만 가져가야 한다면, 이것을 가져가십시오. 신경망 버전에 손을 뻗기 전에 과제의 명료한 심볼릭 버전을 먼저 배우십시오. 그 이유는 순수주의가 아니라 실용적입니다. 건전하고 완전한 답이 무엇일지 — 정확한 47개 원자, 구체적인 두-잎 증명 트리, 지도 엣지의 참된 집합 — 를 말할 수 있게 되면, 여러분에게는 신경망 근사를 견주어 볼 그라운드 트루스(ground truth)가 생깁니다. 그러면 학습기가 정확히 무엇을 반환해야 하는지를 정밀하게 말할 수 있고, 그것이 얼마나 벗어나는지를 측정할 수 있으며, 틀린 추측이 감내할 만한 것인지를 알 수 있습니다. TransE 실행은 이 점을 구체적으로 보여줍니다. 우리는 advises(alice, erin)이 엣지가 아니라는 것을 이미 알고 있으므로, 점수 0.929는 의미를 갖게 됩니다. 우리는 그것이 실제 엣지의 0.399보다 위에 올바르게 순위 매겨졌음을 볼 수 있고, 또한 비교할 심볼릭 진실이 없다면 0.929라는 숫자 하나만으로는 아무것도 말해 주지 못한다는 것도 볼 수 있습니다. 이 단계를 건너뛰면, 유창한 모델은 확신에 찬 답을 건네주지만 그것을 견줄 것이 아무것도 없게 되고, 여러분에게는 운 좋은 추측과 학습된 진실을 구별할 방법이 전혀 없게 됩니다. 심볼릭 절반은 학습이 대체해 버린 옛 방식이 아닙니다. 그것은 학습 절반이 근사하려고 애쓰는 명세(specification)입니다.

아직 풀리지 않은 부분

정직하게 아직 풀리지 않은 질문은 다리를 거래 없이 지을 수 있는가입니다. 이 분야가 지금까지 시도한 모든 부분적인 결합은 하나의 성질을 다른 성질로 값을 치르는 것처럼 보입니다. 학습기가 논리 규칙을 존중하게 만들면 흔히 확장성을 잃고, 추론기가 잡음을 견디게 만들면 흔히 신뢰할 만하게 만들어 주었던 그 보장을 잃습니다 [3]. 1권은 이 거래가 피할 수 없는 것이라고 말해 줄 수 없습니다 — 그리고 그렇다고 단언하는 것은 실수일 것입니다. 이 권은 오직, 하나의 공유된 세계 위에서 두 절반이 상호 보완적인 강점을 지니며 아직 손안에 공짜 점심은 없다는 것을 엄밀하게 확립할 뿐입니다. 증명기는 완전하지만 자신의 규칙 밖에서는 침묵하고, 임베딩은 유창하지만 결코 확신하지 않으며, 각각을 인증하는 열두 가지 검사가 초록불인 것은 정확히 각 절반이 상대방의 과제가 아니라 자신이 만들어진 과제 위에서 측정되기 때문입니다. 단일한 시스템이 증명이 가능한 곳에서는 정확하고, 그렇지 않은 곳에서는 강건하며, 설명 가능하고, 완전하면서도 확장 가능한 것을 모두 동시에 이루어 낼 수 있는가는 진정으로 열려 있는 질문입니다 — 그리고 이는 다음 네 권이 인정하기 위해서가 아니라 공략하기 위해 존재하는 질문입니다.

왜 중요한가

뉴로-심볼릭 프로그램 전체는, 이 권 안의 두 전통이 경쟁하는 것이 아니라 상호 보완적이라는 내기 위에 놓여 있습니다. 논리의 보장과 학습의 도달 범위가, 둘 중 어느 하나도 홀로는 이루지 못하는 무언가로 합쳐질 수 있다는 내기입니다. 이 장은 그 내기가 아직 이기지 못한 이유를 정직하게 진술한 것입니다. 여러분은 같은 세계 위에서, 같은 잣대로, 두 절반이 작동하는 것을 보았고, 그 둘 사이의 이음매가 여전히 열려 있는 것도 보았습니다. 그 그림을 명확하게 붙들고 있는 것 — 탄탄한 두 절반, 아직 지어지지 않은 하나의 다리, 사라지지 않을 세 가지 긴장 — 이야말로 초보자가 이 시리즈의 나머지로 가져갈 수 있는 가장 쓸모 있는 단 하나입니다. 그것은 여러분이 강건한 추측을 증명으로, 혹은 증명을 강건한 시스템으로 착각하지 않게 막아 주며, 진짜 뉴로-심볼릭 방법이 진전으로 인정받기 위해 정확히 무엇을 내놓아야 하는지를 알려줍니다. 한쪽 접시에서 더 높은 숫자가 아니라, 양쪽 모두에서 초록불 검사를 얻어 내는 시스템 말입니다.

핵심 용어

• 뉴로-심볼릭 AI(Neuro-symbolic AI) — 시스템이 일반화하는 동시에 증명할 수 있도록 신경망 학습을 심볼릭 추론과 결합하는 프로그램이며, 이 시리즈 전체의 주제입니다.
• 두 절반(Both halves) — 정확하지만 부서지기 쉬운 심볼릭 절반(증명, 고정점)과 강건하지만 불투명한 신경망 절반(경사, 임베딩)이며, 이 권에서 하나의 공유된 세계 위에 함께 보여집니다.
• 즉각귀결 연산자(Immediate-consequence operator) $T_P$ — 몸체가 현재 참인 모든 규칙을 발동시키고 그 머리를 더하는 사상이며, 전방 연쇄는 이를 반복 적용하는 것입니다.
• 고정점 / 최소 고정점(Fixpoint / least fixpoint) — 규칙이 자기 자신으로 사상하는 집합, 즉 $T_P(S) = S$입니다. 전방 엔진은 그 가운데 최소의 것([23, 41, 47, 47]을 거쳐 도달하는 47개 원자)에 도달하며, 한 번의 통과가 아무것도 더하지 않을 때 끝났음을 압니다.
• 증명 트리(Proof tree) — 후방 증명기가 돌려주는, 감사 가능하고 사람이 읽을 수 있는 단계들의 사슬입니다. 예를 들어 advises(alice, bob)과 advises(bob, carol)로부터 grandAdvisor(alice, carol)을 도출하는 것입니다.
• 건전하고 완전함(Sound and complete) — 따라 나오는 것을, 오직 그것만, 모두 도출한다는 성질이며, 심볼릭 절반은 갖고 신경망 절반은 갖지 못한 성질입니다.
• TransE 점수(TransE score) — 거리 $\lVert \mathbf{h} + \mathbf{r} - \mathbf{t} \rVert$입니다. 낮을수록 더 그럴듯한 트리플이라는 뜻이며, 그래서 참인 트리플(평균 1.609)이 손상된 트리플(2.737)보다 낮은 순위에 놓입니다.
• 결코 침묵하지 않음, 결코 확신하지 않음(Never silent, never certain) — 임베딩의 거울상 트레이드오프입니다. 이름 붙일 수 있는 모든 트리플에 점수를 매기지만, 어떤 점수든 틀릴 수 있습니다.
• 세 가지 긴장(The three tensions) — 정확함 대 강건함, 설명 가능함 대 불투명함, 완전함 대 확장 가능함이며, 이후의 모든 방법이 자리 잡을 수 있는 축들입니다.
• 역량 검사(Competency check) — 관통 예제에 대한 하나의 실행 가능한 단언이며, 이 권의 주장은 곧 그 테스트이고, 종료 코드가 곧 평결입니다.
• 다리(The bridge) — 증명이 존재하는 곳에서는 증명기의 보장을, 그렇지 않은 곳에서는 학습기의 강건함을 지켜 줄, 아직 지어지지 않은 결합입니다.

이 다음으로 이어지는 것

1권은 여러분에게 두 절반과, 어휘와, 그것들을 비교할 세계를 건네주었습니다 — 그리고 아직 답하지 못한 질문 하나도 함께입니다. 두 문화를 하나로 만들 수 있는가? 다음 권인 2권 — 심볼릭 추론은 심볼릭 기둥을 완전한 깊이로 발전시킵니다. 학계 세계에 원칙에 입각한 어휘를 부여하는 온톨로지(ontology), 혼 규칙(Horn rule)이 말할 수 있었던 것보다 훨씬 더 많은 것을 말할 수 있게 해 주는 기술 논리(description logic), 그리고 그것을 판정하는 추론기들입니다. 이는 같은 지식 베이스를 더 날카로운 렌즈로 들여다보는 것입니다 — 이 장의 열린 평결을 지어진 다리로 바꾸려는, 한 번에 한 권씩 시도하는 네 권 가운데 첫 번째입니다.