SATORI 아키텍처: 하나의 연산자, 네 가지 성질

📍 현재 위치: VII부 · SATORI 캡스톤 — 19장. 기호 어텐션은 연산자를 지었습니다: 가중치를 공유하는 하나의 소프트 레이어를 고정된 횟수만큼 펼친 것으로, 그 크리스프 극한에서 1권의 전방 연쇄와 2권의 EL 완성을 정확히 되찾습니다. 이 장은 그 연산자를 시스템에 필요한 다른 모든 것으로 둘러싸며, 결과에 대한 모든 주장을 이 권이 이미 지어 둔 계측 도구에 붙들어 맵니다.

연산자는 아키텍처가 아닙니다. 앞 장의 커널은 하나의 질문, 곧 두 고전적 추론기가 어떻게 하나의 미분 가능한 패스가 되는가에 답할 뿐, 그 밖의 모든 질문을 열어 둡니다: 그 패스가 어떤 자료 구조 위에서 도는지, 그 신뢰도 숫자가 어디서 나오는지, 그 규칙이 주어지는 대신 어떻게 학습될 수 있는지, 그 어텐션 기록이 설명으로서 어떤 값어치를 지니는지, 그리고 지식 베이스가 열세 개의 개체이기를 그만둘 때 무슨 일이 일어나는지입니다. SATORI의 답은 세 부분으로 이루어진 설계입니다: 연산자, 그것이 도는 두 개의 기층(substrate, 주석 달린 규칙 표현과 박스 임베딩 어휘), 그리고 하나의 규율(도출 트레이스는 순전파의 일급 출력이며, 결코 사후에 재구성된 이야기가 아닙니다). 이 조립으로부터 프로젝트는 네 가지 성질을 주장합니다: 학습 가능한 라우팅, 충실한 트레이스, 병렬 규모, 그리고 보정된 열린 세계 신뢰도입니다. 그 주장들은 이 장의 요점이 아닙니다. 요점은 그것들이 만들어지는 방법입니다: 모든 성질은 독립적인 계측 도구와 짝을 이루고, 각 도구는 그것이 이제 판정하는 아키텍처가 존재하기도 전에 이 권의 앞선 부(Part)에서 지어지고 검증되었으며, 여기서 내려지는 모든 평결은 실행할 때마다 스크립트가 다시 유도하는 커밋된 숫자입니다.

쉽게 말하면

빠르고, 안전하고, 효율적이고, 조용한 기계를 홍보하는 스타트업을 상상해 보십시오. 여러분은 두 가지 방식으로 응답할 수 있습니다. 그 홍보를 듣거나, 아니면 자신만의 스톱워치, 자신만의 충돌 시험대, 자신만의 전력계, 자신만의 마이크(그 어느 것도 그 스타트업이 제공한 것이 아닙니다)를 가져와 직접 측정하는 것입니다. 그 기계가 실제로 무엇으로 드러나든, 지식을 만들어 내는 것은 오직 두 번째 응답뿐입니다. 이 장은 추론 아키텍처에 적용된 두 번째 응답이며, 한 가지 반전이 있습니다: 우리는 스톱워치와 시험대와 전력계와 마이크를 여섯 개의 부(Part)에 걸쳐 먼저 지어 두었고, 이제야 비로소 그 기계를 방 안으로 밀어 넣습니다. 광고된 네 가지 성질 각각은 정확히 하나의 계측 도구를 받으며, 무엇이 살아남는지 말해 주는 것은 홍보가 아니라 그 도구입니다.

이 장에서 다루는 내용

쐐기로서의 설계 문제: 저마다 다른 하나가 가진 것을 놓치는 세 계열의 시스템(학습할 수 없는 정확한 추론기, 온톨로지에 눈먼 규칙 학습기, 증명도 보정도 하지 못하는 임베더)과, 올바른 기층 위의 하나의 연산자가 그 세 모서리를 동시에 차지한다는 아키텍처의 내기를 다룹니다.
기층 하나, 주석 달린 온톨로지 IR(intermediate representation, 중간 표현): 모든 공리가 세 가지 규칙 모양으로 정규화되고, 모든 원자가 괴델 세미링 위의 구간 주석을 지니며, 열린 세계의 미지수가 전체 구간으로 인코딩되어 기권이 덧붙인 것이 아니라 데이터 모델 자체의 속성이 되는 방식을 다룹니다.
기층 둘, 박스 어휘: 이 시리즈 자신의 평결(공이 아니라 박스)이 어떻게 하나의 기하로 하여금 TBox 포섭과 질의 영역을 동시에 섬기게 만드는지, 장난감이 이 가운데 무엇을 구현하는지, 그리고 완전한 설계와의 간극이 정확히 어디에 놓여 있는지를 다룹니다.
네 가지 성질, 네 가지 계측 도구, 네 가지 커밋된 영수증: 그래디언트로 훈련된 라우터 가중치로 복원되어 정확히 디코드되는 심어진 규칙; 참된 최소 정당화를 담고 있으며 소거를 통과하는 트레이스; 3단 깊이 법칙 아래 하나의 스택 패스로 닫히는 백 가지 변형의 배치; 그리고 식별 가능성 유보 사항이 함께 붙은, ECE(expected calibration error, 기대 보정 오차) 도구로 감사되는 구간 신뢰도를 다룹니다.
틀 짓는 교훈: 계측 도구를 갖춘 주장이 아키텍처와 홍보를 가르는 차이라는 것과, 장난감 영수증이 아직 보여 주지 못하는 것에 대한 정직한 목록을 다룹니다.

쐐기: 저마다 다른 하나가 가진 것을 놓치는 세 계열

이 시리즈는 이제 이 분야가 실제로 출하하는 세 계열의 추론 시스템 전부를 축소된 규모로 지어 왔으며, 그 각각의 결함은 다른 하나가 지닌 성질입니다. 2권의 정확한 추론기(완성 규칙과 그 산업용 친척인 ELK, HermiT, Konclude)는 건전하고 완전하며 공리까지 설명 가능하지만, 아무것도 학습할 수 없습니다: 모든 규칙은 손으로 쓰였고, 모든 사실은 크리스프하며, 빠진 엣지는 영원히 빠진 채로 남습니다. 4권의 미분 가능한 규칙 학습기(Neural-LP와 DRUM 계열, Neural-LP와 DRUM에서 다시 다루었습니다)는 답만으로 사슬 규칙을 학습하지만, 온톨로지에 눈이 멉니다: 어떤 TBox도 그것이 유도하는 바를 제약하지 않고, 어떤 바닥 규칙도 어떤 가설이 모순임을 말해 주지 않으며, 그 신뢰도는 보정되지 않은 점수일 뿐입니다. 3권의 임베더는 어떤 트리플이든 점수를 매기고 관측된 그래프 너머로 일반화하지만, 증명하지도(확인할 도출이 존재하지 않습니다) 기권하지도 않습니다(답할 수 없는 질의를 포함해 모든 질의에 점수가 매겨집니다). 설계 공간의 세 모서리이며, 저마다 다른 두 모서리에는 결코 닿을 수 없는 시스템이 차지하고 있습니다.

SATORI의 내기는 이것이 삼중고가 아니라 기층 선택의 산물이라는 것입니다: 박스 기하가 실어 나를 수 있는 어휘를 지닌 주석 달린 규칙 표현 위에서 도는 하나의 연산자가 세 모서리를 한꺼번에 차지합니다. 그 연산자가 동시에 추론기이고(그 크리스프 극한은 앞 장에서 증명된 고전적 폐쇄입니다), 훈련 가능한 네트워크이며(모든 단계가 미분 가능합니다), 주석 운반체이기 때문입니다(정도는 원자와 똑같은 대수를 따라 흐릅니다). 박스는 이 설계를 떠받치는 기하학적 선택입니다: 포함 관계는 온톨로지 쪽에서 포섭이고 [1], 정확히 같은 영역 계산법이 응답 쪽에서는 질의 공간이므로 [2], 그라운딩과 질의는 더 이상 서로 다른 어휘가 아니게 됩니다. 이 내기가 규모 앞에서 옳은지 그른지는 이 책상이 결정할 수 없습니다. 이 책상이 할 수 있는 일, 그리고 이 장이 하는 일은 그 방법을 강제하는 것입니다: 계측 도구 없이는 어떤 성질도 없다는 것입니다. 주장된 네 가지 성질 각각은 이 권의 앞선 부(Part)에서 온 장치로 채점되며, 그 장치는 SATORI가 아닌 시스템들에 맞서 설계되고, 유도되고, 커밋되었습니다. 자신의 숙제를 스스로 채점하는 아키텍처는 홍보입니다. 자신보다 먼저 존재한 계측 도구로 채점되는 아키텍처는 실험입니다.

