여덟 가지 주장: C1–C8과 쐐기

📍 현재 위치: VII부 · SATORI 캡스톤 — 20장. SATORI 아키텍처는 연산자와 그것이 도는 두 개의 기층, 그리고 트레이스 규율을 조립하고, 주장된 네 가지 성질을 네 가지 계측 도구와 짝지었습니다. 이 장은 그 장부를 이 프로그램의 완전한 계약으로 넓힙니다: 여덟 가지 주장이며, 그 각각은 무엇이든 지어지기 전에 하나의 실험으로 쓰였고, 그중 어느 것을 책상이 이미 채점할 수 있는지 말해 주는 커밋된 표입니다.

연구 프로그램은 하나의 내기이며, 내기는 그 결과가 알려지기 전에 조건이 적혀 있을 때만 뜻을 지닙니다. SATORI의 조건은 주장-실험 행렬(claims-to-experiments matrix)입니다: 번호가 매겨진 여덟 가지 주장, C1부터 C8까지이며, 구현이 시작되기 전에 각각이 자신의 실험, 기준선 계열, 지표와 함께 얼려져서, 어떤 결과도 프로그램이 "실제로 의도한" 것으로 조용히 다시 짜일 수 없게 합니다. 이 장은 그 행렬로 두 가지 일을 합니다. 첫째, 열세 개체짜리 책상이 평가할 수 있는 가장 큰 정직한 부분집합을 평가합니다: 컴패니언의 satori_eval.py는 C1, C2, C3, C5, C8에 대해 실제 숫자를 커밋하고, C4, C6, C7은 여기서 채점될 수 없는 이유와 함께 인용-전용(cited-only)으로 인쇄합니다. 둘째, 쐐기(wedge)를 조립합니다: 여덟 가지 주장이 함께 설계 공간의 한 모서리, 즉 어떤 기존 계열도 차지하지 않은 모서리를 가리킨다는 관련 연구 논증이며, 이는 이 프로그램이 존재해야 할 이유이자, 냉정하게 읽으면 그 이상은 결코 아닙니다. 이 장의 중심은 산문이 들려주는 이야기가 아니라 코드가 인쇄하는 표입니다.

쉽게 말하면

매 샷을 치기 전에 정확히 어떤 공이 정확히 어떤 포켓에 들어갈지를 미리 선언하는 당구 선수를 상상해 보십시오. 선언된 대로 들어간 샷만 점수로 인정되고, 아무리 멋져 보여도 요행으로 들어간 공은 인정되지 않습니다. 이제 그 선수가 경기 전에 여덟 개의 선언된 샷을 나열한 점수표를 여러분에게 건네고, 그중 세 개 옆에는 이런 메모가 붙어 있다고 상상해 보십시오: "이 테이블에서는 시도할 수 없음; 필요한 테이블은 이것임." 그 점수표가 바로 이 장입니다. 여덟 가지 주장이 선언된 샷이고, 커밋된 평가 스크립트는 그것들이 들어갔는지 빗나갔는지를 지켜본 심판이며, 세 개의 정직한 메모는 이 책상이 갖고 있지 않은 하드웨어나 규모나 두 번째 온톨로지가 필요한 주장들입니다. 이 모든 것을 신뢰할 수 있게 만드는 것은 사건들의 순서입니다: 선언이 먼저 왔다는 것입니다.

이 장에서 다루는 내용

• 계약으로서의 주장: 연구 프로그램이 무엇이든 짓기 전에 왜 자신의 주장-실험 행렬을 공개해야 하는지, 그리고 여덟 가지 주장이 하나씩, 각각 한 문장으로, 그 지표와 기준선 계열의 이름과 함께 진술되는 것을 다룹니다.
• 평가 하니스: satori_eval.py가 이 권의 앞선 각 부(Part)에서 나온 계측 도구 하나씩을 그것이 채점하는 주장에 배선하는 방식과, 모든 행에 장난감 규모에서 검증됨 또는 인용-전용이라는 도장을 찍는 정직성 플래그 메커니즘을 다룹니다.
• 채점된 다섯 가지 주장, 전문으로 읽기: C1의 커밋된 MRR(mean reciprocal rank, 평균 역순위)과 그 재현율이 실제로 어디서 나오는지, 라우터 그래디언트를 단계별로 유도한 C2의 심어진 규칙 복원, 기호적 기둥이 요구하는 건전성 쌍으로서의 C3과 C8, 그리고 II부의 식별 가능성 유보 사항이 함께 붙은 C5의 보정과 기권 숫자를 다룹니다.
• 세 가지 인용-전용 주장: C4, C6, C7이며, 각각 책상 규모에서 채점될 수 없는 이유가 인쇄되어 있고, 독자가 미래의 결과를 심사할 수 있을 만큼 정밀한 증거 계획이 함께 붙어 있습니다.
• 쐐기: 어느 모서리를 쥐고 있는지에 따라 표로 정리된 세 개의 관련 연구 계열, 여덟 가지 주장이 사상되는 빈 연언, 그리고 쐐기란 기회 논증일 뿐 결코 결과가 아니라는 냉정한 읽기를 다룹니다.

계약으로서의 주장

코드를 한 줄도 쓰기 전에 왜 주장 행렬을 얼려 두어야 할까요? 세 가지 이유가 있으며, 각각은 이 분야가 대체로 결여하고 있는 규율입니다. 반증 가능성: 이름 붙은 지표와 이름 붙은 기준선을 지닌 주장은 질 수 있습니다. "어텐션 연산자는 다중 홉 질의에 경쟁력 있게 답한다"는 구호이지만, "질의 유형별 필터링된 MRR을 질의 임베딩 기준선 계열에 맞세운다"는 특정 숫자가 반박할 수 있는 내기입니다. 범위 규율: 행렬은 어떤 증거가 셈해질지를 미리 정해 두므로, 유망한 부수적 결과가 슬며시 헤드라인으로 흘러들 수 없고 실망스러운 주된 결과가 소거법으로 강등될 수도 없습니다. 모든 실험은 번호가 매겨진 주장을 섬기거나, 아예 실행되지 않습니다. 심사자 공정성: 행렬을 손에 쥔 독자는 사후에 재구성된 조건이 아니라 프로그램 자신이 진술한 조건에 맞서 논문을 감사할 수 있습니다. SATORI의 개요는 이 규칙을 한 문장으로 진술합니다: 모든 주장은 구현에 앞서 실험, 기준선 집합, 지표에 사상되어야 하며, 그래서 어떤 실험도 낭비되지 않는다는 것입니다.

다음이 그 여덟 가지이며, 각각 한 문장으로, 행렬이 이름 붙이는 지표와 기준선 계열과 함께 적습니다. C1(다중 홉 응답): 기호적 어텐션 연산자는 다중 홉 EPFO 질의(존재 긍정 1차 질의: 투영, 교집합, 합집합)에 질의 임베딩 계열만큼 경쟁력 있게 답하며, Query2Box, BetaE, GQE, GNN-QE/CQD 계열에 맞서 질의 유형별 필터링된 MRR과 Hits at 1, 3, 10으로 측정됩니다 [1]. C2(규칙 학습): 어텐션 라우팅은 규칙 공간을 열거하지 않고도 올바른 규칙을 학습하며, Neural-LP, TensorLog, DRUM, NTP/GNTP의 미분 가능한 규칙 채굴 계열에 맞선 규칙 정밀도와 재현율, k에서의 복원율로 측정됩니다 [2]. C3(충실한 증명): 이산화된 증명 트레이스는 참된 최소 정당화로 재검증되며, 소거 충분성과 포괄성, 그리고 어텐션-롤아웃과 그래디언트-현저성 설명기에 맞선 증명-검증률로 측정됩니다 [3]. C4(처리량): GPU 배치 추론은 CPU 기호 엔진을 이기며, PyReason, Scallop, DeepProbLog에 맞선 초당 질의 수, 지연 시간, 메모리 규모 곡선으로 측정됩니다. C5(보정과 기권): 구간 주석은 보정된 신뢰도와 유용한 기권을 낳으며 추론 지름길에 견고하고, 온도 스케일링을 갖춘 평범한 소프트맥스 헤드에 맞선 ECE(기대 보정 오차), 위험-커버리지 곡선, 지름길-비율 프로브로 측정됩니다 [4]. C6(그라운딩이 돕는다): 온톨로지 그라운딩은 응답을 측정 가능하게 개선하며, 시스템 자신의 그라운딩 없는 변형에 맞선 온/오프 소거 실험에서의 MRR 변화로 측정됩니다. C7(전이): 학습된 추론은 온톨로지를 가로질러 제로샷과 퓨샷으로 전이하며, 온톨로지별로 재훈련된 기준선(그중에서도 으뜸은 RRN)에 맞선 전이 상태의 MRR로 측정됩니다. C8(크리스프 건전성): 온도가 사라짐에 따라 고전적 건전성이 되찾아지며, ELK나 HermiT 같은 기준 EL 추론기와 데이터로그 최소 고정점에 맞선 함의 일치(정밀도와 재현율)로 측정됩니다.

