소프트 단일화: 벡터 공간에서 기호 맞추기

📍 현재 위치: V부 · 어텐션과 트랜스포머 — 17장. 벡터 기호 구조는 하나의 벡터에 결합과 중첩의 대수를 부여했습니다; 이 장은 그 스택에 남아 있던 마지막 하드 연산, 즉 1권의 모든 증명이 의지했던 기호-동등성 검사를 부드럽게 만듭니다.

이 시리즈가 실행해 온 모든 증명은, 1권의 후방 연쇄기에서 2권의 완결 엔진에 이르기까지, 궁극적으로 단 하나의 원초적 행위에 의지합니다: 두 기호가 같은 것인지를 결정하는 일입니다. 그 결정은 언제나 이진적이었습니다. advises는 advises와 단일화되지만, 그 어떤 사람이 두 단어를 서로 바꿔 써도 무방하다고 여기든 말든, supervises와는 단일화되지 않고, 될 수도 없으며, 앞으로도 결코 되지 않을 것입니다. 이 장은 그 이진적 결정을 등급이 매겨진 결정으로 대체합니다. 각 술어 이름은 하나의 벡터가 되고, 두 이름은 0과 1 사이의 커널 점수로 일치도가 매겨지며, 동일한 이름은 여전히 정확히 1점을 받고, 증명은 진리값 대신 자신이 거친 일치 점수들의 최솟값을 지니고 다닙니다. 그 결과는 상징적 증명의 재귀적 형태(목표, 규칙, 치환, 증명 트리) 전체를 그대로 간직하면서도, 자신의 하드 조상을 죽이는 근사한 실패에서 살아남는 증명기입니다. 커밋된 데모는 그 이득과 대가를 모두 실제 숫자로 측정하며, 그 대가야말로 이 장의 정직한 중심입니다: 소프트 증명은 하나의 점수이며, 점수는 그것을 지켜 주는 수치적 여유만큼만 신뢰할 수 있습니다.

쉽게 말하면

서류를 처리하는 어떤 관공서를 상상해 보세요. 옛날 직원은 서식의 항목 이름표가 규정집과 정확히 일치하지 않는 모든 서식을 거부합니다: 규정집이 "지도교수"라고 적어 둔 자리에 "감독자"라고 쓰면, 의도가 아무리 뻔해도 여러분의 신청서는 그 자리에서 죽어 버립니다. 새로 온 직원은 근사한 일치를 받아들이되, 각각의 옆에 확신도를 적어 넣습니다: "지도교수"/"지도교수"는 1.0을, "지도교수"/"감독자"는 0.98을, "지도교수"/"인용"은 0.36을 받습니다. 여러분의 신청서가 이런 직원들의 사슬을 통과할 때, 최종 도장에는 어느 직원이 적었든 그중 가장 낮은 확신도가 찍히는데, 판단의 사슬은 그중 가장 흔들리는 고리만큼만 신뢰할 수 있기 때문입니다. 그런 다음 관공서는 기준선을 정합니다: 0.80 이상의 도장이 찍힌 신청서만 통과합니다. 이 장에 담긴 모든 것이 바로 이 관공서를 정밀하게 다듬어 놓은 것입니다: 확신도는 벡터 위의 커널이고, 최저-도장 규칙은 t-노름이며, 기준선은 하나의 임계값인데, 그 정확한 위치가 결국 모든 위험이 도사리는 곳으로 밝혀집니다.

이 장에서 다루는 내용

다시 떠올리는 경첩: 세 문장으로 요약한 1권의 단일화(치환, 동등성 게이트, 하드 실패)와, 미지의 술어 이름 하나가 증명 전체를 죽여 버리는 취약성 전시.
커널: $\mathbb{R}^{16}$ 안의 단위 벡터로 표현된 술어 이름들, RBF 일치 함수 $\exp(-\lVert \mathbf{u}-\mathbf{v}\rVert^2/2\sigma^2)$ , 동일한 기호는 정확히 1점을 받는다는 증명, 관용도 다이얼 $\sigma$ , 그리고 무작위 기호들이 어디에 자리 잡는지에 대한 분산 논증.
t-노름에 의한 합성: 증명의 점수는 그 일치 점수들의 MIN이며, 이는 2권의 주석 논리에 나온 괴델 t-노름입니다; MAX는 대안적인 증명들을 모으고, 곱은 언급되는 또 다른 대안입니다.
설계상의 분리: 원조 NTP는 상수를 포함한 모든 비변수 기호를 소프트하게 일치시키지만, 이 모듈은 술어만을 부드럽게 만들고 인자는 여전히 하드하게 바인딩하며, 이 장은 왜 이 좁힌 분리가 여기서 옳은 선택인지를 논증합니다.
한 줄 한 줄 살펴보는 연쇄기: 1권의 깊이 제한 목표 축소에, 모든 재귀 호출을 관통하는 점수를 하나 꿰어 넣은 것입니다.
커밋된 세 개의 데모: 정확한 연쇄가 1.0000으로 재현되는 데모, 하드 증명기가 아무것도 돌려주지 못하는 곳에서 0.9783으로 미지의 술어가 증명되는 데모, 그리고 최선의 증명이 0.4621에 머무르는 대조 데모이며, 누출 임계값들이 실제로 그것이 무엇인지, 즉 조절 나사임을 있는 그대로 출력합니다.
이것이 어떻게 하나의 연구 분야가 되었는가: 처음부터 끝까지 미분 가능한 증명, 유도된 커널의 그래디언트, 증명 폭발의 비용, 그리고 어텐션으로 이어지는 계보.

다시 떠올리는 경첩: 정확히 일치하거나 실패하거나

1권의 귀결과 SLD(SLD는 한정절에 대한 선택적 선형 귀결, 곧 Selective Linear resolution for Definite clauses의 줄임말입니다)는 단일화(unification) 위에 증명을 세웠습니다: 목표 원자와 규칙의 머리(혹은 사실)가 주어졌을 때, 두 원자를 동일하게 만드는 치환(substitution), 즉 변수를 항에 대응시키는 딕셔너리를 찾거나, 그렇지 않으면 실패를 보고합니다[1]. 이 절차는 구성상 전부 아니면 전무입니다: 술어 이름은 문자열로서 같아야 하고, 상수도 문자열로서 같아야 하며, 완전한 1차 논리에서는 발생 검사(occurs check)가 추가로, 어떤 변수를 그 자신을 포함하는 항에 바인딩하는 것을 거부합니다(1권의 함수 없는 파편은 항이 결코 중첩될 수 없었으므로 이를 발동시킬 필요가 전혀 없었습니다). 단일화가 성공하면 치환을 돌려주고 증명이 계속되며, 실패하면 그 증명의 갈래는 "거의"라는 개념 없이 죽어 버립니다.

아래에 나오는 모든 것에 동기를 부여하는 상처는 다음과 같습니다. 1권의 증명기에게 질의 supervises(bob, Z)를 던져 보십시오. examples/logic/kb.py의 지식 베이스는 네 개의 advises 사실을 담고 있고, 그 가운데는 advises(bob, carol)과 advises(bob, dave)도 있으며, 영어를 읽을 줄 아는 사람이라면 누구나 그 사실들이 이 질문에 답한다는 것을 압니다. 증명기는 영어를 읽지 않습니다. 그것은 술어가 문자열 supervises인 사실이나 규칙의 머리를 훑어보고, 아무것도 찾지 못한 채, 빈 답 집합을 돌려줍니다. 낯선 단어 하나 때문에, 답을 뻔히 담고 있는 지식 베이스가 아무 쓸모도 없어집니다. 이 실패는 버그가 아닙니다; 이것은 바로 1권의 증명들을 감사 가능하게 만들어 준 계약 그 자체입니다. 이 장의 질문은 그 계약을 폐기하는 대신 통제된 정도만큼 완화할 수 있는가입니다.