기층 하나: 주석 달린 온톨로지 IR

첫 번째 기층은 2권의 장치를 산업화한 것입니다: 온톨로지 공리와 데이터로그 규칙이 모두 컴파일되어 들어가는 하나의 작은 규칙 모양 집합인 중간 표현(intermediate representation, IR) 하나이며, 모든 원자에는 주석 슬롯이 붙어 있습니다. 그 배후의 정규화 정리는 정규화 장이 증명한 바로 그것입니다: 모든 EL TBox는 정확히 네 가지 고정된 템플릿(NF1–NF4)으로 선형 시간에 환원되며, IR은 이를 세 가지 규칙 모양으로 접어 넣습니다. 왼쪽이 원자 개념들의 논리곱인 것( $A_1 \sqcap \cdots \sqcap A_n \sqsubseteq B$ , $n = 1$ 이면 NF1을, $n = 2$ 이면 NF2를 덮으며, 임의의 $n$ 은 정규형 자체가 만들어 내는 것이 아니라 혼 몸체가 같은 모양에 들어맞도록 한 IR의 일반화입니다), 오른쪽이 존재 제한인 것( $A \sqsubseteq \exists r.B$ ), 그리고 왼쪽이 존재 제한인 것( $\exists r.A \sqsubseteq B$ )입니다. 여기서 $A$ , $B$ 는 개념 이름의 범위를 훑고, $r$ 은 역할 이름의 범위를 훑으며, 색인 $n$ 은 왼쪽 변의 논리곱 항 개수이고, $\sqsubseteq$ 는 "~에 포섭된다", 즉 왼쪽의 모든 인스턴스가 오른쪽의 인스턴스라고 읽으며, $\exists r.B$ 는 " $B$ 의 어떤 원소로 향하는 $r$ -엣지를 가진다"라고 읽습니다. 컴패니언의 커널은 정확히 이 어휘로 말합니다. 그 인스턴스 빌더는 각 정규형을 하나의 IR 규칙으로 사상합니다(satori_lite.py 197–204번째 줄):

        if ax[0] == "nf1":                      # A' ⊑ B
            rules.append(("cr1", (ax[1],), ax[2]))
        elif ax[0] == "nf2":                    # A₁ ⊓ A₂ ⊑ B
            rules.append(("cr1", tuple(ax[1]), ax[2]))
        elif ax[0] == "nf3":                    # A ⊑ ∃r.B  — edge emission
            rules.append(("cr2", ax[1], ax[2], ax[3]))
        elif ax[0] == "nf4":                    # ∃r.B' ⊑ C — message pass
            rules.append(("cr3", ax[1], ax[2], ax[3]))

여기에 역할 합성을 위한, CRχ라 이름 붙은 사슬 모양과 역할 계층을 위한 복사 모양이 더해지고, 역할마다 한 번씩 바닥 규칙 CR⊥이 더해집니다(213번째 줄). 이와 똑같은 다섯 가지 모양이 compile_horn(131–160번째 줄)을 통해 1권의 혼 규칙을 흡수하는데, 이것이 코드로 구현된 "하나의 동질적 커널"이라는 주장입니다: 온톨로지 공리와 데이터로그 규칙은 두 개의 엔진이 아니라, 하나의 규칙 집합을 위한 두 개의 프런트엔드입니다.

주석 슬롯이 바로 이 기층이 더 이상 2권에 머무르지 않는 지점입니다. 모든 원자는 하나의 정도(degree)를 지니며, 정도는 세미링(semiring) 위에서 합성됩니다: 두 개의 연산을 갖춘 대수로, 하나의 도출의 전제들을 결합하는 $\otimes$ ("그리고"라고 읽습니다)와 대안적인 도출들을 병합하는 $\oplus$ ("또는"이라고 읽습니다)이며, 이는 프로버넌스(provenance) 이론이 데이터로그 추론을 관통해 흐르는 것이 정확히 이것임을 보여 준 바로 그 구조입니다 [3]. SATORI의 기본값은 괴델 세미링(Gödel semiring)으로, $[0,1]$ 위에서 $a \otimes b = \min(a,b)$ 이고 $a \oplus b = \max(a,b)$ 입니다: 하나의 도출은 정확히 그 가장 약한 전제만큼 강하고, 하나의 원자는 그 최선의 도출만큼 강합니다. 커널은 온도로 매끄럽게 다듬은 버전인 $\mathrm{softmin}_\tau$ 와 $\mathrm{softmax}_\tau$ 를 계산하며(satori_lite.py 96–107번째 줄), 이는 병합되는 값이 $n$ 개일 때 크리스프 연산자와의 거리가 $\tau \log n$ 으로 한계 지어지므로, 온도 $\tau \to 0$ 일 때 고전적 의미론이 되돌아옵니다; 앞 장은 그 되찾음을 두 고전적 오라클에 맞서 커밋했습니다.

열린 세계에는 하나의 스칼라 정도만으로는 충분하지 않으며, 이는 이 기층에서 가장 신중하게 내려진 설계 결정입니다. 2권의 열린 세계 교훈은 증명되지 않은 원자가 거짓이 아니라 미결정이라는 것이었습니다. 그래서 IR은 각 원자에 구간(interval) $[\ell, u]$ 를 주석으로 답니다: 하한 $\ell$ 은 그 원자가 단언된 것으로부터 도출 가능한 정도이고, 상한 $u$ 는 그것이 모든 제약 아래 가능한 정도이며, 미지수는 전체 구간 $[0,1]$ 로, 아무도 단언하거나 반박하지 않은 모든 원자의 기본 주석입니다. 단언과 부인은 양쪽 끝에서의 임계값 읽기가 됩니다: $\ell$ 이 높으면 단언하고, $u$ 가 낮으면 부인하며, 그 사이에서는 기권합니다. 이로써 기권은 데이터 모델의 속성이 됩니다. 항상 답하는 시스템에 덧붙여진 별도의 "신뢰도 모듈" 같은 것은 없습니다; 기층 자체가 "증명 가능하게 아니오"와 "정보 없음"을 구별하며, III부의 장치는 그 구별을 곧바로 소비할 것입니다. 컴패니언은 이 구간을 크리스프 해상도에서 한 쌍의 답 집합으로, 즉 질의마다 하한 집합과 상한 집합으로, 각 면마다 클레이니 방식 연산자(참, 거짓, 미지의 세 가지 진리값을 쓰는 클레이니의 3치 논리에서 온 이름입니다)를 갖추어 구현합니다(satori_eval.py 348–376번째 줄); 이들이 유지하는 건전성 불변량은 아래에서 성질 넷이 그것을 필요로 하는 곳에서 유도됩니다.

기층 둘: 박스, 두 작업이 공유하는 기하

두 번째 기층은 IR이 열어 둔 질문에 답합니다: 기호가 바닥나면, 즉 질의가 어떤 공리도 단언하지 않고 어떤 규칙도 도출하지 않는 엣지를 언급하면, 무엇이 그 어휘를 실어 나르는가? 3권은 후보 기하들에 세 개의 장을 썼고, 두 문장으로 되새길 가치가 있는 평결로 끝을 맺었습니다. 영역 임베딩은 포함 관계로 포섭을 확인 가능하게 만들지만, 논리곱은 두 영역의 교집합이 같은 패밀리의 영역일 것을 요구하며, 공은 정확히 그 지점에서 실패합니다: 두 공이 겹쳐 만드는 렌즈는 공이 아닌 반면, 축 정렬된 박스는 교집합에 대해 닫혀 있으므로, 공이 증명 가능하게 근사할 수밖에 없는 곳에서 단 하나의 박스 패밀리가 개념과 그 논리곱을 충실하게 표현할 수 있습니다 [1].