이 문장들의 결을 눈여겨보십시오. 어느 것도 "우리 시스템은 해석 가능하다"거나 "우리 시스템은 확장 가능하다"고 말하지 않습니다. 각각은 측정될 양, 이겨야 할 계열, 그리고 암묵적으로 실패할 수도 있는 실험의 이름을 붙입니다. 그 결이야말로 이 장의 나머지를 가능하게 만드는 것입니다: 여덟 문장 가운데 다섯은, 이 권이 이미 짓고 검증해 둔 계측 도구로 무장한 열세 개체짜리 지식 베이스가 오늘 당장 채점할 수 있을 만큼 정밀합니다.

계약과 그 채점: 여덟 가지 사전 등록된 주장 가운데 다섯은 앞선 부(Part)에서 지어진 계측 도구로 채점되고, 셋은 인쇄된 이유와 함께 인용-전용으로 표시되며, 쐐기는 어떤 기존 계열도 쥐지 못한 모서리의 이름을 붙입니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

하니스: 이 권의 도구 상자, 낱낱이 열거하기

이 평가 스크립트는 일부러 독창적이지 않습니다. satori_eval.py는 거의 아무것도 짓지 않습니다. 그것은 배선할 뿐입니다. 그 도구 상자가 곧 이 권의 것입니다: 기호 어텐션에서 온 커널과 그 두 고전적 오라클(satori_lite이며, 이 자신이 1권의 전방 연쇄기와 2권의 EL 완성을 임포트합니다), I부의 정당화 장에서 온 최소 정당화 오라클(justifications.py, Reiter의 적중 집합 트리), I부의 충실성 장을 따라 인라인으로 다시 적용된 소거 프로토콜, III부의 보정 장에서 임포트한 ECE 도우미와 맞춰진 온도(calibration.py), III부의 기권 장을 따라 인라인으로 다시 구현된 기권 정책, 그리고 4권의 필터링된 순위 프로토콜을 갖춘 36개짜리 질의 은행(부정이 없는 아홉 가지 EPFO 유형에 부정을 지닌 다섯 가지 유형을 더한 것; query_dag.py, cqd.py)입니다. 여기서 어떤 주장을 채점하는 모든 계측 도구는 SATORI가 아닌 시스템에 맞서 앞선 장에서 지어지고, 유도되고, 커밋된 것입니다. 이 하니스의 유일한 구조적 발상은 정직성 플래그(honesty flag)입니다: 그것이 인쇄하는 주장 표에는 상태 열이 있으며, 모든 행에는 커밋된 숫자를 증거로 지닌 장난감 규모에서 검증됨(toy-verified), 아니면 이 규모에서 채점이 불가능한 이유를 지닌 인용-전용(cited-only) 가운데 하나가 도장으로 찍힙니다. 그 표는 산문이 아니라 코드 안의 데이터입니다(satori_eval.py 628–649번째 줄):

    rows = (
        ("C1 multi-hop EPFO answering", "toy-verified",
         f"MRR {mrr['godel']['mrr']:.3f} vs random {mrr['random']['mrr']:.3f}"
         " / oracle 1.000"),
        ("C2 router learns rules", "toy-verified",
         f"advises∘advises recovered, α = {out['alpha'][out['top']]:.3f}, "
         "exact decode"),
        ("C3 faithful proof traces", "toy-verified",
         f"comp {out['n_broke']}/{out['n_del']}, suff 4/4, trace ⊇ MinA 2/2"),
        ("C4 GPU-batched scalability", "cited-only",
         "proxy gpu_fixpoint.py; needs PyReason/Scallop at scale"),

모든 증거 문자열은 run() 함수가 불과 몇 초 전에 계산하고 단언해 둔 변수를 보간합니다. 어떤 숫자의 회귀든 표가 인쇄되기 전에 실행을 깨뜨립니다. 채점되는 세계는 이 시리즈 전체가 실어 온 바로 그 세계입니다: 13개의 개체, 18개 엣지짜리 전체 그래프 안에 든 15개 엣지짜리 훈련 그래프, 그리고 14개 질의 유형에 걸친 36개짜리 질의 은행입니다. 헤더는 그 범위와 평결의 분할을 미리 진술합니다:

SATORI-eval: the eight claims at toy scale (honest subset of the claims matrix)
  world  : 13 entities; G_train 15 ⊂ G_full 18 edges; bank 36 queries / 14 types
  claims : C1/C2/C3/C5/C8 toy-verified below; C4/C6/C7 cited-only (see the table)

그 헤더 안의 한 어구는 무게를 지닐 자격이 있습니다: 정직한 부분집합입니다. 이 장의 그 무엇도 벤치마크 규모의 증거가 아니며, 하니스는 결코 그렇지 않은 척하지 않습니다. 책상이 세울 수 있는 것은, 그 메커니즘이 존재하고 낱낱이 검사할 수 있을 만큼 작은 세계 위에서 주장된 대로 행동한다는 것입니다. 책상이 세울 수 없는 것에는 이름이 붙어 있습니다.

C1 전문: 질의 은행 위의 커널

C1은 건전성을 위해 지어진 연산자가 응답도 할 수 있는지를 묻습니다: 커널을 폐쇄까지가 아니라 질의의 계산 DAG를 따라 돌리고, 질의-임베딩 문헌이 표준화한 프로토콜 아래에서 채점하는 것입니다 [1]. 그 평가기는 서른 줄입니다(satori_eval.py 119–151번째 줄): 앵커 개체는 13개 개체에 대한 원-핫 정도 벡터가 되고, 역할 $r$을 따르는 투영은 커널 자신의 메시지 패스입니다. $v'[t] = \mathrm{softmax}_h\, \mathrm{softmin}(v[h],\, M_r[h,t])$(이렇게 읽으십시오: 개체 $t$는 어떤 원천 $h$가 활성이면서 동시에 연결되어 있는 정도만큼 도달되며, softmax는 대안적인 원천들을 병합하고 softmin은 "활성"과 "연결됨"을 논리곱합니다), 교집합은 softmin이고 합집합은 softmax입니다. 여기서 $M_r \in [0,1]^{13 \times 13}$은 역할 $r$에 대한 소프트 인접 행렬로, 그 항목 $M_r[h,t]$가 엣지 $r(h,t)$의 정도인 행렬이고, $v \in [0,1]^{13}$은 진행 중인 답 정도 벡터입니다. 이 장 앞의 장이 $M$을 지었습니다: 3권의 ComplEx 점수 $s$(차원 $d = 16$짜리 임베딩에서 나온 것)를 보정된 시그모이드 $\sigma(s/\tau^\ast)$로 읽어 내되, 여기서 $\tau^\ast = 1.4172$는 III부의 맞춰진 온도이며, 관측된 모든 훈련 엣지를 정확히 $1.0$으로 고정한 것입니다(satori_eval.py 102–116번째 줄).

어떤 소프트 숫자도 신뢰받기 전에, 하니스는 먼저 크리스프 다리를 돌립니다: 사라지는 온도에서 하드 0/1 훈련 인접 행렬 위에서, 임계값을 매긴 커널은 부정을 포함한 14개 유형 전부의 36개 질의 모두에서 기호 실행기의 답 집합을 정확히 되돌려야 합니다(424–431번째 줄, 통계가 아니라 단언입니다). 그다음에야 소프트 순위 매김이 돌아갑니다. 그 지표는 필터링된 MRR(filtered mean reciprocal rank, 필터링된 평균 역순위)입니다: 각 하드 정답, 즉 18개 엣지짜리 전체 그래프 위에서는 그 질의에 답하지만 15개 엣지짜리 훈련 그래프의 어떤 순회로도 도달할 수 없는 개체에 대해, 후보 목록에서 다른 참된 정답들을 제거한 채 모든 개체를 정도로 순위 매기고, 그 하드 정답의 순위의 역수를 취해 평균 냅니다. 기호로 적으면, $H$를 (질의, 하드 정답) 쌍의 집합이라 하고 $\mathrm{rank}(q,a)$를 필터링된 순위라 할 때,

$$\mathrm{MRR} \;=\; \frac{1}{|H|} \sum_{(q,a)\, \in\, H} \frac{1}{\mathrm{rank}(q,a)}, \qquad |H| = 17$$

이는 부정이 없는 아홉 개의 질의 유형에 걸친 것입니다. 아래 표의 두 가지 레이블에는 열쇠가 필요합니다. 커널 행에 Gödel이라고 적힌 것은 이 실행이 앞 장의 기본값인 min/max 의미론, 곧 softmin을 논리곱으로, softmax를 논리합으로 쓰기 때문입니다. 유형별 코드는 4권의 이름 짓기이며 숫자-다음-연산으로 읽습니다: 1p, 2p, 3p는 한 홉, 두 홉, 세 홉짜리 투영 사슬이고, 2i와 3i는 2원과 3원 교집합이며, pi는 투영이 교집합으로 이어지는 것, ip는 교집합이 투영으로 이어지는 것, 2u는 2원 합집합, up은 합집합이 투영으로 이어지는 것입니다. 커밋된 표는 다음과 같습니다:

[1] C1 — the kernel answers the EPFO bank (filtered MRR, 17 hard answers, 9 ¬-free types)
  τ→0 sanity: thresholded kernel == symbolic executor on all 36 queries (asserted)
  adjacency: M = σ(s/τ*) over ComplEx scores, τ* = 1.4172 (calibration.py); TRAIN edges pinned to 1
  G_train traversal (symbolic)    0.1488   0 on every hard answer BY DEFINITION
  random scorer (seed 0)          0.2301   the uninformed floor
  SATORI kernel (Gödel, τ=0.01)   0.5680   the C1 number
  G_full oracle                   1.0000   ceiling; the honest gap is real
  kernel per type: 1p 0.538  2p 0.538  3p 0.545  2i 0.583  3i 0.750  pi 0.667  ip 0.111  2u 0.600  up 0.550

이제 $0.568$이라는 정직한 위치를 봅시다. 이는 리더보드 항목이 아니며, 표의 세 가지 특징이 그것을 말해 줍니다. 첫째, 바닥이 높습니다: 후보 개체가 13개뿐이므로 무작위 순위 매김조차 이미 $0.230$을 벌며, 그래서 장난감 MRR은 수만 개의 후보에 대해 계산된 벤치마크 MRR과 결코 비교되어서는 안 됩니다. 둘째, 하니스는 단순한 승리가 아니라 창(window)을 단언합니다: 커널은 무작위 바닥을 적어도 $0.25$만큼, 순회 기준선을 적어도 $0.30$만큼 이겨야 하며, 동시에 $0.8$ 아래에 머물러야 합니다(448–450번째 줄). $d=16$짜리 장난감 대입기에서 오라클에 가까운 점수가 나온다면 그것은 뛰어남이 아니라 누출을 신호할 것이기 때문입니다. 셋째, 유형별 행은 재현율이 어디서 나오고 어디서 죽는지를 보여 줍니다: 순수하게 기호적인 순회는 정의상 모든 하드 정답에 0점을 주므로(하드 정답이란 정확히 순회가 도달할 수 없는 것입니다), 커널의 $0.568$의 모든 점수는 커널 자신의 대수 안에서 제외해 둔 엣지를 대입하는 보정된 신경망 인접 행렬이 기여한 것입니다. 그리고 가장 약한 칸인 ip의 $0.111$은 교집합이 투영보다 앞서 오는 유형이므로, 교집합에 들어온 대입 오류가 평균으로 상쇄되는 대신 그대로 전파됩니다. 장난감이 보여 줄 수 있고 실제로 보여 주는 것은 메커니즘입니다: 두 개의 고전적 폐쇄를 되찾는 바로 그 커널이 조금도 바뀌지 않은 채, 그 신경망 절반을 잎 행렬에만 가두고서도 합성 질의에 어쨌든 답한다는 것입니다. 같은 메커니즘이 기준선 계열 자신의 벤치마크에서 경쟁력이 있는지는 정확히 행렬이 말하는 그대로입니다: 규모에서의 실험을 기다리는 하나의 주장입니다.

C2 전문: 심어진 규칙과 라우터 그래디언트

C2는 학습 가능성 주장이며, 가장 깔끔한 프로토콜로 채점됩니다: 규칙 하나를 숨긴 다음, 훈련이 그것을 정확히 복원하는지 검사하는 것입니다. 숨겨진 규칙은 1권의 grandAdvisor(x,z) ← advises(x,y) ∧ advises(y,z)입니다. 가설 공간은 5개의 기본 역할에 대한 길이 2짜리 역할 사슬 전부입니다: $25$개의 템플릿이며, 템플릿 $k = (r,s)$는 "$r$ 다음에 $s$"를 뜻합니다. 각 템플릿에 대해 하니스는 전체 그래프 위에서 커널의 사슬 메시지를 미리 계산합니다. $C_k[x,z] = \mathrm{softmax}_y\, \mathrm{softmin}(A_r[x,y],\, A_s[y,z])$이며, 여기서 $A_r$과 $A_s$는 전체 18개 엣지 그래프에 대한 역할 $r$과 $s$의 크리스프 0/1 인접 행렬(C1의 소프트 $M_r$의 하드 짝)입니다: 템플릿마다 하나씩인 $13 \times 13$ 행렬로, 훈련에 대해서는 상수입니다(satori_eval.py 166–179번째 줄). 이는 미분 가능한 규칙 채굴 계열이 도입한 사슬 규칙의 경로-행렬 읽기이며, 25개의 템플릿이 책상에 올라갈 만큼 작기에 여기서는 템플릿마다 사전 계산됩니다 [2]. 훈련 가능한 대상은 오직 라우터뿐입니다: 템플릿마다 실수 하나씩인 로짓 벡터 $\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]$. 지도는 최소한이며 규칙과 무관합니다: 격자 $G \in \lbrace 0,1 \rbrace^{13 \times 13}$은 1권의 폐쇄에서 나온 정확히 3개의 참된 grandAdvisor 쌍에는 $1$을, 그 밖에는 $0$을 지닙니다(454–458번째 줄). 라우터는 규칙도, 템플릿 레이블도, 트레이스도 결코 보지 않습니다; 그것이 보는 것은 답뿐입니다.