벡터가 된 기호: 커널이 일치도를 매기다

신경망 정리 증명기(Neural Theorem Prover, NTP)가 도입한 이 완화는 외과적으로 정교합니다[2]: 증명 기계 전체(목표, 규칙, 치환, 재귀)는 그대로 두고, 기호에 대한 문자열-동등성 검사만을 그 기호들의 임베딩(embedding)에 대한 유사도 점수로 대체합니다. 원조 NTP에서는 이 부드러움이 전면적입니다: 술어 이름이든 상수든, 비변수 기호는 모두 하나의 벡터를 얻고, 같은 위치에 있는 다른 어떤 기호와도 소프트하게 일치할 수 있습니다. 동반 모듈은 이 메커니즘을 채택하되, 의도적으로 술어 이름에만 좁혀 적용하는데, 이 설계상의 제한은 아래 그 자체의 절에서 옹호됩니다. soft_unification.py는 상수 블록(56–58행)에서 그 기하를 설정합니다: 모든 술어 이름 $p$ 는 벡터 $\mathbf{u}_p \in \mathbb{R}^{D}$ 를 얻는데(기호 $\in$ 는 "…의 원소이다"라고 읽고, $\mathbb{R}^{D}$ 는 실수 $D$ 개로 이루어진 모든 목록의 집합입니다), 여기서 $D = 16$ 은 임베딩 차원(각 기호의 벡터가 갖는 좌표의 개수)이고, $\sigma = 1$ (시그마)은 곧 해독할 폭 매개변수이며, $\tau = 0.8$ (타우)은 답의 점수가 도달해야 하는 수락 임계값입니다. 각 벡터는 시드가 고정된 무작위 생성기에서 뽑혀 단위 길이로 정규화되므로, 모든 술어에 대해 $\lVert \mathbf{u}_p \rVert = 1$ 입니다(63–68행); 이중 세로선 $\lVert\cdot\rVert$ 은 유클리드 노름, 즉 좌표들의 제곱합의 제곱근을 나타냅니다. 그런 다음 두 이름은 방사 기저 함수(radial basis function, RBF) 커널로 일치도가 매겨지는데, 여기 파일에서 그대로 인용합니다(soft_unification.py 80–88행):

def kernel(p: str, q: str) -> float:
    """NTP's soft-match score for two predicate names: the RBF kernel

        k(p, q) = exp(-‖u_p − u_q‖² / (2σ²)),   σ = 1.

    Identical symbols have distance 0, so k = e⁰ = 1.0 *exactly*: hard
    unification is the special case the kernel recovers."""
    diff = EMB[p] - EMB[q]
    return float(np.exp(-float(np.dot(diff, diff)) / (2.0 * SIGMA * SIGMA)))

수식을 해독하기 전에 충실성에 관한 메모 하나: 독스트링은 이 메커니즘을 NTP의 공으로 돌리는데, 메커니즘(동등성 검사 자리에 유사도 커널을 놓는 것) 자체는 실제로 NTP의 것이지만, 정확한 수식은 이 모듈의 선택입니다. NTP가 발표한 커널은 제곱하지 않은 평범한 유클리드 거리에 대한 지수 함수인 $\exp\!\big(-\lVert \mathbf{u}_p - \mathbf{u}_q \rVert_2 / (2\mu^2)\big)$ 이고(아래 첨자 2는 위에서 해독한 것과 같은 노름을 표시합니다), 그 폭 $\mu$ (뮤)는 $1/\sqrt{2} \approx 0.707$ 로 고정되어 있습니다[2]. 이 모듈은 그 대신 $\sigma = 1$ 인 표준 제곱-지수(squared-exponential) RBF를 사용합니다; 두 형태 모두 거리에 따라 감소하고 동일한 기호에 정확히 1점을 주며, 이 장의 모든 숫자는 위에 인용된 제곱 형태로 계산된 것입니다.

이 수식을 믿기 전에 먼저 해독해 봅시다. 두 기호 임베딩 사이의 차이 벡터를 $\boldsymbol{\delta} = \mathbf{u}_p - \mathbf{u}_q$ 라고 씁니다. 커널은

k(p, q) \;=\; \exp\!\left(-\,\frac{\lVert \mathbf{u}_p - \mathbf{u}_q \rVert^2}{2\sigma^2}\right),

여기서 $\exp(x) = e^x$ 는 지수 함수입니다. 세 가지 성질이 이 장 전체를 떠받치며, 각각은 단언이 아니라 짧은 유도입니다.

동일한 기호는 정확히 1점을 받습니다. $p = q$ 이면 $\boldsymbol{\delta} = \mathbf{0}$ 이므로 $\lVert\boldsymbol{\delta}\rVert^2 = 0$ 이고, 근사가 아니라 정확히 $k = e^0 = 1$ 입니다. 반대로 $\lVert\boldsymbol{\delta}\rVert^2 \ge 0$ 은 항상 성립하고, 0 이하인 수의 지수는 많아야 1이므로 $k \le 1$ 이며, 등호는 오직 임베딩이 일치할 때만 성립합니다. 따라서 하드 단일화는 특수한 경우로서 소프트 증명기 안에서도 살아남습니다: 옛 증명기가 성공했을 모든 곳에서, 새 증명기도 점수 1로 성공합니다.

단위 벡터 위에서는 커널이 각도만의 함수입니다. $\mathbf{a}\cdot\mathbf{b} = \sum_i a_i b_i$ (대문자 시그마 $\sum_i$ 는 서로 대응하는 성분의 곱 $a_i b_i$ 를 좌표 위치 $i$ 가 1에서 $D$ 까지 움직이는 동안 모두 더하라는 뜻입니다)와 $\lVert\mathbf{a}\rVert^2 = \mathbf{a}\cdot\mathbf{a}$ 를 이용해 내적으로 제곱 거리를 전개하면:

\lVert \mathbf{u}_p - \mathbf{u}_q \rVert^2 = (\mathbf{u}_p - \mathbf{u}_q)\cdot(\mathbf{u}_p - \mathbf{u}_q) = \mathbf{u}_p\cdot\mathbf{u}_p - 2\,\mathbf{u}_p\cdot\mathbf{u}_q + \mathbf{u}_q\cdot\mathbf{u}_q = 2 - 2\,\mathbf{u}_p\cdot\mathbf{u}_q,

두 벡터 모두 단위 노름을 가지기 때문입니다. $\sigma = 1$ 을 대입해 커널에 넣으면:

k(p,q) \;=\; \exp\!\left(-\,\frac{2 - 2\,\mathbf{u}_p\cdot\mathbf{u}_q}{2}\right) \;=\; e^{\,\mathbf{u}_p\cdot\mathbf{u}_q\, -\, 1}.

두 단위 벡터의 내적은 그 사이 각도의 코사인이므로, 점수는 오직 그 각도에만 의존하며, $e^{-2} \approx 0.135$ (정반대 방향)에서 $e^0 = 1$ (같은 방향)까지의 범위를 갖습니다. 데모가 출력하는 모든 커널 숫자는 커밋된 두 벡터에 대해 이 식을 계산한 값입니다.