통합의 통찰은 바로 이 동일한 닫힘 성질이 논리곱 질의 응답에도 필요하다는 것입니다. 4권의 질의 장은 EPFO 응답(존재 긍정 1차 질의: 투영, 교집합, 합집합)을 교집합 노드가 반드시 영역을 교차시켜야 하는 하나의 계산 DAG(directed acyclic graph, 방향 비순환 그래프)로 지었으며, 그것을 작동시킨 시스템은 박스를 질의 영역으로 사용했습니다 [2]. 그래서 하나의 기하가 두 주인을 함께 섬깁니다: 개념마다 하나씩인 TBox로 초기화된 박스는 포섭을 포함 검사로 만들고, 동일한 박스 계산법은 다중 홉 질의를 답 개체들이 반드시 안착해야 하는 하나의 영역으로 만듭니다. 그라운딩과 질의가 어휘를 공유하는 것, 이것이 바로 임베딩을 덧붙인 추론기와 추론기가 실제로 그 안에서 사고하는 임베딩 사이의 아키텍처적 차이입니다.

정직함을 위해서는 그 간극을 있는 그대로 밝혀야 합니다. 완전한 설계는 역할 변환을 갖춘 TBox로 초기화된 박스를 명시하며, 이는 배타성을 인식하는 기하학적 손실로 훈련되고, 학습된 영역 위에서 소프트 단일화를 거칩니다. 장난감은 그보다 훨씬 적게 구현합니다: 그 "신경망 절반"은 보정된 시그모이드를 통해 읽어 낸, 임베딩 차원 $d = 16$ (개체와 역할마다 실수 좌표 16개이며, ComplEx는 이를 복소수 8개로 읽습니다)의 3권 ComplEx 모델이며, 이는 정도로 게이팅되는 기호 표(degree-gated symbol table)를 내놓습니다. 역할 $r$ 마다 하나씩, $|V| = 13$ 개의 개체에 대한 소프트 인접 행렬 $M_r \in [0,1]^{|V| \times |V|}$ 입니다(satori_eval.py 102–116번째 줄):

    e_re, e_im, w_re, w_im, _ = bilinear.train_complex(seed=0)
    S = cqd.complex_score_table(e_re, e_im, w_re, w_im)
    # M = σ(S/τ*): the temperature-scaled probability reading of every score.
    M = calibration._sigmoid(S / tau_platt)
    for h, r, t in kg.TRAIN:
        M[kg.R_ID[r], kg.E_ID[h], kg.E_ID[t]] = 1.0

관측된 모든 훈련 엣지는 정확히 $1.0$ 으로 고정되고(관측된 사실은 예측이 아닙니다), 관측되지 않은 모든 쌍은 보정된 점수 $\sigma(s/\tau^\ast)$ 를 받습니다. 여기서 $\sigma$ 는 로지스틱 시그모이드 $\sigma(x) = 1/(1 + e^{-x})$ 이고 $\tau^\ast = 1.4172$ 는 III부의 보정 장이 맞춘 온도입니다. 학습된 박스가 아니라 기호 위의 정도입니다: 이 장난감에서 기하학적 기층은 오직 커널이 소비하는 인터페이스(역할마다 하나씩인 $[0,1]$ 인접 행렬)로서만 존재하며, 이 장의 모든 숫자는 그 대체를 염두에 두고 읽어야 합니다. 그 대체가 가장 크게 문제 되는 곳에서는 마지막 절이 그것을 밝힙니다.

연산자와 규율

연산자 자체는 그저 되새기기만 하면 됩니다. 앞 장이 그것을 짓고 인증했기 때문입니다: 가중치를 공유하는 하나의 레이어가 이전 상태 위에서 모든 IR 규칙을 동시에 발동시키며(논리곱은 $\mathrm{softmin}_\tau$ 로, 대안적 도출들은 $\mathrm{softmax}_\tau$ 로 병합되고, 역할 합성은 괴델 세미링 행렬 곱으로 이루어집니다), 네트워크는 그런 레이어 $L$ 개로 이루어진, 수렴 검사가 전혀 없는 고정된 스택입니다. 고정된 깊이에는 물리학이 있습니다: 트랜스포머를 포함해 로그 정밀도 산술로 실행되는 고정 깊이 순전파 스택은 작은 병렬-회로 클래스 안에 놓이며, 그 클래스들이 다항 시간 전체를 담고 있는 것으로 밝혀지지 않는 한 임의로 깊은 폐쇄를 계산할 수 없으므로 [4], 그 스택은 건전하지만 절단된 추론기이며, $L$ 이 지식 베이스의 포화 깊이 $D$ 에 도달할 때 정확히 완전해집니다(합쳐진 학계 세계에서는 $D = 3$ 입니다). 성질 셋은 이 값을 정직하게 매깁니다.

규율이 이 설계를 완성합니다. 커널이 도출을 진행하는 동안, 레이어 $k$ 에서 처음 도출된 모든 원자에 대해 (레이어, 규칙, 아그맥스 부모)라는 삼중항인 트레이스 텐서(trace tensor)를 기록합니다(satori_lite.py 261–301번째 줄). 두 가지 사실이 이 기록을 I부가 우리에게 불신하도록 가르친 사후적 귀속과 다르게 만듭니다. 첫째, 이는 나중에 현저성 방법으로 재구성되는 것이 아니라 순전파 자체에 의해 만들어집니다: 설계는 기록되는 부모를 도출들을 병합했던 바로 그 $\mathrm{softmax}$ 의 아그맥스로 명시하며, 장난감은 이를 소프트 레이어의 크리스프 불리언 거울상으로 실현하는데, 이는 보조를 맞추어 실행되고 모든 깊이에서 임계값이 매겨진 소프트 상태와 같음이 단언되며, 그 안에서는 모든 크리스프 도출이 정도 1에서 동점을 이루므로 결정론적 동점 해소(고정된 규칙 순서, 그다음 정렬된 원자 순서)가 곧 아그맥스가 됩니다. 둘째, 이는 기계로 검사 가능합니다: check_proof(337–371번째 줄)는 트레이스에 담긴 모든 원자를 다시 도출하여 결함이 있으면 예외를 일으키며, 커밋된 실행은 두 얼굴 모두의 도출된 원자 $24 + 23 = 47$ 개 전부를 다시 검사합니다. 일급 트레이스는 하나의 기능이 아니라 설계 제약이며, 이것이 바로 성질 둘을 애초에 검사 가능하게 만드는 것입니다.

성질 하나: 학습 가능한 라우팅, 심어진 규칙 영수증

주장: 커널이 발동시키는 규칙은 주어질 필요가 없습니다; 후보 규칙 몸체들에 대한 훈련 가능한 어텐션 분포인 라우터(router)가 오직 질의 답만으로 그것들을 학습할 수 있습니다. 계측 도구는 I부의 규칙 추출 표준을 심어진 규칙 프로토콜(planted-rule protocol)로 벼려낸 것입니다: 알려진 규칙 하나를 숨기고, 오직 그 규칙의 답만으로 라우터를 훈련시킨 다음, 훈련된 가중치가 근사적으로가 아니라 정확히 그 숨겨진 규칙으로 디코드되어 돌아올 것을 요구합니다. 정확한 디코드야말로 이것을 막연한 느낌이 아니라 하나의 계측 도구로 만드는 것입니다; 그저 옳은 규칙 "근처에 가중치를 둘" 뿐인 라우터는 검사 가능한 것을 아무것도 추출하지 못한 것입니다.

커밋된 실험(satori_eval.py 154–217번째 줄과 452–473번째 줄)은 규칙 집합에서 grandAdvisor 규칙 grandAdvisor(x,z) ← advises(x,y) ∧ advises(y,z)를 숨깁니다(←는 오른쪽에서 왼쪽으로, ∧는 "그리고"로 읽습니다: $x$ 가 $y$ 를 지도하고 $y$ 가 $z$ 를 지도하면, grandAdvisor( $x,z$ )입니다). 후보 공간은 실행 예제의 다섯 개 기본 역할에 대한 길이 2짜리 사슬 몸체 $r(x,y) \wedge s(y,z)$ 전부입니다: $5 \times 5 = 25$ 개의 템플릿이며, 그중 하나(advises∘advises, 숨겨진 규칙의 몸체를 합성으로 쓴 것으로, ∘가 첫 번째 홉을 두 번째 홉으로 이어 붙입니다)가 숨겨진 규칙입니다. 각 템플릿 $k$ 에 대해 커널 자신이 특징 행렬 $C_k \in [0,1]^{13 \times 13}$ 을 미리 계산합니다. 이는 전체 18개 엣지 그래프 위에서 그 자신의 사슬 메시지 $C_k[x,z] = \mathrm{softmax}_y\,\mathrm{softmin}(A_r[x,y], A_s[y,z])$ 이며, 여기서 $A_r$ 과 $A_s$ 는 그 그래프 위에서 역할 $r$ 과 $s$ 의 크리스프 $0/1$ 인접 행렬입니다(기층 하나의 개념 이름이 아니라 인접 행렬 $A$ 입니다)(166–179번째 줄); 이들은 커널의 CRχ 규칙을 템플릿마다 한 번씩 적용한 것이며, 라우터에 대해서는 상수입니다. 라우터는 템플릿마다 실수 하나씩인 가중치 벡터 $\mathbf{w} \in \mathbb{R}^{25}$ 이며, 소프트맥스 $\alpha_k = e^{w_k} / \sum_j e^{w_j}$ 에 의해 어텐션 분포로 눌러집니다. 그리고 라우팅된 예측은 혼합 $P[x,z] = \sum_k \alpha_k\, C_k[x,z]$ 입니다: "주목받은 어떤 규칙이 그 쌍을 도출하는 정도"입니다. 지도(supervision)는 오직 그 질의의 답뿐입니다. 정확히 세 개의 1을 지닌 정답 행렬 $G \in \{0,1\}^{13 \times 13}$ 이며, 세 개의 참된 grandAdvisor 쌍입니다(하니스는 $G$ 의 정확히 세 개의 칸이 1임을 단언합니다, satori_eval.py 458번째 줄).

