기호 어텐션: 단 한 번의 섬광 같은 추론

📍 현재 위치: VII부 · SATORI 캡스톤 — 18장. 함의 벤치마크의 공백은 벤치마크가 실제 함의를 얼마나 드물게 강제하는지 측정함으로써 VI부를 마무리했습니다; 이제 VII부는 이 시리즈 전체가 한 권씩 조립해 온 바로 그 연산자를 짓고, 그것을 앞선 열일곱 개 장이 세운 기준에 붙들어 맵니다.

이 시리즈의 모든 권은 전체에 이름을 붙이지 않은 채 기계의 절반씩을 지어 왔습니다. 2권은 파동을 이루어 발동하는 규칙들을 공급했고, 3권은 대안들을 저울질하는 미분 가능한 방법인 어텐션을 공급했으며, 4권은 대안을 저울질하는 것이 곧 논리가 되는 의미론을 공급했습니다. 이 장은 그 부품들을 볼트로 조여 기호 어텐션(symbolic attention)으로 만듭니다: 전체 상태가 정도(degree)들의 행렬이고, 단일 층이 모든 완성 규칙을 세 종류의 어텐션으로서 동시에 발동시키며, 그 네트워크는 가중치가 공유되어 펼쳐진, 정지 검사도 발동 일정도 없는 그 한 층의 고정된 스택인 추론기입니다. 이 구성이 여기서 멈춘다면 하나의 비유에 그쳤을 것입니다. 그러나 멈추지 않습니다. 컴패니언 모듈 examples/frontier/satori_lite.py는 단언(assert) 하나하나로 이 주장의 각 절을 벌어들입니다: 결정적 극한은 1권의 원자 47개짜리 혼(Horn) 폐쇄와 2권의 EL 분류를 정확히 복원하며, 이는 두 오라클 모두에 대한 집합 동등성으로 확인됩니다; 재현율-대-깊이 표는 모든 깊이에서 건전성이 검사된 채로 IV부의 절단 법칙을 재현합니다; 그리고 도출된 원자 하나하나의 배후에 있는 어텐션 흔적은 증명 검사기가 규칙 적용 하나하나까지 검증하는 도출로 다시 지어집니다. 이 장의 책무는 처음부터 밝혀 둡니다: 이 융합을 정확하게 만들고, 검사 가능하게 만들고, 정직하게 값을 매기는 것입니다.

쉽게 말하면

거대한 스프레드시트를 하나 상상해 보십시오. 모든 칸에는 0과 1 사이의 숫자가 들어 있어 어떤 사실이 얼마나 강하게 믿어지는지를 말해 주고, 모든 칸은 똑같은 수식을 가지고 있습니다: 바로 앞 틱(tick)에서 다른 칸들이 뭐라고 말했는지를 살펴보고, 내 규칙이 필요로 하는 칸들을 (대략 가장 약한 것을 취해) 결합한 다음, 여러 규칙이 나를 제안한다면 (대략 가장 강한 제안을) 지키는 것입니다. 이제 "다시 계산하기"를 정확히 세 번 누르십시오. 어떤 칸도 다른 칸을 기다리지 않습니다: 시트 전체가 록스텝(lockstep)으로 갱신되며, 세 틱 뒤에는 시트가 그 규칙들이 결론 내릴 수 있었던 모든 것을 담고 있는데, 이는 이 세계에서 어떤 결론도 조상의 사슬이 세 단계를 넘어설 필요가 없기 때문입니다. 더 좋은 것은, 모든 칸이 자신이 어떤 칸들을 읽었는지를 조용히 적어 두었으므로, 어떤 결론이든 원래의 항목까지 거슬러 감사할 수 있다는 것입니다. 기호 어텐션이 바로 그 스프레드시트입니다: 수식은 완성 규칙이고, "대략 가장 약한 것/대략 가장 강한 것"이라는 다이얼은 어텐션의 온도이며, 세 번의 틱은 네트워크의 층들이고, 감사 열은 기계로 검사 가능한 증명입니다.

이 장에서 다루는 것

수렴: 2권, 3권, 4권이 각각 무엇을 기여했는지, 그리고 융합 주장을 평이하게 진술합니다: 완성 규칙을 괴델 정도 위의 어텐션으로 표현하는 것입니다.
연산자 이전의 상태: 소프트 레이블 행렬 $S$ 와 역할별 소프트 인접 행렬 $R_r$ , 여기서 "소프트"가 무슨 뜻인지(확률이 아니라 괴델 정도), 그리고 모든 것을 붙들어 매는 결정적(crisp) 특수 사례를 다룹니다.
한 층, 세 가지 어텐션: 전제에 대한 온도-제어 소프트민(softmin)으로서의 논리곱, 규칙에 대한 소프트맥스로서의 도출 간 경쟁, 소프트 엣지 위의 메시지 전달로서의 역할 합성을 다루며, 각 수식은 유도된 다음 커밋된 코드에서 그대로 인용됩니다.
록스텝이 정당한 이유: 완성 연산자의 단조성 덕분에 발동 순서가 무관해져서, 모든 규칙이 어떤 일정도 수렴 검사도 없이 매 층마다 발동할 수 있으며, 그 대가는 지름 아래에서의 완전성으로 명시됩니다.
결정적 복원, 두 오라클 모두: 온도가 0에 가까울 때 커널의 문턱 처리된 상태는 1권의 전방 연쇄 폐쇄 및 2권의 EL 분류와 정확히 같으며, 두 단언 모두 커밋되어 있습니다.
절단 법칙과 흔적: 재현율은 깊이에 따라 오르며 학계 세계의 도출 지름인 $L = 3$ 에서 정확히 완전해지고, 모든 깊이에서 건전성이 단언됩니다; 그리고 기록된 아그맥스(argmax) 부모들은 검사기가 단계별로 검증하는 grandAdvisor(alice, carol)의 도출을 재구성합니다.
정직한 섬광: PTIME-완전(다항 시간 완전) 핵심 위에서 "단 한 번의 섬광"이란 깊이-영 통찰이 아니라, $L$ 을 미리 골라 둔 경계-깊이 현저성을 뜻합니다.

수렴, 이 시리즈 자신의 이야기로 말하다

2권은 규칙을 기여했습니다. 완성 규칙 장은 모든 EL TBox를 한 줌의 정규형으로 환원하고, 몸체가 레이블과 엣지를 읽고 머리가 레이블과 엣지를 쓰는 포화 절차인 CR1부터 CR⊥까지에 역할-사슬 규칙(CRχ)을 더해 제공했으며, 이는 다항 시간이고 건전하며 완전합니다 [1]. 3권은 어텐션을 기여했습니다: 관련성으로 가중된 집계, 그리고 하드 아그맥스와 균일한 흐림 사이를 온도로 다이얼 조절하는 소프트맥스입니다 [2]; 이 장은 트랜스포머의 고정-깊이 층 스택을 빌려 오고 거기에 자신만의 규율 하나를 더합니다: 가중치를 묶어, 하나의 층을 반복하는 것이 네트워크 전체가 되게 하는 것입니다. 4권은 앞의 둘이 만날 수 있게 해 주는 의미론을 기여했습니다: 모든 원자에 $[0, 1]$ 안의 정도를 부여하고, 논리곱을 괴델 t-노름(최솟값)으로, 논리합을 괴델 t-코노름(최댓값)으로 읽으면, 그렇게 얻어지는 다치 논리는 어림짐작이 아니라, 그 결정적 파편이 고전 논리인 정리-보증 체계입니다 [3].