폭 $\sigma$ 는 관용도 다이얼입니다. 단위 벡터 위에서의 일반형 $k = \exp(-(1 - \cos\theta)/\sigma^2)$ 을 놓고 두 극한을 살펴봅시다. $\sigma \to 0$ 이면 $\theta \neq 0$ 인 모든 각도에서 지수가 $-\infty$ 로 발산하므로, 동일한 쌍은 1에 머무르는 반면 동일하지 않은 모든 쌍에서는 $k \to 0$ 이 됩니다: 커널은 동등성의 지시 함수로 퇴화하며, 하드 단일화는 단순한 특수 사례가 아니라 하나의 극한으로 회복됩니다. $\sigma \to \infty$ 이면 모든 쌍에서 지수가 0으로 가므로 어디서나 $k \to 1$ 이 되고, 모든 기호가 서로 바꿔 쓸 수 있게 됩니다. 이 두 극단 사이에서 $\sigma$ 는 각도상의 불일치가 얼마만큼의 비용을 치르게 할지를 정하며, 데모는 $\sigma = 1$ 로 고정해 두고 모든 조정을 대신 임계값 $\tau$ 를 통해 수행합니다.

시드로 고정된 기하, 측정하다

무관한 기호들은 어디에 자리 잡을까요? 이 모듈은 지식 베이스나 규칙의 머리에 등장하는 여덟 개의 술어를, 서로 독립인 무작위 단위 방향들로 임베딩합니다(아홉 번째인 supervises는 의도적으로 구성된 것으로, 데모 B의 몫입니다). 차원 $D$ 안의 독립적인 무작위 단위 벡터들에 대해서는, 대칭성에 의해 기대 내적이 0이며, 그 분산은 유도해 볼 만한 정확한 값을 갖습니다. $\mathbb{E}[\cdot]$ 를 기댓값(expected value), 즉 어떤 무작위량을 그 무작위 추출에 대해 평균한 값이라고 씁시다. $\mathbf{v}$ 를 무작위 단위 벡터, $\mathbf{u}$ 를 임의로 고정된 단위 벡터라고 합시다. $\mathbf{v}$ 의 좌표들은 교환 가능(exchangeable, 좌표를 어떻게 재배열해도 분포가 같다는 뜻)하므로, $D$ 개의 좌표 모두가 하나의 공통된 기대 제곱값을 공유합니다; $\sum_{i=1}^{D} \mathbb{E}[v_i^2] = \mathbb{E}[\lVert\mathbf{v}\rVert^2] = 1$ 이므로, 그 공통값은 $\mathbb{E}[v_i^2] = 1/D$ 입니다. 서로 다른 좌표들은 부호 대칭성(한 좌표의 부호를 뒤집어도 분포는 그대로이지만 곱은 부호가 바뀐다는 사실)에 의해 $\mathbb{E}[v_i v_j] = 0$ 을 만족합니다. 그러면

\operatorname{Var}(\mathbf{u}\cdot\mathbf{v}) = \mathbb{E}\!\left[\Big(\sum_{i=1}^{D} u_i v_i\Big)^{2}\right] = \sum_{i=1}^{D}\sum_{j=1}^{D} u_i u_j\, \mathbb{E}[v_i v_j] = \sum_{i=1}^{D} u_i^2 \cdot \frac{1}{D} = \frac{1}{D}.

$D = 16$ 이면 전형적인 내적은 $\pm 1/\sqrt{16} = \pm 0.25$ 이므로, 무관한 기호들은 $e^{0 \pm 0.25 - 1}$ 근처, 즉 대략 $e^{-1.25} \approx 0.287$ 과 $e^{-0.75} \approx 0.472$ 사이에서 $e^{-1} \approx 0.368$ 을 중심으로 점수를 받아야 합니다. 실행 결과가 이를 확인해 줍니다. 다음은 python3 soft_unification.py가 커밋한 출력으로, advises와 다른 모든 술어 사이의 커널 행입니다:

kernel row of advises (its soft match against every other predicate):
  supervises   0.9783   student      0.5292   about        0.4692   professor    0.4189
  cites        0.3621   authored     0.3555   grandAdvisor 0.2939   affiliated   0.2455
  (supervises is constructed: normalize(e_advises + 0.25·noise), a
   stand-in for what training on text would learn; the rest are
   independent random directions, so they land near exp(−1) ≈ 0.37)

유도한 결과에 비추어 이 행을 읽어 봅시다. $k = e^{\cos\theta - 1}$ 을 뒤집으면 $\cos\theta = 1 + \ln k$ 를 얻는데, 여기서 $\ln$ 은 자연로그입니다. 따라서 0.5292인 student는 $\cos\theta = 0.364$ (0보다 약 $1.5$ 표준편차 위)에 있고, 0.2455인 affiliated는 $\cos\theta = -0.405$ (약 $1.6$ 표준편차 아래)에 있습니다; 이 행의 무작위 기호 일곱 개 모두가 예측된 중심으로부터 표준편차 두 개 이내에 들어오는데, 이는 $1/D$ 분산이 약속하는 바로 그 집중도입니다(advises는 자기 자신의 행에는 등장하지 않고, 여덟 번째 항목인 supervises가 공학적으로 설계된 예외입니다). 그 유일한 공학적 항목은 0.9783점을 받습니다. 커널 자체의 계산 과정을 따라가 보면: 커밋된 임베딩은 $\mathbf{u}_{\text{supervises}}\cdot\mathbf{u}_{\text{advises}} = 0.97802$ 를 내주므로, $\lVert\boldsymbol{\delta}\rVert^2 = 2 - 2(0.97802) = 0.04396$ 이고 $k = e^{-0.04396/2} = e^{-0.02198} = 0.9783$ 이며, 이는 출력된 값과 일치합니다; 중간 계산은 소수점 다섯 자리까지 유지해야 하는데, 내적을 먼저 0.9780으로 반올림하면 0.9782에 이르러 마지막 자릿수를 놓치기 때문입니다. cites의 경우 $\cos\theta = -0.0157$ 이 $k = e^{-1.0157} = 0.3621$ 을 줍니다. 한 숫자는 "근사 동의어"를 뜻하고 다른 숫자는 "잡음 바닥"을 뜻하며, 이 장 전체는 바로 그 둘 사이의 간극에 관한 것입니다.

증명의 대수: 경로를 따라서는 MIN, 증명들에 걸쳐서는 MAX

하나의 소프트 일치는 하나의 점수를 만들어 내고, 하나의 증명은 여러 일치를 사슬로 엮으며, 하나의 질의는 여러 개의 증명을 가질 수 있습니다. 이 두 가지 합성 모두 하나의 대수가 필요하며, 데모는 그 둘 모두를 2권에서 가져옵니다. t-노름(t-norm)이란 구간 $[0,1]$ 위의 이항 연산으로, 교환법칙과 결합법칙을 만족하고, 각 인자에 대해 단조적이며, 1을 항등원으로 갖는 것입니다: 논리적 AND를 등급이 매겨진 진리값으로 일반화하는 표준적인 방법입니다. 이 모듈은 증명의 일치들을 괴델 t-노름(Gödel t-norm), 즉 최솟값으로 합성합니다:

\text{score}(\text{proof}) \;=\; \min\big(k_1, k_2, \ldots, k_m\big),

여기서 $k_1, \ldots, k_m$ 은 증명의 $m$ 개 술어 일치(경로를 따라 사실이나 규칙 머리와의 일치마다 하나씩)에 대한 커널 점수입니다. 일치들의 사슬은 정확히 그 가장 약한 고리만큼 강합니다. 같은 답에 대한 대안적인 증명들은 괴델 t-여노름(Gödel t-conorm)인 MAX로 모입니다: 답은 그 최선의 증명만큼 좋습니다. 이는 정확히 주석 논리가 2권에서 도출을 거쳐 확신도를 전파하는 데 사용했던 ⟨min, max⟩ 확신도 대수이며, 이제 초대받지 않은 채 신경망 증명기 안에 다시 나타난 것이고, 원조 NTP가 증명에 점수를 매기는 데 사용하는 바로 그 합성입니다[2].