손실은 전체 $N_{\text{cells}} = 13 \times 13 = 169$ 개 칸에 대한 평균 이진 교차 엔트로피이며(이 개수를 $N_{\text{cells}}$ 로 쓰는 이유는 $M$ 이 이미 위에서 소프트 인접 행렬의 이름으로 쓰였기 때문입니다), 로그 안에는 작은 보호 장치 $\varepsilon = 10^{-6}$ 이 들어갑니다:

L \;=\; -\frac{1}{N_{\text{cells}}} \sum_{x,z} \Big[ G[x,z]\,\ln\!\big(P[x,z] + \varepsilon\big) + \big(1 - G[x,z]\big)\,\ln\!\big(1 - P[x,z] + \varepsilon\big) \Big].

그래디언트 경로는 소프트맥스를 관통해 흐르며, 컴패니언은 그 경로를 인용하고 검사할 수 있도록 정확히 하기 위해 오토그래드 라이브러리를 호출하는 대신 손으로 그것을 유도합니다. 세 개의 고리입니다. 첫째, $L$ 을 칸별로 미분하면,

\frac{\partial L}{\partial P[x,z]} \;=\; -\frac{1}{N_{\text{cells}}} \left[ \frac{G[x,z]}{P[x,z] + \varepsilon} - \frac{1 - G[x,z]}{1 - P[x,z] + \varepsilon} \right].

둘째, $P$ 는 $\alpha$ 에 대해 선형이므로, $k$ 번째 어텐션 가중치에 대한 미분은 각 칸의 민감도를 그 템플릿의 특징에 대해 모읍니다: $g_k = \partial L / \partial \alpha_k = \sum_{x,z} (\partial L / \partial P[x,z])\, C_k[x,z]$ 입니다. 셋째, 소프트맥스 야코비안(Jacobian)입니다. $Z = \sum_u e^{w_u}$ 라 써서 $\alpha_j = e^{w_j}/Z$ 가 되게 하면, 몫의 법칙(quotient rule)은 다음을 줍니다

\frac{\partial \alpha_j}{\partial w_i} = \frac{\delta_{ij}\, e^{w_j}\, Z - e^{w_j}\, e^{w_i}}{Z^2} = \alpha_j \delta_{ij} - \alpha_j \alpha_i = \alpha_j\big(\delta_{ij} - \alpha_i\big),

여기서 $\delta_{ij}$ 는 크로네커 델타(Kronecker delta)로, $i = j$ 일 때 $1$ 이고 그 밖에는 $0$ 입니다. 연쇄시키고, 그 델타에서 합을 쪼개어 $j = i$ 항만이 첫 조각에서 살아남게 하면:

\frac{\partial L}{\partial w_i} \;=\; \sum_j g_j\, \alpha_j\big(\delta_{ij} - \alpha_i\big) \;=\; g_i \alpha_i - \alpha_i \sum_j \alpha_j g_j \;=\; \alpha_i \Big( g_i - \sum_j \alpha_j g_j \Big).

각 템플릿의 가중치는 자신의 그래디언트 신호 $g_i$ 가 어텐션으로 가중된 평균 $\sum_j \alpha_j g_j$ 보다 얼마나 더 나은지에 비례해 움직입니다: 현재의 혼합보다 답을 더 잘 설명하는 템플릿은 질량을 얻고, 나머지는 잃습니다. 이 세 개의 고리는 일곱 줄의 커밋된 코드로 안착합니다(satori_eval.py 195–201번째 줄):

    ex = np.exp(w - w.max())
    alpha = ex / ex.sum()
    P = np.tensordot(alpha, feats, axes=1)
    L = -float(np.mean(G * np.log(P + EPS) + (1 - G) * np.log(1 - P + EPS)))
    dP = -(G / (P + EPS) - (1 - G) / (1 - P + EPS)) / G.size
    g = np.tensordot(feats, dP, axes=([1, 2], [0, 1]))
    gw = alpha * (g - float(alpha @ g))

균등한 라우터( $\mathbf{w} = \mathbf{0}$ , 그래서 $\alpha_k = 1/25$ )로부터 학습률 $5.0$ 으로 400 스텝 동안의 평범한 경사 하강이며, 커밋된 실행은 다음을 보고합니다:

[2] C2 — planted-rule recovery (softmax router over 25 chain templates)
  hidden: grandAdvisor(x,z) ← advises(x,y) ∧ advises(y,z); supervision: its 3 query answers
  hand gradient vs central differences: max error 1.17e-11 over 25 coordinates
  loss: 0.0730 (step 1)  →  0.0658 (step 10)  →  0.0231 (step 100)  →  0.0197 (step 400)
  router attention: advises∘advises 0.9718   advises∘cites 0.0012   cites∘advises 0.0012   (rest ≤ the third)
  decoded rule == the hidden kb rule, exactly (asserted)

이 영수증을 순서대로 읽어 봅시다. 손으로 유도한 그래디언트는 25개 좌표 전체에서 중심 유한차분과 $1.17 \times 10^{-11}$ 까지 일치하므로, 훈련 신호는 참된 도함수입니다. 손실은 스냅숏 전체에 걸쳐 단조롭게 떨어집니다. 훈련된 어텐션은 그 질량의 $0.9718$ 을 advises∘advises에 집중시키며, 차점자는 $0.0012$ 로 세 자릿수 아래입니다. 그리고 디코드는 정확합니다: $\alpha$ 에 대한 argmax를 IR 구문으로 다시 감싼 것이 숨겨진 규칙 자신의 컴파일된 형태인 compile_horn([kb.RULES[3]])[0]과 같으며, 정확한 튜플 동등성으로 단언됩니다(469–471번째 줄). 이것은 규칙 공간에 대한 이산적 탐색 없는 규칙 귀납입니다: 어떤 조합적 탐색도 25개의 후보를 하나씩 방문하며 채점하고 쳐내지 않습니다; 모든 후보 몸체가 커널 특징으로 한 번씩 구체화되고, 하나의 미분 가능한 어텐션이 그것들 사이에서 함께 선택하며, 경사 하강이 그 질량을 옮깁니다. 정직한 범위 주석이 이 굵은 주장 옆에 붙어야 합니다: 25개 템플릿 공간은 특징으로서 남김없이 열거되며, 이는 정확히 Neural LP의 미리 계산된 경로 행렬 읽기이고, 장난감이 아닌 규칙 공간이라면 그런 열거를 허락하지 않을 것입니다. 4권의 Neural-LP와 DRUM은 지식 그래프 위의 사슬 규칙에 대해 정확히 이 움직임을 지었으며, 그것을 질의에 조건화하여, 증명기 안에서 하는 것에 가장 가까운 선조는 미분 가능한 증명에서의 학습된 추론 전략에 관한 연구 계열입니다 [5]. 장난감이 그 선조들에 더하는 것은 힘이 아니라 감사 가능성입니다: 심어진 규칙 프로토콜은 "모델이 규칙을 학습했다"는 것을 해석에서 단언으로 바꿉니다.

성질 둘: 충실한 트레이스, I부에 배선됨