손실은 전체 $N_{\text{cells}} = 13 \times 13 = 169$개 칸에 대한 평균 교차 엔트로피이며(칸의 개수에 자기만의 기호를 주어 인접 행렬 $M$과 충돌하지 않게 합니다), 각 로그 안에는 유한하게 유지하기 위한 보호 장치 $\varepsilon = 10^{-6}$이 들어갑니다:

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

그래디언트는 손으로 세 개의 고리로 유도됩니다. 이 장이 커밋하는 수학을 스스로 소유하기 때문입니다. 첫째 고리, 손실에서 예측으로: $L$의 각 항을 그것이 언급하는 단 하나의 칸 $P_{xz}$에 대해 미분하면, $\frac{\partial}{\partial P}\ln(P+\varepsilon) = \frac{1}{P+\varepsilon}$이고 $\frac{\partial}{\partial P}\ln(1-P+\varepsilon) = \frac{-1}{1-P+\varepsilon}$이므로,

$$\frac{\partial L}{\partial P_{xz}} \;=\; -\frac{1}{N_{\text{cells}}}\left[ \frac{G_{xz}}{P_{xz}+\varepsilon} \;-\; \frac{1-G_{xz}}{1-P_{xz}+\varepsilon} \right].$$

둘째 고리, 예측에서 어텐션으로: $P_{xz}$는 계수 $C_k[x,z]$를 지니고 $\alpha_k$에 대해 선형이므로, 연쇄 법칙은 그 어텐션이 건드리는 모든 칸에 대해 합을 냅니다,

