신경 정리 증명: NTP와 CTP

📍 현재 위치: 4부 · 미분 가능 규칙 학습 — 13장. Neural-LP와 DRUM은 규칙의 선택을 완화했습니다: 관계 행렬들의 고정된 메뉴에 대한 주의 가중치이며, 증명기는 행렬 대수로 대체되었습니다. 이 장은 증명기를 그대로 두고 일치 판정을 완화합니다: 후방 연쇄는 고스란히 살아남고, 그 안의 기호-동등성 게이트만이 학습된 커널이 됩니다.

1권은 모든 결정이 문자열 비교였던 후방 연쇄기를 지었습니다: 목표 술어는 규칙-머리 술어와 같거나, 아니면 그 갈래는 죽습니다. 3권의 소프트 단일화 미리보기는 손으로 배치한 임베딩으로 그 게이트를 느슨하게 만들어 추론이 그 변화에서 살아남는 모습을 보여 주었지만, 아무것도 학습시키지 않았고 의도적으로 단순화한 커널을 사용했는데, 그 자신이 그것을 대체물이라고 표시해 두었습니다. 이 장은 그 빠진 두 조각을 모두 채워 넣습니다. 신경망 정리 증명기(Neural Theorem Prover, NTP)는 진짜 SLD 방식(Selective Linear Definite-clause resolution, 한정절에 대한 선택적 선형 귀결, 1권의 후방-연쇄 전략)의 증명 탐색을 실행하는데, 사실들에 대해서는 OR로 갈라지고 규칙 몸체에 대해서는 AND로 갈라지며, 깊이가 제한되어 있고, 치환은 이전과 정확히 똑같이 변수를 바인딩합니다. 다만 모든 술어 비교(전체 시스템에서는 상수를 포함한 모든 기호 비교)가 $\lbrace$ 실패, 성공 $\rbrace$ 이라는 판정 대신 $(0, 1]$ 구간의 유사도를 돌려준다는 점만 다릅니다 [1]. 증명의 점수는 그 비교들의 최솟값이고, 목표의 점수는 그 증명들에 대한 최댓값이며, 최솟값과 최댓값과 커널이 모두 (하위)미분 가능하므로, 증명기 전체가 하나의 손실 곡면이 됩니다. 바로 이것이 이 장의 표제 격 성과를 가능하게 만드는 것입니다: 알려지지 않은 술어 슬롯을 가진 규칙 템플릿(rule template) #1(X,Z) ← #2(X,Y) ∧ #2(Y,Z)를 지식 베이스에 떨어뜨려 놓으면, 그 슬롯들은 자유 벡터이고, 증명기를 관통하는 경사 하강이 템플릿이 하나의 규칙이 될 때까지 그 벡터들을 움직입니다. 동반 모듈 ntp_mini.py는 학술 세계 위에서 이 실험 전체를 실행하고 끝에 가서 정직한 청구서를 인쇄합니다: 그 지수적 증가가 이 장의 끝에서 다루는 두 규모 확장 후계자, GNTP(Greedy NTP)와 CTP(Conditional Theorem Prover, 조건부 정리 증명기)를 낳은 증명-경로 개수입니다.

쉽게 말하면

어떤 계보학자가 대학 기록 더미를 뒤져 "조부 지도교수" 사슬을 추적한다고 상상해 보십시오. 서로 다른 학과들은 같은 관계를 두고 "지도한다", "감독한다", "멘토링한다"처럼 저마다 다른 말을 적어 두었습니다. 옛 서기(1권의 증명기)는 단어를 글자 하나하나까지 맞춰 보는 사람이라서, 중간에 어휘가 바뀐 사슬은 그냥 잃어버립니다. 새 서기는 근사한 일치도 받아들이지만, 그때마다 확신도를 하나씩 찍어 두고, 사슬 전체는 그 가운데 가장 약한 확신도로 채점합니다. 여러 사슬이 같은 결론에 이르면, 가장 좋은 사슬이 그 결론을 대변합니다. 여기서 묘미는 서기가 어떤 단어를 믿어야 할지 배우는 방식입니다: 그녀는 사전을 하나도 갖지 않은 채 시작하고, 오직 이미 풀린 사례들이 담긴 폴더 하나만 가지고 있습니다. "감독한다"를 "지도한다"로 취급하는 것이 이미 풀린 사례들이 확인해 주는 사슬을 완성할 때마다, 그 짝에 대한 그녀의 신뢰는 자라납니다; 그것이 이미 틀렸다고 알려진 결론을 뒷받침할 때마다, 신뢰는 줄어듭니다. 충분한 사례를 겪고 나면 사전은 스스로를 써낸 셈이 되고, 그녀의 규칙집에 있던 빈 색인 카드 하나, "어떤 ___의 ___는 조부 지도교수다"는 올바른 단어들로 저절로 채워집니다. 대가는 자료 보관소가 커질 때 나타납니다: "일치하는 것이 없다"고 결코 말하지 않는 서기는 모든 사슬의 모든 단계에서 모든 기록을 고려해야만 합니다.

이 장에서 다루는 내용