주장: 트레이스 텐서는 커널이 도출한 것을 왜 도출했는지에 대한 정직한 기록입니다. I부는 정확히 이를 위한 두 가지 계측 도구를 지었으며, 이 아키텍처는 둘 다를 통과해야 합니다. 첫 번째는 정당화 장의 금본위입니다: 어떤 함의에 대한 MinA(최소 공리 집합, 정당화라고도 불립니다)는 여전히 그것을 함의하는, 부분집합 관계에서 최소인 공리 집합이며, Reiter의 적중 집합 트리로 열거될 수 있습니다. 두 번째는 충실성 장의 소거 프로토콜입니다: 설명이 인용하는 증거를 지우면 결론이 반드시 깨져야 하고(포괄성), 인용된 증거만 남기면 결론이 반드시 살아남아야 하며(충분성), 인용되지 않은 증거를 지우면 아무것도 달라져서는 안 됩니다.

MinA 검사에는 프로버넌스(provenance, 출처)가 필요하므로, 컴패니언은 각 IR 규칙이 어떤 원래 공리가 그것을 만들어 냈는지를 기억하도록 EL 인스턴스를 다시 지은 다음(el_provenance_instance, satori_eval.py 290–319번째 줄), 트레이스 기록과 함께 커널을 다시 실행하고, 도출된 포섭 관계에 대해 그 기록된 도출 트리 어디엔가 나타나는 원래 공리 식별자들의 집합을 모읍니다(trace_axioms, 322–329번째 줄). 그런 다음 이 계측 도구는 요구합니다: 그 집합은 justifications.py(504–510번째 줄)가 독립적으로 찾아낸 참된 MinA를 포함해야 합니다. 커밋된 행들은 다음과 같습니다:

  TBox face — the discretized trace vs justifications.py:
    Professor ⊑ Researcher: trace axioms {1} ⊇ MinA {1}   (all MinAs: {1} {4, 5})
    TenuredStudentAdvisor ⊑ ⊥: trace axioms {6, 10, 11, 12} ⊇ MinA {6, 10, 11, 12}   (all MinAs: {6, 10, 11, 12})

정직한 주장은 동등성이 아니라 포함 관계이며, 여기에는 두 가지 이유가 있습니다. 트레이스는 커널이 실제로 발동시킨 도출을 기록하며, 이는 부분집합 관계에서 최소일 필요가 없습니다: 여러 도출이 존재할 때(Professor ⊑ Researcher는 $\{1\}$ 과 $\{4,5\}$ 라는 두 개의 MinA를 가집니다), 트레이스는 아그맥스에서 이긴 쪽을 무엇이든 실어 나르며, 더 긴 도출이 이기지 못하도록 막는 것은 아무것도 없습니다. 그리고 진정으로 소프트한 설정에서는 기록되는 부모가 정도들에 대한 $\mathrm{softmax}$ 의 아그맥스입니다; 이긴 도출보다 정도가 근소하게 낮은 아깝게 놓친 부모들은, 임계값을 매긴 읽기라면 탈락시켰을 텐데도, 적당한 온도에서는 그 기록에 들어올 수 있습니다. "트레이스는 인증된 최소 증명을 담고 있다"는 증명 가능하지만, "트레이스는 정확히 최소 증명이다"는 거짓 광고일 것입니다.

소거 절반은 혼 얼굴 위에서 실행됩니다. 도출된 네 개의 원자 각각에 대해, 트레이스의 잎 사실들이 모이고(trace_leaves, 228–234번째 줄), 모델은 그대로 둔 채 개별 사실들을 입력 상태에서 하나씩 지워 커널을 다시 실행합니다(derives_without, 237–251번째 줄). 잎 사실 하나하나의 삭제는 반드시 그 원자를 죽여야 하고, 잎들만으로도 그것을 다시 도출해야 하며, 트레이스에 없는 사실들의 시드가 부여된 삭제는 아무것도 바꾸지 말아야 합니다:

[3] C3 — faithful traces: erasure + MinA containment
  Horn face, 4 derived atoms — e.g. grandAdvisor(alice, carol) has trace leaves advises(alice, bob), advises(bob, carol)
    comprehensiveness 8/8: every leaf deletion kills its atom; leaves ALONE re-derive it (4/4)
    12 seeded non-trace deletions (default_rng(5)): nothing breaks (asserted)

포괄성 $8/8$ , 충분성 $4/4$ , 그리고 아무 효과도 없는 열두 번의 통제 삭제입니다. 이를 I부의 커밋된 실험실이 평범한 분류기의 어텐션 가중치에 대해 보여 준 것과 비교해 봅시다: 그곳에서 어텐션은 포괄성에서 실패했는데, 소프트 가중치를 계산이 그 입력에 의존하는 정도에 구조적으로 묶어 주는 것이 아무것도 없었기 때문입니다. 여기서는 같은 프로토콜이 통과하는데, 아키텍처가 구성에 의해 그것을 통과하도록 만들었기 때문입니다: 트레이스가 곧 도출이므로, 그 잎을 지우는 것은 그 도출이 소비한 전제들을 제거하는 것입니다. 충실성은 나중에 시스템 안으로 측정되어 들어온 것이 아닙니다; 그것은 설계되어 들어간 것이며, 계측 도구는 그 설계가 말한 바를 실제로 해냈음을 확인해 줍니다.

성질 셋: 병렬 규모, 법칙이 매긴 값

주장: 하나의 레이어가 모든 규칙을 동시에 발동시키고 레이어들이 평범한 텐서 대수이므로, 이 아키텍처는 질의에 걸쳐서도, 지식 베이스 변형에 걸쳐서도, 깊이를 제외한 그 무엇에 걸쳐서도 배치화됩니다. 이 배치 영수증은 IV부의 GPU 장에서 옵니다. 그 벡터화된 완성을 캡스톤 커널이 공유합니다: 알려진 포섭 관계 하나씩만 서로 다른 백 개의 TBox 변형이, 배치에 대한 파이썬 루프 없이 하나의 스택된 $(100, 12, 12)$ 텐서 패스(맨 앞의 100은 변형의 개수이고, 각 $12 \times 12$ 조각은 TBox의 12개 개념 이름에 대한 개념 대 개념 포섭 행렬입니다. 13개의 개체가 아니라 개념입니다)로 닫히며, 모든 조각이 자신의 변형별 폐쇄, 그리고 다시 재생된 고전적 오라클과 같음이 단언됩니다(gpu_fixpoint.py 365–386번째 줄과 447–477번째 줄). 커밋된 타이밍은 다음과 같습니다:

    timing, best of 5 (measured wall-clock: varies run to run, asserted NOWHERE):
      Python loop over 100 closures :   14.75 ms
      one stacked tensor pass       :    1.79 ms   (≈8.2× faster)

블록 안의 이름표 자체가 이 영수증의 일부입니다: 실제 시계(wall-clock) 밀리초는 기계마다 다르므로, 이 모듈은 의미론(칸 대 칸 오라클 동등성)을 단언하고 속도 향상은 결코 보장된 숫자가 아니라 하나의 프록시로서 보고합니다. 이것이 장난감 규모에서 확장성 주장이 취해야 할 정직한 형태이며, 다음 장의 완전한 주장 행렬이 GPU 규모의 처리량을 인용-전용으로 기록하는 이유이기도 합니다.

배치화가 결코 사 줄 수 없는 것이 바로 깊이이며, 여기서 이 아키텍처는 이 권이 IV부와 V부의 세 개 장에 걸쳐 유도한 법칙을 물려받습니다. 이를 세 개의 단으로 진술하되, 각각에 정확한 복잡도 진술과 그 출처, 그리고 컴패니언이 증명 대신 무엇을 보여 주는지를 함께 답니다. 이 전체에서 $D$ 는 포화 깊이(saturation depth), 즉 그 폐쇄가 필요로 하는 보조를 맞춘 파동의 개수이고, $L$ 은 연산자의 고정된 레이어 개수입니다. 표에는 완전한 해독보다 먼저 세 가지 표기가 등장합니다: $O(\log D)$ 는 "깊이가 많아야 $\log D$ 에 비례해 자란다"로, $\Theta(D)$ 는 "깊이가 정확히 $D$ 에 비례하며, 점근적으로 더 빠른 모양은 불가능하다"로 읽고, NC는 다항로그 깊이로 병렬화 가능한 문제들의 클래스로서, 다항 시간에 풀 수 있는 문제들의 클래스인 P와 맞세워집니다; 표 아래 문단이 두 클래스를 풀어냅니다.