융합 주장은 이렇습니다: 완성 절차와 어텐션 스택은 같은 연산자입니다. 전제들에 대해 최솟값을 취하는 규칙 몸체는 온도를 낮춘 전제에 대한 어텐션이고; 같은 머리에 대한 경쟁하는 도출들을 최댓값으로 병합하는 것은 규칙에 대한 어텐션이며; 역할 엣지를 가로질러 레이블을 전파하는 것은 소프트 인접 행렬 위의 메시지 전달입니다. 이 융합의 조상뻘 버전은 반대 방향으로 달렸습니다: 미분 가능한 증명은 소프트 점수를 후방 연쇄(backward chaining)에 접목하여, 매 깊이마다 가지치기가 반복되는 증명 트리를 탐색했습니다 [4]. 기호 어텐션은 그 탐색을 포화로 대체합니다: 목표도 없고, 역추적도 없으며, 모든 규칙이 모든 곳에서 한꺼번에 발동하는데, 이것이야말로 고정된 병렬 스택을 가능하게 만드는 바로 그 움직임입니다. 원천 프로젝트의 이름인 SATORI(Symbolic ATtention Over Ontological Reasoning and Inference, 온톨로지 추론과 추리에 대한 기호적 어텐션)는 이 장의 제목을 진지하게 받아들이며, 이 장은 끝에서 물리학이 그것을 얼마나 진지하게 허락하는지로 되돌아올 것입니다.

상태: 추론기가 층들 사이에 간직하는 것

연산자가 손대기 전에 그 상태를 해독해 봅시다. 추론이 대상으로 삼는 것들인 노드(node)들의 유한 집합, 단항 술어 또는 개념 이름인 레이블 이름(label name)들의 유한 집합, 그리고 이항 술어인 역할 이름(role name)들의 유한 집합을 고정합니다. 노드의 개수를 $n$ 으로, 레이블의 개수를 $m$ 으로 씁니다. 추론기의 전체 상태는 다음과 같습니다:

소프트 레이블 행렬(soft label matrix) $S \in [0,1]^{n \times m}$ : 노드마다 한 행, 레이블마다 한 열이며, 그 항목 $S[x, A]$ 는 레이블 $A$ 가 노드 $x$ 에 대해 성립하는 정도(degree)입니다; 그리고
역할 $r$ 마다 하나씩인 소프트 인접 행렬(soft adjacency matrix) $R_r \in [0,1]^{n \times n}$ : $R_r[x, y]$ 는 엣지 $r(x, y)$ 가 성립하는 정도입니다.

여기서 $[0,1]^{n \times m}$ 은 각 항목이 0과 1 사이(양 끝 포함)인 $n$ 행 $m$ 열의 실수 격자들의 집합을 뜻하며, 기호 $\in$ 는 "~의 원소이다"라고 읽습니다: $S$ 는 그런 격자 중 하나입니다. "정도"는 확률이 아니라 4권이 부여한 뜻을 그대로 지닙니다 [3]. grandAdvisor(alice, carol)에 대한 정도 $0.7$ 은 "70%의 세계에서 참이다"라고 말하는 것이 아니며, 한 노드에 대한 $S$ 의 행은 합이 1이 되지 않습니다; 어디에도 정규화도 독립성 가정도 없습니다. 괴델식 독법 아래에서, 도출된 원자의 정도는 그 최선의 도출을 따라간 가장 약한 전제의 강도입니다: 논리곱은 최솟값을 취하고, 대안들은 최댓값을 취합니다. 그 독법은 이 장이 현금화할 두 가지 귀결을 지닙니다. 첫째, 결정적 특수 사례(crisp special case)는 진짜 특수 사례입니다: 모든 항목을 정확히 0 또는 1로 두면 최솟값과 최댓값의 대수는 불(Boolean) AND와 OR가 되므로, 소프트 커널이 정도 0/1에서 무엇을 하든 그것은 고전적 추론기와 일치해야 하며, 그렇지 않으면 커널이 틀린 것입니다. 둘째, 정도들은 확률의 장부 정리(세계도, 셈도) 없이 합성되는데, 이것이 바로 전체 상태가 두 개의 조밀한 배열 안에서 살 수 있게 해 주는 이유입니다.

컴패니언은 같은 실행 예제로부터 이 상태를 두 번 구체화하며, 이 이중 구체화가 바로 요점입니다. 혼(Horn) 얼굴(satori_lite.py, 163–185행)은 1권의 학계 세계를 취합니다: 3권의 정준적 개체 순서로 정렬된 13개 노드, 4개의 레이블(person, professor, researcher, student), 8개의 역할, 그리고 하드한 정도 1.0으로 입력된 kb.py의 23개 기본 사실입니다. EL 얼굴(188–223행)은 정규화를 거친 2권의 TBox를 취하는데, 여기서 $S$ 의 독법은 잠시 멈춰 볼 만한 방식으로 옮겨 갑니다: 노드가 곧 개념 이름이므로, $S$ 는 정사각형 $12 \times 12$ 행렬이고 $S[A, B]$ 는 포섭(subsumption) $A \sqsubseteq B$ 의 정도입니다. 그 초기화는 완성 알고리즘 자신의 것입니다: $S_0$ 는 대각선에 1.0을 가지며(모든 개념은 자기 자신을 포섭합니다) ⊤ 열에도 1.0을 가지고(모든 것은 ⊤에 포섭됩니다), 모든 $R_r$ 은 비어 있는 채로 시작하는데, 이는 정확히 EL 완성 오라클의 시작 상태인 $S(A) = \lbrace A, \top \rbrace$ , $R(r) = \emptyset$ 과 같습니다(el_completion.py, 186–188행).

두 얼굴 모두 하나의 다섯-모양 규칙 중간 표현(rule intermediate representation, IR)으로 컴파일되는데, 이는 kb.RULES와 정규화된 TBox로부터 모양 분석(shape analysis)으로 읽어 낸 것일 뿐 결코 다시 타이핑되지 않습니다(compile_horn, 131–160행; el_instance, 196–213행). 표에 앞서 두 가지를 해독해 둡시다. 고전적 독법 열에서 $\sqcap$ 은 개념들 사이의 "그리고"로, $\exists r.b$ 는 " $b$ 로 가는 $r$ -엣지를 가진다"로, $r \circ s$ 는 " $r$ 다음에 $s$ "로, $\bot$ 은 바닥(bottom), 곧 아무것도 만족할 수 없는 개념으로 읽으십시오. 소프트 갱신 열에서 $\mathrm{softmin}_\tau$ 와 $\mathrm{softmax}_\tau$ 는 최솟값과 최댓값을 온도로 매끄럽게 만든 것으로 다음 절에서 정의되고 유도되며, 아래 첨자 $\tau$ 는 3권의 어텐션에서 이어받은 날카로움 다이얼이고, $k$ 는 결합되는 값들의 개수를 셉니다:

IR 모양	고전적 독법	매 층마다 발동하는 소프트 갱신
`("cr1", (A₁..A_k), B)`	$A_1 \sqcap \cdots \sqcap A_k \sqsubseteq B$ , 또는 하나의 단항 혼 규칙	$S[x,B] \mathrel{\oplus}= \mathrm{softmin}_\tau\big(S[x,A_1], \ldots, S[x,A_k]\big)$
`("cr2", A, r, b)`	$A \sqsubseteq \exists r.b$	$R_r[x,b] \mathrel{\oplus}= S[x,A]$
`("cr3", r, A, B)`	$\exists r.A \sqsubseteq B$	$S[x,B] \mathrel{\oplus}= \mathrm{softmax}_y\, \mathrm{softmin}\big(R_r[x,y],\, S[y,A]\big)$
`("chain", r, s, t, …)`	$r \circ s \sqsubseteq t$ , 또는 두-원자 혼 사슬	$R_t[x,z] \mathrel{\oplus}= \mathrm{softmax}_y\, \mathrm{softmin}\big(R_r[x,y],\, R_s[y,z]\big)$
`("copy", r, s)`	$r \sqsubseteq s$ , 또는 하나의 단일-원자 혼 규칙	$R_s \mathrel{\oplus}= R_r$

기호 $\mathrel{\oplus}=$ 는 "소프트 논리합으로 누산기에 병합한다"라고 읽습니다: 새로운 기여분은 그 칸이 이미 지니고 있는 정도와 경쟁하고, 둘의 소프트맥스가 살아남습니다. 충돌 규칙 CR⊥은 자신만의 모양이 필요 없습니다; 이는 $A = B = \bot$ 인 CR3이며, 역할마다 하나의 인스턴스를 가집니다(213행). 커밋된 실행은 그 집계를 보고합니다: 혼 얼굴은 7개의 IR 규칙으로, EL 얼굴은 19개(CR1 8개, CR2 3개, CR3 7개 중 3개는 CR⊥, 사슬 1개)로 컴파일되며, 출력물은 혼 규칙을 하나하나 나열하고 EL 얼굴의 집계는 모양별로 보고합니다.

하나의 연산자를, 단 한 번 그리다: 소프트 상태(왼쪽)는 모든 완성 규칙을 세 종류의 어텐션으로서 발동시키는 단일 층에 의해 변환되고(가운데), 가중치가 공유된 세 개의 사본으로 이루어진 고정 깊이로 펼쳐지는데, 그 결정적 극한은 두 고전적 오라클 모두와 일치하고 그 흔적은 기계로 검사 가능한 증명이다(오른쪽). 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

한 층, 세 가지 어텐션

이 층은 정확히 두 개의 스칼라 연산자만을 필요로 하며, 둘 다 4권의 괴델 쌍을 매끄럽게 만든 것입니다. 온도(temperature) $\tau$ 는 양의 실수로, 3권의 어텐션 장이 소프트맥스에 부여했던 것과 똑같은 날카로움 다이얼입니다 [2]: $\tau$ 가 작으면 매끄러운 연산자가 하드한 연산자에 바짝 달라붙고, $\tau$ 가 크면 평균 쪽으로 흐려집니다. 결합할 값의 개수를 $k$ 라 하고, 정도들의 목록 $v = (v_1, \ldots, v_k)$ ( $x$ 는 이미 노드의 이름이므로 새 글자를 씁니다)에 대해 다음과 같이 정의합니다:

\mathrm{softmin}_\tau(v) \;=\; -\tau \,\ln \sum_{i=1}^{k} e^{-v_i/\tau}, \qquad \mathrm{softmax}_\tau(v) \;=\; +\tau \,\ln \sum_{i=1}^{k} e^{+v_i/\tau},

여기서 $\ln$ 은 자연로그이고 $e^{v_i/\tau}$ 는 온도로 나눈 정도에 지수 함수를 적용한 것입니다. 이들은 최솟값과 최댓값을 로그-합-지수(log-sum-exp)로 매끄럽게 만든 것입니다. 이들에 관한 두 가지 사실이 모든 일을 해내며, 둘 다 유도를 받을 자격이 있습니다.

사실 1: 각 연산자는 자신의 하드한 짝과 $\tau \ln k$ 만큼의 틈을 두고 조여집니다. 소프트민을 취하고, 가장 작은 항목을 $\mu = \min_i v_i$ 라고 씁시다. 합의 모든 항은 $e^{-v_i/\tau} \le e^{-\mu/\tau}$ 를 만족하는데, 이는 $v_i \ge \mu$ 이고 사상 $t \mapsto e^{-t/\tau}$ 가 감소 함수이기 때문입니다; 그리고 최솟값을 주는 항 자체는 정확히 $e^{-\mu/\tau}$ 와 같습니다. 따라서 $k$ 개 항을 합하면 그 합은 가장 큰 항의 한 배와 $k$ 배 사이에 고정됩니다:

e^{-\mu/\tau} \;\le\; \sum_{i=1}^{k} e^{-v_i/\tau} \;\le\; k\, e^{-\mu/\tau}.

로그는 증가 함수이므로 $\ln$ 을 취해도 두 부등식 모두 보존됩니다: $-\mu/\tau \le \ln \sum_i e^{-v_i/\tau} \le \ln k - \mu/\tau$ . 음수인 $-\tau$ 를 양변에 곱하면 두 부등식의 방향이 모두 뒤집히며, 다음을 얻습니다:

\mu - \tau \ln k \;\le\; \mathrm{softmin}_\tau(v) \;\le\; \mu.

매끄러운 논리곱은 참된 최솟값을 결코 넘어서지 않으며, 많아야 $\tau \ln k$ 만큼만 그 아래로 못 미칩니다. $\tau \to 0$ 이 되면 그 틈 $\tau \ln k$ 는 사라지고 조임은 $\mathrm{softmin}_\tau \to \min$ 을 강제합니다; 거울상 논증(또는 정의에 $-v$ 를 대입하고 바깥의 음의 부호를 분배하면 얻어지는 쌍대성 $\mathrm{softmax}_\tau(v) = -\,\mathrm{softmin}_\tau(-v)$ )은 $\max \le \mathrm{softmax}_\tau \le \max + \tau \ln k$ 를 줍니다. 이것이 "결정적 극한"이 뜻하는 전부입니다: 이 장 뒤에 나오는 모든 복원 주장은 $\tau \to 0$ 진술이며, 이 조임에 의해 허가됩니다.

사실 2: 각 매끄러운 연산자의 도함수는 하나의 어텐션 분포입니다. 로그와 지수를 관통하는 연쇄 법칙으로, 하나의 입력 $v_i$ 에 대해 $\mathrm{softmax}_\tau$ 를 미분합니다:

\frac{\partial\, \mathrm{softmax}_\tau(v)}{\partial v_i} \;=\; \tau \cdot \frac{1}{\sum_j e^{v_j/\tau}} \cdot e^{v_i/\tau} \cdot \frac{1}{\tau} \;=\; \frac{e^{v_i/\tau}}{\sum_j e^{v_j/\tau}},

이는 정확히 3권의 정규화된 소프트맥스 가중치 벡터, 즉 $k$ 개의 대안에 대한 어텐션 분포입니다 [2]; 소프트민에 대해 같은 계산을 하면 가장 작은 입력들에 기대는 $-v/\tau$ 의 어텐션 가중치가 나오는데, 이는 4권의 컴패니언이 논리곱 그래디언트를 계산했던 방식과 같습니다(fuzzy_grad.py, 127–134행). 그러므로 "기호 어텐션"이라는 말장난은 장식이 아닙니다. 그래디언트가 이 커널을 관통해 흐를 때, 공(功)은 전제들과 경쟁하는 도출들에 걸쳐 문자 그대로의 어텐션 가중치로 분배됩니다; 순전파는 하나의 논리를 계산하고, 역전파는 그 논리에 대한 어텐션을 계산합니다.