$$g_k \;\equiv\; \frac{\partial L}{\partial \alpha_k} \;=\; \sum_{x,z} \frac{\partial L}{\partial P_{xz}}\, C_k[x,z].$$

셋째 고리, 어텐션에서 로짓으로, 소프트맥스 야코비안 $\frac{\partial \alpha_j}{\partial w_i} = \alpha_j(\delta_{ij} - \alpha_i)$을 통해서입니다. 여기서 $\delta_{ij}$는 크로네커 델타로, $i = j$일 때 $1$이고 그 밖에는 $0$입니다(3권의 어텐션 장이 몫의 법칙으로 이 항목을 유도했습니다). 이를 $g$에 맞서 축약하면:

$$\frac{\partial L}{\partial w_i} \;=\; \sum_j g_j\, \alpha_j (\delta_{ij} - \alpha_i) \;=\; g_i \alpha_i \;-\; \alpha_i \sum_j \alpha_j g_j \;=\; \alpha_i \Big( g_i - \bar{g} \Big), \qquad \bar{g} \equiv \sum_j \alpha_j g_j,$$

여기서 첫 번째 등식은 그 델타에서 합을 쪼갠 것이고($\delta_{ij}$ 항에서는 오직 $j=i$만이 살아남습니다), 두 번째 등식은 $\alpha_i$를 인수로 뽑아낸 것입니다. 이 닫힌 형식은 어텐션 기반 규칙 학습의 전체 이야기를 한 줄로 담습니다: 각 템플릿의 로짓은 자신의 현재 어텐션에, 그 그래디언트 신호 $g_i$가 어텐션 가중 평균 $\bar{g}$보다 얼마나 더 나은지를 곱한 만큼 움직입니다. 현재의 혼합보다 답을 더 잘 설명하는 템플릿은 어텐션을 자신 쪽으로 끌어당기고, 나머지는 쇠퇴합니다. 커밋된 코드는 이 대수를 그대로 옮긴 것입니다(satori_eval.py 195–202번째 줄):

    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))
    return L, gw, alpha

신뢰하되 검증하라: 훈련에 앞서 하니스는 균등한 라우터에서 이 손 그래디언트를 25개 좌표 전부에 대한 중심 유한차분과 비교하여 $10^{-8}$ 아래의 일치를 요구합니다(460–466번째 줄). 그런 다음 평범한 경사 하강, $\mathbf{w} \leftarrow \mathbf{w} - \eta\, \partial L/\partial \mathbf{w}$을 학습률 $\eta = 5.0$으로, $\mathbf{w} = \mathbf{0}$(모든 템플릿이 $\alpha_k = 1/25 = 0.04$인 상태)에서 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)

이 트레이스를 회의적인 눈으로 읽어 봅시다. 손실이 낮게 시작하는 것($0.0730$)은 $G$가 169개 칸 가운데 3개의 양성만을 지니고 있어서, 균등한 혼합조차 어디서나 작은 값을 예측함으로써 대체로 옳기 때문입니다. 유의미한 사건은 손실이 떨어지는 것이 아니라 어텐션이 advises∘advises에 $0.04$에서 $0.9718$까지 집중하는 것이며, 차점자는 $0.0012$에 머뭅니다. 그리고 통과 조건은 단지 높은 어텐션만이 아닙니다(승자에 대한 $\alpha > 0.9$ 보호 단언도 있습니다, 472번째 줄); 결정적인 검사는 정확한 디코드입니다: IR(intermediate representation, 중간 표현) 규칙으로 재구성된 아그맥스 템플릿은 숨겨진 지식 베이스 규칙에서 compile_horn이 만들어 내는 것과 튜플 하나하나까지 같아야 합니다(467–471번째 줄). 여기서의 복원은 유사도 점수가 아니라 구문적 동일성입니다.

이제 이 주장의 실제 내용을, 정직하게 한계 지어 봅시다. 대조 부류의 가설 공간은 길이 한계까지의 사슬 규칙이며, 그 한계에 대해 지수적인 공간입니다; Neural-LP와 DRUM 계열은 그것을 실체화하는 일을 피하지만(Neural-LP는 관계 연산자에 대한 순환 어텐션으로, DRUM은 규칙-신뢰도 텐서의 저계수 인수분해로), 그 탈출의 대가로 사슬 전용 규칙 모양, 엄격한 길이 상한, 약한 체계적 일반화를 치르며, 이것이 그 계열 스스로가 인정하는 벽입니다; NTP는 증명 경로를 말 그대로 열거하는 구성원입니다 [2]. 25개의 템플릿에서 이 장난감은 그 시스템들이 일부러 인수분해하는 공간을 그냥 실체화합니다; 그 밖의 어떤 것도 정직하게 인정할 수 없을 것입니다. 그러므로 책상이 검증하는 것은 복원 메커니즘입니다: 커널 자신의 softmin/softmax 대수를 관통하는 경사 하강이 심어진 규칙 위에 라우터를 집중시키고 그것을 정확히 디코드합니다. C2가 규모에서 주장하는 바는 이보다 더 강하며 여기서는 증명되지 않은 채로 남습니다: 탐색 없는 귀납(search-free induction)이며, 열거하기에는 너무 큰 구조화된 템플릿 공간 위에서 라우팅하되 커널의 대수가 열거를 대신하는 것입니다. 통제 가능한 깊이, 분기, 잡음을 지닌 행렬의 합성 온톨로지 실험들이 바로 그 조항이 채점받는 곳입니다.

C3과 C8: 건전성 쌍

두 가지 주장이 이 프로그램의 정체성을 붙들어 매며, 그 숫자를 읽기 전에 왜 그런지 말해 둘 가치가 있습니다. C3과 C8을 벗겨 내면 SATORI는 어텐션 지도를 지닌 또 하나의 신경망 질의 응답기일 뿐입니다; 그것들을 지키면 학습한 추론기가 됩니다: 신경망 절반이 무엇을 하든, 크리스프 극한은 고전적 폐쇄(C8)이고 도출 기록은 검사 가능한 증명(C3)입니다. 이들은 기호적 기둥의 보증이며, 신경망 기둥에게 지키라고 요구되는 바로 그것들입니다. 이들은 또한, 우연이 아니게도, 장난감 규모에서 채점하기에 행렬 가운데 가장 값싼 행이기도 합니다. 그 이유는 하나의 구조적인 것입니다: 오라클이 존재하기 때문이며, 이 시리즈가 그것들을 지었기 때문입니다. 1권의 전방 연쇄기는 정확한 혼 폐쇄를 계산하고, 2권의 완성 알고리즘은 정확한 EL 폐쇄를 계산하며, I부의 justifications.py는 Reiter의 적중 집합 트리로 모든 최소 정당화를 열거합니다. 어떤 주장을 검증하는 값은 정확히 그 근거 진실을 계산하는 값만큼 싸며, 이 둘에 대해서는 근거 진실이 열세 개체에서 풀린 문제입니다.