단	조각	병렬 깊이	이 권이 그것을 지은 곳	장난감이 놓인 곳
1	FO-재작성 가능한 조각(DL-Lite/QL 방식 질의)	상수: 재작성된 질의 패스 한 번, 고정점 반복 0번	구체화 대 재작성	실행되지 않음(학계 TBox는 QL이 아니라 EL입니다)
2	도달 가능성 조각(원자적 포섭 사슬, 추이적·계층적 역할)	$(I \oplus A)$ 의 반복 제곱에 의한 $O(\log D)$ , $I$ 는 항등 행렬이고 $A$ 는 크리스프 도달 가능성 인접 행렬입니다(트릴레마 장의 $M$ 을 바꿔 부른 것인데, 위에서 $M$ 이 이미 소프트 인접 행렬의 이름이기 때문입니다)	작업-깊이 트릴레마	그곳에서 실행됨; 핵심부에서는 제곱이 거부됨
3	완전한 논리곱 핵심부(다중 원자 몸체, 존재 방출, 역할 교차 사슬)	$\Theta(D)$ : NC = P가 아닌 한 상수도 다항로그 평탄화도 없음	트릴레마 장의 경계 + 깊이 천장	여기: $D = 3$ 이므로 $L = 3$ 이면 충분함

수입된 진술들을 해독해 봅시다. 이 장은 그것들을 증명 없이 진술하기 때문입니다. 단 2는 추이 폐쇄가 NC²에 있다는 교과서적 결과에 의지합니다. NC²는 다항 크기이고 깊이가 입력 크기의 $\log^2$ 로만 자라는 균일한 회로족으로 풀 수 있는 문제들의 클래스입니다; 제곱 구성은 트릴레마 장에서 지어지고 연산 횟수가 셈해졌으며, 그 장은 또한 그것이 왜 단 3에서는 거부되는지도 보여 주었습니다: 논리곱 핵심부의 도출은 레이블 사실과 엣지 사실을 번갈아 오가는데, 하나의 관계를 제곱하는 것으로는 그 둘을 엮어 짤 수 없습니다. 단 3은 그 증명이 이 권의 범위를 훨씬 넘어서는 두 결과에 의지합니다. 첫째, EL 계열에서의 추론은 PTIME-완전입니다(2권의 복잡도 장이 이를 그 출처와 함께 제시했습니다), 그러므로 그것을 위한 다항로그 깊이 폐쇄가 있다면 P를 다항로그 깊이로 병렬화 가능한 문제들의 클래스인 NC로 붕괴시킬 것이며(즉 NC = P를 강제할 것이며), 이는 거짓으로 믿어집니다. 둘째, 같은 동전의 트랜스포머 쪽 면입니다: 로그 정밀도 산술로 실행되는 고정 깊이 트랜스포머는 균일한 TC⁰ 회로족으로 시뮬레이션될 수 있으며, 여기서 TC⁰은 상수 깊이, 다항 크기 문턱 회로들의 클래스입니다 [4]. 이를 종합하면: TC⁰ = P가 아닌 한, 어텐션 기반이든 아니든 어떤 로그 정밀도 고정 깊이 스택도 무한정한 $D$ 에 대한 단-3 폐쇄를 계산하지 못합니다. 그러므로 이 아키텍처의 고정- $L$ 펼침은 구현이 아니라 정리의 문제로서 절단되어 있으며, 컴패니언이 증명 대신 보여 주는 것은 절단 법칙, 즉 satori_lite.py의 커밋된 표입니다(모든 $L$ 에서 건전함이 단언됩니다, 462–476번째 줄):

[3] the truncation law — sound at every L, complete iff L ≥ D = 3
      L   Horn atoms  recall    EL atoms  recall
         23   0.000         23   0.000
         41   0.750         32   0.391
         47   1.000         41   0.783
         47   1.000         46   1.000   ← D = 3: joint task complete
         47   1.000         46   1.000

장난감의 숫자들은 정확히 단 3이 반드시 그래야 한다고 말하는 곳에 놓입니다: 재현율은 $L$ 과 함께 단조롭게 오르고, 건전성은 결코 깨지지 않으며(도출된 집합은 모든 깊이에서 참된 폐쇄의 부분집합임이 단언됩니다), 완전성은 정확히 $L = D = 3$ 에서, 즉 충돌이 안착하는 그 파동에서 도착합니다: "불가능"을 뜻하는 바닥 개념 $\bot$ 이, 완성이 그 개념에 대해 도출해 둔 레이블들의 집합인 $S(\mathrm{TenuredStudentAdvisor})$ 에 들어옵니다. 여기서 하나 더 중요한 구별이 있습니다. 성질 넷이 그것에 의존하기 때문입니다. 이 아키텍처는 두 가지 오류 방향을 동시에 지니며, 이 둘은 결코 혼동되어서는 안 됩니다: 깊이 절단은 건전하지만 불완전하며, 재현율만을, 오직 재현율만을 잃습니다; 임베딩 쪽 채점(관측되지 않은 엣지를 대입하는 소프트 인접 행렬)은 완전하지만 불건전하며, 정밀도만을, 오직 정밀도만을 잃습니다. 하나의 "정확도" 숫자는 결코 거짓말하지 않는 추론기와 때때로 거짓말하는 채점기를 뭉뚱그려 평균 내 버릴 것입니다. 보정은 이 둘을 따로 보아야 하며, 이것이 바로 네 번째 성질로 들어가는 문입니다.

성질 넷: 보정된 열린 세계 신뢰도

주장: 커널이 내놓는 정도는 장식이 아닙니다; 이는 하류의 결정이 그에 따라 행동할 수 있는 신뢰도이며, 여기에는 아무 말도 하지 않기로 하는 결정도 포함됩니다. III부에서 온 두 가지 계측 도구가 이를 채점하고, II부에서 온 하나의 유보 사항이 그 점수가 뜻하는 바의 한계를 정합니다.

첫째, 전파 그 자체입니다. 기층 하나의 구간 주석은 클레이니 방식 규칙에 의해 질의 연산자들을 관통해 흐르며, 각 면마다 구현되어 있습니다(satori_eval.py 363–371번째 줄):

    if query_dag._is_chain(q):
        lo, hi = interval_eval(q[0], typed)
        for tok in q[1]:
            if tok == N:
                lo, hi = V - hi, V - lo     # [ℓ,u] ↦ [1−u, 1−ℓ]
            else:
                lo = query_dag._project(lo, tok, query_dag.TRAIN_EDGES)
                hi = query_dag._project(hi, tok, typed)
        return lo, hi

여기서 lo와 hi는 이 구간의 크리스프 답 집합 면입니다: 하한 집합은 관측된 훈련 엣지만으로 도출되는 것이고, 상한 집합은 그래프의 어떤 허용 가능한 완성 아래에서도 여전히 가능한 것입니다( $\mathrm{train} \subseteq H \subseteq \mathrm{typed}$ 를 만족하는 임의의 $H$ 이며, $G$ 가 이미 성질 하나의 정답 행렬의 이름이므로 이 글자를 골랐습니다. 여기서 타입 완성(typed completion)은 온톨로지의 타입 서명이 허용하는 모든 엣지로, 18개의 참된 엣지 전부를 담고 있음이 단언됩니다). 증명해야 할 불변량은 이 구간의 건전성입니다: 모든 허용 가능한 완성 $H$ 에 대해 $\mathrm{LO} \subseteq [\![q]\!]_H \subseteq \mathrm{HI}$ 이며, 여기서 $[\![q]\!]_H$ 는 $H$ 위에서의 그 질의의 참된 답 집합을 뜻합니다. 증명은 질의 구조에 대한 귀납입니다. 하나의 정박점에서는 두 면이 같은 한원소 집합이고 포함 관계는 자명합니다. 투영, 교집합, 합집합은 자신의 인수 집합에 대해 단조이며, 각각은 하한 면에서는 과소 근사하는 그래프로, 상한 면에서는 과대 근사하는 그래프로 계산되므로, 두 포함 관계 모두 보존됩니다. 단조가 아닌 유일한 단계는 부정이며, 코드는 그 수선을 보여 줍니다: 여집합을 취하는 것은 포함 관계를 뒤집습니다. 하위 질의의 참된 답 $A$ 에 대해 $\mathrm{LO} \subseteq A \subseteq \mathrm{HI}$ 라면, 개체 전체 집합 $V$ 안에서 여집합을 취하는 것은 모든 포함 관계를 뒤집어 $V \setminus \mathrm{HI} \subseteq V \setminus A \subseteq V \setminus \mathrm{LO}$ 가 되므로, 부정된 구간은 자신의 면을 맞바꾸어야 합니다. 새 하한은 옛 상한에서, 새 상한은 옛 하한에서 오며, 이것이 정확히 lo, hi = V - hi, V - lo라는 줄입니다. 하니스는 아래 표로 가는 길에 있는 저장소의 모든 질의에 대해 이 불변량을 단언합니다.