커밋된 구현들은 각각 네 줄이며, 표준적인 시프트(합으로부터 인자 $e^{-\mu/\tau}$ 를 빼내어 어떤 지수도 양수가 되지 않게 하는 것)로 수치적으로 안정화되어 있고, run()은 이들이 4권의 스칼라 fuzzy_grad.softmin과 $10^{-12}$ 까지 일치하고 쌍대성을 만족함을 단언합니다(satori_lite.py, 96–107행 및 435–438행):

def smin(x: np.ndarray, tau: float, axis: int = 0) -> np.ndarray:
    """softmin_τ along ``axis``:  m - τ·log Σ exp(-(x-m)/τ),  m = min."""
    m = np.min(x, axis=axis)
    return m - tau * np.log(np.sum(np.exp(-(x - np.expand_dims(m, axis)) / tau),
                                   axis=axis))

이제 층 자체를 봅시다. soft_layer(228–258행)는 오직 이전 상태 $(S^{(k-1)}, R^{(k-1)})$ 만을 읽고, 모든 IR 규칙을 발동시키며, 각 기여분을 $\oplus$ 로 누산기에 병합합니다; 세 규칙 계열이 바로 이 장 제목의 세 가지 어텐션입니다.

전제에 대한 어텐션: 논리곱 몸체. 몸체 레이블 $A_1, \ldots, A_k$ 를 가진 CR1 규칙은 노드 $x$ 에서 자신의 몸체를 전제 정도들의 소프트민으로 채점한 다음, 이를 머리 열에 병합합니다(239–241행):

        if ru[0] == "cr1":      # S[x,B] ⊕= softmin_k S[x,A_k]
            c = smin(np.stack([Sp[:, li[a]] for a in ru[1]]), tau, axis=0)
            Sa[:, li[ru[2]]] = smax2(Sa[:, li[ru[2]]], c, tau)

몸체는 소프트하게, 가장 약한 전제만큼 강합니다; 온도는 "가장 약한"이 얼마나 관대한지를 조절합니다. 이 하나의 분기는 두 얼굴 모두를 실어 나릅니다: 1권의 professor(x) → researcher(x), 그리고 서로소 공리 Professor ⊓ Student ⊑ ⊥와 같은 2권의 정규형 논리곱들입니다 [1].

규칙에 대한 어텐션: ⊕-병합. 모든 분기는 같은 방식으로 끝납니다: smax2(accumulator, contribution, tau). 서로 다른 두 규칙, 또는 하나의 규칙의 서로 다른 두 인스턴스가 같은 머리 칸을 도출할 때, 그 정도들은 경쟁하고 소프트 최댓값이 살아남습니다. 이는 대안 도출들에 대한 논리합, 곧 4권의 괴델 t-코노름입니다 [3]. 그리고 이는 또한 정확히, 머리 하나의 도출들에 대한 소프트맥스, 즉 규칙들에 걸친 어텐션이기도 합니다.

목격자에 대한 어텐션: 메시지 전달. CR3 규칙 $\exists r.A \sqsubseteq B$ 는 각 노드 $x$ 에 대해 후보 목격자(witness) $y$ 전부를 훑어야 합니다: $x$ 에서의 결론은 가장 좋은 $y$ 만큼 강하고, 각 $y$ 의 제안은 엣지 정도 $R_r[x,y]$ 와 레이블 정도 $S[y,A]$ 중 더 약한 쪽만큼 강합니다(245–248행):

        elif ru[0] == "cr3":    # S[x,B] ⊕= softmax_y softmin(R_r[x,y], S[y,A])
            _, r, a, bl = ru
            c = smax(smin2(Rp[r], Sp[:, li[a]][None, :], tau), tau, axis=1)
            Sa[:, li[bl]] = smax2(Sa[:, li[bl]], c, tau)

이를 어텐션으로 읽으십시오: 행 $R_r[x, \cdot]$ 는 소프트 엣지 가중치들의 벡터이고, 열 $S[\cdot, A]$ 는 소프트 값들의 벡터이며, 소프트민이 이 둘을 짝짓고, $y$ 에 대한 소프트맥스가 집계합니다. "곱"이 최솟값인 괴델의 통화로 엣지 정도 곱하기 원천 레이블인 셈입니다. 역할 합성(chain, 249–255행)은 레이블 열 자리에 두 번째 인접 행렬을 넣은 같은 패스입니다, $R_t[x,z] \mathrel{\oplus}= \mathrm{softmax}_y\, \mathrm{softmin}(R_r[x,y], R_s[y,z])$ : 결정적 0/1 사례가 정확히 IV부가 GPU에서 돌렸던 불(boolean) 곱이 되는 괴델-세미링 행렬 곱이, 이제는 다섯 분기 중 하나가 된 것입니다. 엣지 방출(cr2, 242–244행)과 역할 포함(copy, 256–257행)은 전혀 집계가 필요 없습니다: 레이블 정도가 엣지 칸으로 흘러들거나, 엣지 행렬이 다른 엣지 행렬로 흘러들 뿐이며, 다른 모든 것과 마찬가지로 각각 ⊕-병합됩니다.

온도 다이얼, 커밋된 스윕으로 값매기다

결정적 주장들이 도착하기 전에, 커밋된 실험 하나가 $\tau$ 의 값을 매깁니다. 두 개의 기본 사실, advises(alice, bob)을 0.9로, advises(bob, carol)을 0.7로 등급 매기고, 다른 모든 정도는 1.0으로 남겨 둔 다음, $L = 3$ 개 층 뒤에 $R$ 에서 세 개의 grandAdvisor 정도를 읽습니다(annotation_demo, 409–424행). 괴델 의미론은 도출이 정확히 그 가장 약한 전제만큼 강하다고 말하므로, 참된 정도들은 (alice, carol)에 대해 $\min(0.9, 0.7) = 0.7$ , (alice, dave)에 대해 $\min(0.9, 1.0) = 0.9$ , 그리고 bob의 등급 매겨진 엣지를 거쳐 도출되는 (bob, erin)에 대해 $0.7$ 입니다. 커밋된 스윕은 다음과 같습니다:

[5] annotations: advises(alice,bob) graded 0.9, advises(bob,carol) 0.7; L = 3
      τ    gA(alice,carol)  gA(alice,dave)  gA(bob,erin)
  Gödel             0.7000          0.9000        0.7000   (min of premises)
   0.01            0.7110          0.9110        0.7110
   0.05            0.7540          0.9486        0.7548
   0.15            0.8406          1.0000        0.8563
   0.30            1.0000          1.0000        1.0000

$\tau = 0.01$ 에서 커널은 괴델 진리값으로부터 0.03 이내에 머무르며, 이는 단언되어 있습니다(499–505행); $\tau = 0.30$ 에 이르면 모든 정도가 1.0으로 포화되어 주석 의미론이 사라져 버립니다. 이 표류에는 유도 가능한 두 가지 원인이 있습니다. 첫째, 소프트 $\oplus$ 는 멱등적이지 않습니다: 한 정도 $v$ 를 자기 자신과 병합하면 $\mathrm{softmax}_\tau(v, v) = \tau \ln\!\big(e^{v/\tau} + e^{v/\tau}\big) = \tau \ln\!\big(2\,e^{v/\tau}\big) = v + \tau \ln 2$ 가 되므로, 매 층마다 다시 도출되는 원자는 층마다 최대 $\tau \ln 2$ 씩, 도합 $L\,\tau \ln 2$ 만큼 위로 기어오릅니다. 둘째, 목격자에 대한 소프트맥스는 제안이 0이지만 $e^{0/\tau} = 1$ 항은 여전히 합에 들어가는 12개의 죽은 후보 $y$ 로부터 유령 질량을 더합니다. 두 효과 모두 $\tau$ 에 비례해 커지는데, 이것이 바로 결정적 복원이 $\tau \to 0$ 진술일 수밖에 없는 이유입니다.