min만이 유일한 후보는 아닙니다. 곱 t-노름(product t-norm) $k_1 k_2 \cdots k_m$ 은 몇몇 미분 가능한 증명 변형이 사용하는 또 다른 표준적 선택이며, 독립적인 불확실성들을 복합시킨다는 확률론자의 미덕을 지니고 있습니다. 이 데모에서는 min이 출력된 숫자들을 읽기 쉽게 만들어 주는 세 가지 성질을 갖습니다. 첫째, min은 멱등적(idempotent)입니다: $\min(a, a) = a$ 이므로, 증명은 단지 길다는 이유만으로 값이 줄어들지 않습니다. 곱셈 아래에서라면 0.9783인 세 개의 일치는 $0.9783^3 = 0.9363$ 으로 복합되었을 것인데, 이는 여기서는 아무런 의미상의 근거도 없는, 깊이에 대한 벌점입니다. 둘째, 모든 증명 점수는 귀속 가능(attributable)합니다: 출력된 숫자는 여러 값들의 혼합이 아니라, 식별 가능한 하나의 일치에 대한 식별 가능한 하나의 커널 값 그 자체입니다. 셋째, 정확한 하위 증명은 공짜입니다: 아무리 많은 1.0 일치가 있어도 min은 그대로 유지되며, 이것이 바로 소프트 증명기가 하드 결과를 정확히 재현할 수 있게 해 주는 이유입니다. 아래 커밋된 데모 A 표에서 min이 작동하는 모습을 직접 볼 수 있습니다: 답 logic은 압축된 경로 grandAdvisor~grandAdvisor 1.0000 · advises~authored 0.3555 · advises~about 0.4692를 거쳐 0.3555점을 받는데, 실제로 $\min(1.0000,\, 0.3555,\, 0.4692) = 0.3555$ 이며, 이는 가운데 일치, 즉 가장 약한 고리입니다.

하드한 인자, 소프트한 술어

그 어떤 임계값보다도 안전에 더 크게 기여하는 설계상의 결정이 하나 있으며, 이는 NTP가 아니라 이 모듈에 속합니다. 원조 NTP는 모든 비변수 기호를 임베딩하고, 상수든 술어 이름이든 그 어떤 쌍이든 소프트하게 일치시킵니다[2]. 동반 모듈은 이 완화를 좁힙니다: 술어 검사만 부드러워지고, 원자 안의 상수와 변수인 인자는 여전히 1권의 치환 기계 그대로 하드하게 단일화됩니다. 이 분리는 두 개의 작은 함수에서 눈에 보입니다. 술어 게이트는 다음과 같습니다(soft_unification.py 119–127행):

def _pred_match(p: str, q: str, soft: bool) -> float | None:
    """Score of matching goal predicate ``p`` against KB predicate ``q``.
    Hard mode is Volume 1's gate: 1.0 iff the names are equal, else fail.
    Soft mode is NTP's: always succeed, with the kernel as the score."""
    if not soft:
        return 1.0 if p == q else None
    if p not in EMB or q not in EMB:
        return None
    return kernel(p, q)

그리고 인자 단일화기 _unify_args(soft_unification.py 98–116행)는 술어-동등성 게이트를 뺀 1권의 unify와 같으며, 그 마지막 분기는 여전히 하드한 절 return None # two different constants — arguments never go soft로 끝납니다. 이 제한의 근거는 감상적인 것이 아니라 의미론적인 것입니다. 술어 이름은 어휘적 이름표이고, 동의어 관계는 어휘 수준에서 살아 있습니다: supervises와 advises는 그럴듯하게 같은 관계를 가리킬 수 있습니다. 상수는 한 개체를 가리키는 포인터입니다: carol과 dave는 서로 다른 사람이며, 둘의 임베딩이 아무리 비슷하다 해도 한쪽에 관한 질문에 다른 쪽에 관한 사실로 답하는 것을 정당화하지는 못합니다. 술어를 흐리는 것은 답이 얼마나 확신되는지를 바꾸고, 인자를 흐리는 것은 답이 누구에 관한 것인지를 바꿔 버립니다. 인자를 하드하게 유지하는 것은 또한 답 집합을 이산적으로(각 답은 실제 치환으로 찾아낸 진짜 바인딩입니다) 유지해 주며, 이것이 바로 데모의 표들을 애초에 가능하게 만들어 주는 것입니다. 그 대가 또한 정직하게 인정됩니다: 이 모듈은 개체들에 걸쳐 일반화하는 NTP의 능력을 포기하며, 그 교환을 감사 가능성과 맞바꿉니다.

하드 단일화의 동등성 게이트와 그것을 대체하는 RBF 커널을 나란히 놓고, 그 아래에는 증명 경로의 MIN 합성과 데모들이 자리 잡는 수락 축을 함께 보여준다: 정확한 경우는 1.0000, 바꿔 말한 경우는 0.9783, 가장 나쁜 무작위 충돌은 0.6806, 대조군은 0.4621이며, 임계값 τ = 0.80은 그 실질적인 여유 구간 안에 놓여 있다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

연쇄기: 1권의 기계 장치를 관통하는 점수

이 증명기는 1권의 깊이 제한 후방 연쇄기에 새로운 동승자 하나를 태운 것입니다: 이제 모든 재귀 호출은 치환과 함께 점수도 하나 산출합니다. 지식 베이스는 다시 타이핑된 것이 아니라 임포트된 것입니다: 사실들은 examples/logic/kb.py에서 곧바로 가져오고, 유일한 규칙은 1권의 연쇄 규칙을 깊이 제한 2로 다시 선언한 것입니다(soft_unification.py 49–52행):

RULES: list[tuple] = [
    (("grandAdvisor", "X", "Z"), [("advises", "X", "Y"), ("advises", "Y", "Z")]),
]
MAX_DEPTH: int = 2

핵심 생성기 _prove는 목표의 모든 증명을 세 쌍으로 산출합니다: 확장된 치환, 증명의 점수, 그리고 일치 단계들의 목록입니다. 사실이 먼저 시도됩니다(soft_unification.py 150–160행):

    # 1. Facts.  Predicate match is soft; argument unification is hard.
    for fact in FACTS:
        if len(fact) != len(g):
            continue
        kv = _pred_match(g[0], fact[0], soft)
        if kv is None:
            continue
        s2 = _unify_args(g, fact, sub)
        if s2 is None:
            continue
        yield s2, kv, [Step(indent, g, f"fact {_atom(fact)}", g[0], fact[0], kv)]

코드를 한 줄씩 따라가 봅시다. 항수(arity) 검사(len(fact) != len(g))는 구조적 불일치를 곧바로 거부합니다; 항수는 결코 소프트해지지 않습니다. _pred_match는 커널 점수 kv를 돌려주거나, 하드 모드에서 이름이 다를 때는 None을 돌려주는데, 이 단 하나의 호출 지점이 1권의 증명기와 이 증명기 사이의 차이 전부입니다. 그런 다음 _unify_args는 1권이 했던 것과 정확히 똑같이 인자를 하드하게 바인딩합니다; 상수 충돌은 여전히 그 갈래를 죽입니다. 성공적인 사실 일치는 점수가 그저 kv인 한 단계짜리 증명인데, 원소 하나의 min은 그 자신이기 때문입니다. 다음은 규칙입니다(162–179행): 목표의 술어가 규칙 머리의 술어와 점수 kv로 소프트하게 일치하고, 머리의 인자는 하드하게 바인딩되며, 몸체는 한 단계 더 깊이 증명되는데, 깊이 제한(if depth == 0: return)이 재귀를 유한하게 유지합니다. 점수들은 산출 지점에서 만납니다:

        for s3, body_score, body_steps in _prove_all(
                body, s2, depth - 1, indent + 1, soft, counter):
            # score = min(head match, body score): the Gödel t-norm again.
            yield s3, min(kv, body_score), [head_step] + body_steps