둘째, 기권 규칙입니다. 이는 III부의 선택적 예측이 이 구간을 소비하는 것입니다: 개체가 하한 집합 안에 있으면(증명 가능함) YES로 답하고, 상한 집합 밖에 있으면(불가능함) NO로 답하며, 그 사이에서는, 즉 그 원자의 주석이 여전히 열린 세계의 기본값 $[0,1]$ 인 영역에서는 기권합니다. 커밋된 비교는 이를 항상 답하는 닫힌 세계 정책과 맞세웁니다:

[4] C5 — calibration + open-world abstention
  kernel degrees on the 306 imputation-needing (query, entity) pairs: ECE = 0.0186
  interval [ℓ, u]: ℓ from G_train, u from the 62-edge typed completion (⊇ all 18 true edges)
  policy                    coverage   acc-on-answered
  closed-world traversal      1.0000   0.9487   (24 errors = 23 hard answers + the 2in witness)
  interval + abstain          0.8205   1.0000   (19 yes + 365 no; abstains 84/468)

이 거래는 III부가 유도한 위험-커버리지 기하입니다: 닫힌 세계는 468개의 (질의, 개체) 결정 전부에 답하며 24번 틀립니다; 구간 정책은 그중 384개에 답하고(커버리지 $0.8205$ ), 단 한 번도 틀리지 않으며, 그라운딩할 수 없는 84개의 결정은 거부합니다. 이 거부는 소심함이 아닙니다; 이는 열린 세계의 기본값이 제 할 일을 하는 것입니다. 커밋된 증인은 질의 affiliated(dave, x) ∧ ¬affiliated(erin, x)입니다: 닫힌 세계는 cmu라고 답하고 전체 그래프 위에서 틀리는데, erin의 CMU 소속이 실재하지만 관측되지 않았기 때문입니다; 구간은 그 원자를 미지수 $[0,1]$ 로 읽어 기권하며, 이는 정확히 2권이 열린 세계라면 마땅히 그래야 한다고 말했던 그 행동입니다.

셋째, 정도 자체가 III부의 ECE 도구로 감사됩니다. 실제로 대입이 필요한 306개의 (질의, 개체) 쌍(기호적 순회로는 답할 수 없는 쌍들)에 대해, 전체 그래프 위의 정답에 맞서 채점된 커널의 괴델 정도는 $0.0186$ 의 기대 보정 오차(발표된 신뢰도와 실현된 정확도 사이의 구간-가중 평균 격차)를 냅니다(satori_eval.py 513–523번째 줄). 이 커널에서 $0.7$ 의 정도는 "약 70%의 시간 동안 옳다"에 가까운 무언가를 뜻하며, 이것이 바로 기권 임계값을 장식이 아니라 의미 있는 것으로 만들어 주는 것입니다.

그리고 이제 유보 사항입니다. II부가 그것을 얻어 냈으므로 그대로 붙입니다: 보정은 신뢰도-정확성 연결을 인증할 뿐, 개념 그라운딩을 인증하지는 않습니다; 식별 가능성이 모든 보정 주장의 배후에 서 있습니다. 완벽하게 보정된 시스템도 잘못된 개념에 대해 완벽하게 보정되어 있을 수 있습니다: 식별 가능성 장은 라벨 사상이 단사(injective)가 아닐 때마다 과제에 최적이고 잘 보정되어 있으면서도 내부가 잘못 그라운딩된 해가 존재함을 증명했으며, 어떤 ECE 숫자도 그것들을 배제할 수 없습니다. 이 장난감에서는 개념이 구성에 의해 고정되어 있으므로(기호는 학습되는 것이 아니라 주어진 것입니다), 이 유보 사항은 여기서는 아무 대가도 치르지 않습니다; 박스가 학습되는 완전한 설계에서는, 이것이 바로 열린 취약점입니다.

조립된 그림: 계측 도구를 갖춘 주장들

한 걸음 물러서면 이 설계는 스스로 그려집니다: 아래에는 두 개의 기층, 가운데에는 하나의 연산자, 그 둘레에는 네 개의 성질 블록이 있고, 성질에서 그 계측 도구로 향하는 모든 화살표에는 그 도구를 지은 이 권의 부(Part)가 이름표로 붙어 있습니다. 이 권 자체의 아키텍처가 이 시스템의 아키텍처에 그대로 비춰지며, 이는 서술의 우연이 아닙니다. 계측 도구들은 캡스톤이 자신의 숙제를 스스로 채점할 수 없도록 하기 위해 먼저 지어졌습니다.

하나의 연산자 아래 두 개의 기층, 그 둘레의 네 가지 성질, 그리고 모든 주장의 화살표가 이 권의 앞선 부(Part)가 지은 계측 도구에서 끝맺는 모습입니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

성적표를 하나의 표로 정리하면:

성질	계측 도구	지어진 곳	커밋된 영수증
학습 가능한 라우팅	심어진 규칙 프로토콜, 정확한 디코드	I부(추출 충실도)	advises∘advises에서 $\alpha = 0.9718$ ; 디코드 정확함
충실한 트레이스	소거 프로브 + MinA 포함 관계	I부(정당화, 충실성)	포괄성 8/8, 충분성 4/4, 트레이스 ⊇ MinA 2/2
병렬 규모	배치된 고정점 + 절단 법칙	IV부(GPU 추론, 작업-깊이)	하나의 스택 패스로 닫힌 100가지 변형; $L \ge D = 3$ 이면 완전함
보정된 열린 세계 신뢰도	ECE 감사 + 위험-커버리지 행	III부(보정, 기권); II부가 한계를 지음	ECE $0.0186$ ; 커버리지 $0.8205$ 에 답변 정확도 $1.000$

이 표야말로, 그 안의 어떤 개별 숫자가 아니라, 이 장의 수출품입니다. 아키텍처는 하나의 주장 집합이며, 계측 도구를 갖춘 주장이 바로 아키텍처와 홍보를 가르는 것입니다: 광고하려는 모든 성질에는 (a) 그것이 측정하는 대상과 나란히 설계되지 않았고, (b) assert가 지킬 수 있는 숫자를 내놓으며, (c) 실패할 수 있는 측정 장치가 반드시 존재해야 합니다. 위의 모든 행은 실패할 수도 있었습니다. 라우터는 cites∘advises에 집중했을 수도 있었습니다; 트레이스는 모든 MinA를 놓쳤을 수도 있었습니다; 재현율은 올라가는 길에 건전성을 깨뜨렸을 수도 있었습니다; 기권 정책은 틀리게 답했을 수도 있었습니다. 이 영수증들이 값어치를 지니는 것은 정확히 그 계측 도구들이 나쁜 소식을 되돌려줄 수도 있었기 때문입니다.

아직 풀리지 않은 부분

네 가지 성질은 개별적으로는 증거가 있지만 함께는 검토되지 않았습니다. 위의 모든 영수증은 다른 하나를 측정하는 동안 한 성질만은 그대로 붙들어 둡니다: 라우팅 실험은 주석을 끈 크리스프 특징 위에서 돌고, 보정 감사는 학습된 것이 아니라 주어진 규칙 위에서 돌며, 절단 표는 루프 안에 신경망 대입이 전혀 없는 채로 돕니다. 상호작용이야말로 실제 시스템이 실제로 살아가는 곳이며, 정확히 이 책상이 숫자를 갖고 있지 않은 곳입니다. 라우터를 훈련시키는 것이, 판별적 미세조정이 다른 곳에서 습관적으로 보정을 저하시키는 것처럼, 그를 관통해 흐르는 정도의 보정을 저하시킬까요? $D$ 보다 낮은 $L$ 에서의 절단이 트레이스를 편향시켜, 참된 정당화가 깊은 곳에서 체계적으로 얕은 도출을 기록하여, 설명의 분포는 옮겨 가면서도 충실성은 통과하게 만들까요? 상한이 타입 서명이 아니라 학습된 박스에서 올 때도 기권 규칙은 건전한 채로 남을까요? 이런 질문들에 답할 절제 행렬, 즉 네 가지 성질을 조합으로 켜고 끄는 것은 이 프로젝트의 자료 안에 하나의 계획으로만 존재할 뿐, 어디에도 결과로는 존재하지 않습니다. 그리고 그 상호작용 아래에는 위의 모든 절에서 표시해 둔 기층 간극이 놓여 있습니다: 장난감은 주어진 기호 위에서 정도를 게이팅하는 반면, 설계는 소프트 단일화를 거치는, TBox로 초기화되고, 배타성으로 정칙화되며, 전이 가능한 학습된 박스를 명시합니다. 그 둘 사이에는 정확히 열세 개의 개체를 가진 책상이 만들어 낼 수 없는 증거가 놓여 있으며, 다음 장의 주장 행렬은 자신의 어느 행이 그 증거를 기다리고 있는지 정직하게 밝힙니다.