C8이 먼저 채점됩니다. 다른 모든 것이 그 위에 서 있기 때문입니다. 하니스는 앞선 장들의 단언 모음 전체를 다시 호출하여 그 핵심 등식들을 다시 검사합니다(satori_eval.py 417–419번째 줄):

    sat = satori_lite.run()
    assert len(sat["closure"]) == 47 and len(sat["el_closure"]) == 46
    assert sat["recall"][3][0][1] == sat["recall"][3][1][1] == 1.0  # L ≥ D = 3

해독하면: 사라지는 온도에서 임계값을 매긴 커널 상태는 집합으로서 47개 원자짜리 혼 폐쇄와 46개 원자짜리 EL 폐쇄와 같으며, 재현율은 공동 포화 깊이인 $L = 3$에서 정확히 $1.0$에 이릅니다. 이것이 바로 기준 추론기들에 맞선 함의 일치가 정밀도와 재현율 $1.0$을 이루는 것, 곧 행렬의 C8 지표이며, 남김없는 일치를 검사할 수 있는 유일한 지식 베이스 위에서입니다. 주장 표의 행은 이를 Horn 47/47, EL 46/46, complete iff L ≥ 3으로 압축합니다.

C3은 두 개의 독립적인 계측 도구로 채점됩니다. 실행 예제의 각 면마다 하나씩입니다. 첫 번째는 I부의 소거 프로토콜 [3]을 결정론적 추론기에 맞게 강화한 것입니다: ERASER는 근거 전체를 지우고 신뢰도가 떨어지는 것을 지켜보지만, 여기서는 트레이스가 인용하는 각 사실을 하나씩 지웠을 때 그 삭제 하나하나가 결론을 깨뜨려야만 포괄적으로 채점되고(사실별 필요성, 곧 정당화 장의 조건입니다), 인용된 사실만으로도 결론을 다시 도출할 수 있으면 충분한데, 이 절은 ERASER의 형태 그대로입니다. 하니스는 네 개의 도출된 원자의 트레이스가 지닌 바닥 사실 잎들을 모은 다음, 모델은 그대로 둔 채 사실들을 입력에서 0으로 만들고 커널을 다시 실행합니다(satori_eval.py 237–251번째 줄). 두 번째 계측 도구는 I부의 정당화 오라클입니다: 모든 컴파일된 규칙이 자신을 만들어 낸 원래 공리를 기억하도록 EL 인스턴스를 다시 지은 다음(290–319번째 줄), 어떤 포섭의 이산화된 트레이스를 그 도출 트리 어디엔가 나타나는 공리 식별자들의 집합으로 읽고, 이 집합이 적중 집합 트리가 찾아낸 참된 MinA, 즉 그 포섭을 함의하는 부분집합-최소 공리 집합을 포함할 것을 요구합니다. 두 평결 모두 커밋됩니다:

[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)
  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})

8개의 잎 삭제 하나하나가 그 원자를 죽이고, 잎만으로 4개의 원자 전부를 다시 도출하며, 트레이스에 없는 사실들에 대한 12번의 시드가 붙은 통제 삭제는 아무것도 바꾸지 않습니다: 포괄성과 충분성 모두 $1.0$이며, I부가 평범한 어텐션 가중치는 실패한다고 보여 준 바로 그 프로토콜에 맞선 것입니다. TBox 면에서는 앞 장이 고정하고 이 장도 지키는 표현에 주목하십시오: 트레이스는 MinA를 포함할 뿐, 그것과 같을 필요는 없습니다. Professor ⊑ Researcher는 두 개의 MinA를 지니며, 트레이스는 아그맥스에서 이긴 도출이 무엇이든 그것을 싣습니다; 충족 불가능성 증명은 마침 그 자신의 유일한 MinA이므로, 그곳에서는 포함 관계가 곧 동등성입니다. 행렬의 C3 문장, "이산화된 증명 트레이스는 참된 최소 정당화로 재검증된다"는 여기서 정밀한 형태로 채점됩니다: 인증된 최소 증명은 오라클의 출력과의 교집합을 통해 트레이스에서 추출될 수 있는데, 트레이스가 증명 가능하게 그것 하나를 덮고 있기 때문입니다(505–510번째 줄). 진술하기 값싸고, 검사하기 값싸며, 이것이야말로 이 프로그램에서 "충실한"이라는 단어가 그저 어떤 분위기가 아니라 정리 모양의 주장인 온전한 이유입니다.

II부의 유보 사항이 붙은 C5

C5는 세 개의 절을 지닙니다: 주석은 보정되어 있고, 기권을 지지하며, 그 패키지는 추론 지름길에 견고합니다. 책상은 처음 둘을 채점하며, 셋째를 채점할 수 없는 이유에 대해 정직하게 말할 것이 있습니다.

먼저 보정입니다. 커널의 질의 정도는 신뢰도로 읽히며, III부의 계측 도구인 기대 보정 오차로 채점됩니다 [5]: $N$개의 예측을 $B$개의 동일 너비 신뢰도 구간으로 정렬하고, $\mathrm{ECE} = \sum_{b=1}^{B} \frac{n_b}{N}\, \lvert \mathrm{acc}(b) - \mathrm{conf}(b) \rvert$를 계산합니다. 여기서 $n_b$는 구간 $b$ 안의 예측 개수를 세고, $\mathrm{acc}(b)$는 그 가운데 참인 것의 비율이며, $\mathrm{conf}(b)$는 그것들의 평균 진술 신뢰도입니다; 0이라는 것은 진술된 숫자가 정직한 빈도라는 뜻입니다. 모집단은 실제로 대입이 필요한, 즉 그 개체가 아직 순회로 답해지지 않은 모든 (질의, 개체) 쌍입니다: 부정이 없는 아홉 개 유형에 걸친 306개 쌍이며, 그 가운데 정확히 17개의 하드 정답이 참입니다(satori_eval.py 513–523번째 줄). 커밋된 숫자는 $\mathrm{ECE} = 0.0186$으로, 단언된 $0.05$ 기준 아래입니다; 여기서 커널의 정도는 사용 가능한 신뢰도이며, 그 공은 대체로, 온도 스케일링 [4]으로 맞춰져 이미 인접 행렬 안에 들어 있는 III부의 온도 $\tau^\ast$에 돌아갑니다.

기권이야말로 아키텍처의 구간 주석이 제 몫을 하는 곳입니다. 모든 질의는 답 집합 쌍 $[\ell, u]$으로 두 번 평가됩니다: 하한 집합은 관측된 훈련 엣지만으로부터(무엇이 도출 가능한지), 상한 집합은 훈련 그래프가 그 역할에 대해 보이는 패턴과 끝점 개념이 일치하는 모든 엣지를 담은 62개 엣지짜리 타입 완성(typed completion)으로부터(무엇이 가능한지)이며, 단언되지 않은 원자는 전체 구간, 곧 열린 세계의 미지수로 기본값이 매겨집니다(334–376번째 줄). 결정 정책은 하한 집합 안에서는 YES로, 상한 집합 밖에서는 NO로 답하며, 그 사이에서는 기권합니다. 전체 은행의 $36 \times 13 = 468$개 결정 전부에 걸쳐 채점하면:

[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)
  witness affiliated(dave,x) ∧ ¬affiliated(erin,x): the closed world answers cmu — WRONG on
  G_full; the interval reads cmu as unknown [0,1] and abstains (the open-world default)

이 행을 풀어 봅시다. 닫힌 세계 정책은 모든 것에 답하고(커버리지 $1.0$) 24번 틀리므로, 그 정확도는 $(468 - 24)/468 = 0.9487$입니다; 그 24개의 오류는 정확히 전체 은행의 23개 하드 정답에 "도출되지 않음"을 "거짓"으로 취급함으로써 잘못된 예를 만들어 내는 부정 질의 증인 하나를 더한 것입니다. 구간 정책은 $19 + 365 = 384$개의 결정에 답하며, 커버리지는 $384/468 = 0.8205$이고, 답한 모든 결정이 옳아서 단언으로 강제되는 답변 정확도가 $1.000$입니다(528–530번째 줄). 그 거래는 숫자 스스로가 진술합니다: 결정의 약 18퍼센트가 거부되고, 그 대가로 답해진 것은 아무것도 틀리지 않으며, 하니스는 그 길을 따라 모든 질의에 대해 구간의 건전성 불변량, 즉 하한 집합 $\subseteq$ 참된 정답 $\subseteq$ 상한 집합을 검사합니다(390번째 줄). 이는 덧붙여진 신뢰도 헤드가 아니라 아키텍처 자신의 데이터 모델 위에서 돌아가는 III부의 위험-커버리지 이야기입니다.

이제 세 번째 절을, 이 주장 가운데 가장 어려운 것으로 정직하게 이름 붙여 봅시다. 행렬은 추론 지름길에 대한 견고함을 약속하는데, 이는 잘못된 내부 이유로 옳은 모델이라는 II부의 현상입니다. 이 책상에서는 이 절이 거의 공허합니다: 이 장난감의 개념은 학습되는 것이 아니라 주어진 고정된 기호이므로, 지름길이 숨을 개념-추출 층이 아예 없고, 지름길 표면은 구성상 최소화되어 있습니다; 그 세는 계측 도구는 컴패니언의 shortcuts.py와 rsbench_lite.py에 살아 있으며, II부의 장들은 자신의 영역에서 하나의 과제가 얼마나 많은 레이블-일관적인 틀린 개념 지도를 허용할 수 있는지를 보여 주었습니다. 규모에서는 상황이 뒤집힙니다. 배포된 SATORI는 자신의 기호를 학습된 지각이나 학습된 임베딩에 그라운딩하며, 개념 어휘가 학습되는 순간 C5는 식별 가능성 문제를 온전히 물려받습니다: 잘못 레이블된 개념에 대한 보정된 정도는 보정된 헛소리이며, 질의 수준에서 계산된 어떤 ECE도 그것을 탐지할 수 없습니다. 이 주장 자신의 지표 목록은 ECE와 나란히 지름길-비율 프로브를 포함시킴으로써 이를 인정합니다. C5는 처음 두 절에서는 장난감 규모에서 검증되었고, 세 번째 절에서는 조건부로 진술된 것으로 읽혀야 합니다; 채점된 다섯 가지 주장 가운데, 그 채점이 가장 멀리 이동하지 못하는 것이 바로 이것입니다.

C4, C6, C7: 인용-전용, 이유와 증거 계획과 함께

행렬의 세 행은 책상에서 채점될 수 없으며, 하니스는 억지로 늘리는 대신 그 이유를 인쇄합니다. 이 규율은 숫자만큼이나 중요합니다: 언제나 "검증됨"이라고만 말하는 주장 표는 광고에 지나지 않습니다.

C4, 처리량은 논문에 남습니다. 처리량이 하드웨어와 규모의 성질이며, 이 책상은 둘 다 갖고 있지 않기 때문입니다. 스위트 안의 산출물은 측정이 아니라 프록시입니다: IV부의 gpu_fixpoint.py는 백 가지 지식 베이스 변형의 배치를 하나의 쌓인 조밀 패스로 닫아, 가속기를 시험하기에는 턱없이 작은 행렬 위에서 그 승리의 모양(고정점이 배치가 공짜로 딸려 오는 평범한 텐서 대수로 표현되는 것)을 보여 줍니다. 이 주장이 이겨야 할 선행 기술은 순진한 파이썬이 아니라 공학적으로 다듬어진 CPU 병렬성이며, 이 권은 이미 그 숫자를 인용해 두었습니다: RDFox 계열은 초당 610만 개의 트리플로 LUBM-50K 폐쇄를, 즉 명시적 트리플 67억 개가 92억 개까지 자라나는 것을 실체화했으며, 128개 스레드 실행은 자신의 단일 스레드보다 69.6배 빨랐습니다 [6]; C4의 기준선으로 이름 붙은 신경-기호 엔진들(PyReason [7], Scallop [8], DeepProbLog)은 그 계열 아래에 있으며, 그 기호 코어는 CPU에 매여 있습니다. 그러므로 심사 가능한 긍정적 결과는 구체적입니다: 지식 베이스 크기와 질의 깊이의 함수로서 초당 질의 수와 지연 시간을, 비교 가능한 하드웨어 예산 위에서 그 엔진들에 맞선 실제 가속기 위의 배치 커널에 대해, 건전성을 맞춘 채로, 단일한 점이 아니라 규모 곡선을 전시물로 삼아 측정하는 것입니다. 구체화 대 재작성과 GPU 추론이 이 이야기의 장난감 절반을 쥐고 있습니다.

C6, 그라운딩이 돕는다는 것은 장난감 규모에서는 퇴화하며, 그 이유는 알아 둘 가치가 있습니다: 소거 실험이 끌 것이 아무것도 없다는 것입니다. 장난감 커널은 TBox로부터 지어져 있습니다; 그 규칙은 컴파일된 공리이므로, "그라운딩 끄기"는 어떤 기능을 소거하는 것이 아니라 추론기 자체를 지워 버립니다. 이 주장은 시스템이 그라운딩되지 않은 자유도, 즉 온톨로지를 무시할 수도 있는 임베딩을 지닐 때에야 비로소 검사 가능해집니다: 그때에야 행렬의 실험이 정확해집니다(TBox 구조로부터 초기화하는 것 대 무작위로 초기화하는 것; OWL 2 EL과 OWL 2 RL 프로파일 목적 함수를 따로 그리고 함께 실행; 박스 대 공; MRR 차이를 자기-소거하여 보고). 그라운딩이 온톨로지 규모에서 실제 신호를 실어 나른다는 기하학적 증거는 박스-임베딩 계열, 곧 그 포함 손실이 TBox 구조를 직접 인코딩하는 Box2EL [9]과 TransBox [10]와 함께 삽니다; 장난감의 기여는 공이 아니라 박스가 포섭 순서를 충실하게 실어 나를 수 있다는 3권의 평결이었습니다. 긍정적인 C6은 GALEN이나 유전자 온톨로지 크기의 온톨로지 위에서, 오직 구조 초기화만으로 귀속되는 양의 Δ MRR이며, 소거 격자가 함께 공개됩니다.

C7, 전이는 두 번째 온톨로지를 필요로 하며, 장난감은 하나의 세계만을 지닙니다. 이 주장의 대조는 정밀합니다: C7이 개선해야 할 깊은 온톨로지-추론 계열은 한 도메인 안에서는 정확하게 답하지만 온톨로지마다 재훈련되어야 하며, 이것이 그 계열 스스로가 이름 붙인 한계입니다 [11]. C7은 어느 한 온톨로지의 규칙 어휘 위에서 훈련된 라우터와 커널이 다른 온톨로지에서 제로샷과 퓨샷으로 답할 것이라는 데 걸며, 이는 학습된 것이 하나의 도메인에 관한 사실이 아니라 규칙 모양에 대한 라우팅이기 때문입니다. 심사 가능한 긍정적 결과는 이렇습니다: 온톨로지 A에서 훈련하고, 고정한 다음, B의 전체 훈련 예산이 주어졌을 때 도메인별로 재훈련된 기준선에 맞서 온톨로지 B 위에서 MRR을 평가하고, 재훈련된 성능 가운데 제로샷과 퓨샷에서 회복된 비율을, 어휘 중첩 정도가 다른 온톨로지 쌍들에 걸쳐 보고하는 것입니다. 이보다 작은 그 무엇도 이를 해결하지 못하며, 바로 이것이 그 행이 인용-전용이라고 말하는 이유입니다.