록스텝이 정당한 이유: 단조성이 순서-독립성을 사들이다

위의 층은 야코비 방식(Jacobi-style)으로, 어떤 의제도 규칙 순서도 수렴 검사도 없이 이전 상태로부터 모든 규칙을 발동시킵니다; 네트워크 unroll(315–332행)은 그저 그것을 $L$ 번 적용할 뿐입니다:

    S, R = inst["S0"].copy(), {r: M.copy() for r, M in inst["R0"].items()}
    ...
    for k in range(1, L + 1):
        S, R = soft_layer(S, R, inst, tau)

고전적 추론기는 규칙을 어떤 순서로든 발동시킬 권리를 하나의 정리로부터 얻어 내며, 그 정리는 1권의 고정점 교훈입니다. 즉시-귀결 연산자는 단조(monotone)입니다: 더 많이 도출된 사실이 어떤 규칙도 결코 무력화하지 않으므로(어떤 규칙 몸체도 부재를 언급하지 않습니다) 어떤 도출도 결코 철회되지 않으며, 유한 격자 위에서 단조롭고 팽창적인 연산자는 공정한 발동 순서라면 무엇이든 도달하는 최소 고정점을 가집니다; 순서는 경로를 바꿀 뿐 목적지를 결코 바꾸지 않습니다. 2권의 완성 절차도 같은 모양을 물려받았으며(el_completion.py의 while changed 루프, 211–259행은 CR1부터 CRχ까지를 고정된 순회로 발동시키는데, 이는 정확히 어떤 순회든 통하기 때문입니다), 산업용 EL 추론도 같은 규율 위에 서 있습니다: ELK의 포화는 공격적인 동시성 아래에서 완성 규칙을 고정점까지 발동시키며, 정확성은 뒤섞임(interleaving)에 손대이지 않는데, 바로 이것이 그것을 빠르게 만드는 이유입니다 [5]. 소프트 커널은 이 성질을 두 조각으로 나누어 들여옵니다. 한 층 내부의 순서-독립성은 대수로부터 나옵니다: 안쪽 병합을 지수화하면 그 부분합이 복원되어 $e^{\mathrm{smax}_\tau(a,b)/\tau} = e^{a/\tau} + e^{b/\tau}$ 이고, 따라서 $\mathrm{smax}_\tau\big(\mathrm{smax}_\tau(a,b),\, c\big) = \tau \ln\!\big(e^{a/\tau} + e^{b/\tau} + e^{c/\tau}\big)$ 입니다: 로그-합-지수는 결합적이고 교환적이므로, 어떤 순서로든 도출들을 둘씩 병합하는 것은 그것들 전부에 대한 하나의 합동 소프트맥스와 같습니다. 층을 가로지르는 팽창성은 읽은 뒤에 병합하는 데서 나옵니다: 사실 1의 하한에 의해 $\mathrm{smax}_\tau(\text{old}, c) \ge \max(\text{old}, c) \ge \text{old}$ 이므로, 어떤 칸도 결코 줄어들지 않으며, 커밋된 실행은 결정적이라 하기 어려운 $\tau = 0.15$ 에서, 층 세 개 깊이로, 정확히 이것을 단언합니다(491–497행).

바로 이것이 고정- $L$ , 가중치-공유, 정지 검사 없는 스택을 안전하게 지을 수 있게 해 주는 것입니다. 모든 곳에서 모든 것을 발동시키는 것이 지나칠 수 없고(건전성은 순서에 대해 증명되어 있습니다) 후퇴할 수도 없으므로(상태는 오직 자라기만 합니다), 걸려 있는 유일한 양은 상태가 고정점을 향해 얼마나 멀리 올라갔는가이며, 이는 오직 깊이만으로 지배됩니다. 무엇이 포기되는지도 같은 숨결로 말해 둡시다: while 루프는 수렴을 검사하며 언제나 그 오름을 끝마칩니다; $L$ 개 층의 고정된 스택은 고정점이 도착했든 아니든 $L$ 번의 파동에서 멈추므로, $L$ 이 지식 베이스가 요구하는 가장 깊은 도출의 깊이인 지름(diameter) $D$ 보다 작을 때마다 완전성은 포기됩니다. 그 밖의 것은 아무것도 포기되지 않습니다. 이는 IV부의 절단 다이얼이 하나의 아키텍처로서 다시 나타난 것입니다.

오라클이 단언하다: 결정적 복원, 두 번

조상들을 그저 닮기만 한 캡스톤은 결과가 아니라 도해에 불과할 것입니다. 신뢰성 검사는 정확합니다: 소프트 커널을 결정적-복원 온도 $\tau = 10^{-3}$ 에서 하드한 0/1 입력 위에 돌리고, 모든 칸을 0.5에서 문턱 처리하고, 임포트되었을 뿐 결코 다시 구현되지 않은 고전적 오라클들과의 집합 동등성을 요구합니다. 두 단언 모두 커밋되어 있습니다(run(), 448–460행):

    Sh, Rh, tr_h, sizes_h = unroll(horn, 3, TAU_CRISP, record_trace=True)
    assert atoms_of(Sh, Rh, horn) == closure and len(closure) == 47
    assert sizes_h == tp_sizes, "wave profile differs from T_P's"
    Se, Re, tr_e, _ = unroll(el, 3, TAU_CRISP, record_trace=True)
    assert atoms_of(Se, Re, el) == el_closure and len(el_closure) == 46

첫 번째 오라클은 1권의 전방 연쇄기입니다: least_fixpoint는 즉시-귀결 연산자 $T_P$ 를 아무것도 바뀌지 않을 때까지 반복하며(forward_chain.py, 52–63행), 학계 세계 위에서 23개의 기본 사실을 47개의 원자로 닫는데, 새 도출의 두 파동과 고정점을 확인해 주는 세 번째 파동이 있습니다. 커널의 문턱 처리된 상태는 그 폐쇄와 정확히 같으며, 그 이상입니다: 층별 원자 개수가 $T_P$ 의 파동 프로필 23 → 41 → 47 → 47을 단계마다 그대로 재현하는데, 파동 1에서 18개의 새 원자, 파동 2에서 6개, 파동 3에서는 없습니다. 두 번째 오라클은 2권의 EL 완성입니다. 커널의 포화된 상태는 오라클의 포화된 $S$ 와 $R$ (46개 원자)과 같으며, 하니스는 공정성에서 한 걸음 더 나아갑니다: 커널 자신의 문턱 처리된 상태를 오라클 자신의 보고 생성기인 elc.subsumptions와 elc.unsatisfiable에 건네주고, 그 분류가 일치함을 단언하는데, 이름 붙은 개념들 사이의 8개 포섭 관계와 2개의 충족 불가능한 개념 TenuredStudent, TenuredStudentAdvisor입니다(454–460행). 커밋된 출력물은 다음과 같으며, 그 이름표 "the C8 dry run"은 앞을 미리 읽은 것입니다: C8은 SATORI 주장 행렬이 자신의 결정적-건전성 주장에 부여한 번호이고, 주장 장이 그것을 온전히 채점합니다:

[2] crisp recovery at L = 3 (the C8 dry run) — exact, both oracles
  Horn: 47 atoms == the forward-chain closure; wave profile 23→41→47→47 == T_P's
  EL  : 46 atoms == el_completion's saturated S/R; 8 subsumptions,
        unsatisfiable = ['TenuredStudent', 'TenuredStudentAdvisor']

왜 두 오라클 모두를 고집할까요? 이 둘이 서로 다른 규칙 모양을 시험하기 때문입니다. 혼 얼굴은 전부 개체와 이항 구조입니다: 사슬, 자기 몸체에 스스로를 공급하는 이행적 폐쇄, 대각선-마스킹된 동료 규칙이며, CR2, CR3, ⊥에는 결코 손대지 않습니다. EL 얼굴은 전부 개념 이름과 존재적 구조입니다: 공리 $A \sqsubseteq \exists r.B$ 로부터의 엣지 방출, $\exists r.A \sqsubseteq B$ 를 위한 메시지 전달, 그리고 역할을 따라 거꾸로 충족 불가능성을 전파하는 충돌 규칙이며, 그 가장 깊은 도출은 정확히 혼 얼굴에 없는 종류입니다. 한쪽 얼굴을 복원하는 커널이라 해도 다른 쪽을 여전히 망칠 수 있습니다. 하나의 층과 하나의 IR로부터 두 얼굴 모두를 복원하는 것이야말로, 이 융합이 트렌치코트를 입은 두 개의 연산자가 아니라 하나의 연산자라는 증거입니다.

절단 법칙, 어텐션의 옷을 입고 다시 실행되다

IV부는 고정된 깊이 예산이 추론기에게 어떤 대가를 치르게 하는지 측정했습니다; 여기서는 같은 법칙이 네트워크 내부로부터 다시 떠오릅니다. 0부터 4까지의 모든 $L$ 에 대해 하니스는 스택을 펼치고, 원자들을 읽고, 두 가지를 검사합니다: 건전성, 즉 원자 집합이 모든 깊이에서 참된 폐쇄의 부분집합인가, 그리고 재현율, 즉 도출 가능하지만 주어지지 않은 원자들 가운데 실제로 도출된 비율(462–476행). 커밋된 표는 다음과 같습니다:

[3] the truncation law — sound at every L, complete iff L ≥ D = 3
      L   Horn atoms  recall    EL atoms  recall
      0           23   0.000         23   0.000
      1           41   0.750         32   0.391
      2           47   1.000         41   0.783
      3           47   1.000         46   1.000   ← D = 3: joint task complete
      4           47   1.000         46   1.000
  (the Horn face saturates at L = 2; the EL clash ⊥ ∈ S(TenuredStudentAdvisor)
   needs the third wave — truncation only ever loses recall, never soundness)

두 열을 서로 견주어 읽으십시오. 혼 얼굴은 $L = 2$ 에서 포화됩니다: 그 가장 긴 도출은 citesTransitively(p3, p1)로, 복사 단계 하나에 사슬 단계 하나를 더한 것입니다. EL 얼굴은 $L = 3$ 을 필요로 합니다: 충돌 ⊥ ∈ S(TenuredStudentAdvisor)는 세-파동짜리 도출입니다(파동 1은 Professor와 Student를 S(TenuredStudent)에 안착시키고 TenuredStudentAdvisor로부터 advises 엣지를 방출합니다; 파동 2는 그 엣지의 목표에서 서로소 논리곱 Professor ⊓ Student ⊑ ⊥를 발동시킵니다; 파동 3은 ⊥를 엣지를 가로질러 되돌려 보내는 CR⊥입니다), 그러므로 합동 과제는 학계 세계의 도출 지름인 $L = 3$ 에서 정확히 완전해지고, 고정점이란 일단 도달하면 고정되어 있으므로 $L = 4$ 에서도 완전한 채로 남습니다. 단언들은 표보다 더 날카롭습니다: 재현율은 두 얼굴 모두에서 $L$ 에 대해 단조적이며, 혼 얼굴은 2에서 이미 1.000에 도달하는 반면 EL 얼굴은 아직 1.000에 못 미친다고 단언되고(표에서는 0.783), 깊이 3은 둘 다를 닫습니다(473–476행).

이 권의 앞부분에서 나온 규율 하나를 여기서 다시 진술해야 하는데, VII부의 주장 장이 이에 기댈 것이기 때문입니다. 이 커널의 오류는 정확히 한 방향으로만 흐릅니다: $L \lt D$ 일 때 도출 가능한 사실을 놓칠 뿐 결코 도출 불가능한 사실을 단언하지 않으며, 건전하지만 불완전하고, 정밀도는 1.0이며 재현율은 표에 값매겨져 있습니다. 3권과 4권의 질의 임베딩은 정반대 방향으로 흘렀습니다: 기하는 일반화하므로, 박스나 베타 분포는 지식 베이스가 함의하지 않는 원자에도 기꺼이 점수를 매기며, 완전한 듯하지만 불건전하고, 재현율을 정밀도로 사들입니다. 이 둘을 함께 쌓는 실전 시스템(이 커널을 기반으로 삼고 그 위에 학습된 임베딩을 얹은)은 두 오류 방향 모두를 한꺼번에 물려받으며, 각 구성 요소가 어느 방향으로 오류를 내는지를 추적하지 않는 보정 이야기는 정직할 수 없습니다. 그것이 바로 이 장이 발행하고 SATORI 주장 장이 갚아야 할 어음(promissory note)입니다.

흔적은 일급 출력이지, 사후 합리화가 아니다

이 권의 I부는 결정 절차로부터 추출된 설명과 그것에 관해 재구성된 설명 사이에 굵은 선을 그었습니다: 정당화는 정리로 증명되었고, 충실성은 사후(post-hoc) 이야기가 메커니즘으로부터 자유롭게 떠다니기 때문에 정확히 삭제 실험으로 검사되어야 했습니다. 기호 어텐션은 I부의 교훈을 아키텍처화합니다: 커널은 추론하는 동안 자신의 어텐션을 기록하며, 그 기록이 곧 증명입니다. 결정적 극한에서, 층 $k$ 에서 처음 도출된 모든 원자는 흔적 항목 $(k, \text{규칙}, \text{부모})$ 를 얻는데, 여기서 부모는 발동된 도출의 아그맥스(argmax)입니다; $\tau \to 0$ 에서는 모든 결정적 도출이 정도 1에서 동점을 이루므로, 결정론적 동점 해소(고정된 규칙 순서, 그다음 정렬된 원자)가 곧 아그맥스입니다(crisp_step, 261–301행). 그 흔적은 이제 가장 까다로운 독자, 곧 증명 검사기에 의해 소비됩니다: check_proof(337–371행)는 기록된 원자 하나하나를 다시 도출하며, 그 규칙이 규칙 집합 안에 있는지, 부모들이 일관된 변수 바인딩 아래에서 그 규칙의 모양을 인스턴스화하는지, 가드가 성립하는지, 그리고 모든 전제가 엄격히 더 일찍 도출되었는지를 단언합니다. 두 얼굴에 걸친 47개의 도출된 원자 전부가 통과하며, 이는 단언되어 있습니다(478–489행). 커밋된 실행은 이 시리즈가 1권 이래로 줄곧 도출해 온 그 도출을 인쇄합니다:

[4] attention trace → machine-checked proofs (all 24 + 23 = 47 derived atoms pass)
  grandAdvisor(alice, carol)   [layer 1, CRχ: advises(x,y) ∧ advises(y,z) → grandAdvisor(x,z)]
      advises(alice, bob)   [base fact]
      advises(bob, carol)   [base fact]
  citesTransitively(p3, p1)   [layer 2, CRχ: cites(x,y) ∧ citesTransitively(y,z) → citesTransitively(x,z)]
      cites(p3, p2)   [base fact]
      citesTransitively(p2, p1)   [layer 1, copy: cites(x,y) → citesTransitively(x,y)]
          cites(p2, p1)   [base fact]
  proof depths: grandAdvisor(alice, carol) = 1, citesTransitively(p3, p1) = 2

이것이 어떤 종류의 대상인지 주목하십시오. VII부의 유물(어텐션 기록)이 I부의 기계 장치(규칙-인스턴스화 검사기)에 의해 검증되고 있으며, 그 검증은 유사도 점수가 아니라 모든 단계에 대한 이항 통과입니다. 이 권이 만나 온 두 가지 설명 체제를 대조해 봅시다. 블랙박스 모델에 대한 사후 귀인은 "어떤 입력을 교란시키면 답이 바뀌는가?"라고 묻고, 아무도 눈치채지 못한 채 불충실할 수 있습니다. 이 흔적은 그런 의미에서 불충실할 수가 없는데, 이는 그것이 계산에 관한 증언이 아니라, 검사기를 허용하는 언어(규칙 인스턴스화)로, 일어난 그대로 적어 둔 계산 그 자체이기 때문입니다. 그 설계 비용은 위쪽에서 이미 치러졌습니다: "아그맥스 부모"가 기록할 값으로서 애당초 잘 유형화된 것이 되려면, 커널의 상태가 고정된 뜻을 지닌 기호들(레이블 열, 역할 행렬)로 만들어져 있어야만 했습니다. 그 비용이 바로 II부 전체의 주제입니다: 내부 기호가 표류하는 학습된 모델은 정확히 이 성질을 잃으며, 이것이 바로 추론 지름길과 식별 가능성이 이 장과, 훈련된 SATORI가 그 보증을 물려받는다는 어떤 주장 사이에 놓이는 이유입니다.

단 한 번의 섬광, 정직하게

원천 프로젝트의 이름은 스스로를 하나의 비유에 붙들어 맵니다. SATORI는 갑작스러운 깨달음을 뜻하는 선불교 용어이며, 프로젝트 자체의 주석은 점수(漸修, 점진적 수행, gradual cultivation)와 대비되는 돈오(頓悟, 갑작스러운 깨달음, sudden enlightenment)를 내세웁니다: 미분 가능한 증명 계보가 물려받은 계산 방식인, 후방-연쇄 증명 탐색의 느리고 목표별로 기어가는 걸음걸이 대신, 추론을 하나의 현저성 섬광으로 보는 것입니다 [4]. 이 장은 이제 그 비유가 어느 정도의 값어치를 지니는지 진술할 만큼 충분히 지어졌으며, IV부는 이미 그 환율을 고정해 두었습니다. OWL 2 EL과 RL 프로파일의 완성 핵심은 PTIME-완전(다항 시간에 대해 완전)이며, 작업-깊이 트레이드오프는 그 귀결을 정확히 진술했습니다: NC(다항 개수의 프로세서로 다항로그 깊이에서 풀 수 있는 문제들의 부류)와 다항-시간 부류 P가 일치하지 않는 한(그렇게 믿어지지 않습니다) 그 고정점은 다항 총작업량을 갖는 어떤 상수-깊이 또는 다항로그-깊이 평가도, 곧 NC 안에서의 어떤 평가도 허용하지 않으며, 그 증명은 이 권의 범위를 훨씬 넘어서므로 컴패니언은 정리가 아니라 절단 표 안의 행동을 시연합니다. 그러므로 이 핵심 위에서, "단 한 번의 섬광"은 깊이-영 통찰을 뜻할 수가 없습니다. 그것이 정직하게 뜻하는 바는 경계-깊이 현저성(bounded-depth salience)입니다: 실제로 존재하는 모든 병렬성은 소진되고, 모든 규칙이 매 층 모든 곳에서 의제도 목표 스택도 없이 발동하며, 순차적 잔여물은 그 개수가 미리 골라지고 재현율이 커밋된 표에 의해 깊이마다 값매겨지는 $L$ 번의 록스텝 파동으로 압축됩니다. 깊이-영 추론은 존재하지만, 오직 이론이 그것을 허락하는 곳에서만 그렇습니다: 구체화 대 재작성이 상수-깊이 질의 재작성으로 실행했던 1차-재작성 가능한 파편들이 그것이며, 이 커널은 의도적으로 그 차선을 차지하지 않습니다. 느리고 신중한 시스템 2가 섬광 같은 시스템 1로 무너져 내린다는 이중-처리 로맨스는 수정된 형태로 살아남습니다: 그 섬광은 실재하지만, 그저 $L$ 프레임 길이일 뿐이며, 정직한 엔지니어는 $L$ 을 공표하고, $D$ 를 공표하며, 그 사이의 재현율 곡선을 공표합니다.

아직 풀리지 않은 부분

이 커널을 그것이 예시하는 시스템으로부터 갈라놓는 의도적인 부재가 둘 있으며, 둘 다 다음 장이 여는 문제입니다. 첫째, 이 커널의 "소프트 단일화"는 기존 기호들에 대한 정도-게이팅일 뿐입니다: advises에 대한 규칙은 오직 advises 행렬 위에서만, 그 칸들이 지닌 정도가 무엇이든 그 정도로만 발동할 수 있습니다. 이 커널은 규칙이 한 번도 주어진 적 없는 기호인 supervises가 거의 동일하게 행동하며 같은 추론을 받을 자격이 있다는 것을 알아챌 수 없습니다. 단지 비슷한 기호들을 맞추는 일은 이 융합의 진짜 신경망적 절반으로, 3권의 소프트 단일화로부터 4권의 미분 가능한 증명기들을 관통하는 계보입니다 [4]. 이는 임베딩 기반이 필요하기 때문에 이 장의 커널로부터 의도적으로 제외되어 있습니다: 기호들 사이의 유사성이 정의되기라도 하려면 기호들이 먼저 하나의 기하 안에 살아야 합니다. 그 기반, 그리고 그것이 다시 들여오는 정밀도 위험은 아키텍처 장에서 등장합니다. 둘째, 여기서 $\tau$ 는 스택 전체에 걸쳐 얼어붙은 단 하나의 전역 다이얼이며, 커밋된 스윕은 이 다이얼이 의미론 노브임을 보여 주었습니다: 0.01은 괴델 진리값을 0.03 이내로 보존하지만, 0.30은 그것을 완전히 파괴합니다. 실전 커널은 규칙마다 몸체가 엄격해야 하는 곳에서는 날카롭고, 긴 도출을 관통하는 그래디언트 흐름이 정확함보다 더 중요한 곳에서는 부드러운, 규칙별로 학습된 온도를 원합니다. 최적화기가 "모든 것을 1.0으로 흐리는 것"이 손실을 최소화하는 추론 지름길임을 발견하는 일 없이 규칙별 온도가 학습될 수 있는지는, 정확히 II부가 이 권에게 물으라고 가르쳤던 종류의 식별 가능성 질문이며, 아직 열려 있습니다.