왜 중요한가

이 장은 이 권의 논증이 스스로에게 되접힌 것입니다. I부에서 VI부까지는 서로 다른 프론티어 주제들의 순회처럼 보였습니다: 증명, 지름길, 보정, 규모 법칙, 깊이 천장, 벤치마크입니다. 여기서 조립되고 나니, 그것들은 계측 도구를 짓는 하나의 지속된 행위였음이 드러나며, 캡스톤 아키텍처는 그 완전한 도구 상자가 겨냥하는 첫 번째 시스템입니다. 자기 자신의 연구로 나아가는 독자에게, 옮겨 갈 수 있는 교훈은 시스템이 아니라 방법입니다. 다음에 어떤 아키텍처를 짓거나 검토하든, 그것이 광고하는 성질들을 세고, 그다음 그 독립적인 계측 도구들을 세십시오; 그 두 숫자 사이의 차이가 바로 그 논문 안에 담긴 홍보의 양입니다. 여기 있는 네 가지 영수증은 장난감 영수증이며, 이 장은 매 순간 그렇게 밝혀 왔습니다; 하지만 이 논증의 형태, 즉 닫힘 성질을 위해 골라진 기층, 계산에 대한 주석이 아니라 계산 그 자체인 트레이스, 주장마다 하나씩인 계측 도구, 보정자를 위해 따로 유지되는 오류 방향은 어떤 규모로도 확장됩니다. 시스템은 이 장이 신뢰를 쓰는 바로 그 방식으로 신뢰를 얻습니다: 한 번에 하나씩의 커밋된 숫자로 말입니다.

핵심 용어

기층(substrate): 연산자가 도는 하나의 표현으로, 익숙함이 아니라 닫힘 성질을 위해 선택됩니다; SATORI는 두 개를 가지며, 주석 달린 규칙 IR과 박스 어휘입니다.
주석 달린 온톨로지 IR(annotated ontology IR): EL 공리와 혼 규칙이 모두 컴파일되어 들어가는 단일 규칙 표현(CR1/CR2/CR3에 사슬 모양과 복사 모양을 더한 것)이며, 모든 원자에는 정도 슬롯이 있습니다.
구간 주석(interval annotation) $[\ell, u]$ : 양쪽으로 된 정도로, 하한은 도출 가능함을, 상한은 가능함을 뜻합니다; 열린 세계의 미지수는 전체 구간 $[0,1]$ 이며, 이는 기권을 데이터 모델의 속성으로 만듭니다.
괴델 세미링(Gödel semiring): 정도가 하나의 도출의 전제들에 대해서는 $\min$ 으로, 대안적 도출들에 대해서는 $\max$ 로 합성됩니다; 커널은 그 온도로 매끄럽게 다듬은 상을 계산하며 $\tau \to 0$ 일 때 그것을 되찾습니다.
트레이스 텐서(trace tensor): 순전파 자체가 내보내는 원자별 기록(레이어, 규칙, 아그맥스 부모)입니다; 기계로 검사 가능하며, 충실성 계측 도구가 탐침하는 대상입니다.
심어진 규칙 프로토콜(planted-rule protocol): 알려진 규칙을 숨기고, 오직 그 규칙의 답만으로 템플릿 공간 위에서 라우터를 훈련시킨 다음, 훈련된 가중치가 정확히 그 숨겨진 규칙으로 디코드되어 돌아올 것을 요구합니다.
라우터(router): 후보 규칙 몸체들에 대한 소프트맥스 분포 $\alpha$ 입니다; 라우팅된 예측은 템플릿별 커널 메시지의 $\alpha$ -혼합이며, 손으로 유도한 그래디언트 $\partial L/\partial w_i = \alpha_i (g_i - \sum_j \alpha_j g_j)$ 로 훈련됩니다.
MinA 포함 관계(MinA containment): 트레이스를 위한 충실성 표준으로, 기록된 공리 집합은 참된 최소 정당화를 포함해야 합니다; 트레이스가 최소일 필요는 없으므로 동등성이 아니라 포함 관계입니다.
3단 규모 법칙(three-tier scaling law): FO-재작성 가능한 조각에는 상수 깊이, 도달 가능성 조각에는 $O(\log D)$ , 논리곱 핵심부에는 $\Theta(D)$ 입니다; 고정- $L$ 절단은 단 3에서는 공학적 부족함이 아니라 정리 수준의 한계입니다.
두 가지 오류 방향(two error directions): 절단은 재현율만을 잃습니다(건전하지만 불완전함); 임베딩 쪽 채점은 정밀도만을 잃습니다(완전하지만 불건전함); 보정은 이 둘을 따로 감사해야 합니다.
계측 도구를 갖춘 주장(claims-with-instruments): 이 장이 수출하는 설계 규율로, 독립적이고 실패할 수 있는 측정 장치와 커밋된 숫자 없이는 어떤 성질도 광고되지 않습니다.

이 다음으로 이어지는 것

이 캡스톤에는 한 장이 남아 있으며, 그것은 결산입니다. 이 장은 네 가지 성질에 이 권의 홈그라운드에서 그 계측 도구를 붙여 주었습니다; 이 프로젝트의 논문 개요는 더 큰 행렬을 고정해 두고 있습니다. 다중 홉 응답, 규칙 학습, 충실한 트레이스, GPU 규모, 보정, 온톨로지 그라운딩, 온톨로지 간 전이, 크리스프 건전성에 걸친 여덟 개의 주장이며, 그 전부를 열세 개의 개체 위에서 정직하게 검사할 수는 없습니다. 여덟 가지 주장은 가장 큰 정직한 부분집합을 실행하여, 모든 행에 대해 이 숫자로 장난감 규모에서 검증됨 또는 인용-전용, 그리고 그 이유라고 말하는 표를 인쇄하며, "여기서는 보여 주지 않음"이라고 말할 수 없는 주장 행렬은 그저 더 긴 홍보에 불과하므로, 그 거부들을 영수증만큼이나 신중하게 다룹니다.

컴패니언 코드: examples/frontier/satori_lite.py는 커널, 두 이전 권 규칙 집합 모두로부터의 IR 컴파일, 트레이스 기록기, 그리고 절단 법칙을 구현합니다; examples/frontier/satori_eval.py는 심어진 규칙 라우터, 소거 및 MinA 교차 검사, 기권을 갖춘 구간 전파, 그리고 ECE 감사를 구현합니다; examples/frontier/gpu_fixpoint.py는 배치된 고정점을 구현합니다. 이 장의 모든 숫자를 재현하려면 각각을 examples/frontier/에서 python3로 실행하십시오; 모든 주장은 실제 시계 타이밍을 제외하고는 assert로 지켜지며, 그 타이밍은 자신의 출력이 스스로 어디에서도 단언되지 않는다고 이름표를 답니다.

이 장에서 다루는 내용​

쐐기: 저마다 다른 하나가 가진 것을 놓치는 세 계열​

기층 하나: 주석 달린 온톨로지 IR​

기층 둘: 박스, 두 작업이 공유하는 기하​

연산자와 규율​

성질 하나: 학습 가능한 라우팅, 심어진 규칙 영수증​

성질 둘: 충실한 트레이스, I부에 배선됨​

성질 셋: 병렬 규모, 법칙이 매긴 값​

성질 넷: 보정된 열린 세계 신뢰도​

조립된 그림: 계측 도구를 갖춘 주장들​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 다음으로 이어지는 것​