정확히 다시 이어붙인 두 조상: 1권의 후방 연쇄기(목표, 머리 단일화, 재귀적 몸체 증명)와 3권의 훈련되지 않은 미리보기, 그리고 정확히 어떤 두 조각이 빠져 있었는지: 논문의 커널과 증명 성공으로부터의 학습입니다.
커널, 정확히: $k(a, b) = \exp(-\lVert \theta_a - \theta_b \rVert_2 / (2\mu^2))$ 이며 $\mu = 1/\sqrt{2}$ 이고, 유클리드 거리는 제곱하지 않습니다. 문헌이 "RBF"(radial basis function, 방사 기저 함수)라는 이름표를 붙였음에도 원본 코드가 못 박아 두는 세부 사항이며, 3권의 제곱 변형과 정직하게 대비됩니다.
점수 매겨진 탐색으로서의 증명기: 동반 코드에서 그대로 인용한 or/and 재귀, 증명 경로를 따라가는 최솟값(괴델 t-노름이 증명기 안에서 되돌아온 것, I부의 귀환), 증명들에 걸친 최댓값, 깊이 제한, 그리고 술어는 부드러워지되 치환은 하드하게 유지하는 설계상의 분리입니다.
학습 가능한 규칙으로서의 템플릿: 이제 "규칙을 학습한다"는 것이 뜻하는 바(슬롯 #1과 #2를 임베딩 공간에서 실제 술어 근처에 놓는 것), 에포크마다 오염된 음성을 쓰는 음의 로그 가능도 목적함수, 그리고 못 박힌 두 가지 요령, 곧 논문의 자기-단일화 마스킹과 이 모듈의 단위-노름 임베딩(논문의 Adam + ℓ2를 대신한다고 문서화된 대체물)입니다.
최솟값과 최댓값을 관통하는 그래디언트: 서브그래디언트 라우팅(승리한 증명의 가장 약한 고리만 움직입니다), 연쇄 법칙으로 끝까지 구해 낸 커널의 도함수, 그리고 0.4579에서 0.0333까지 내려가는 커밋된 손실 추적입니다.
꼼꼼히 읽어 낸 커밋된 결과들: 골드 연쇄 규칙으로 도로 해독된 템플릿, 오염 천장 0.1354에 맞선 0.9032의 홀드아웃 grandAdvisor 증명들, 그리고 두 사실로부터 학습된 동의어입니다.
주장이 아니라 헤아려진 비용 장부: 인쇄된 증명-경로 표, 그것이 보여 주는 깊이별 폭증, 그리고 이 분야가 내놓은 두 가지 답인 GNTP의 상위- $k$ 사실 걸러내기와 CTP의 학습된 규칙 선택입니다.

두 조상, 빠져 있던 나머지 절반

1권의 귀결과 SLD 장은 grandAdvisor(alice, carol)와 같이, 확립해야 할 원자인 목표(goal)를 받아들이는 증명기를 지었습니다. 그것은 목표와 단일화(unify)되는 머리를 가진 규칙을 프로그램에서 찾아 훑는데, 단일화된다는 것은 변수에 항을 대입함으로써 두 원자를 동일하게 만들 수 있다는 뜻이며, 단일화는 바로 그 치환을 계산해 냅니다. 그런 다음 그 치환 아래에서 규칙 몸체의 모든 원자를 재귀적으로 증명하는데, 사실은 몸체가 빈 규칙으로 취급되며, 목표는 그런 재귀 가운데 어느 하나가 온전히 사실에서 바닥을 이룰 때 정확히 성공합니다. 이 재귀는 커밋된 코드에서 눈으로 볼 수 있습니다: sld.py의 52–60행은 규칙들에 대해 반복하며, unify(head, g, sub)를 호출하고, 성공하면 _solve(body, ...)로 내려갑니다. 그 반복문의 한 줄이 바로 이 장 전체의 주제입니다: if s is None: continue. 단일화는 성공하거나 실패하는데, 1권의 unify 안에서 맨 먼저 이루어지는 검사가 술어-이름 동등성이므로, supervises로 쓰인 목표는 advises로 쓰인 사실을 결코 건드릴 수 없습니다. 두 단어가 아무리 투명하게 같은 관계를 가리킨다 해도 말입니다.

두 번째 조상은 이미 그 줄을 공격한 바 있습니다. 3권의 소프트 단일화 미리보기는 모든 술어 이름에 임베딩을 부여하고 동등성 게이트를 유사도 점수로 대체했으며, 그 커밋된 실행은 사실이 전혀 없는 술어인 supervises(bob, Z)에 대해 advises 사실들을 거쳐 점수 0.9783으로 답했는데, 하드 증명기는 아무것도 돌려주지 못했던 자리였습니다. 하지만 그 시연은 의도적으로 아이디어의 절반에 지나지 않았습니다. 그 임베딩은 손으로 배치된 것이었습니다: 시드가 고정된 무작위 단위 벡터였고, supervises는 _sup = EMB["advises"] + 0.25 * _noise라는 줄(soft_unification.py 74–77행)에 의해 advises 근처에 놓이도록 구성되어, 학습이 만들어 냈을 법한 것을 대신했습니다. 그리고 그 커널은 거리를 제곱했습니다, $\exp(-\lVert u_p - u_q \rVert^2 / (2\sigma^2))$ 이고 $\sigma = 1$ (soft_unification.py 80–88행)인데, 이는 미리보기 스스로가 표시해 두었고 이 장이 이제 갚아 주는 단순화입니다. 빠진 두 조각은 정확히 NTP의 두 가지 기여입니다 [1]: 다음에 나올 논문의 커널과, 그 뒤에 나올, 임베딩이 증명 성공으로부터 그 위치를 얻어 내게 만드는 훈련 루프입니다.

커널, 정확히

표기법부터 짚고 넘어갑시다. 모든 술어 기호 $a$ 는 하나의 임베딩(embedding) $\theta_a \in \mathbb{R}^{16}$ 을 갖는데, 이는 16개의 실수로 이루어진 행이며, 16은 임베딩 차원으로 코드에서는 $D$ 라고 부릅니다(ntp_mini.py 72행). 기호 $\lVert v \rVert_2$ 는 벡터 $v$ 의 유클리드 노름(Euclidean norm)으로, 그 좌표들의 제곱합의 제곱근이며, 따라서 $\lVert \theta_a - \theta_b \rVert_2$ 는 두 임베딩 사이의 평범한 직선 거리입니다(아래 첨자 2 때문에 이 거리를 L2 거리라고도 부릅니다). 두 술어 기호의 소프트 단일화 점수(soft unification score)는 다음과 같습니다

k(a, b) \;=\; \exp\!\left(-\,\frac{\lVert \theta_a - \theta_b \rVert_2}{2\mu^2}\right), \qquad \mu = \frac{1}{\sqrt{2}},

여기서 $\mu$ 는 고정된 대역폭(bandwidth, 유사도가 거리에 따라 얼마나 빨리 줄어드는지)이고 $\exp$ 는 지수 함수입니다. 이렇게 고른 대역폭은 분모를 눈앞에서 사라지게 만듭니다: $2\mu^2 = 2 \cdot (1/\sqrt{2})^2 = 2 \cdot \tfrac{1}{2} = 1$ 이므로, 커널은 그저 $k = e^{-d}$ 일 뿐이며 $d = \lVert \theta_a - \theta_b \rVert_2$ 입니다. 두 가지 결과가 곧바로 따라 나옵니다. 첫째, 동일한 기호는 $d = 0$ 을 가지므로, $k = e^{0} = 1$ 이 정확히 성립합니다: 하드 단일화는 특수한 경우로서 살아남고, 정확한 일치를 결코 벗어나지 않는 증명은 고전적인 1점을 받습니다. 둘째, 커널은 결코 0이 되지 않는데, 유한한 모든 $d$ 에 대해 $e^{-d} \gt 0$ 이기 때문입니다: 소프트 단일화는 결코 실패하지 않으며, 이 사실이 뒤이은 비용 분석을 지배하게 됩니다. 단위-노름 임베딩 위에서는 이 실패-없음이 정량적이기까지 합니다. 삼각 부등식은 두 단위 벡터 사이의 거리를 그 길이들의 합으로 묶어 둡니다, $\lVert \theta_a - \theta_b \rVert_2 \le \lVert \theta_a \rVert_2 + \lVert \theta_b \rVert_2 = 1 + 1 = 2$ 이며, 등호는 정확히 두 벡터가 대척점(구 위에서 서로 반대편에 있는 점)에 있을 때 성립합니다. 그러므로 모든 커널 값은 $[e^{-2}, 1]$ 안에 살며, $e^{-2} \approx 0.1353$ 은 단단한 바닥입니다: 구조적으로 유효한 어떤 증명이든 그 술어가 아무리 틀렸다 해도 적어도 그만큼은 점수를 받습니다. 0.135라는 숫자를 기억해 두십시오; 이 수는 소수점 셋째 자리까지 커밋된 오염 표에 다시 나타날 것입니다.

이제 정직함을 위한 메모를 정면에 내세웁니다. 그 지수 안의 거리는 제곱되지 않습니다. 문헌은 이 커널을 RBF(radial basis function, 방사 기저 함수) 커널이라 부르고, 표준적인 가우스 RBF는 실제로 거리를 제곱합니다; 하지만 참조 구현의 유사도는 있는 그대로의 L2 거리를 계산하는데, 이는 이 함수를 가우스 계열이 아니라 라플라스 계열의 유사도로 만들며, 동반 모듈은 그 코드를 그대로 따릅니다(ntp_mini.py 5–16행이 그 검증을 진술하고, 커널 자체는 125–138행입니다):

def kernel(theta: np.ndarray, a: str, b: str) -> float:
    """Soft unification score of two predicate symbols — the paper's §3.1
    kernel on the UNSQUARED Euclidean distance (μ = 1/√2, so 2μ² = 1):

        k(a, b) = exp( -‖θ_a − θ_b‖₂ / (2μ²) ).

    Identical symbols have distance 0, so k = e⁰ = 1.0 exactly: hard
    unification survives as the special case.  On the unit sphere the
    distance is at most 2 (antipodal), so every kernel is ≥ e⁻² ≈ 0.135 —
    any structurally valid proof scores at least that."""
    # d = ‖θ_a − θ_b‖₂  (plain L2 — NOT squared; the pinned detail)
    d = float(np.linalg.norm(theta[S_ID[a]] - theta[S_ID[b]]))
    # k = exp(-d / (2μ²)) = exp(-d) since 2μ² = 1
    return math.exp(-d / TWO_MU_SQ)

3권의 미리보기와의 대비에 대해 정직한 문단 하나를 두겠습니다. 두 변형 모두 타당하기 때문입니다. 제곱형 $e^{-d^2/2}$ 와 있는 그대로의 형태 $e^{-d}$ 는 둘 다 거리를 $(0, 1]$ 로 사상하는 유효한 유사도 함수이고, 둘 다 $d = 0$ 에서 1과 같으며, 단위-구 임베딩 위에서는 둘 다 마침 $e^{-2}$ 에서 바닥을 이룹니다(제곱형의 경우 $d^2 \le 4$ 이고 $2\sigma^2 = 2$ 이기 때문입니다). 이 둘은 모양에서 갈리며, 그 모양이 훈련에 영향을 미칩니다. 각각을 $d$ 에 대해 미분해 봅시다: 가우스형의 경우 $\frac{\partial}{\partial d} e^{-d^2/2} = -d\, e^{-d^2/2}$ 인데, 이는 $d \to 0$ 일 때 사라집니다; 라플라스형의 경우 $\frac{\partial}{\partial d} e^{-d} = -e^{-d}$ 인데, 이는 $d \to 0$ 일 때 $-1$ 에 접근합니다. 그러므로 가우스 커널은 두 기호가 거의 동의어에 가까워지는 바로 그 지점에서 평평해져, 그 짝짓기가 흥미로워지는 순간에 그래디언트를 굶겨 버리는 반면, 제곱하지 않은 커널은 거의 동의어인 기호들을 온전한 세기로 계속 끌어당깁니다. 미리보기는 3권의 가우스적 직관과의 연속성을 위해 제곱형을 골랐습니다; 이 재구현은 논문 자신의 코드가 그렇게 하기 때문에 논문을 따릅니다 [1].

	3권 미리보기 (`soft_unification.py`)	이 장 (`ntp_mini.py`)
지수 안의 거리	$\lVert u_p - u_q \rVert^2$ (제곱)	$\lVert \theta_a - \theta_b \rVert_2$ (있는 그대로)
대역폭	$\sigma = 1$ , 따라서 $2\sigma^2 = 2$	$\mu = 1/\sqrt{2}$ , 따라서 $2\mu^2 = 1$
커널 계열	가우스	라플라스 스타일
$d \to 0$ 에서의 기울기	$0$ (동의어 근처에서 평평함)	$-1$ (온전한 세기)
단위 벡터 위에서의 바닥	$e^{-4/2} = e^{-2} \approx 0.135$	$e^{-2} \approx 0.135$
임베딩	손으로 배치, 시드 고정	증명기를 통해 학습됨

후방 연쇄는 살아남는다; 오직 동등성 게이트만 바뀐다: 커널이 각 일치에 점수를 매기고, min이 증명을 채점하며, max가 승자를 고르고, 오른쪽 패널은 결코 실패하지 않는 매처가 반드시 치러야 하는 탐색 비용의 값을 매긴다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

점수 매겨진 탐색으로서의 증명기

증명기의 골격은 1권과 달라지지 않았습니다: OR-모듈(or-module)은 하나의 목표를 확립하는 모든 방법(각 사실, 각 규칙 머리)을 시도하고, AND-모듈(and-module)은 치환을 꿰어 나가면서 규칙 몸체의 원자들을 왼쪽에서 오른쪽으로 증명합니다. 바뀌는 것은 각 갈래가 이제 점수 하나를 지니고 다니며, 두 모듈이 I부가 검증한 두 연산자로 점수를 합성한다는 점입니다. 하나의 증명을 따라가면, 일치들은 논리곱이며, 그 점수들은 t-노름과 t-코노름 장의 괴델 t-노름인 최솟값(minimum)으로 합쳐집니다: 일치들의 사슬은 정확히 가장 약한 고리만큼만 강합니다. 같은 목표의 증명들에 걸쳐서는, 그 대안들은 논리합이며, 그 점수들은 괴델 t-여노름인 최댓값(maximum)으로 합쳐집니다. 커널 $k_1, \dots, k_m$ 을 가진 단일화 단계들로 지어진 하나의 증명 $\rho$ 의 점수를 $S_\rho$ 로 쓰면(여기서 $m$ 은 그 증명 안의 소프트 일치의 개수를 셉니다),

S_\rho = \min(k_1, \dots, k_m), \qquad \mathrm{ntp}(G) = \max_{\rho \,\vdash\, G} S_\rho,

여기서 아래 첨자 $\rho \vdash G$ 는 깊이 제한(depth bound) 2(코드의 DEPTH 상수; 문자 $d$ 는 커널의 거리를 위해 남겨 둡니다) 안에서 완결되는 목표 $G$ 의 증명들에 걸쳐 있습니다: 템플릿은 한 번만 펼쳐질 수 있고, 그 몸체는 그런 다음 사실들 위에서 닫혀야 합니다. 이 제한이 3권의 미리보기에서와 정확히 똑같이 재귀를 유한하게 유지해 주는 것이며, 이는 이 장이 끝에서 다시 돌아오게 될 단단한 천장입니다. 다음은 탐색의 깊이-2 절반인데, 점수의 꿰어 나가기가 이 절 전체의 교훈이므로 점수를 통해 그대로 인용하며, 231–239행의 증명-기록 장부 정리는 생략합니다(ntp_mini.py 211–230행):

    # -- depth 2: goal ~ template head, body against facts ---------------------
    # unify(goal, #1(X,Z)): predicates compare soft, X/a and Z/b bind free.
    counts[2]["attempts"] += 1
    k_head = kernel(theta, p, "#1")
    for q1, c1, y in KB:                      # first body atom  #2(a, Y)
        counts[2]["attempts"] += 1
        if mask_self and (q1, c1, y) == goal:
            continue
        if c1 != a:
            continue
        k1 = kernel(theta, "#2", q1)          # Y binds to y symbolically
        for q2, c2, d2 in KB:                 # second body atom #2(y, b)
            counts[2]["attempts"] += 1
            if mask_self and (q2, c2, d2) == goal:
                continue
            if (c2, d2) != (y, b):
                continue
            k2 = kernel(theta, "#2", q2)
            # S_ρ = min(k_head, k1, k2): the soft AND along this proof.
            score = min(k_head, k1, k2)

구조를 읽어 봅시다. 목표 (p, a, b)는 템플릿 머리 #1(X, Z)와 단일화됩니다: 술어 비교는 소프트하지만(k_head), 변수 X와 Z는 1권과 정확히 똑같이 공짜로, 기호적으로 상수 a와 b에 바인딩됩니다. 바깥쪽 반복문은 첫 번째 몸체 원자 #2(a, Y)를 위한 OR-모듈입니다: 모든 지식-베이스 사실이 후보이고, Y는 그 사실의 두 번째 인자에 바인딩되며, 그 바인딩은 안쪽 반복문, 곧 두 번째 몸체 원자 #2(Y, b)를 위한 OR-모듈로 꿰어져 들어갑니다. 완료된 안쪽 반복 하나하나가 하나의 증명이며, 그 세 커널의 min으로 점수가 매겨집니다.

이 코드는 또한 NTP를 흐릿한 뭉개짐이 아니라 하나의 하이브리드로 만들어 주는 설계상의 분리를 보여줍니다: 인자는 바인딩되고, 술어는 부드러워집니다. 변수-대-상수 치환은 정확한 채로 남는데, 바인딩은 증거가 아니라 장부 정리이기 때문입니다; "Y가 이제 carol을 가리킨다"는 데에는 등급이 매겨질 것이 아무것도 없습니다. 술어 일치는 부드러워지는데, 그곳이 바로 의미가 사는 곳이기 때문입니다: supervises와 advises는 의미론적 판단이며, 임베딩은 바로 그런 의미론적 판단을 위한 것입니다. 이 축소판의 단순화 하나는 같은 숨결로 진술해 두어야 합니다: if c1 != a: continue라는 줄들은 상수 또한 하드하게 단일화되도록 만들어서, 인자가 충돌하는 사실은 곧바로 가지치기됩니다. 실제 NTP는 술어뿐 아니라 상수도 임베딩하므로, 같은 항수(arity, 인자의 개수)의 원자들 사이에서는 모든 사실이 모든 하위 목표와 어떤 0이 아닌 커널로 소프트-단일화되며 아무것도 가지치기되지 않습니다(항수 불일치는 여전히 FAIL이며, 이는 논문이 유지하는 유일한 하드 게이트이고, 여기 있는 모든 사실은 이항입니다) [1]; 모듈의 독스트링은 이 단순화와 그 결과를 못 박아 두며, 커밋된 출력은 우리 쪽 경로 개수와 가지치기되지 않은 쪽 경로 개수를 나란히 인쇄합니다. 집계 방식 또한 논문의 것입니다: goal_score(ntp_mini.py 242–256행)는 반환된 증명들에 대해 최댓값을 취하며, 동점은 열거 순서에 따라 결정론적으로 깨집니다.

메커니즘	1권의 증명기	`ntp_mini.py`	전체 NTP
술어 일치	문자열 동등성, 아니면 실패	커널 $k(a,b) \in [e^{-2}, 1]$	커널
상수 일치	동등성, 아니면 실패	동등성, 아니면 실패(못 박힌 단순화)	커널
변수 바인딩	치환, 정확함	치환, 정확함	치환, 정확함
논리곱 (증명 하나)	모든 몸체 원자가 성공	단계별 커널의 최솟값	최솟값
논리합 (증명 여럿)	첫 성공	증명들에 대한 최댓값	최댓값
실패	가지치기된 갈래	오직 인자 충돌만 가지치기	오직 항수 불일치만 가지치기

템플릿: 이제 "규칙을 학습한다"는 것이 뜻하는 바

Neural-LP와 DRUM 장은 기존 관계들 가운데에서 부드럽게 고름으로써 규칙을 학습했습니다. NTP는 규칙 그 자체를 매개변수화함으로써 규칙을 학습합니다. 이 모듈은 하나의 규칙 템플릿(rule template)을 선언합니다(ntp_mini.py 154행):

TEMPLATE: str = "#1(X,Z) :- #2(X,Y), #2(Y,Z)"

머리 슬롯 #1과 (묶여 있는) 몸체 슬롯 #2는 술어 이름이 아닙니다; 이들은 임베딩 행렬 $\theta$ 의 추가된 두 행으로, 일곱 개의 실제 술어들과 나란히 무작위 단위 벡터로 초기화됩니다(ntp_mini.py 119–121행이 어휘를 짓고, 141–147행이 아홉 행 전부를 초기화합니다). 템플릿은 하나의 모양을 주장합니다, "무언가(X, Z)는 무언가(X, Y)와 그 같은 무언가(Y, Z)로부터 따라 나온다"는 것이며, 두 개의 "무언가"는 자유 매개변수로 남겨져 있습니다. 이제 규칙을 학습한다는 것은 정확한 기하학적 의미를 갖습니다: 경사 하강이 $\theta_{\#1}$ 과 $\theta_{\#2}$ 를 $\mathbb{R}^{16}$ 안에서 움직이고, 그것들이 어디에 가서 멈추든, 템플릿은 그것들이 내려앉은 근처의 실제 술어가 무엇이든 그것을 의미하게 됩니다. 훈련이 끝나면, 규칙은 최근접 이웃으로 해독(decode)됩니다: 각 슬롯에 가장 높은 커널을 갖는 알려진 술어를 보고하고(ntp_mini.py 377–382행), 그 커널들의 min을 규칙의 신뢰도로 삼는데, 이는 해독된 해석을 거쳐 가는 어떤 증명의 점수에 대해서도 상한이 됩니다.

훈련 신호는 알려진 원자들에 대한 증명 성공입니다. 양성 사례는 네 개입니다: 1권의 사실들 위에서 advises와 advises를 합성하여 도출할 수 있는 두 개의 grandAdvisor 쌍은 다시 타이핑된 것이 아니라 계산된 것이며, 세 번째 쌍 (bob, erin)은 완전히 홀드아웃되어 있습니다(ntp_mini.py 99–107행). 여기에 더해, 의도적으로 심어 둔 동의어 술어 supervises의 사실 두 개가 있는데, 이는 지도 관계의 부분집합을 다른 이름으로 주장합니다(91–94행). 음성 사례는 오염된 원자(corrupted atom)입니다: 각 양성 (p, a, b)에 대해 머리 오염 (p, ã, b) 하나와 꼬리 오염 (p, a, b̃) 하나가 있으며, 대체할 사람은 균등하게 뽑되 그 오염이 알려진 참 원자이면 다시 뽑는데, 이는 3권의 순위 매김 장들과 똑같이 걸러진 프로토콜이며, 에포크마다 새로 다시 표집됩니다(ntp_mini.py 327–343행). 레이블 $y$ (양성이면 1, 오염이면 0)를 갖는 한 원자에 대한 손실은 증명 점수의 음의 로그 가능도(negative log-likelihood, NLL)이며, $\mathrm{ntp}(G)$ 를 마치 참일 확률인 것처럼 취급합니다 [1]: $s = \mathrm{ntp}(G)$ 를 0과 1로부터 멀어지도록 클램프하면,

L = -\,y \ln s \;-\; (1 - y)\,\ln(1 - s).

못 박힌 두 가지 요령이 이 목적함수를 훈련 가능하게 만들어 주며, 둘 다 코드에서 그대로 인용합니다. 재구현이 죽어 나가는 것이 바로 이런 세부 사항이기 때문입니다(첫 번째 요령은 논문의 것이고, 두 번째는 이 모듈 자신의 것입니다). 첫 번째는 자기-단일화 마스킹(self-unification masking)입니다. 두 supervises 양성은 지식-베이스 사실이기도 합니다; 아무 개입이 없다면, 원자 supervises(alice, bob)은 깊이 1에서 자기 자신과 단일화됨으로써 스스로를 증명하며, 커널 $k(\text{supervises}, \text{supervises}) = 1$ 이 정확히 성립합니다. 그 증명은 언제나 max를 이기므로 그 양성에 대한 손실은 이미 0이고, 설상가상으로, 승리한 커널이 하나의 임베딩을 자기 자신과 비교하는 것이므로 그 그래디언트는 아무것도 움직이지 않습니다. 그러므로 이 마스크를 빼놓으면 supervises 양성 사례들은 무력해집니다: 두 사실이 주던 직접적인 동의어 신호가 사라지고, supervises는 오직 간접적으로만 자리를 잡게 되는데, grandAdvisor 증명 몸체들이 #2 원자를 advises 사실뿐 아니라 supervises 사실을 거쳐서도 지을 수 있어서, supervises가 #2 쪽으로 끌려가는 동안 #2는 advises 쪽으로 끌려가기 때문입니다(마스크를 끈 채 다시 훈련해 보면, 커밋된 출력에는 없는 절제 실험이지만, supervises는 여전히 advises에 가장 가깝게 내려앉되 커널은 커밋된 0.9111 대신 0.883에 그칩니다); 템플릿 자체는 여전히 grandAdvisor 양성 사례들로부터 학습될 것인데, 그 목표들은 도출된 쌍이지 지식-베이스 사실이 아니어서 결코 자기-단일화하지 않기 때문입니다. 그 해결책은 사실 행을 시도하는 자리마다 적용되는 가드 하나입니다. 아래는 깊이-1 OR-모듈에서 인용한 것이며, 깊이-2의 두 몸체 OR-모듈이 저마다의 반복문 변수로 같은 가드를 반복합니다(217–218행과 224–225행). 이 가드는 훈련 도중 목표가 자기 자신의 사실 행과 단일화되는 것을 건너뜁니다 [1](ntp_mini.py 200–201행):

        if mask_self and (q, c, d_) == goal:
            continue  # self-unification masked to 0 (paper §4.1)

두 번째 요령은 단위-노름 제약(unit-norm constraint)으로, 논문의 Adam 최적화기와 ℓ2 정규화를 이 모듈이 대신하는 대체물입니다(독스트링이 이 대체를 못 박아 둡니다, ntp_mini.py 37–38행): 모든 그래디언트 스텝 이후, 건드려진 각 임베딩 행(코드의 theta[row], 술어 이름이나 템플릿 슬롯마다 한 행)은 단위 구 위로 다시 사영됩니다, $\theta_{\text{row}} \leftarrow \theta_{\text{row}} / \lVert \theta_{\text{row}} \rVert_2$ (ntp_mini.py 368–369행):

                theta[row] -= LR * g
                theta[row] /= float(np.linalg.norm(theta[row]))

스텝과 사영은 훈련 루프 안에서 하나의 동작입니다: LR은 학습률(learning rate) $\eta = 0.1$ 이며(각 그래디언트에 곱해지는 스텝 크기입니다), g는 nll_and_grads가 계산한 그래디언트 행이고, 노름으로 나누는 것이 바로 그 사영입니다. 이것이 바로 앞 절의 커널-바닥 논증을 이 모듈의 훈련 내내 참으로 유지해 주는 것이며(사영 대신 Adam과 ℓ2로 훈련하는 실제 NTP는 그런 바닥을 유지하지 않습니다), 모든 거리를 $[0, 2]$ 안에 두어 하나의 고정된 대역폭이 모든 쌍에 다 통하게 해 주고, 최적화기가 모든 노름을 0을 향해 줄여 버리는 퇴화된 도피처를 쓰지 못하게 막아 줍니다. 그런 도피는 어떤 술어들이 함께 속하는지에 대해 아무것도 배우지 않은 채로 모든 커널을 1을 향해 부풀려 버렸을 것입니다.

최솟값과 최댓값을 관통하는 그래디언트

이제 손실은 세 개의 층을 관통하여 미분되어야 합니다: NLL, 그다음 증명들에 걸친 max와 증명 안에서의 min 라우팅(함께 다뤄집니다), 그리고 마지막으로 커널입니다. 모든 단계는 nll_and_grads(ntp_mini.py 261–324행) 안에 있으며, 모든 단계가 여기서 유도됩니다.

1층, NLL. $s$ 를 클램프된 증명 점수라 하면, $L = -y \ln s - (1-y)\ln(1-s)$ 입니다. $\frac{d}{ds}\ln s = 1/s$ 를 쓰고, 안쪽 함수 $1 - s$ (그 도함수는 $-1$ 입니다)에 대한 연쇄 법칙으로 $\frac{d}{ds}\ln(1-s) = -1/(1-s)$ 를 얻어, 항별로 미분합니다:

\frac{\partial L}{\partial s} = -\frac{y}{s} + \frac{1-y}{1-s}.

양성( $y = 1$ )에 대해서는 이것이 $-1/s \lt 0$ 입니다: 점수가 오를수록 손실이 떨어지므로, 갱신은 점수를 올립니다. 오염( $y = 0$ )에 대해서는 $+1/(1-s) \gt 0$ 입니다: 갱신은 점수를 낮춥니다.

2층, max와 min. 두 연산자 모두 조각별 선형이며, 그 논증은 퍼지에서 신경망으로가 괴델 t-노름을 위해 펼쳤던 것과 같습니다. 최대화하는 증명 $\rho^\ast$ 가 유일할 때는, 매개변수를 조금 흔들어도 그것이 여전히 최대라는 사실이 바뀌지 않으므로, 어떤 근방 전체에서 $\mathrm{ntp}(G) = S_{\rho^\ast}$ 가 함수로서의 항등식으로 성립합니다; 양변을 미분하면 $\partial\, \mathrm{ntp}(G) / \partial S_{\rho^\ast} = 1$ 이 나오고, 패배한 모든 증명에 대해서는 정확히 0이 나옵니다. 한 단계 아래에서도 같은 논증이 성립합니다: $\rho^\ast$ 안에서 최소화하는 커널 $k_{\min}$ 이 유일할 때는, $S_{\rho^\ast} = k_{\min}$ 이 항등적으로 성립하므로, 도함수는 가장 약한 단계를 거쳐서는 1이고 나머지를 거쳐서는 0입니다. 동점에서는 두 연산자 모두 미분 가능하지 않으며, 코드는 첫 번째 최소화 원소를 결정론적으로 택하는데, 이는 유효한 서브그래디언트(subgradient, 꺾인 함수가 꺾임점에서 허용하는 임의의 기울기; 첫 번째 최소화 원소가 왜 그 하나가 되는지는 링크된 장이 유도했습니다)입니다(ntp_mini.py 307–313행). 이렇게 합성된 라우팅은 잔혹할 만큼 단순합니다: 하나의 훈련 원자에 딸린 모든 증명의 모든 커널 가운데, 정확히 하나만이 그래디언트를 받는데, 그것은 승리한 증명의 가장 약한 고리입니다. I부는 이 희소성을 추상적으로 측정한 바 있습니다(50개의 논리곱으로 이루어진 몸체 가운데 98퍼센트가 스텝마다 굶주립니다); 여기서는 그것이 탐색 안에서 구체적인 결과를 얻으며, 아래에서 그 결과로 돌아옵니다.

3층, 커널. 승리한 단계에서 두 임베딩의 차이 벡터를 $\delta = \theta_a - \theta_b$ 라 하고 그 길이를 $d = \lVert \delta \rVert_2$ 라 합시다. 3권의 EL 임베딩 장은 노름의 그래디언트를 좌표 하나하나씩 유도한 바 있습니다: $d = (\sum_{j=1}^{16} \delta_j^2)^{1/2}$ 이라 쓰면, 여기서 $j$ 는 16개 좌표에 대한 첨자이고, 제곱근에 대한 연쇄 법칙은 임의의 한 좌표 $\delta_i$ 에 대해(첨자 $i$ 는 지금 변화시키는 그 좌표의 이름입니다) $\partial d / \partial \delta_i = \tfrac{1}{2}(\sum_j \delta_j^2)^{-1/2} \cdot 2\delta_i = \delta_i / d$ 를 주므로, $\partial d / \partial \delta = \delta / d$ , 곧 차이 방향을 따르는 단위 벡터가 됩니다. $\delta$ 가 $\theta_a$ 에는 계수 $+1$ 로, $\theta_b$ 에는 계수 $-1$ 로 의존하므로, $\partial d / \partial \theta_a = \delta / d$ 와 $\partial d / \partial \theta_b = -\delta / d$ 를 얻습니다. 이제 도함수가 자기 자신인 지수 함수를 관통시켜 봅시다: $k = e^{-d}$ 이므로 $\partial k / \partial d = -e^{-d} = -k$ 이고, 연쇄 법칙에 의해

\frac{\partial k}{\partial \theta_a} = -k \cdot \frac{\theta_a - \theta_b}{d}, \qquad \frac{\partial k}{\partial \theta_b} = +k \cdot \frac{\theta_a - \theta_b}{d},

노름이 꺾이고 커널이 이미 최댓값에 있는 $d = 0$ 에서는 서브그래디언트 0을 고릅니다. 이것은 TransE의 노름 그래디언트가 새 옷을 입은 것입니다: 양성은 승리한 두 기호를 그 차이 방향을 따라 서로 끌어당기고, 오염은 그 둘을 밀어냅니다. 완전한 연쇄는 세 층을 곱합니다, $\partial L / \partial \theta_a = \frac{\partial L}{\partial s} \cdot 1 \cdot 1 \cdot \frac{\partial k_{\min}}{\partial \theta_a}$ 이며, 가운데 두 인자는 max와 min 라우팅입니다. 코드는 이 유도를 그대로 옮겨 적은 것입니다(ntp_mini.py 315–324행):

    diff = theta[ia] - theta[ib]
    d = float(np.linalg.norm(diff))
    if d < 1e-12:
        return loss, {}  # subgradient 0 at d = 0 (kernel already maximal)
    # ∂k/∂θ_a = -k·(θ_a − θ_b)/d   and   ∂k/∂θ_b = +k·(θ_a − θ_b)/d
    dk_da = -min_k * diff / d
    # ∂L/∂θ = ∂L/∂s · ∂s/∂k_min · ∂k_min/∂θ, with ∂s/∂k_min = 1 (max∘min
    # both pass the unique winner through at slope 1).
    grads = {ia: dL_ds * dk_da, ib: -dL_ds * dk_da}
    return loss, grads

훈련은 사영된 확률적 경사 하강법(projected stochastic gradient descent, SGD)입니다: 매 에포크마다 네 개의 양성과 각각에 대해 새로 뽑은 두 개의 오염을 방문하며, 학습률 $\eta = 0.1$ 로 행 단위로 $\theta \leftarrow \theta - \eta\, \partial L / \partial \theta$ 를 적용하고, 건드려진 각 행을 단위 구 위로 다시 사영합니다(ntp_mini.py 357–372행). 커밋된 실행의 손실 추적은 시드 0 아래에서 결정론적입니다:

[1] training: NLL on the proof score, 500 epochs of projected SGD (η = 0.1)
    positives: grandAdvisor(alice,carol) grandAdvisor(alice,dave) (derived; grandAdvisor(bob,erin) HELD OUT)
    + supervises facts; 2 corruptions per positive, resampled each epoch;
    self-unification masked: a fact never proves itself
    epoch :  mean NLL
        1 :    0.4579
       10 :    0.0745
       50 :    0.0605
      100 :    0.0581
      250 :    0.0818
      500 :    0.0333

평균 NLL은 열 에포크 안에 여섯 분의 일로 떨어져 0.0333에 이릅니다. 이는 단조롭지 않습니다: 에포크 250의 스냅숏은 0.0818로, 에포크 50보다 높은데, 오염이 에포크마다 다시 표집되고 어떤 표집은 다른 것보다 결정 경계에 더 가깝게 떨어지기 때문입니다. 이 모듈은 확률적 목적함수가 갖지 않는 매끄러움을 주장하는 대신, "훈련이 통했다"의 정직한 버전, 곧 최종 NLL이 0.10 아래이고 시작은 그 위였다는 것을 단언합니다(ntp_mini.py 431–432행).

커밋된 실행 읽어 내기

훈련이 끝나면, 이 실행은 최근접 이웃으로 템플릿을 해독합니다:

[2] decoded template (nearest known predicate per learned slot)
    #1 → grandAdvisor k = 0.9769
    #2 → advises      k = 0.9032   (supervises a near-tie at 0.9026 — it
         learned to be advises' synonym, so #2 is close to both
         names of the same relation)
    induced rule (0.9032 confidence, the paper's min-kernel decode):
      grandAdvisor(X,Z) :- advises(X,Y), advises(Y,Z)   — Volume 1's chain rule, relearned from pairs
    synonym check: supervises embeds nearest advises (k = 0.9111)

천천히 읽으십시오. 세 가지 별개의 주장이 동시에 검증되고 있기 때문입니다. 첫째, 유도된 규칙은 골드 규칙입니다: #1은 커널 0.9769에서 grandAdvisor로, #2는 0.9032에서 advises로 해독되었으므로, 템플릿이 학습한 해석은 1권이 손으로 적어 두었던 바로 그 연쇄 규칙이며, 오직 개체 쌍과 증명 피드백만으로 복원된 것입니다. 둘째, 이 근접 동점은 잡음이 아니라 정확함입니다: #2는 advises로부터 0.9032, supervises로부터 0.9026에 자리하는데, 이는 지식 베이스가 하나의 관계를 두 이름 아래 담고 있을 때 슬롯이 정확히 해야 할 일입니다. 셋째, 그 동의어 자체가 스스로 얻어 낸 것이며, 그 메커니즘은 이 실행에서 가장 깔끔합니다. 3권의 미리보기는 supervises를 손으로 advises 옆에 구성해 두었습니다; 여기서는 두 임베딩이 독립적인 무작위 단위 벡터로 시작하여, 두 사실만큼의 증명 성공에 의해 커널 0.9111까지 끌려왔습니다. 자기-단일화가 마스킹된 상태에서 각 supervises 양성에는 정확히 하나의 증명, 곧 평행한 advises 사실과의 깊이-1 소프트 단일화만 존재합니다. 이 목표들에 대해 템플릿 몸체는 결코 닫힐 수 없는데, 하드한 상수 일치 아래에서는 alice에서 bob으로, 또는 bob에서 carol로 이어지는 두 홉짜리 사실 연쇄가 없기 때문입니다. 그러므로 승리한 증명의 유일한 커널이 곧 $k(\text{supervises}, \text{advises})$ 이고, 이 양성 사례들에 대한 모든 그래디언트 스텝은 정확히 그 두 행의 쌍을 서로 끌어당깁니다.

다음은 훈련 중에 결코 본 적 없는 홀드아웃 쌍입니다:

[3] held-out pair grandAdvisor(bob,erin) — never trained on
    proof score = 0.9032   (winning proof below; the proof path IS the explanation)
      grandAdvisor(bob,erin) ~ head #1(X,Z)   k(grandAdvisor,#1)=0.9769
          #2(bob,Y) ~ fact advises(bob,carol)   k(#2,advises)=0.9032   Y:=carol
          #2(carol,erin) ~ fact advises(carol,erin)   k(#2,advises)=0.9032
      score = min of the three kernels = 0.9032

이 점수는 모듈의 0.5 문턱을 여유 있게 넘기며, 승리한 증명은 블랙박스가 아닙니다: 그것은 읽을 수 있는 유도 과정입니다. 템플릿 머리는 0.9769에서 일치했고, 두 몸체 원자는 각각 0.9032에서 실제 advises 사실들과 일치했으며, 변수 Y는 carol에 기호적으로 바인딩되었고, 그런 다음 min이 취해졌습니다. 모듈의 독스트링이 굳이 짚어 두는 정직한 메모 하나: 이 축소판은 상수를 기호적으로 유지하기 때문에, 홀드아웃 쌍은 훈련 쌍들과 똑같은 세 커널로 증명되며(이 실행은 세 개의 grandAdvisor 점수 모두를 동일한 0.9032로 인쇄합니다), 따라서 여기 보이는 일반화는 개체 공간에서의 거리 기반 일반화가 아니라 구조적 일반화, 곧 유도된 규칙이 보지 못한 개체 쌍으로 전이되는 것입니다. 오염 표는 그 반대편을 가늠합니다:

[4] corruptions of the held-out pair (filtered: true pairs skipped)
    atom                            score
    grandAdvisor(alice,erin)        0.0000  (no proof at depth 2)
    grandAdvisor(bob,alice)         0.0000  (no proof at depth 2)
    grandAdvisor(bob,bob)           0.0000  (no proof at depth 2)
    grandAdvisor(bob,carol)         0.1354  (fact-level k(grandAdvisor,advises): antipodal floor e^-2)
    grandAdvisor(bob,dave)          0.1354  (fact-level k(grandAdvisor,advises): antipodal floor e^-2)
    grandAdvisor(carol,erin)        0.1354  (fact-level k(grandAdvisor,advises): antipodal floor e^-2)
    grandAdvisor(dave,erin)         0.0000  (no proof at depth 2)
    grandAdvisor(erin,erin)         0.0000  (no proof at depth 2)
    max corrupted = 0.1354   →   margin = 0.7678

홀드아웃 쌍의 모든 오염은 최대 0.1354점을 받으므로, 참인 쌍은 $0.9032 - 0.1354 = 0.7678$ 의 마진으로 이깁니다. 그리고 그 천장 값은 낯익은 값입니다: 0.1354는 커널 절에서 유도한 대척점 커널 바닥 $e^{-2} \approx 0.1353$ 보다 약 $10^{-4}$ 위에 있습니다. 그 값에 이르는 세 개의 오염은 마침 그 개체 쌍이 실제 advises 간선인 경우로, 단 하나의 커널 $k(\text{grandAdvisor}, \text{advises})$ 를 갖는 깊이-1 증명을 내놓습니다; 바로 이런 오염들을 먹인 훈련은 그 두 임베딩을 구의 거의 반대쪽 극으로 밀어붙여, 점수를 기하가 허용하는 바닥의 약 만분의 일 안쪽까지 몰아넣었습니다. 이 바닥은 여기서는 하나의 특징(틀린 원자가 그보다 더 낮은 점수를 받을 수는 없습니다)이면서, 나중을 위한 경고이기도 합니다: 소프트 증명기의 "아니요"는 결코 0이 아닙니다.

주장이 아니라 헤아려진 비용 장부

위의 모든 것이 통했던 이유는 지식 베이스가 아주 작기 때문이며, 이 모듈은 그 대가를 값 매기지 않은 채로 넘어가기를 거부합니다. 하나의 목표에 대한 탐색 트리를 세어 봅시다. 깊이 1에서, OR-모듈은 $K$ 개의 사실(여기서는 $K = 20$ ) 모두와 단일화를 시도합니다. 깊이 2에서, 목표는 템플릿 머리와 단일화되고, 그런 다음 두 개의 몸체 원자 각각이 $K$ 개의 사실 전부에 걸쳐 저마다의 OR-모듈을 돌리는데, 첫 번째 원자의 바인딩이 두 번째로 꿰어져 들어갑니다: 그러므로 몸체만으로도 $K \times K$ 개의 후보 사실 쌍에 걸쳐 있습니다. 일반적으로, $m$ 개의 원자로 이루어진 규칙 몸체는 한 번 펼쳐질 때마다 $K^m$ 개의 조합을 살려 두며, 규칙 중첩이 한 단계 더해질 때마다 다시 곱해집니다: 트리는 깊이마다 지식 베이스(knowledge base, KB) 크기를 몸체 길이만큼 거듭제곱한 만큼 자라납니다. 커밋된 실행은 그것을 주장하는 대신 세어 봅니다:

[5] proof paths explored for grandAdvisor(bob,erin) (K = 20 facts)
    depth   this mini (hard constants)      full NTP (soft constants)
        1     20 attempts,  0 proofs           20 live paths (K^1)
        2    121 attempts,  2 proofs          400 live paths (K^2)
    real NTP embeds constants too, so nothing prunes: the 2-atom body alone
    keeps K² = 400 paths alive per goal — the blowup behind the paper's
    batch proving and K_max truncation (and behind GNTP/CTP after it)

이 두 열이 바로 정직한 비교입니다. 우리의 축소판은 깊이 2에서 121번의 단일화를 시도하고(머리 하나, 거기에 첫 원자의 후보 20개, 거기에 하드한 상수 검사를 통과한 첫 인자를 가진 5개의 사실 각각에 대해 다시 20개씩) 겨우 2개의 증명만을 완결하는데, 기호적 상수가 가차 없이 가지치기를 하기 때문입니다. 전체 NTP에는 그런 자비를 불러올 여지가 없습니다: 상수까지 임베딩되면, 이 모든 이항 사실은 어떤 0이 아닌 커널로 모든 하위 목표와 소프트-단일화되고, 아무것도 결코 실패하지 않으며, 이 하나의 목표에 대해 $K^2 = 400$ 개의 경로 전부가, 훈련 원자마다, 에포크마다, 그래디언트를 흘려보내며 살아남습니다(ntp_mini.py 455–456행의 단언들이 깊이-1 개수와 완결된 두 증명을 못 박고, 깊이-2 시도 횟수를 400-경로 폭증보다 엄격히 아래로 제한합니다). 그 산술을 한 번 규모를 키워 봅시다: $10^5$ 개의 사실로 이루어진 지식 베이스와 두-원자 몸체는 목표당 $10^{10}$ 개의 살아 있는 경로를 내놓습니다. 의미론의 어떤 미묘함이 아니라 바로 이 숫자가, 미분 가능한 증명이 작은 벤치마크 위에서 멈춰 서고만 있었던 이유이며, 이 분야가 내놓은 두 가지 답은 탐색의 두 반복문을 각각 공략합니다.

GNTP(Greedy NTP)는 사실 반복문을 공략합니다 [2]. 단일화하기에 앞서, 그것은 임베딩 공간 위에서의 최근접-이웃 탐색으로, 현재 목표에 임베딩이 가장 가까운 상위- $k$ 개의 사실과 규칙만을 검색해 오고(이 $k$ 는 작은 검색 예산이며, 커널 $k(a,b)$ 의 $k$ 와는 다른 글자 쓰임입니다), 지식 베이스의 나머지는 아무런 기여도 하지 못하게 둡니다: 증명 점수가 min들의 max이므로, 멀리 떨어진 사실의 커널은 어차피 min을 거의 살아남지 못하는데, 그러니 그것을 버려도 달라지는 것은 거의 없으면서, 분기 계수를 $K$ 에서 작은 상수로 무너뜨립니다. 보고된 효과는 미분 가능한 증명을, 원래 평가의 몇천 개짜리 사실 벤치마크로부터, 걸러지지 않은 시스템은 돌아갈 수 없었던 몇 자릿수는 더 큰 지식 베이스와 자연어 말뭉치 위로 옮겨 놓은 것이었습니다 [2]. CTP(Conditional Theorem Prover, 조건부 정리 증명기)는 규칙 반복문을 공략합니다 [3]. 모든 목표에 대해 모든 템플릿을 반복하는 대신, 학습된 select 모듈이 목표를 읽고 그것에 조건화되어 시도해 볼 만한 소수의 규칙을 생성합니다; 이 생성 과정은 미분 가능하므로 선택은 증명과 함께 종단간(end-to-end)으로 훈련되며, 논문은 이 모듈을 세 가지 방식으로 구체화합니다. 목표 술어의 임베딩에서 규칙의 술어 임베딩으로 가는 선형 사상, 알려진 술어들에 걸친 주의 분포, 그리고 메모리 기반 조회입니다 [3]. 이 계보는 하나의 교훈으로서 진술해 둘 가치가 있습니다. 귀결 원리(resolution principle) 이래로 하드 단일화는 최일반 단일자(most general unifier)를 계산하거나 실패하며, 실패는 공짜 가지치기입니다: 부분 트리 전체가 문자열 비교 한 번에 사라집니다 [4]. 커널은 결코 실패하지 않음으로써 동의어를 사들였고, GNTP의 검색과 CTP의 선택은 그렇게 잃어버렸던 규율을 소프트한 형태로 재설계한 것, 곧 정확한 "아니요"를 내주고 얻은 자리에 근사적인 "아니요"를 되돌려 놓은 것입니다.

아직 풀리지 않은 부분

홀드아웃 증명은 0.9032점을 받았고, 이 장은 그 숫자가 무엇인지를 조심스럽게 말해 왔습니다: 세 커널의 min을, 증명들에 걸쳐 최대화한 것입니다. 그 숫자가 아닌 것에 대해서도 정직해야 합니다. 그것은 증명이 아닙니다: 1권의 증명기는 그 정확함이 정리(theorem)인 유도를 돌려주었지만, 0.9032점의 소프트 증명은 그 세 개의 일치가 그저 학습된 기하 안에서 가까울 뿐인, 증명 모양을 한 대상입니다. 그것은 확률도 아닙니다: 훈련 손실은 그 점수를 가능도(likelihood)인 것처럼 다루었지만, min/max 대수의 그 무엇도 점수를 보정된(calibrated) 것으로 만들어 주지 않으며, I부는 이미 괴델 쌍이 정도가 아니라 순서만을 보존한다는 것을 보여 준 바 있습니다. 하나의 질의 안에서는 순서가 의미를 갖습니다(참인 쌍의 0.9032가 그 오염들의 천장 0.1354에 맞서는 것은 진짜 마진입니다); 그러나 질의들에 걸쳐서는 그 숫자들이 서로 견줄 수 있는 것이 아니어서, 한 목표의 0.83과 다른 목표의 0.79는 어느 쪽이 더 그럴듯한지에 대해 아무것도 부호화하지 않으며, 커널 바닥은 심지어 헛소리조차 적어도 $e^{-2}$ 는 받도록 보장합니다. 그런 점수가 보정될 수 있는지, 그리고 소프트 증명이 대체 무엇을 보증해 낼 수 있는지는 5권의 몫이며, 이 장은 그 물음을 의도적으로 열어 둔 채로 남겨 둡니다. 어떤 커널도 누그러뜨릴 수 없는 두 번째 한계는 깊이 제한입니다. 템플릿이 깊이 2에서 grandAdvisor를 닫아낼 수 있었던 것은 그 규칙이 두-홉 사슬이기 때문입니다; 세-홉짜리 great-grandAdvisor 질의는 어떤 임베딩으로도 깊이 2에서는 증명 불가능한데, 어떤 커널 값도 빠진 재귀의 단계를 불러낼 수는 없기 때문입니다. 이것은 3권의 표현력 천장 교훈이 증명기의 옷을 걸친 것입니다: 가설 공간이 빠뜨린 것은, 아무리 많은 훈련으로도 되찾을 수 없습니다.

왜 중요한가

이 장은 이 권의 제목이 갖는 가장 순수한 표본입니다: 게이트 하나만 바꾸어 미분 가능하게 만든 논리입니다. 알고리즘은 여전히 SLD 방식의 후방 연쇄이고, 치환은 여전히 정확하며, 증명 대상은 여전히 읽을 수 있는 유도입니다; 오직 기호 동등성만이 대체되었고, 이 권이 쌓아 온 모든 것이 바로 그 대체로 수렴했습니다. I부의 괴델 t-노름은 논리곱에 대한 추상적인 선택이기를 멈추고 증명 경로들을 채점하는 연산자가 되었으며, 그 원-핫 그래디언트는 이제 탐색 트리 전체 가운데 어느 두 기호가 주어진 스텝에서 무언가를 배우는지를 결정합니다. 그 결과는 또한 3권이 그저 무대에 올려 볼 수밖에 없었던 두 가지 주장을 얻어 냅니다: 손으로 배치된 것이 아니라 증명 성공으로부터 학습된 기하를 갖는 소프트 매칭, 그리고 사람이 읽을 수 있는 절로 도로 해독되는, 데이터로부터 유도된 규칙입니다. 커밋된 실행이 인쇄하는 증명 경로는 그 시스템의 계산이면서 동시에 그 설명이기도 한데, 이는 정확히 5권이 신뢰할 만한 추론기에게 요구하게 될 충실성(faithfulness) 속성이며, 이 비용 장부는 5권이 물려받게 될 규모의 문제입니다: 정직한 $K^{\text{depth}}$ 표는 "미분 가능하게 만들라"가 "돌아가게 만들라"와 충돌하는 지점이며, GNTP와 CTP는 그곳에서 이어지는 연구 프로그램의 첫 두 항목입니다.

핵심 용어

신경망 정리 증명기(Neural Theorem Prover, NTP) — 술어 비교가 실패/성공 대신 커널 유사도를 돌려주고, 증명 점수는 커널들의 min이며, 목표 점수는 증명들에 대한 max이고, 모든 것이 탐색을 관통하는 경사 하강으로 종단간(end-to-end) 훈련되는 후방 연쇄기입니다 [1].
소프트 단일화 커널(soft unification kernel) — $k(a, b) = \exp(-\lVert \theta_a - \theta_b \rVert_2 / (2\mu^2))$ 이며 $\mu = 1/\sqrt{2}$ 이고, 그리하여 있는 그대로의, 제곱하지 않은 유클리드 거리 위에서 $k = e^{-d}$ 입니다; 동일한 기호는 정확히 1점을 받고, 단위-노름 임베딩은 모든 점수를 $e^{-2} \approx 0.135$ 에서 바닥짓습니다.
규칙 템플릿(rule template) — 자유로운 술어 슬롯을 가진 규칙 모양으로, 여기서는 #1(X,Z) ← #2(X,Y) ∧ #2(Y,Z)이며, 그 슬롯들은 학습 가능한 임베딩 행입니다; 규칙을 학습한다는 것은 그 슬롯들을 실제 술어 근처로 옮긴다는 뜻이고, 해독은 각 슬롯을 그 최근접 알려진 술어로 읽어 냅니다.
자기-단일화 마스킹(self-unification masking) — 사실이 자기 자신을 증명하는 것을 금지하는, 훈련 시점의 가드입니다; 이것이 없으면 그 자체로 사실이기도 한 양성이 그래디언트 0으로 1점을 받아 아무것도 가르치지 못합니다.
서브그래디언트 라우팅(subgradient routing) — max와 min을 관통하는 공로 배분(credit assignment)입니다: 오직 승리한 증명만, 그리고 그 안에서도 오직 가장 약한 커널만 그래디언트를 받습니다; 훈련 원자 하나당 두 개의 임베딩 행이 움직입니다.
증명-경로 폭증(proof-path blowup) — 탐색 트리가 깊이마다 (KB 크기)를 몸체 길이만큼 거듭제곱하여 자라나는 것입니다; 여기서는 사실 20개에 대해 400개의 살아 있는 경로로 측정되며, 규모 확장 연구의 직접적인 동기입니다.
GNTP(Greedy NTP) — 단일화에 앞서 사실과 규칙을 상위- $k$ 개 최근접-이웃 검색으로 가져오는 미분 가능한 증명이며, 근사적인 조기-실패(fail-fast) 가지치기를 되살립니다 [2].
CTP(Conditional Theorem Prover, 조건부 정리 증명기) — 학습된 select 모듈이 모든 규칙을 반복하는 대신 목표에 조건화된 소수의 규칙을 생성하는 미분 가능한 증명이며, 선형·주의 기반·메모리 기반 변형을 갖습니다 [3].

이 장이 이어지는 곳

NTP는 규칙 학습을 증명 탐색에 용접해 붙였고, 그 용접의 대가를 치렀습니다: 모든 그래디언트 스텝이 증명기를 돌리고, 증명기의 트리는 지수적으로 자라납니다. 다음 장인 RNNLogic과 AnyBURL은 그 용접을 풀어냅니다. RNNLogic은 NTP가 하나로 녹여 버린 두 역할, 곧 후보 규칙을 제안하는 생성기와 그것들에 점수를 매기는 예측기를 분리하며, 잠재 변수 모델로 훈련하여 어느 쪽도 다른 쪽의 탐색 비용을 치르지 않도록 합니다; AnyBURL은 그래디언트를 아예 버리고, 접지 경로(ground path)를 표집하고 일반화함으로써 훨씬 적은 계산량으로 1초짜리 시간 조각 안에서 규칙을 채굴하는데, 그 민망할 만큼의 경쟁력은 이 부 전체가 필요로 하는 대조 실험입니다: 규칙 학습을 미분 가능하게 만드는 두 장을 거친 뒤, 정직한 물음은 그 미분 가능성이 실제로 무엇을 사 주었는가 하는 것입니다.

동반 코드: examples/integration/ntp_mini.py는 이 장 전체를 구현합니다: 제곱하지 않은 커널(125–138행), 깊이 제한과 자기-단일화 마스크를 지닌 점수 매겨진 or/and 증명기(169–239행), max 집계(242–256행), max와 min과 커널을 관통하여 손으로 유도한 NLL 서브그래디언트(261–324행), 에포크마다의 오염 표집(327–343행), 단위 구 위에서의 사영된 SGD(346–372행), 템플릿 해독(377–382행), 그리고 여기서 이루어진 모든 주장을 지키는 역량 단언들(430–456행)입니다. python3 examples/integration/ntp_mini.py를 실행하면 이 장의 모든 숫자를 바이트 단위까지 그대로 재현하며, 그 실행은 다음으로 끝납니다: SUMMARY ntp_mini: final_nll=0.0333 decode_#1=grandAdvisor:0.9769 decode_#2=advises:0.9032 conf=0.9032 held_out=0.9032 max_corrupt=0.1354 margin=0.7678 paths_d2=121/400.

이 장에서 다루는 내용​

두 조상, 빠져 있던 나머지 절반​

커널, 정확히​

점수 매겨진 탐색으로서의 증명기​

템플릿: 이제 "규칙을 학습한다"는 것이 뜻하는 바​

최솟값과 최댓값을 관통하는 그래디언트​

커밋된 실행 읽어 내기​

주장이 아니라 헤아려진 비용 장부​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 장이 이어지는 곳​