논리곱도 같은 방식으로 합성됩니다(soft_unification.py 182–192행): _prove_all은 첫 번째 연언지를 증명하고, 그 치환을 나머지에 꿰어 넣은 다음, min(sc1, sc2)를 산출합니다; 빈 연언은 min의 항등원인 1.0을 산출하므로, 몸체가 다 소진된 규칙은 아무 비용도 치르지 않습니다. 마지막으로 answers(195–212행)는 생성기를 끝까지 실행하고, 서로 다른 바인딩마다 최선의 증명을 보관하며(MAX 풀링), 각 최선의 증명을 출력 가능한 단계별 줄로 렌더링합니다. 답은 그것의 풀링된 점수가 임계값에 도달할 때 수락됩니다: $\text{score} \ge \tau = 0.8$ .

데모 A: 정확한 연쇄, 1.0000으로 재현되다

첫 번째 데모는 하드 증명기가 이미 답할 수 있는 질문인 grandAdvisor(alice, Z)를 소프트 증명기에게 던져서, 기호가 정확할 때는 부드러움이 아무런 대가도 치르지 않는지 확인합니다. 커밋된 출력이며, 이번에는 전체 표입니다:

Demo A — exact: grandAdvisor(alice, Z) via the chain rule
  Z         score  ≥τ   best proof (pred~pred kernel, MIN-composed)
  carol    1.0000  yes  grandAdvisor~grandAdvisor 1.0000 · advises~advises 1.0000 · advises~advises 1.0000
  dave     1.0000  yes  grandAdvisor~grandAdvisor 1.0000 · advises~advises 1.0000 · advises~advises 1.0000
  mit      0.6806  -    grandAdvisor~affiliated 0.6806
  p1       0.4208  -    grandAdvisor~authored 0.4208
  logic    0.3555  -    grandAdvisor~grandAdvisor 1.0000 · advises~authored 0.3555 · advises~about 0.4692
  bob      0.2939  -    grandAdvisor~advises 0.2939
  erin     0.2939  -    grandAdvisor~grandAdvisor 1.0000 · advises~advises 1.0000 · advises~grandAdvisor 0.2939 · +2 more
  … 5 more bindings, all ≤ 0.2939

수락된 집합은 정확히 쌍 {carol, dave}이며, 각각 $\min(1, 1, 1) = 1.0000$ 을 받습니다: 목표가 규칙의 머리와 정확히 일치했고, 두 몸체 원자 모두 advises 사실들과 정확히 일치하여, alice → bob → carol과 alice → bob → dave를 추적합니다. p1 이하의 모든 것은 분산 분석이 예측한 바로 그대로 행동하는 잡음 바닥이며, 0.25–0.42대의 무작위 충돌들입니다. 출력된 증명 경로는 이 재현을 감사 가능하게 만들어 줍니다:

  proof of Z = carol (score 1.0000):
    grandAdvisor(alice,carol) ~ rule grandAdvisor(X,Z) ← advises(X,Y), advises(Y,Z)   k(grandAdvisor,grandAdvisor)=1.0000
      advises(alice,bob) ~ fact advises(alice,bob)   k(advises,advises)=1.0000
      advises(bob,carol) ~ fact advises(bob,carol)   k(advises,advises)=1.0000

같은 목표에 대해 실행한 하드 증명기는 똑같은 두 바인딩을 돌려주며, 이 모듈은 그 일치를 단언합니다(soft_unification.py 279–280행). 한 행은 다시 살펴볼 가치가 있습니다. 차점자인 0.6806의 mit은 근사 동의어 효과가 아닙니다; 이것은 목표 술어 grandAdvisor가 시드로 고정된 두 방향의 순전한 무작위 충돌을 통해 사실 affiliated(alice, mit)과 소프트하게 일치한 것으로, $\cos\theta = 0.615$ 이며, $D = 16$ 에 대한 평균보다 약 $2.5$ 표준편차 위에 있습니다. 이 어휘 안의 28개 무작위 쌍 가운데 이것이 최댓값입니다: 0.6806은 어휘 전체에서 가장 나쁜 충돌이며, 어떤 안전한 임계값이든 반드시 넘어서야 하는 단 하나의 숫자이고, 이것이 바로 데모의 $\tau = 0.8$ 이 0.37 근처의 잡음 바닥보다 그토록 높이 자리 잡은 이유입니다. 이 숫자를 기억해 두십시오; 데모 C의 정직성 감사는 바로 이 행에 달려 있습니다.

데모 B: 사실이 하나도 없는 술어로 증명하기

핵심 데모는 이 장에 동기를 부여한 바로 그 질문을 던집니다: supervises(bob, Z), 이는 어떤 사실에도 어떤 규칙에도 등장하지 않는 술어입니다. 먼저, supervises가 애초에 어떻게 벡터를 얻게 되었는지, 그 정직성 메모를 그대로 살려 인용합니다(soft_unification.py 70–77행):

# The UNSEEN query predicate ``supervises``: no fact and no rule mentions it.
# Its vector is placed *near* ``advises`` — normalize(e_advises + 0.25·noise),
# with unit noise — standing in for what training on text would learn, because
# "X supervises Y" is used in the same contexts as "X advises Y".
_noise = _rng.standard_normal(D)
_noise /= float(np.linalg.norm(_noise))
_sup = EMB["advises"] + 0.25 * _noise
EMB["supervises"] = _sup / float(np.linalg.norm(_sup))

이 모듈 안에서는 어떤 훈련도 일어나지 않습니다; 그 배치는 분포적 학습을 대신하는, 시드로 고정된 기하입니다. 훈련된 시스템이라면 supervises의 벡터는 두 단어가 같은 맥락에서 등장하기 때문에 결국 advises 근처에 자리 잡았을 것입니다; 여기서 데모는 그 결과를 직접 구성해 놓고 그 사실을 그대로 밝힙니다. 벡터가 자리 잡고 나면, 커밋된 출력은 하드 증명기와 소프트 증명기를 나란히 놓아 보여줍니다:

Demo B — soft: supervises(bob, Z), an UNSEEN predicate (no facts)
  hard prover (Volume 1's equality gate): answers = []  — symbolic unification fails outright
  soft prover: k(supervises, advises) = 0.9783, so advises facts carry the query
  Z         score  ≥τ   best proof (pred~pred kernel, MIN-composed)
  carol    0.9783  yes  supervises~advises 0.9783
  dave     0.9783  yes  supervises~advises 0.9783
  p1       0.3638  -    supervises~authored 0.3638
  erin     0.3285  -    supervises~grandAdvisor 0.3285 · advises~advises 1.0000 · advises~advises 1.0000
  logic    0.3285  -    supervises~grandAdvisor 0.3285 · advises~authored 0.3555 · advises~about 0.4692
  p2       0.3285  -    supervises~grandAdvisor 0.3285 · advises~advises 1.0000 · advises~authored 0.3555
  p3       0.3285  -    supervises~grandAdvisor 0.3285 · advises~advises 1.0000 · advises~authored 0.3555
  … 4 more bindings, all ≤ 0.2939

첫 줄의 빈 목록이 1권의 판정 전부입니다: supervises라는 이름의 사실은 없으므로, 증명할 것이 아무것도 없습니다. 소프트 증명기는 {carol, dave}를 0.9783으로 수락하는데, 각각 목표 supervises(bob,carol)이 사실 advises(bob,carol)과 일치하는 한 단계짜리 증명을 거쳐, 점수 $\min(0.9783) = 0.9783$ 으로, $\tau = 0.8$ 을 넘어섭니다. 네 번째 행은 규칙도 참여하는 모습을 보여줍니다: erin은 supervises~grandAdvisor 0.3285 · advises~advises 1.0000 · advises~advises 1.0000를 거쳐 0.3285점을 받는데, 목표가 규칙의 머리와 소프트하게 일치하는 동안 몸체는 정확히 증명되며, min은 그 사슬의 유일한 약한 고리를 정확히 보고하고, 0.3285는 마땅히 기준선을 통과하지 못합니다. 이것이 표 하나에 담긴 소프트 단일화의 약속 전부입니다: 재귀적 증명 기계는 그대로 유지되고, 지식 베이스는 손대지 않은 채이며, 미지의 어휘로 된 질의가 수량화되고 귀속 가능한 확신도로 답해집니다.

데모 C: 대조군, 그리고 정직하게 읽는 임계값

advises 사실을 거쳐 supervises를 증명할 수 있는 방법이라면, 그것이 그 밖에 또 무엇을 증명해 낼지도 반드시 점검해야 합니다. 대조 질의는 cites(bob, Z)입니다: cites는 실제 술어(논문은 논문을 인용합니다)이지만, 그 벡터는 advises와 무관한 독립적인 무작위 방향이며, bob은 아무것도 인용하지 않습니다. 하드 증명기는 여기서도 아무것도 돌려주지 못할 텐데, cites(bob, ...) 형태의 사실이 전혀 없기 때문입니다. 커밋된 소프트 결과이며, 다시 전체를 보여드립니다:

Demo C — control: cites(bob, Z), a predicate that embeds far away
  Z         score  ≥τ   best proof (pred~pred kernel, MIN-composed)
  mit      0.4621  -    cites~affiliated 0.4621
  carol    0.3621  -    cites~advises 0.3621
  dave     0.3621  -    cites~advises 0.3621
  p1       0.2818  -    cites~authored 0.2818
  erin     0.2627  -    cites~grandAdvisor 0.2627 · advises~advises 1.0000 · advises~advises 1.0000
  logic    0.2627  -    cites~grandAdvisor 0.2627 · advises~authored 0.3555 · advises~about 0.4692
  ml       0.2627  -    cites~grandAdvisor 0.2627 · advises~advises 1.0000 · advises~grandAdvisor 0.2939 · +2 more
  … 4 more bindings, all ≤ 0.2627

$\tau = 0.8$ 에 도달하는 것은 아무것도 없고, 수락되는 것도 아무것도 없습니다; 소프트 일치는 환각을 일으키지 않았습니다. 하지만 이 모듈은 "일으키지 않았다"에서 멈추기를 거부하는데, 그 기하가 정확히 언제라면 일으켰을지를 보여주기 때문입니다. 출력된 실패-모드 메모:

  best soft proof: Z = mit at 0.4621 — under τ = 0.80, so NOTHING is
  accepted: soft matching does not hallucinate an unrelated predicate.
  failure-mode note: acceptance would leak as τ falls.  τ below
  0.4621 (= k(cites,affiliated)) admits mit; τ below k(cites,advises)
  = 0.3621 admits carol/dave through the advises facts.  The guard
  is the kernel margin: paraphrase 0.9783 vs unrelated-symbol noise ≤ 0.4621.

출력된 한계를 그 적용 범위와 함께 읽어 봅시다. "unrelated-symbol noise ≤ 0.4621"이라는 줄은 이 질의에 관한 진술입니다: 0.4621은 cites에서 출발하는 어떤 증명이든 도달할 수 있는 최고 점수인데, cites의 가장 강한 무작위 이웃이 마침 affiliated이기 때문입니다. 이것은 어휘 전체에서 가장 나쁜 충돌이 아닙니다; 데모 A가 이미 그 충돌을 보여주었으며, $k(\text{grandAdvisor}, \text{affiliated}) = 0.6806$ 으로, 28개 무작위 쌍 전체에 걸친 최댓값입니다. 증명은 min으로 합성되므로, 단 하나의 무작위 쌍 일치에라도 기대는 어떤 증명도 많아야 0.6806점을 받을 수 있는 반면, 세 데모의 모든 의도된 답은 0.9783점이나 1.0000점을 받습니다. 따라서 $\tau = 0.8$ 을 실제로 지켜 주는 마진은 0.6806에서 0.9783까지의 간극이며: 전자보다는 위이고 후자보다는 위가 아닌 어떤 $\tau$ 든 이 어휘 안의 모든 무작위 충돌을 거부하면서 모든 의도된 답을 수락하고, 0.8은 그 구간 안에 자리 잡고 있는데, 반올림된 숫자가 암시하는 것보다 충돌 쪽에 더 가깝습니다. 이 대조군만을 기준으로 조정된 임계값은 속임수가 될 것입니다: $\tau = 0.6$ 은 데모 C를 흠 없이 유지해 주지만, 데모 A의 질의에서는 0.6806인 가짜 mit을 받아들이고 맙니다. 대조군 자신의 체제를 그것이 설명하는 조절 나사로서 표에 늘어놓아 봅시다:

임계값 설정	`cites(bob, Z)`에 대한 수락 집합	해석
$\tau \gt 0.4621$	없음	데모의 체제: 대조군이 깨끗하게 유지됩니다
$0.3621 \lt \tau \le 0.4621$	`mit`	충돌 `cites~affiliated`(0.4621)가 새어 들어옵니다
$0.2818 \lt \tau \le 0.3621$	`mit`, `carol`, `dave`	잡음 바닥 자체(0.3621인 `cites~advises`)가 무언가를 증명하기 시작합니다; 0.2818 이하에서는 `p1`(`cites~authored`를 거쳐)과 나머지 꼬리가 뒤따릅니다

분명히 말해 둡시다: 이 데모에서 소프트 단일화의 안전성은 보장이 아니라 수치적 마진입니다. 바꿔 말한 답은 0.9783점을, 가장 나쁜 무작위 충돌은 0.6806점을 받습니다; $\tau = 0.8$ 은 여기서 그 둘을 갈라놓지만, 깨끗한 대조군 표가 암시하는 것보다 남는 여유는 더 적습니다. 그리고 이 마진은 아홉 개 술어로 이루어진 이 어휘를 지닌 이 시드 고정 기하의 속성입니다. 어휘를 키우면 수많은 무작위 내적들의 최댓값도 함께 커지고, 훈련이 벡터를 움직이게 두면 마진도 함께 움직이는데, 그 어떤 정리도 통제하지 못하는 방향으로 움직입니다. 이 모듈의 능력 단언(soft_unification.py 275–287행)은 세 데모 모두를 고정합니다: A는 정확히 {carol, dave}를 1.0으로 수락하고, B는 하드 증명기가 아무것도 돌려주지 못하는 동안 정확히 {carol, dave}를 0.8 이상으로 수락하며, C의 최선의 증명은 0.5 이하에 머무릅니다. 실행이 끝날 때 나오는 한 줄짜리 요약은 데모들의 대표 숫자들을 모아 놓습니다:

SUMMARY soft_unification: A_answers=2 A_score=1.0000 B_answers=2 B_score=0.9783 k_supervises_advises=0.9783 C_best=0.4621 k_cites_advises=0.3621 hard_B=0 tau=0.80

그리고 세 데모를 한눈에 보면:

데모	질의	하드 증명기	소프트 증명기, $\tau = 0.8$ 에서 수락됨	최선 점수	판정
A (정확)	`grandAdvisor(alice, Z)`	carol, dave	carol, dave	1.0000	소프트가 하드를 정확히 재현함
B (바꿔 말함)	`supervises(bob, Z)`	없음	carol, dave	0.9783	하드가 못하는 곳에서 소프트가 증명함
C (대조군)	`cites(bob, Z)`	없음(그런 사실이 없음)	없음	0.4621	측정된 마진만큼 누출이 없음

데모에서 연구 분야로: 증명 성공으로부터 임베딩 학습하기

지금까지는 모두 고정된 임베딩을 사용했습니다. 소프트 단일화를 하나의 연구 분야로 만든 계기는 커널이 미분 가능하다는 사실에 있으며, 그래서 임베딩은 증명 성공으로부터 학습될 수 있습니다[2]: 참으로 알려진 질의의 최선 증명 점수는 1을 향해 밀어붙이고, 거짓으로 알려진 질의의 점수는 0을 향해 밀어붙일 대상으로 취급하여, 기호 벡터 그 자체에 대해 1권의 경사 하강법을 실행하는 것입니다. 그래디언트는 유도해 볼 가치가 있는데, 그 형태가 훈련의 동역학을 설명해 주기 때문입니다. $\mathbf{u}_q$ 를 고정하고 $\mathbf{u}_p$ 의 $i$ 번째 좌표에 대해 $k$ 를 미분해 봅시다. $\boldsymbol{\delta} = \mathbf{u}_p - \mathbf{u}_q$ 와 $s = \lVert\boldsymbol{\delta}\rVert^2 = \sum_j \delta_j^2$ 라고 하면, 먼저

\frac{\partial s}{\partial u_{p,i}} \;=\; \frac{\partial}{\partial u_{p,i}} \sum_j \big(u_{p,j} - u_{q,j}\big)^2 \;=\; 2\big(u_{p,i} - u_{q,i}\big) \;=\; 2\,\delta_i,

합 안에서 오직 $j = i$ 인 항만이 $u_{p,i}$ 에 의존하고, 그 안쪽 도함수가 1이기 때문입니다. 그런 다음 $k = \exp(-s/2\sigma^2)$ 에 연쇄 법칙을 적용하면:

\frac{\partial k}{\partial u_{p,i}} \;=\; \exp\!\left(-\frac{s}{2\sigma^2}\right)\cdot\left(-\frac{1}{2\sigma^2}\right)\cdot 2\,\delta_i \;=\; -\,\frac{k}{\sigma^2}\,\delta_i, \qquad\text{so}\qquad \nabla_{\mathbf{u}_p}\, k \;=\; \frac{k}{\sigma^2}\,\big(\mathbf{u}_q - \mathbf{u}_p\big).

여기서 $\nabla_{\mathbf{u}_p} k$ ("나블라"라고 읽으며, $\mathbf{u}_p$ 에 대한 $k$ 의 그래디언트입니다)는 $D$ 개의 편도함수 $\partial k / \partial u_{p,i}$ 를 하나의 방향으로 모아 놓은 벡터입니다; $\delta_i = u_{p,i} - u_{q,i}$ 이므로, $D$ 개의 성분 $-(k/\sigma^2)\,\delta_i$ 는 $(k/\sigma^2)(\mathbf{u}_q - \mathbf{u}_p)$ 로 조립됩니다. $k$ 에 대한 경사 상승은 $\mathbf{u}_p$ 를 $\mathbf{u}_q$ 쪽으로 곧장 끌어당기는데, 그 세기는 $k$ 에 남은 거리를 곱한 것에 비례합니다: 근사한 실패는 강한 인력을 느끼는 반면, 멀리 떨어진 기호( $k \approx 0$ )는 거의 아무런 인력도 느끼지 않으므로, 훈련은 어휘 전체를 한 점으로 무너뜨리는 대신 그럴듯한 근사 동의어들을 다듬어 나갑니다. 합성 또한 그래디언트를 그만큼 선택적으로 보냅니다. $\min(a, b)$ 의 서브그래디언트(subgradient), 즉 두 인자가 같아지는 꺾인 지점에서의 도함수를 일반화한 것(같지 않을 때는 그냥 보통의 도함수입니다)은, 더 작은 인자에 대해서는 1이고 더 큰 인자에 대해서는 0입니다; 대칭적으로 MAX는 오직 자신의 가장 큰 인자에게만 그래디언트를 전달합니다. 그래서 답의 점수를 통과하는 한 번의 역전파는 정확히 하나의 커널, 즉 최선 증명의 가장 약한 일치만을 건드립니다. 지도 신호는 정확히 결론을 제한했던 그 고리 위에 내려앉습니다.

이러한 우아함에 따라오는 대가는 열거(enumeration)입니다. 위의 연쇄기는 모든 목표에서 모든 사실과 모든 규칙을 시도하는데, 소프트 모드에서는 _pred_match가 임베딩된 기호에 대해 결코 None을 돌려주지 않기 때문입니다; 하드 단일화가 이름이 일치하는 소수의 후보로 가지치기했던 OR-분기가 매 단계마다 지식 베이스 전체가 되어 버리고, 증명 트리는 깊이에 따라 지수적으로 자라납니다. 학술 세계의 수십 개 사실 위에서는 이것이 눈에 띄지 않지만, 실제 지식 베이스에서는 치명적이며, 원조 NTP는 작은 벤치마크를 넘어서는 규모로는 확장될 수 없었습니다[2]. 그 뒤를 이은 연구 계보는 정확히 이 병목을 공략했습니다: 그리디 NTP(Greedy NTP, GNTP)는 각 목표의 사실 일치를 임베딩 공간에서의 최근접 이웃으로 제한하여 몇 자릿수의 규모를 회복하고, 큰 지식 베이스와 자연어 코퍼스에까지 다다랐으며[3], 조건부 정리 증명기(Conditional Theorem Prover, CTP)는 주어진 목표에 대해 시도해 볼 가치가 있는 소수의 규칙만을 만들어 내는 규칙 선택 모듈을 학습하여, 맹목적인 열거를 학습된 추론 전략으로 대체합니다[4].

이제 어텐션 장이 마지막에 남긴 약속을 지킬 수 있습니다. 스케일된 내적 어텐션은 한 단계짜리 소프트 조회입니다: 쿼리 벡터가 모든 키를 채점하고, 소프트맥스가 그 일치들에 등급을 매기며, 가중된 값이 돌아옵니다; 변수도, 치환도, 재귀도 없는 단 한 번의 일치 라운드입니다. 소프트 단일화는 같은 행위의 구조화된 버전입니다: 일치 점수는 소프트맥스 가중치가 아니라 커널이고, 조회된 내용은 이후의 목표들을 관통해 이어지는 변수를 바인딩하며, 재귀는 t-노름으로 점수들을 합성해 감사 가능한 증명 경로를 만들어 냅니다. 어텐션은 소프트 조회이고, 소프트 단일화는 그 둘레에 논리를 감아 놓은 소프트 조회이며, 그 논리라는 감싸개가 바로 4권의 미분 가능한 추론 장들이 일반화하게 될 대상입니다.

아직 풀리지 않은 부분

하드 증명은 하나의 증명서(certificate)입니다: 1권의 건전성 정리는 증명기가 어떤 답을 도출해 낸다면 그 답은 지식 베이스의 모든 모델에서 참이라고 말하며, 2권은 그 보장 위에 추론 스택 전체를 다시 세웠습니다. 소프트 증명은 하나의 점수이며, 이 장의 그 어떤 정리도 점수를 진리와 연결해 주지 않습니다. 커널이 supervises를 advises로 흐려 놓으면, supervises(bob, carol)의 증명은 0.9783으로 "통과"하지만, 결론이 전제로부터 따라 나온다는 모델 이론적 의미는 전혀 없습니다; 지식 베이스는 supervises에 관해 아무것도 말하지 않으며, 숫자 0.9783은 함의가 아니라 구성된 두 벡터의 기하를 측정한 것입니다. 데모 C는 이 요점을 더욱 날카롭게 만들었습니다: "환각을 일으키지 않는다"와 "환각을 일으킨다" 사이의 차이는 이 방법의 의미론적 속성이 아니라, 어휘 전체에서 가장 나쁜 무작위 충돌인 0.6806이 손으로 정한 0.8 아래에 있고 0.9783은 그 위에 있다는 우연이었습니다. 커널 마진이 훈련 목적함수나 보정(calibration), 혹은 어휘 구조를 통해 보장에 걸맞은 신뢰성을 지닌 무언가로 공학적으로 설계될 수 있는지, 그리고 그 유래가 증명이 아니라 0.83이라는 숫자인 결론을 시스템이 어떻게 보고해야 하는지는, 이 권이 마무리 지을 수 없는 열린 질문들입니다. 이 권이 할 수 있는 일은 장부를 정직하게 결산하는 것이며, 그것이 바로 다음 장의 몫입니다.

왜 중요한가

소프트 단일화는 결론뿐 아니라 상징적 추론의 절차 그 자체가 벡터 공간으로의 번역에서 살아남는, 이 시리즈 최초의 구성물입니다: 목표는 규칙에 대해 축소되고, 치환은 바인딩되며, 증명 트리가 출력되지만, 그럼에도 파이프라인 전체는 훈련이 빚어낼 수 있는 미분 가능한 조각들로 지어져 있습니다. 이것이 바로 4권을 떠받치는 선례가 되는 이유인데, 4권의 통합들(의미론적 손실, 미분 가능한 질의 응답, 대규모 신경망 정리 증명)은 모두 그래디언트를 통과시키는 추론 단계를 필요로 하기 때문입니다. 이는 또한 이 시리즈가 그런 시스템을 감사할 때 사용할 어휘를 확정해 줍니다: 정확히 일치하는 경우는 반드시 점수 1로 되돌아와야 하고(데모 A), 일반화하는 경우는 반드시 식별 가능한 완화 하나로 귀속될 수 있어야 하며(데모 B의 커널 하나), 모든 수락 임계값은 반드시 그것을 지켜 주는 마진과 함께 보고되어야 합니다(대조군의 깨끗한 표만이 아니라 0.9783 대 0.6806의 간극). 이 장난감보다 덜 구체적으로 평가되는 신경망 증명기는 증거가 아니라 그럴듯함으로 채점받고 있는 것입니다.

핵심 용어

단일화(Unification): 1권의 일치 연산: 두 원자를 동일하게 만드는 치환을 찾거나, 그렇지 않으면 실패합니다; 이 장이 부드럽게 만드는 동등성 게이트입니다.
소프트 단일화(Soft unification): 기호-동등성 검사를 기호 임베딩에 대한 커널 점수로 대체하여, 근사 동의어는 어느 정도 일치하고 동일한 기호는 여전히 정확히 1점을 받게 하는 것입니다.
RBF 커널(RBF kernel): $k(p,q) = \exp(-\lVert\mathbf{u}_p-\mathbf{u}_q\rVert^2/2\sigma^2)$ ; 단위 벡터 위에서 $\sigma = 1$ 일 때 $e^{\cos\theta - 1}$ 과 같습니다.
폭 $\sigma$ (Width): 관용도 다이얼입니다: $\sigma \to 0$ 은 극한으로서 하드한 동등성을 회복하고, $\sigma \to \infty$ 는 모든 것을 일치시킵니다.
괴델 t-노름 / t-여노름(Gödel t-norm / t-conorm): min과 max입니다; 증명은 자신의 일치들의 MIN으로 점수가 매겨지고(가장 약한 고리), 답은 자신의 증명들에 걸친 MAX로 점수가 매겨집니다; 증명기 안에 들어온 2권의 ⟨min, max⟩ 확신도 대수입니다.
하드한 인자, 소프트한 술어(Hard arguments, soft predicates): NTP의 완전히 소프트한 일치보다 좁은, 이 모듈의 설계상 분리입니다: 어휘적 이름표는 흐려질 수 있지만, 개체를 가리키는 포인터는 흐려질 수 없습니다.
수락 임계값 $\tau$ (Acceptance threshold): 답이 도달해야 하는 점수(여기서는 0.8)입니다; 그 안전성은 바꿔 말한 점수와 가장 나쁜 무작위 충돌 점수 사이의 수치적 마진입니다.
신경망 정리 증명기(Neural Theorem Prover, NTP): 증명 성공을 미분 가능하게 만든 아키텍처로, 상수를 포함한 모든 비변수 기호를 임베딩하고, 커널로 점수가 매겨진 증명을 통해 역전파하여 임베딩을 학습합니다.
커널 마진(Kernel margin): 의도된 일치(0.9783)와 어휘 전체에서 가장 나쁜 무작위 충돌(0.6806, grandAdvisor~affiliated) 사이의 간극입니다; 대조 질의 자신의 잡음은 그보다 낮은 0.4621에서 정점을 찍습니다. 이 마진이 바로 환각적인 증명에 맞선 데모의 유일한 방어선입니다.

이 다음으로 이어지는 곳

V부가 완결되었습니다: 어텐션은 벡터에게 미분 가능한 어디를 볼 것인가를 주었고, 벡터 기호 구조는 무엇이 무엇과 어울리는가를, 그리고 이 장은 어떻게 증명할 것인가를 주었으며, 각각의 힘과 대가는 같은 작은 세계 위에서 측정되었습니다. 이제 남은 것은 결산입니다. 다음 장인 솔직한 평결은 이 권의 장부를 결산합니다: 임베딩의 기하가 진정으로 지니고 있는 것(유사도, 위계, 합성, 조회, 심지어 점수로 매겨진 증명 모양의 추론까지), 오직 기호만이 보장하는 것(건전성, 완전성, 정밀한 검토를 견뎌 내는 증명서), 그리고 그 경계선 위 어디에 4권의 신경-기호 통합이 지어져야 하는지입니다.

동반 코드: examples/neural/soft_unification.py는 커널, 점수를 꿰어 넣은 후방 연쇄기, 그리고 하나의 시드 고정 생성기로부터 나오는 세 데모 모두를 구현하며, examples/logic/에서 1권의 사실과 치환 기계를 변경 없이 그대로 가져와 임포트합니다. 이 장의 모든 숫자를 재현하려면 examples/neural/에서 python3 soft_unification.py를 실행하십시오; 수락 하니스 examples/neural/validate.py는 이 권의 평결의 일부로서 그 능력 단언들(정확한 연쇄는 1.0, 하드 증명기가 비어 있는 동안 소프트 회복은 0.8 이상, 대조군은 0.5 이하)을 다시 실행합니다.

이 장에서 다루는 내용​

다시 떠올리는 경첩: 정확히 일치하거나 실패하거나​

벡터가 된 기호: 커널이 일치도를 매기다​

시드로 고정된 기하, 측정하다​

증명의 대수: 경로를 따라서는 MIN, 증명들에 걸쳐서는 MAX​

하드한 인자, 소프트한 술어​

연쇄기: 1권의 기계 장치를 관통하는 점수​

데모 A: 정확한 연쇄, 1.0000으로 재현되다​

데모 B: 사실이 하나도 없는 술어로 증명하기​

데모 C: 대조군, 그리고 정직하게 읽는 임계값​

데모에서 연구 분야로: 증명 성공으로부터 임베딩 학습하기​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 다음으로 이어지는 곳​