왜 중요한가

이 시리즈에게 이 장은 서문이 약속했던 도착점입니다: 기호와 신경의 절반들이 서로 다른 권의 장으로 머무르기를 멈추고, 두 가지 독법을 가진 하나의 대상이 되는 지점입니다. 하중을 떠받치는 모든 부분은 앞서 지어졌고 재사용될 뿐 다시 발명되지 않습니다: 1권의 고정점 이론은 록스텝 스택을 허가하고, 2권의 완성 계산법은 규칙을 공급하며, 3권의 어텐션 대수는 연산자와 온도를 공급하고, 4권의 괴델 의미론은 그 연산자들을 하나의 논리로 만들며, 이 권의 I부부터 IV부까지의 신뢰 도구들은 그 커널이 그에 붙들려 있는 대상입니다: 오라클 동등성, 깊이별 건전성, 검사 가능한 흔적, 정직한 깊이 값입니다. 독자 자신의 연구를 위해, 이 장은 프론티어가 점점 더 요구하는 주장 방식의 실제 작동 템플릿입니다. 흥미로운 진술은 거의 결코 "우리는 X와 Y를 융합했다"가 아닙니다; 그것은 그 밑에 있는 장부입니다: 어떤 고전적 보증이 그 융합에서 살아남는지(여기서는 건전성), 어떤 것이 소비되고 계량되는지(재현율 표에 의한 완전성), 어떤 유물이 그 생존자들을 인증하는지(오라클에 대한 단언들, 흔적에 대한 증명 검사기), 그리고 부주의하게 학습되면 어떤 노브가 의미론을 깨뜨릴지( $\tau$ )입니다. 그 장부를 채워 넣는 융합 논문은 연구이며, 그렇지 않은 논문은 도해일 뿐입니다.

핵심 용어

기호 어텐션(symbolic attention): 완성 절차를 어텐션 연산자로 표현한 것입니다: 규칙 몸체는 전제들에 대한 소프트민으로 채점되고, 경쟁하는 도출들은 소프트맥스로 병합되며, 역할 합성은 소프트 인접 행렬 위의 메시지 전달로, 괴델 정도들의 상태 위에서 이루어집니다.
소프트 레이블 행렬 $S$ / 소프트 인접 행렬 $R_r$ : 추론기의 전체 상태입니다; $S[x, A]$ 는 레이블 $A$ 가 노드 $x$ 에 대해 성립하는 정도이고(TBox 얼굴에서는 포섭 $A \sqsubseteq B$ 의 정도), $R_r[x, y]$ 는 엣지 $r(x, y)$ 의 정도입니다.
괴델 정도(Gödel degree): 최솟값(논리곱)과 최댓값(논리합)으로 결합되는 $[0,1]$ 안의 진리값입니다; 확률이 아니며, 독립성이나 정규화 가정을 전혀 지니지 않습니다.
소프트민 $_\tau$ / 소프트맥스 $_\tau$ : 최솟값과 최댓값을 로그-합-지수로 매끄럽게 만든 것으로, 하드한 짝으로부터 $\tau \ln k$ 이내로 조여지며 $\tau \to 0$ 일 때 그것들로 수렴합니다; 그 도함수는 어텐션 분포입니다.
온도 $\tau$ : 3권의 어텐션과 공유되는 날카로움 다이얼입니다; 0 근처에서 커널은 고전적 추론기이며, 커밋된 스윕은 $\tau$ 가 커질수록 주석 의미론이 씻겨 나감을 보여줍니다.
록스텝(야코비) 발동: 모든 규칙이 어떤 일정도 없이 이전 상태로부터 동시에 발동합니다; 완성 연산자가 단조롭고 팽창적이어서 발동 순서가 고정점을 바꿀 수 없기 때문에 정당합니다.
고정- $L$ 가중치-공유 펼침: 정지 검사 없이 같은 층을 $L$ 번 적용하는 것입니다; 모든 $L$ 에서 건전하며, $L \ge D$ 일 때 정확히 완전합니다.
도출 지름 $D$ : 지식 베이스가 요구하는 가장 깊은 도출의 깊이입니다; 합동 학계-세계 과제에서는 $D = 3$ 이며, 이는 EL 충돌 도출에 의해 정해집니다.
어텐션 흔적: 순전파 동안 기록되는 원자별 기록(층, 규칙, 아그맥스 부모)입니다; 여기서는 기계로 검사되어 하나의 증명이 되는, 구성에 의한 충실성(faithfulness-by-construction) 성질입니다.
결정적 복원: 문턱 처리된 소프트 상태가 고전적 폐쇄와 같다는 $\tau \to 0$ 진술입니다; 1권과 2권의 오라클 모두에 대한 집합 동등성으로 단언됩니다.

다음으로 이어지는 곳

이 장은 모든 가중치를 1로 얼려 두었습니다: 규칙은 주어져 있었고, 라우터는 선택할 것이 아무것도 없었으며, 유일한 신경망적 유물은 매끄럽게 만드는 일 그 자체였습니다. SATORI 아키텍처는 그 설계를 풀어 줍니다: 소프트 단일화가 구문적으로는 결코 동일하지 않았던 것들을 맞출 수 있도록 기호들 아래에 놓인 임베딩 기반, 어떤 규칙이 어텐션을 받을 자격이 있는지 결정하는 학습된 라우터, 상태가 실제 온톨로지에서도 살아남도록 하는 역할별 희소 인접 행렬과 지역성 샤드, 그리고 이 장이 짓고 감사한 그 하나의 연산자 위에 걸려 있는 네 가지 주장된 성질(학습 가능한 라우팅, 충실한 흔적, 병렬 확장성, 보정된 확신)입니다. 커널은 그대로 남고, 그 주위의 모든 것이 훈련 가능해지며, 이 권의 모든 신뢰 도구가 훈련이 그 보증에 무슨 일을 하는지 검사하기 위해 함께 따라옵니다.

컴패니언 코드: examples/frontier/satori_lite.py는 소프트 괴델 연산자, 다섯-모양 규칙 IR, 록스텝 층, 고정- $L$ 펼침, 흔적 기록기, 증명 검사기를 구현하며, 1권의 forward_chain.py와 2권의 el_completion.py를 오라클로, 4권의 fuzzy_grad.py를 스칼라 대조 검사로 임포트합니다. 이 장의 모든 숫자를 재현하려면 python3 examples/frontier/satori_lite.py를 실행하십시오; 이 실행은 결정론적이며, 모든 주장, 즉 두 오라클 동등성, 모든 깊이에서의 건전성, 47개 증명 검사 전부, 그리고 주석 스윕은 단언(assert)으로 지켜집니다.

이 장에서 다루는 것​

수렴, 이 시리즈 자신의 이야기로 말하다​

상태: 추론기가 층들 사이에 간직하는 것​

한 층, 세 가지 어텐션​

온도 다이얼, 커밋된 스윕으로 값매기다​

록스텝이 정당한 이유: 단조성이 순서-독립성을 사들이다​

오라클이 단언하다: 결정적 복원, 두 번​

절단 법칙, 어텐션의 옷을 입고 다시 실행되다​

흔적은 일급 출력이지, 사후 합리화가 아니다​

단 한 번의 섬광, 정직하게​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

다음으로 이어지는 곳​