커밋된 중심부: 주장 표

위의 모든 것은 하니스가 마지막에 인쇄하는 표, 곧 이 장의 실제 산출물로 압축됩니다. 다섯 개의 행은 단언이 지키는 커밋된 숫자를 싣고, 세 개의 행은 이유를 싣습니다. 이를 통째로 재현할 가치가 있습니다. 옆으로는 주장, 가운데에는 정직성 플래그, 오른쪽에는 증거라는 그 모양 자체가 이 권의 방법론적 수출품이기 때문입니다:

[5] the claims table (C4/C6/C7 stay with the paper: stated, not stretched)
  C1 multi-hop EPFO answering   toy-verified  MRR 0.568 vs random 0.230 / oracle 1.000
  C2 router learns rules        toy-verified  advises∘advises recovered, α = 0.972, exact decode
  C3 faithful proof traces      toy-verified  comp 8/8, suff 4/4, trace ⊇ MinA 2/2
  C4 GPU-batched scalability    cited-only    proxy gpu_fixpoint.py; needs PyReason/Scallop at scale
  C5 calibration + abstention   toy-verified  ECE 0.019; coverage 0.821 @ acc-on-answered 1.000
  C6 ontology grounding Δ MRR   cited-only    ablation degenerate here; Box2EL / TransBox carry it
  C7 cross-ontology transfer    cited-only    needs a 2nd ontology; RRN is the failing baseline
  C8 crisp soundness (τ→0)      toy-verified  satori_lite re-run: Horn 47/47, EL 46/46, complete iff L ≥ 3

여덟 가운데 다섯이 장난감 규모에서 검증되었고, 셋은 진술되고 출처가 붙어 있습니다. 성적표로 읽으면 이는 소박합니다. 방법으로 읽으면, 즉 주장이 먼저이고, 계측 도구는 독립적이며, 영수증은 커밋되어 있고, 플래그는 정직하다는 것으로 읽으면, 이는 표준 출력 열네 줄에 담긴 이 권 전체의 논증입니다.

쐐기: 빈 모서리

여덟 가지 주장은 야심으로 골라진 것이 아니라, 지도로 골라진 것입니다. 이 프로그램의 관련 연구 조사는 이 분야를 여러 계열로 조직하고 각각이 무엇을 쥐고 무엇을 놓치는지를 표로 정리하며, 그로부터 떠오르는 패턴이 바로 쐐기입니다: 모든 계열이 주장이 이름 붙이는 성질 가운데 두세 가지를 덮지만, 어떤 계열도 그 연언을 덮지 못합니다. 세 개의 계열이 이 논증을 떠받칩니다:

계열	대표 사례	쥐고 있는 것	놓치는 것
정확한 주석 논리	PyReason [7], ProbLog/DeepProbLog, 그리고 고전적으로는 RDFox [6]	건전성과 증명(C3, C8); PyReason 계열의 주석 달린 열린 세계 의미론(C5의 기층)	규칙은 손으로 지어질 뿐 결코 학습되지 않음(C2); CPU에 매인 추론(C4)
미분 가능한 규칙 학습기	Neural-LP, DRUM, NTP [2]	답으로부터의 규칙 학습(C2); GPU 친화적 대수(C4를 향해)	온톨로지에 눈이 멂(C6); 엄격한 길이 상한 아래의 사슬 전용 규칙(C2의 규모 절); 검증된 증명 없음(트레이스가 정당화로 재검사되지 않음), 보정 없음(C3, C5)
온톨로지 임베더 / 신경 온톨로지 추론기	Box2EL [9], TransBox [10], RRN [11]	기하학적 TBox 그라운딩(C6); 확장 가능한 추론(C4를 향해)	검사할 도출이 없음(C3, C8); 온톨로지마다 재훈련(C7)

이 지도의 네 번째 줄은 설계 계열이 아니라 과제 계보입니다: C1의 벤치마크를 쥐고 있는 질의-임베딩 시스템은 다중 홉 질의에 경쟁력 있게 답하지만, 구성상 온톨로지에 그라운딩되어 있지 않고, 증명에 충실하지 않으며, 기권을 위해 보정되어 있지도 않습니다 [1]. 여덟 가지 주장을 이 표 위에 겹쳐 놓으면 각 주장은 하나의 구멍 위에 떨어집니다: C2는 정확한 계열의 구멍에, C3과 C8은 임베더와 질의 계열의 구멍에, C4는 정확한 계열의 구멍에, C5는 거의 모두의 구멍에, C6은 규칙 학습기의 구멍에, C7은 RRN의 구멍에 떨어집니다. 여덟 개 전부의 연언이 어떤 행도 도달하지 못하는 모서리이며, SATORI의 쐐기란 정확히 주석 달린, 박스로 실어 나르는 기층 위의 하나의 연산자가 그곳에 설 수 있다는 주장입니다.

이제 냉정한 읽기입니다. 쐐기 논증에는 하나의 실패 양상이 있기 때문입니다: 간극이 존재한다는 것을 그 간극이 채워질 수 있다는 증거로 착각하는 것입니다. 간극이 실재한다는 것은 문헌에 관한 사실입니다; 그것을 채우는 것은 세계에 대한 내기입니다. 모서리는 아무도 시도하지 않았기 때문에 비어 있을 수도 있고, 그 성질들이 서로 맞바꿔지기 때문에 비어 있을 수도 있습니다: 정확성 대 학습 가능성, 배치화 대 구간 의미론, 전이 대 그라운딩입니다. 책상 자신의 숫자는 이미 그 긴장을 암시하며(다음 절이 그것을 명시적으로 만듭니다), 정확-대-학습-가능 분열에서 메타인지에 이르는 여덟 개의 이름 붙은 간극 G1부터 G8까지인 이 프로그램의 간극 지도는, 이 장의 영수증 이후에도 그 모서리의 얼마만큼이 여전히 비어 있는지에 대해 정직합니다. 그 지도는 미해결 문제 장의 교과 과정이며, 이는 그것이 있어야 할 올바른 자리입니다: 기회 논증은 연구 프로그램의 시작에 속하고, 미해결 문제는 교과서의 끝에 속합니다.

아직 풀리지 않은 부분

행렬은 행을 지니지만 상호작용 항은 지니지 않으며, 이 프로그램이 실제로 결판나는 곳은 바로 그 상호작용입니다. C2와 C3은 서로를 잡아당깁니다: C3의 채점은 규칙이 주어진 커널로 얻어졌지만, C2의 요점 전체는 훈련이 그것들을 고른다는 것이며, 답 정확도를 위해 훈련된 라우터가 그 이산화가 MinA를 포함하는 트레이스를 계속 만들어 낸다는 것은 아직 아무것도 증명하지 못합니다. 하니스 자체가 두 실험을 분리해 둡니다. 얼려진 커널 위에서는 트레이스 프로브를, 라우터 위에서는 복원을 돌리며, 이는 정확히 그 결합 검사가 아직 존재하지 않기 때문입니다. C4와 C5도 같은 방향으로 잡아당깁니다: 배치화된 처리량은 조밀한 커널을 관통해 흐르는 원자당 스칼라 정도 하나를 원하는 반면, C5의 기권은 두 개의 구간 끝점과 기호적 서명으로부터 지어진 타입 상한을 필요로 하며, 그래서 구간을 그 하한으로 평평하게 만드는 모든 시스템 최적화는 C5의 $1.000$이라는 답변 정확도가 사들여진 그 열린 세계를 조용히 지워 버립니다. 완전한 계약이라면 "C2 훈련은 훈련된 시스템 위에서 소거와 MinA 포함 관계를 다시 실행함으로써 측정되는 C3 충실성을 보존한다" 같은 행을 지녔을 것이며, 얼려진 그대로의 이 행렬에는 그런 행이 하나도 없습니다. 더 넓은 아직 풀리지 않은 부분은 규범적입니다: 이런 종류의 사전 등록된 주장 행렬은 아키텍처 논문에서는 여전히 드물며, 그런 논문에서 주장은 대개 실험이 무엇을 내놓았든 거기서 역공학된 것입니다. 이 장은 그에 대해 내놓을 정리가 없으며, 오직 그 대안적 규율의 입증된 비용만이 있습니다: 표를 인쇄하는 코드 몇십 줄과, "인용-전용"이라고 세 번 쓸 의향입니다.

왜 중요한가

이 장은 이 권이 설계된 대로, 단 한 번, 처음부터 끝까지 작동하는 모습입니다. 어떤 주장을 채점한 모든 계측 도구는 앞서 다른 시스템에 맞서 지어졌습니다: I부의 소거, I부의 정당화, III부의 ECE와 기권, IV부의 배치화 프록시, 4권의 질의 은행, 1권과 2권의 오라클입니다. 그런 다음 캡스톤 아키텍처가 도착하여 채점되었을 뿐, 감탄의 대상이 아니었으며, 계측 도구가 닿을 수 없던 곳에서는 표가 인쇄로 그렇게 말했습니다. 연구로 나아가는 독자에게, 옮겨 갈 수 있는 대상은 SATORI가 아니라 계약의 형식입니다. 짓기 전에, 각 주장을 지표와 기준선 계열을 지닌 한 문장으로 적으십시오; 주장마다 상태 플래그를 인쇄하는 평가를 배선하십시오; "인용-전용, 왜냐하면"이 그 플래그의 정당하고 부끄럽지 않은 값이 되게 하십시오. 이렇게 쓰인 프로그램은 낯선 이가 심사할 수 있고, 후계자가 물려받을 수 있으며, 자기 자신의 하니스로 반증될 수 있는데, 이는 같은 미덕의 세 가지 정의입니다. 그리고 다섯 개의 장난감 영수증은, 규모에 대해 증명하지 못하는 것이 무엇이든, 정확히 한 가지는 증명합니다: 여덟 문장은 실행 가능하며, 각각은 이미 그것을 채점할 수 있는 코드에 붙어 있다는 것이며, 이는 대부분의 아키텍처 주장이 만들어지는 그날에 말할 수 있는 것보다 더 많습니다.

핵심 용어

• 주장-실험 행렬(claims-to-experiments matrix): 연구 프로그램의 모든 주장을 실험, 기준선 계열, 지표에 사상하는 사전 등록된 표로, 구현에 앞서 얼려집니다.
• 정직성 플래그(honesty flag, 장난감 규모에서 검증됨 / 인용-전용): 커밋된 주장 표의 상태 열입니다; 장난감 규모에서 검증됨 행은 단언된 숫자를 싣고, 인용-전용 행은 책상 규모에서 채점이 불가능한 인쇄된 이유를 싣습니다.
• 하드 정답(hard answer): 전체 그래프 위에서는 질의에 답하지만 훈련 그래프의 순회로는 도달할 수 없는 개체입니다; 필터링된 순위 지표가 계산되는 모집단입니다.
• 필터링된 MRR(filtered MRR, 필터링된 평균 역순위): 각 순위 매김에서 다른 참된 정답들을 제거한 채 하드 정답에 대한 $1/\mathrm{rank}$의 평균입니다; 이 장의 C1 지표입니다.
• 심어진 규칙 복원(planted-rule recovery): C2의 프로토콜입니다: 알려진 규칙을 숨기고, 오직 그 질의 답만으로 훈련한 다음, 학습된 모델이 숨겨진 규칙으로 정확히 디코드되어 돌아올 것을 요구합니다.
• 정확한 디코드(exact decode): 라우터의 아그맥스 템플릿이 IR(intermediate representation, 중간 표현) 규칙으로 재구성되었을 때 컴파일된 숨겨진 규칙과 튜플 단위로 동일해야 한다는 통과 조건입니다; 복원은 유사도가 아니라 구문적 동일성입니다.
• 이산화된 트레이스(discretized trace): 도출된 원자의 기록된 도출 트리 어디엔가 나타나는 원래 공리 식별자들의 집합입니다; C3은 이것이 참된 MinA를 포함할 것을 요구합니다.
• MinA(최소 공리 집합, minimal axiom set / justification): 주어진 귀결을 함의하는 부분집합-최소 공리 집합입니다; 장난감 규모에서는 적중 집합 트리로 열거 가능합니다.
• ECE(기대 보정 오차, expected calibration error): 진술된 신뢰도와 실현된 정확도 사이의 구간-가중 평균 격차, $\sum_b (n_b/N)\lvert \mathrm{acc}(b) - \mathrm{conf}(b)\rvert$입니다.
• 구간 주석(interval annotation) $[\ell, u]$: 원자마다의 하한과 상한 정도이며, 도출 가능함 대 가능함을 나타내고, 미지수는 전체 구간입니다; C5의 기권 정책의 기층입니다.
• 커버리지 / 답변 정확도(coverage / accuracy-on-answered): 선택적 정책이 답하는 결정의 비율과, 정확히 그것들에 대한 정확도입니다; 커밋된 C5 쌍은 $1.000$에서의 $0.8205$입니다.
• 쐐기(wedge): 어떤 기존 계열도 덮지 못하는 성질들의 빈 연언을 짚어내는 관련 연구 논증입니다; 결코 결과가 아니라 기회 주장입니다.

이 다음으로 이어지는 것

쐐기는 그 모서리가 비어 있다고 말했습니다; 영수증은 그리로 가는 길의 8분의 5가 장난감 규모에서 존재한다고 말했습니다; 상호작용에 대한 걱정은 남은 길이 직선이 아니라고 말했습니다. 남은 것은 이 프로그램만이 아니라 이 분야 전체가 어떻게 해야 할지 모르는 것의 이름을 붙이는 일입니다. 미해결 문제는 관련 연구 조사가 그려 둔 간극 지도 G1부터 G8까지를, 정확-대-학습-가능 분열에서, 규칙-탐색 폭발, CPU에 매인 추론, 온톨로지에 눈먼 학습, 전이 불가능성을 거쳐, 설명 충실성, 지름길 아래에서의 보정, 메타인지에 이르기까지 취하며, 이 장이 각 주장을 다룬 방식 그대로 각 간극을 다룹니다: 정밀하게 진술되고, 진전을 측정할 계측 도구에 묶이며, 누군가 얼마나 멀리 갔는지에 대해 정직하게 채점됩니다.

---

컴패니언 코드: examples/frontier/satori_eval.py는 이 권의 계측 도구들을 주장 행렬에 배선합니다: satori_lite.py에서 온 커널과 오라클, 4권의 query_dag.py와 cqd.py에서 온 질의 은행과 필터링된 프로토콜, calibration.py에서 온 ECE와 맞춰진 온도, 그리고 justifications.py에서 온 MinA 오라클입니다. 이 장의 모든 숫자를, 주장 표를 포함하여, 재현하려면 python3 examples/frontier/satori_eval.py를 실행하십시오; 그 실행은 결정론적이며, 장난감 규모에서 검증된 모든 행은 단언으로 지켜집니다.