다음 연구 하기: 사각지대와 첫걸음

📍 현재 위치: VIII부 · 연구의 활주로 — 22장. 미해결 문제는 여덟 개의 공백 G1–G8을 지도로 그리고 의도적으로 열어 둔 채 남겨 두었습니다; 이 장은 그중 하나를 집어 드는 방법입니다: 이 시리즈가 다섯 권에 걸쳐 시연해 온 규율을 명시적으로 드러내고, 월요일 아침에 공백 하나에 착수하는 실제 계획을 제시합니다.

지금까지 모든 장은 결과 하나를 가르쳤습니다. 이 장은 그 결과들을 만들어 낸 절차를 가르치는데, 그 절차야말로 독자가 자기 자신의 연구로 가져갈 부분이기 때문입니다. 이 장의 주장은, 연구 방법이란 대개 불확실성 아래에서의 규율이며, 이 시리즈는 그 규율 하나를 이름 붙이지 않은 채 처음부터 시연해 왔다는 것입니다. 그 규율에는 다섯 부분이 있습니다: 학습된 시스템보다 먼저 정확한 참조를 짓는 것, 무엇이든 짓기 전에 모든 주장을 실험으로 적는 것, 모든 실행을 결정론적으로 만들고 인용되는 모든 숫자를 실행 가능한 단언으로 만드는 것, 자기 자신의 연구를 자기 분야의 이름 붙은 실패 모드로 감사하는 것, 그리고 아픈 열까지 포함해 장부를 공개하는 것입니다. 이 가운데 어느 것도 심오하지 않습니다. 전부 습관이며, 습관이야말로 아직 아무도 풀지 못한 문제와의 접촉에서 살아남는 바로 그것입니다.

쉽게 말하면

천재의 번뜩이는 통찰이 아니라 조종사의 일상적 절차를 상상해 보십시오. 이륙 전에 조종사는 항공기가 어디로 가는지, 도착이 어떻게 확인될지를 적은 비행 계획서를 제출합니다. 계기들은 옳다고 알려진 참조 기준에 맞추어 지상에서 보정되었습니다. 비행 기록 장치는 모든 것을 기록하므로, 무슨 일이 있었는지에 대한 어떤 주장이든 기억이 아니라 재생을 통해 확인할 수 있습니다. 이륙 전 점검표는 항공기가 고장 나는 알려진 방식들을 하나씩 훑으며, 각 항목은 느낌이 아니라 확인으로 체크됩니다. 그리고 사고 이후의 보고서는 무엇이 잘못되었는지를 있는 그대로 진술합니다. 실패를 숨긴 보고서는 다음 승무원을 죽음으로 몰아넣을 것이기 때문입니다. 연구를 잘한다는 것은 바로 이 절차를 옮겨 심는 일입니다: 참조 구현이 지상 보정이고, 주장 표가 비행 계획서이며, 시드가 붙고 단언으로 지켜지는 companion 스위트가 비행 기록 장치이고, 실패-모드 점검표가 기체 외부 점검(walk-around)이며, 정직한 장부가 사고 보고서입니다. 이 가운데 어느 것도 천재성을 요구하지 않습니다. 요구되는 것은 오직, 건너뛰고 싶은 유혹이 가장 강할 때 바로 그 순간에 단계를 건너뛰기를 거부하는 것뿐입니다.

이 장에서 다루는 내용

숨은 교과과정을 명시적으로 드러내기: 독자가 이미 겪은 세 순간, 즉 2권의 HermiT 교차 검사, 4권의 통제된 세-기하학 비교, 그리고 이 권의 트레이스-대-MinA(최소 공리 집합) 검사를 다루며, 각각을 일반 규율의 한 사례로 이름 붙입니다.
오라클 우선: 정확한 참조가 왜 학습된 시스템보다 먼저 오는지, 그것이 정직하게 치르는 비용(이 시리즈가 13개체짜리 세계에 머무는 데는 이유가 있습니다), 그리고 목표 규모에 오라클이 존재하지 않을 때의 처방, 즉 장난감 규모에서 하나를 짓고 참값을 심는 방법을 다룹니다.
실험으로서의 주장: 캡스톤의 행렬을 사전 등록 규율로 일반화하고, 실제 한 행을 끝까지 걸어 보며, 지적 정직성을 활자로 옮긴 것으로서의 장난감 규모에서 검증됨 대 인용-전용 열을 다룹니다.
인식론으로서의 결정론: 시드, 바이트 단위로 동일한 재실행, 의미론적 성질에 대한 단언, 그리고 커밋된 모든 표제 숫자를 자릿수까지 다시 유도하는 suite_harness.py의 회귀 규율을 다룹니다.
적대적 자기 감사: 이 권의 이름 붙은 다섯 가지 실패 모드를 출판 전 점검표로 바꾸어, 각 행이 이 권이 그것을 위해 지은 커밋된 계측 도구를 가리키게 합니다.
월요일 계획: 계측 도구 준비성 점검에서 출판 장부에 이르기까지, 하나의 공백, G5 온톨로지 간 전이에 대한 완전한 소규모 연구 계획을 다루며, 포크하기에 충분할 만큼 작습니다.
사각지대 목록: 이 시리즈 자신의 방법이 체계적으로 경시하는 것을 의도적으로 공개하는데, 자기 자신의 책을 예외로 두는 방법론 장은 스스로의 감사에 실패할 것이기 때문입니다.

숨은 교과과정, 명시적으로 드러내기

방법은 영수증으로 가르치는 것이 가장 쉬우므로, 독자가 이미 겪은 세 순간에서 시작하여 각각이 예시하는 패턴에 이름을 붙여 봅시다.

첫 번째는 2권의 오라클 교차 검사입니다. 처음부터 새로 지은 EL 완성 추론기는 자신의 말만으로 신뢰받도록 요구받은 적이 결코 없습니다: examples/symbolic/reasoners.py는 완전한 OWL 2 DL 추론기인 HermiT을 owlready2를 통해 구동하고, 손으로 지은 완성이 내놓은 포섭 관계와 충족 불가능한 개념들을 그것에 맞대어, 클래스 하나하나까지 검사합니다. 그 패턴은 다음과 같습니다: 여러분이 지은 시스템이 자기 숙제를 스스로 채점하게 두지 마십시오. 같은 의미론의 독립적인 구현, 이상적으로는 여러분이 직접 짜지 않은 구현이야말로 존재하는 것 중 가장 값싸면서도 강력한 증거입니다.

두 번째는 4권의 세-기하학 비교입니다. 복합 질의 장들이 GQE(Graph Query Embedding)의 점, Query2Box의 박스, BetaE의 베타 분포를 비교했을 때, clqa_models.py는 셋 모두를 하나의 프로토콜 아래 돌렸습니다: 하나의 질의 은행, 하나의 훈련 예산, 하나의 평가입니다. 그렇게 하여 관측된 모든 차이가 오직 기하학에만 귀속될 수 있게 했습니다; 수락 하니스는 그 결과로 나온 커버리지 표가 구조적 이론과 칸 하나하나까지 일치한다고 단언합니다(examples/integration/validate.py, 85–87번째 줄). 그 패턴은 다음과 같습니다: 관심 변수를 제외한 모든 것이 통제될 때에만 비교는 실험입니다, 그리고 그 통제는 의도가 아니라 코드로 검사되어야 합니다.

세 번째는 이 권의 트레이스-대-MinA 교차 검사입니다. SATORI-lite 커널은 자신이 도출하는 모든 원자에 대해 도출 트레이스를 기록합니다; 1장의 justifications.py는 완전히 독립적인 도구인 Reiter의 적중 집합 트리로 참된 최소 공리 집합(MinA)을 계산합니다. 주장 평가는 커널의 이산화된 트레이스가 시험된 모든 함의마다 참된 MinA를 포함한다고 단언하며(satori_eval.py, 494–510번째 줄), 커밋된 실행은 그 영수증을 인쇄합니다:

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

그 패턴은 다음과 같습니다: 설명이 얼마나 설득력 있어 보이는지가 아니라, 설명에 대한 오라클에 맞대어 설명 주장을 검사합니다. 세 순간, 근본에 깔린 하나의 태도가 낳은 세 사례입니다: 모든 주장은 계측 도구를 얻으며, 그 계측 도구는 그것이 측정하는 대상으로부터 독립적입니다. 기계학습 문헌은 이 태도가 없을 때 번성하는 실패 패턴들에 이름을 붙여 왔습니다: 암시에 의한 설명, 출처가 확인되지 않은 성과, 장식으로서의 수학입니다 [1]. 아래의 다섯 규율은 그것의 구성적 보완물이며, 이 장의 나머지는 그것들을 하나씩 걸어갑니다.

규율	이미 겪은 순간	커밋된 영수증
오라클 우선	1권의 연쇄기, 2권의 완성, 4–5권의 기호 실행기	다섯 권에 걸친 모든 건전성 프로브와 크리스프-극한 단언
실험으로서의 주장	캡스톤의 C1–C8 행렬	`satori_eval.py` 주장 표: 장난감 규모에서 검증됨 5건, 인용-전용 3건
인식론으로서의 결정론	바이트 단위로 동일한 companion 실행, 종료 코드 판정	`suite_harness.py`: 자릿수까지 다시 유도된 26개의 표제 값
적대적 자기 감사	지름길, 보정, 충실성, 절단, 일관성 장들	이름 붙은 실패 모드마다 하나씩 커밋된 계측 도구
정직한 장부	모든 권의 평결 장	사는 것 / 치르는 것 / 지키는 것, 갚지 못한 빚이 열거됨

다섯 가지 규율이 각각 독자가 이미 겪은 영수증으로 도입되어, 포크 가능한 하나의 월요일 아침 계획으로 모여들며, 그 아래에는 이 시리즈 자신의 사각지대 목록이 인쇄되어 있다.

저자가 AI의 도움을 받아 직접 제작한 원본 도해.

오라클 우선: 학습기보다 먼저 오는 참조

첫 번째 규율은 순서 제약입니다. 학습된 시스템이 존재하기 전에, 먼저 오라클(oracle)을 지으십시오: 여러분의 학습된 시스템이 훗날 그것에 맞대어 측정될 의미론을 정확하고 남김없이 검사 가능하게 구현한 것입니다. 1권은 어떤 임베딩이 존재하기도 전에 전방 연쇄기를 지었고, 2권은 어떤 박스가 개념 둘레에 그려지기도 전에 EL 완성을 지었으며, 4권과 5권은 어떤 소프트 커널이 질의를 건드리기도 전에 기호적 질의 실행기를 지었습니다. 이 순서를 옹호하는 논거는 반증 가능성입니다. 정확한 참조 없이 평가된 학습된 시스템은 오직 레이블에 맞대어서만 채점될 수 있으며, 레이블은 답을 채점할 뿐 추론을 채점하지 않습니다. "모델이 작동한다"는 그러면 반증 불가능한 문장이 되는데, 그 실패가 이 문장을 논박할 만한 커밋된 절차가 존재하지 않기 때문입니다. 오라클이 있으면, 모든 소프트 주장은 검사 가능한 크리스프 그림자를 얻습니다: 커널의 답은 크리스프 극한에서 실행기의 답과 같아야 하고(36개 질의 전부, satori_eval.py, 424–431번째 줄에서 단언됨), 절단은 정확히 오라클이 지평선 너머에서 도출하는 원자들만큼의 대가를 치러야 하며, 설명은 오라클이 검증한 MinA를 포함해야 합니다. 다섯 권에 걸친 모든 건전성 프로브, 모든 재현율-대-예산 표, 모든 크리스프-극한 단언은 먼저 존재했던 오라클의 하위에 있습니다.

그 비용은 정직하게 값이 매겨져야 합니다: 오라클은 규모를 제약합니다. 정확한 참조는 본성상 남김없이 검사되며, 폐쇄는 열거되고, MinA는 탐색되며, 질의 은행은 기호적으로 실행되고, 남김없는 검사는 지수적인 대가를 동반합니다. 이것이 바로 이 시리즈 전체가 23개의 기본 사실(그중 18개는 그래프 엣지)과 14개 공리 TBox를 지닌 13개체짜리 학계 세계 위에서 사는 이유입니다. 그 선택은 겸손함이 아니었습니다; 그것은 모든 주장을 여전히 몇 초 안에 정확한 참조에 맞대어 검사할 수 있는 가장 큰 세계였습니다. 그 거래는 연구 시점에 한 방향으로만 흐릅니다: 작은 세계에서 검증된 주장은 아무것도 검사할 수 없는 큰 세계에서 보고된 숫자보다 더 값어치가 있습니다. 앞엣것은 증거이고 뒤엣것은 증언이기 때문입니다.

여러분의 목표 규모에 오라클이 존재하지 않을 때의 실용적인 처방에는 두 가지 동작이 있으며, 둘 다 이 권의 companion에 실제 사례로 나타납니다.

동작 하나: 장난감 규모에서 오라클을 지으십시오. 정확한 의미론을 계산할 수 있을 때까지 문제를 줄인 다음, 그곳에서 정확한 일치를 요구하십시오. 그 장난감은 그 방법이 규모에서 작동함을 증명하지 않습니다; 그것은 그 방법이 어떤 규모에서도 이미 고장 나 있지는 않다는 것을 증명하며, 이는 더 값싸면서도 더 자주 실패하는 검사입니다.

동작 둘: 참값을 심으십시오. 여러분이 복원한다고 주장하는 잠재 구조에 자연스러운 오라클이 없을 때, 구성에 의해 그것을 알고 있는 세계를 지으십시오. 심어진-규칙 생성기가 그 축소판 패턴입니다: grandAdvisor 규칙은 학습기로부터 숨겨져 있고, 길이-2 사슬 템플릿 25개 전부에 대한 소프트맥스 라우터는 오직 질의 응답만으로 훈련되며, 수락 기준은 점수가 아니라 정확한 동일성입니다: 디코딩된 규칙은 심어진 규칙과 같아야 합니다(satori_eval.py, 467–471번째 줄):

    alpha, rlosses = train_router(feats, G)
    top = int(np.argmax(alpha))
    decoded = ("chain", *TEMPLATES[top], "grandAdvisor", False, False)
    planted = satori_lite.compile_horn([kb.RULES[3]])[0]  # the hidden rule
    assert decoded == planted, f"decoded {decoded} ≠ planted {planted}"

같은 동작이 지름길 지표들에도 동력을 공급합니다: rsbench_lite는 분할별로 정답 개념이 알려진 과제들을 생성하므로, 개념 품질은 눈대중이 아니라 심어진 참값에 맞대어 측정됩니다. 심기는 "모델이 무언가를 학습했다"를 "모델이 이것을 정확히 복원했으며, 그렇지 않았다면 실패했을 단언이 여기 있다"로 바꾸어 주는 것입니다.

실험으로서의 주장: 사전 등록된 행렬

두 번째 규율은 여러분이 무언가를 짓기 전에 무엇을 적어 두는지를 지배합니다. 캡스톤은 SATORI의 여덟 가지 주장을 하나의 행렬로 얼려 두었으며, 그 일반화는 하나의 형식입니다: 모든 주장은 다섯 개의 필드를 지닌 한 행입니다,

\langle\; \text{claim},\ \text{metric},\ \text{baseline},\ \text{instrument},\ \text{phase} \;\rangle,

여기서 claim(주장)은 반증 가능한 문장이고, metric(지표)은 그것을 결정하는 숫자이며, baseline(기준선)은 그 숫자가 이겨야 하는 대상(그리고 정직성이 요구할 때는 넘어서면 안 되는 대상)이고, instrument(계측 도구)는 그 숫자를 산출하는 커밋된 코드이며, phase(단계)는 그 행이 프로젝트 안에서 언제 만기가 되는지를 말합니다. 이런 식으로 적힌 주장은 하나의 내기입니다. 어느 필드든 빠진 주장은 그저 느낌일 뿐입니다: 지표가 없으면 결정될 수 없고, 기준선이 없으면 맥락화될 수 없으며, 계측 도구가 없으면 재현될 수 없고, 단계가 없으면 영원히 미뤄질 수 있습니다.

실제 행 하나를 걸어 봅시다. 주장 C1, 다중 홉 EPFO(존재 긍정 1차) 응답은 다음과 같이 분해됩니다: 주장, 괴델 커널은 보정된 신경 인접 행렬 위에서 존재-긍정 질의에 답한다; 지표, 은행의 17개 하드 정답(전체 그래프 위에서는 그 질의에 답하지만 훈련 그래프의 어떤 순회로도 도달할 수 없는 개체)에 대한 필터링된 평균 역순위(MRR); 기준선, 무작위 채점기(정보 없는 바닥), 훈련 그래프의 기호적 순회(정의상 모든 하드 정답에서 영), 그리고 전체 그래프 오라클(천장); 계측 도구, 4권의 고정된 프로토콜 아래 보정된 인접 행렬 위에서 실행되는 godel_eval(satori_eval.py, 100–151번째 줄); 단계, 지금 장난감 규모에서 검증됨. 커밋된 단언들은 실행 가능한 형태로 만들어진 사전 등록입니다(satori_eval.py, 448–450번째 줄): 커널은 무작위 바닥을 최소 0.25 MRR만큼 이겨야 하고, 순회를 최소 0.30만큼 이겨야 하며, 그리고 놀랍게도 0.8 아래에 머물러야 합니다. 그보다 오라클에 더 가까워 보이는 16차원짜리 장난감 대입기는 명석함이 아니라 누출을 알리는 신호이기 때문입니다. 커밋된 실행은 이 내기를 해결합니다: 커널 0.5680, 무작위 0.2301, 순회 0.1488, 오라클 1.0000. 하한과 나란히 상한까지 사전 등록하는 것이야말로 규율이 최대한의 힘을 발휘하는 지점입니다: 주장 표는 결과가 존재하기도 전에 결과를 양쪽 방향에서 제약합니다.

이 형식이 막아 주는 것은 사전 등록이 발명된 바로 그 이유인 한 쌍의 실패입니다: 골대 옮기기(숫자를 본 뒤에 성공을 다시 정의하는 것)와 사후적 지표 쇼핑(하나가 돋보일 때까지 지표를 훑는 것)입니다. 둘 다 가상의 위험이 아니라 실제로 살아 있는 위험입니다; 재평가 문헌은 지식 그래프 임베딩 리더보드가 훈련 프로토콜이 동등화되었을 때 상당히 재정렬되었음을 보여 주었으며, 이는 원래의 순위가 부분적으로는 방법론적 선택에 대한 측정이었음을 뜻합니다. 이는 3권이 물려받은 방법론적 교훈이기도 합니다 [2]. 이 형식이 치르는 비용은 공개적인 실패입니다: 미달로 끝난 사전 등록된 행은 눈에 보입니다. 그 비용이 바로 범위 설정 규칙, 즉 존재하거나 여러분이 짓기로 약속한 계측 도구에 맞대어서만 행을 적으라는 규칙의 이유입니다; 그리고 계측 도구가 존재하지 않을 때, 그것을 짓는 일 자체가 하나의 출판 가능한 연구 기여이며, 이것이 바로 rsbench 스위트가 NeurIPS 자리를 얻어 낸 정확한 방식입니다 [3].

마지막 열이 바로 정직성이 활자가 되는 곳입니다. satori_eval.py는 행렬 가운데 가장 큰 정직한 부분집합을 실행하고, 주장마다 장난감 규모에서 검증됨과 그 숫자, 또는 인용-전용과 그 이유 가운데 하나를 인쇄합니다(satori_eval.py, 628–651번째 줄). 표 안의 기호 하나는 해독이 필요합니다: τ는 커널의 온도, 곧 AND와 OR를 매끄럽게 만드는 소프트민과 소프트맥스의 매개변수이며, τ→0은 두 연산자가 정확한 괴델 min과 max로 되돌아가는 크리스프 극한입니다. 커밋된 표는 다음과 같습니다:

[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

다섯 행은 숫자를 지니고, 세 행은 이유를 지닙니다. 인용-전용 행들은 표의 약점이 아니라 표가 작동하고 있다는 증거입니다: 각 행은 어떤 증거가 정확히 빠져 있는지, 그리고 그 빠진 증거가 지금 어디에 있는지를 진술합니다. C7을 눈여겨보십시오; 그것이 곧 월요일 계획이 됩니다.

인식론으로서의 결정론: 스스로를 검사하는 논문

세 번째 규율은 공학처럼 들리지만 실제로는 인식론입니다. 공학적 규칙은 네 가지이며, 이 시리즈의 모든 companion 스위트는 그것을 따릅니다. 무작위성의 모든 원천에 시드를 고정하여, "그 실행"이 일화들의 집합이 아니라 잘 정의된 하나의 대상이 되게 하십시오. 전체 출력에 대해 두 번의 실행이 바이트 단위로 같을 것을 요구하여, 어떤 비결정성이든 넷째 자리 소수점에 숨는 대신 스스로를 알리게 하십시오. 한 번의 운 좋은 실행에서 뽑아낸 날것의 부동소수점 대신, 의미론적 성질(정확한 규칙 복원, 오라클에 맞선 건전성, 시스템 간의 마진, 단조로운 재현율)에 단언을 적어, 그 검사들이 실험이 뜻하는 바를 진술하게 하십시오. 그리고 모든 단언에서 벽시계 시간은 제외하십시오. 타이밍은 기계가 바꿀 자격이 있는 유일한 숫자이기 때문입니다(suite_harness.py, 61–63번째 줄 및 352–353번째 줄).

이 규칙들이 사들이는 것은 바로 인식론적 독법입니다. 결정론적이고 단언으로 지켜지는 companion은 스스로를 검사하는 논문입니다: 산문에서 인용되는 모든 숫자는 동시에 상시 회귀 테스트이며, 참이기를 멈추는 순간 시끄럽게 실패하는 실행 가능한 진술입니다. 이것이 바로 다섯 권이 서로를 표류 없이 인용할 수 있게 해 준 것입니다. 5권의 보정 장이 3권의 ComplEx 점수를 인용할 때, 그것은 두 권 전의 복사-붙여넣기를 신뢰하지 않습니다; 대신 그 트레이너를 다시 임포트하고, 커밋된 시드 아래 다시 실행하며, 그 숫자를 단언합니다. 재현성 운동은 이것의 공동체-규모 버전을 제도화했습니다. 즉 점검표, 시드, 그리고 심사 시점의 코드 제출입니다 [4]; companion 스위트들은 같은 정책을 제출 시점 단 한 번이 아니라 계속해서 강제합니다.

권 규모의 강제는 suite_harness.py에 살아 있습니다. 그 COMMITTED 딕셔너리는 증거 장들이 인용하는 26개의 표제 값 전부를, 각 소유 모듈이 인쇄하는 정밀도 그대로 얼려 두며, 그 회귀 관문은 캐싱 없이 매 실행마다 모든 것을 처음부터 다시 유도하여 자릿수까지 동등성을 단언합니다(suite_harness.py, 133–143번째 줄):

def _regress(instrument: str, derived: dict[str, str]) -> None:
    """The regression gate for one instrument: every re-derived headline
    string must equal its committed value exactly.  Committed and derived
    must also cover the SAME keys, so a silently dropped check fails too."""
    want = COMMITTED[instrument]
    assert set(derived) == set(want), \
        f"{instrument}: check set drifted ({set(derived) ^ set(want)})"
    for key, got in derived.items():
        assert got == want[key], \
            f"{instrument} regression: {key!r} committed {want[key]!r}, " \
            f"re-derived {got!r}"

첫 번째 단언을 눈여겨보십시오: 검사들의 집합 그 자체도 지켜집니다. 그래서 검사 하나가 불편해졌을 때 조용히 삭제될 수 없습니다. 커밋된 실행의 장부는 이 규율이 작동하는 모습을 보여줍니다; 다음은 그 출력의 보정 블록입니다:

    calibration (calibration.py):
      temperature tau*                         1.4172                       = re-derived  OK
      eval ECE  before->after                  0.0245->0.0167               = re-derived  OK
      eval NLL  before->after                  0.1708->0.1387               = re-derived  OK
      eval acc  before=after                   0.9683=0.9683                = re-derived  OK
      eval AUC  before=after                   0.9136=0.9136                = re-derived  OK

그리고 실행의 한 줄짜리 판정인 SUMMARY suite_harness: checks=26/26 ...는 이 권의 증거 사슬이 스스로를 인증하는 순간입니다: 어떤 모듈에 대한 지나가는 편집이든, 어떤 자매-권 의존성이든, 어떤 시드든, 그것은 이 파일에서 실패한 동등성으로 표면에 드러납니다. 같은 발상이 수락 단위에서 나타난 것이 4권의 validate.py로, 장(chapter)마다 이름 붙은 역량 검사 하나씩이 있고, 각각은 커밋된 모든 단언을 살려 둔 채 자기 모듈의 run()을 호출하며, 프로세스의 종료 코드가 곧 수락 판정입니다: 21개 검사 전부가 통과할 때 그리고 오직 그때에만 0입니다(examples/integration/validate.py, 31–125번째 줄). 그러면 지속적 검증은 말 그대로 명령 하나입니다.

적대적 자기 감사: 모든 실패 모드는 여러분이 실행한 검사에 대응됩니다

네 번째 규율은 이 권의 교과과정을 출판 전 점검표로 바꿉니다. 5권은 앞의 여섯 부(Part)를 추론 시스템이 옳아 보이면서도 틀릴 수 있는 방식들에 이름 붙이는 데 썼습니다; 감사 규율은 이렇게 말합니다: 출판하기 전에, 여러분의 분야에서 이름 붙은 모든 실패 모드에 맞서 여러분 자신의 시스템을 그것을 위해 지어진 계측 도구로 돌려 보라는 것입니다. 이 권의 다섯 가지에 대해, 점검표 행과 그 커밋된 계측 도구는 다음과 같습니다:

실패 모드	출판 전에 던질 질문	커밋된 계측 도구
추론 지름길	잠재 개념을 지닌 무언가가 잘못된 개념으로부터 올바른 레이블을 얻어 내는가?	`rsbench_lite.py`: 지름길 계수, AccC(개념 정확도), Cls(C)(개념 붕괴, 예측된 개념 출현 벡터의 정규화된 엔트로피를 1에서 뺀 값), 심어진 개념에 맞선 개념 ECE(expected calibration error, 기대 보정 오차)
잘못된 보정	확신을 인용하기 전에, 그 확신이 실제로 무언가를 뜻하는가?	`calibration.py`: 10-빈 ECE, 온도 적합, 전/후 장부
불충실한 설명	설명을 보여 주기 전에, 설명이 메커니즘과 함께 움직이는가?	`faithfulness.py`: 소거 기반 포괄성과 충분성, 무작위-근거 대조
침묵하는 절단	완전성이 여러분이 실제로 돌리는 계산 예산에서도 살아남는가?	`satori_lite.py` 재현율-대-예산: 펼침 깊이가 폐쇄를 덮을 때에만 완전함
비일관성	논리적으로 동치인 재진술 아래에서도 "추론"이 살아남는가?	`entailment_gap.py`: 대우, 확장, 바꿔 쓰기, 드모르간 프로브

각 행이 존재하는 이유는 평범한 정확도가 그 실패를 볼 수 없기 때문입니다: 하니스의 성적표는 계측 도구마다, 정확도가 동점이라고 부르는 두 시스템과 그것들을 결정적으로 갈라놓는 정확도-너머 지표를 짝짓습니다(레이블 정확도는 1.000 = 1.000이지만 개념 정확도는 0.750 대 1.000으로 갈라집니다; 평범한 정확도는 0.9896 대 1.0000이지만 최악-계열 일관성은 0.486 대 1.000으로 갈라집니다). 스위트의 단언들은 이 분리를 느낌이 아니라 마진으로서 지킵니다(suite_harness.py, 363–367번째 줄). 메타 규칙은 이 권을 넘어 일반화됩니다: 여러분의 하위 분야에서 이름 붙은 실패 모드들을 열거하고, 각각에 대해 여러분이 실행한 검사를 가리키거나, 그것을 실행하지 않았다고 소리 내어 말하십시오. 심사자보다 먼저 자기 자신의 작업을 적대적으로 감사하는 것은 자학이 아닙니다; 그것은 정밀 검토에서 살아남는 논문과 아직 어떤 정밀 검토도 받지 않은 논문 사이의 차이입니다 [1]. 그리고 여러분 분야의 점검표에 계측 도구가 없는 행이 있을 때, 여러분은 지어지기를 기다리는 연구 기여 하나를 발견한 것입니다. 이것이 바로 지름길-측정 스위트 자체가 존재하게 된 방식입니다 [3].

정직한 장부: 아픈 열을 보고하기

다섯 번째 규율은 하나의 출판 형식입니다. 이 시리즈의 모든 권은 하나의 평결 장으로 끝나며, 그 형식은 장부입니다: 방법마다 그것이 사는 것, 그것이 치르는 것, 그리고 그 행을 증명하는 커밋된 지킴입니다. 이 형식의 하중을 떠받치는 성질은 치르는 것 열이 사는 것 열과 동등한 지위를 지닌다는 것입니다. 이 권 자신의 숫자들이 그 습관의 결을 공급합니다: 커널의 표제 MRR 0.5680은 그것의 유형별 최악의 숫자(교집합이 투영보다 앞서 오는 질의 유형인 ip에서 0.111)와 오라클의 1.0에 이르지 못한 채 닫히지 않은 격차를 같은 표 안에 나란히 싣습니다; 기권 결과는 답한 질의들에 대한 정확도 1.0을 내세우면서도, 같은 줄에서 그 대가, 곧 커버리지 0.8205, 즉 468개 결정 중 84개가 거부되었다는 것을 밝힙니다; 미니 스위트의 설계 점검표는 실제 벤치마크 스위트가 제도화하는 성질들에 맞대어 스스로를 4개 예, 3개 아니오로 채점하며, 하니스는 그 인정들이 결코 조용히 사라지지 않는다고 단언합니다(suite_harness.py, 369–372번째 줄: "점검표가 아무것도 인정하지 않게 되었다"는 것이 실패 조건입니다). 치르는 것 열이 비어 있는 장부는 마케팅입니다. 자기 자신의 인정을 단언으로 지키는 장부는 측정입니다.

월요일 계획: G5를 처음부터 끝까지 공략하기

이제 방법을 앞으로 돌려 봅시다. 독자가 미해결 문제 지도에 나온 실제 공백 하나를 놓고 월요일 아침에 실제 프로젝트를 시작하고 싶다고 해 봅시다. 다섯 규율은 일곱 단계의 수열로 조합됩니다; 여기서는 G5, 비전이성, 즉 도메인마다 재훈련되어야 하는 추론 시스템, 변환적(transductive)일 뿐인 임베딩, 캡스톤 행 C7이 아직 인용-전용으로 남아 있는 그 공백 위에서 처음부터 끝까지 그것을 실행해 봅니다.

1단계: 계측 도구 준비성으로 고르기. 여러분이 흥미롭다고 느끼는 공백들 가운데, 계측 도구가 이미 존재하는 것을 선호하십시오. 계측 도구를 짓는 시간이야말로 예산을 조용히 갉아먹는 살인자이기 때문입니다. G5는 좋은 점수를 받습니다. 주장 행은 이미 실패하는 기준선(도메인별 재훈련, RRN(Recursive Reasoning Network) 패턴)의 이름을 붙여 두었고, 정확히 무엇이 빠져 있는지도 진술해 두었습니다: 두 번째 온톨로지입니다(satori_eval.py, 644–645번째 줄). 평가 프로토콜도 존재합니다(4권의 고정된 질의 은행과 필터링된 MRR). 장난감 규모에서의 전이 결과조차 선례로 존재합니다: 4권의 ultra_lite.py는 12개 매개변수짜리 구조적 채점기를 제로샷으로 병원 세계에 전이시켜, 무작위 바닥 0.22에 맞서 MRR 0.83을 얻었으며, 관계 재명명 아래에서도 불변이었습니다(examples/integration/validate.py, 91–94번째 줄). 결코 시험된 적이 없는 것은 단순한 링크 채점기가 아니라 자신의 TBox를 지닌 추론 커널 자체가 전이되는가입니다.

2단계: 오라클을 갖춘 장난감으로 범위 좁히기. 목표 규모(이를테면 SNOMED CT에서 유전자 온톨로지로의 전이)는 여러분이 열거할 수 있는 오라클을 허락하지 않습니다. 그러니 범위를 좁히십시오: 자신만의 EL TBox와 겹치지 않는 어휘, 비교 가능한 형태를 지닌 13개에서 15개체짜리 두 번째 세계입니다. 병원 세계가 자연스러운 후보입니다. 임상의, 환자, 병동, 시술을 위한 개체들이 있고, advises와 cites를 거울처럼 비추는 supervises와 treats 같은 역할들이 있습니다. 오라클 스택은 전부 재사용 가능합니다: 2권의 el_completion.py가 새 TBox의 분류를 계산하고, reasoners.py가 HermiT에 맞대어 그것을 교차 검사하며, 1권의 연쇄기가 혼 폐쇄를 계산하고, 4권의 실행기가 정확한 질의 답을 계산합니다. 이틀 오후 분량의 작업이며, 그 어느 것도 새롭지 않지만 전부가 하중을 떠받칩니다.

3단계: 참값 심기. 병원 세계에 하나의 사슬 규칙, grandAdvisor의 유사물(예컨대 두 개의 supervises 엣지로 합성된 지도-임상의 규칙)을 숨기고, query_dag.py가 했던 그대로 닫힌 세계로부터 질의 은행을 생성하십시오. 이제 모든 전이 주장은 심어진 정확한 목표를 지닙니다: 규칙 복원은 점수가 아니라 동일성 검사입니다.

4단계: 주장 표를 사전 등록하기. 어떤 코드보다도 먼저 적어 두며, 정직하게 작습니다:

주장	지표	기준선 / 한계	계측 도구	단계
T1: 학계 세계에서 훈련된 커널이 병원 질의에 제로샷으로 답한다	병원 은행의 하드 정답에 대한 필터링된 MRR	무작위 바닥보다 +0.25 이상; 도메인 내 재훈련(정직한 천장)보다는 낮게	4권에서 고정된 프로토콜을 따르는, 병원 인접 행렬 위의 `godel_eval`	1주차
T2: 규칙 복원이 전이된다	디코딩된 규칙 == 심어진 병원 규칙, 정확히	균등 라우터(우연 = 1/25)	병원 템플릿 위에 재인스턴스화된 C2 라우터	2주차
T3: 크리스프 건전성이 이동에도 살아남는다	τ→0에서 임계값을 매긴 커널 == 모든 병원 질의에 대한 기호 실행기	정확한 동일성, 허용 오차 없음	C1 정합성 검사, 새로운 세계	1주차
T4: 확신이 여전히 의미를 지닌다	병원 ECE ≤ 학계 ECE(0.0186)의 2배	도메인 내 보정	전이된 정도 위에서의 `calibration.py`의 ECE 도우미	2주차
T5: 실패 경계가 실재한다	전이가 무너지는 사전에 이름 붙은 조건이 최소 하나 있음(예: 본 적 없는 역할 서명)	없음: 이 행은 정직하게 채워지기 위해 존재함	어휘 중첩에 대한 절제 실험	3주차

T5는 한마디 논평을 받을 만합니다: 입증된 실패 경계가 없는 전이 논문은 그것을 찾아보지 않은 논문입니다. 그 경계를 찾는 탐색을 사전 등록하는 것은 그것을 찾아내는 일을 창피함이 아니라 성공으로 만들어 줍니다.

5단계: 순서대로 짓기. 오라클이 먼저입니다(병원 TBox, 그 완성, HermiT 교차 검사), 생성기가 둘째입니다(심어진 규칙과 질의 은행), 기준선이 셋째입니다(도메인별 재훈련, 그래야 시스템이 존재하기 전에 비교 대상이 존재합니다), 시스템이 넷째입니다(전이된 커널), 감사가 다섯째입니다(위의 다섯 행짜리 점검표를 여러분 자신의 결과에 대해 실행합니다). 이 순서 자체가 핵심입니다: 각 단계는 그 앞의 단계들에 의해 측정되므로, 측정 불가능한 인공물이 존재하는 순간은 결코 없습니다.

6단계: 자기 감사 실행하기. 지름길: 라우터가 그 작은 은행 안의 가짜 동시 출현으로부터 올바른 규칙을 디코딩해 낼 수 있는가? 계수 도구를 돌리십시오. 보정: T4의 ECE가 존재하기 전까지는 어떤 확신도 인용하지 마십시오. 충실성: 트레이스가 무언가를 설명한다고 주장하기 전에 병원 세계에서 트레이스 말단을 소거하십시오. 절단: 펼침 깊이가 병원 폐쇄의 실제 깊이를 덮는지 검증하십시오. 일관성: 새 은행 위에서 함의 프로브를 돌리십시오.

7단계: 장부 공개하기. 사는 것: 캡스톤 행렬의 인용-전용 행 하나가 커밋된 숫자를 갖춘 장난감 규모에서 검증됨으로 바뀝니다. 치르는 것: 15개체는 SNOMED가 아니고, 하나의 목표 도메인은 도메인들에 대한 분포가 아니며, 심어진 규칙은 규칙 하나뿐입니다. 지킴: T1–T5의 단언, 시드가 붙어 있고, 바이트 단위로 동일하며, 종료 코드 0입니다. 그것이 작은 논문이며, 동시에 진짜 논문입니다: 계획을 포크하고 공백을 바꾸면, 그 골격은 G7에도 그대로 유지됩니다(같은 일곱 단계를, 이미 준비된 계측 도구인 calibration.py, abstention.py, rsbench_lite.py로 실행하십시오), 또는 여러분이 계측 도구를 체크해 낼 수 있는 어떤 공백에도 유지됩니다.

사각지대 목록, 이 시리즈 자신에게 돌리기

자기 자신의 책을 예외로 두는 방법론 장은 스스로의 감사에 실패할 것입니다. 그러므로 마지막 표는 이 시리즈가 자기 자신에 대해 빚지고 있는 표입니다. 위의 다섯 규율은 실재하며, 정확히 그것들이 최적화하는 대상 때문에 다섯 가지를 체계적으로 경시합니다.

지각. 오라클 우선은 오라클이 존재할 수 있는 세계를 편애하며, 그런 세계는 기호가 먼저인 세계입니다. 우리의 개체들은 이미 기호화된 채로 도착합니다; 다섯 권 어디에서도 어떤 픽셀 영역이 alice인지를 결정해야 했던 적이 없습니다. 시각을 마주하는 NeSy(neuro-symbolic, 신경-기호) 프론티어, 즉 장면 그래프, 시각 질의 응답, 지각적 개념 추출은 이 시리즈에서 오직 인용을 통해서만 나타나며, 미니 스위트는 이를 명시적으로 인정합니다: 그것의 개념 추출기는 가우스 군집과 토큰 개수를 보며, "MNIST 숫자도, Blender 장면도, LogiCity의 시뮬레이션 도시도 아닙니다"(suite_harness.py, 319–321번째 줄).

인간 요인. 이 시리즈의 모든 설명은 기계에 의해 평가되었습니다: 소거 프로브, MinA 포함, 충분성 점수입니다. 어떤 사람도 우리의 정당화를 읽고 그것이 도움이 되었는지 보고한 적이 없으며, 어떤 기권 정책도 유보를 신뢰할지 결정하는 사람을 대상으로 시험된 적이 없습니다. 충실성 점수는 유용성 점수가 아닙니다; 둘은 갈라질 수 있고 실제로 갈라지는데, 우리의 증거 사슬 어디에도 그 둘 중 하나만 나타납니다.

적대적 환경. 이 시리즈의 어떤 위협 모델에도 공격자는 없습니다. 우리의 실패 모드는 통계적(지름길, 잘못된 보정)이거나 구조적(절단, 비일관성)일 뿐, 결코 전략적이지 않습니다. 오염된 사실을 지닌 지식 베이스, 소프트맥스 유령을 악용하도록 공들여 만든 질의, 정확도는 건드리지 않은 채 확신을 재구성하는 보정 공격, 이런 것들은 우리의 어떤 계측 도구도 알아채지 못할 것입니다. 그 어느 것도 그쪽을 겨냥한 적이 없기 때문입니다.

컴퓨팅 현실. NumPy 책상은 데이터센터가 아닙니다. 규모 확장 장들은 작업-깊이 개수를 유도하고 시스템 결과를 인용했지만, 다섯 권에 걸쳐 장난감 규모를 넘어서는 모든 규모 확장 숫자는 측정된 것이 아니라 인용된 것입니다; 캡스톤의 C4 행이 이를 인쇄물로 그대로 말합니다. 10억 개 사실에서의 배치된-고정점 거동, 메모리 벽, 통신 비용, 우리의 방법은 이런 질문들의 형태를 시연할 뿐 그 어느 것도 측정한 적이 없습니다.

인용에서의 생존 편향. 우리는 효과가 있었던 것을 가르쳤습니다. 다섯 권의 참고문헌 목록은 살아남은 방법들로 채워져 있습니다; 조용히 실패한 합리적인 발상들의 무덤, 결코 지면에 도달하지 못한 부정적 결과들은, 생존자 편향이 예측하는 바로 그 방식대로 보이지 않습니다. 오직 우리의 참고문헌만으로 "이 분야가 얼마나 어려운가"를 가늠하는 독자는 그것을 과소평가할 것입니다.

이 관행의 커밋된 축소판은 하니스 자신의 설계 점검표이며, 이는 모범이 되는 벤치마크 스위트들이 제도화하는 성질들에 맞대어 미니 스위트를 채점하고, 자신의 인정을 승리와 똑같은 활자로 인쇄합니다:

    [ no] multiple model families per instrument
          one extractor family each; rsbench's harness compares six
    [ no] perceptual concept extraction
          Gaussian corner clusters and token counts, not MNIST digits, Blender scenes, or LogiCity's simulated city
    [ no] public scale: big OOD splits, (eps,delta)-guaranteed counting
          exact enumeration and 10^2-10^3-point probes throughout
    score: 4 yes / 3 no — the no-rows are the
    distance between a runnable miniature and a citable benchmark suite

이 목록을 공개하는 것은 이 작업을 약화시키기는커녕 강화합니다. 인용-전용 열이 주장 표를 강화했던 것과 같은 이유에서입니다: 진술된 한계는 범위가 정해진 주장이며, 범위가 정해진 주장이야말로 실제로 참일 수 있는 주장입니다. 그 대안은 사각지대 없는 책이 아닙니다; 그것은 독자가 힘들게 스스로 발견해야 하는 사각지대를 지닌 책입니다.

아직 풀리지 않은 부분

이 방법 자체에는 측정되지 않은 입력이 하나 있습니다: 안목입니다. 이 장의 모든 규율은 문제가 선택된 다음에 작동합니다; 그 어느 것도 문제를 고르는 데는 도움이 되지 않습니다. 계측 도구 준비성은 여러분이 이미 유망하다고 느끼는 공백들 사이의 승부를 가르는 요인일 뿐, 어떤 공백이 중요한지에 대한 이론이 아닙니다. 그리고 정직하게 관찰하자면, 문제의 선택이 그 하위에서 적용되는 어떤 규율보다도 연구의 결과를 더 크게 좌우합니다. 더 나쁘게도, 이 규율들 자체에도 나름의 선택 편향이 있으며, 이는 방금 사각지대 목록이 이름 붙인 바로 그것입니다: 오라클 우선은 정확한 참조가 존재할 수 있는 문제 쪽으로 끌어당기고, 실험으로서의 주장은 프로젝트의 기한 안에 해결되는 주장 쪽으로 끌어당기며, 이 둘은 가장 어려운 질문들(물리적 세계에 그라운딩된 지각, 사람이 판단하는 설명, 적응적 적대자에 맞선 견고성)을 조용히 무기한 인용-전용 열로 밀어냅니다. 검사 가능성에 이토록 헌신적인 방법이, 참값이 다투어지거나 값비싸거나 사람에게 달려 있는 영역으로, 다시 느낌으로 무너지지 않은 채 확장될 수 있는지는 방법에 관한 미해결 문제이며, 이 장은 그것을 위한 계측 도구를 갖고 있지 않습니다.

왜 중요한가

이 장은 이 시리즈가 실천으로 현금화되는 지점입니다. 다섯 권의 모든 정리를 간직하되 그 어떤 습관도 간직하지 못한 독자는 둘 다 재현하지 못할 것입니다; 오직 습관만을 간직한 독자는 필요한 정리들을 다시 발견해 낼 것입니다. 그 습관들이 정확한 참조와 커밋된 증거와의 접촉을 강제하기 때문입니다. 다섯 규율은 또한 의도적으로 값이 쌉니다: 이 장의 그 무엇도 클러스터나 연구비나 팀을 요구하지 않았으며, 오직 작업의 고정된 순서(오라클, 생성기, 기준선, 시스템, 감사)와 결과가 존재하기도 전에 주장을 적어 두는 배짱만을 요구했습니다. 자기 자신의 연구로 향하는 독자에게 이 이전(transfer)은 직접적입니다: G1–G8 지도는 열린 땅이 어디인지 말해 주고, 이 장은 그 위에서 어떻게 움직일지 말해 주며, companion 스위트들은 그 방법이 책상 규모에서 처음부터 끝까지 실행된다는 것을 보여 주는 작동하는, 포크 가능한 시연입니다. 이 방법이 공급할 수 없는 것, 즉 문제에 대한 안목, 적대자, 사람, 데이터센터를, 이 장은 이제 적어도 이름은 붙여 둡니다. 계측 도구를 우선하는 문화가 자신의 사각지대에 마땅히 갚아야 할 것이 바로 그것입니다.

핵심 용어

오라클 우선(oracle-first): 어떤 학습된 시스템보다도 먼저 목표 의미론의 정확한 참조 구현을 짓는 순서 규율로, 이후의 모든 주장이 그것을 반증할 수 있는 커밋된 절차를 갖게 만듭니다.
심어진 참값(planted ground truth): 생성된 세계 안에 구성에 의해 삽입된 잠재 구조(규칙, 개념 배정)로, 복원이 눈대중이 아니라 정확한 동일성으로 검사될 수 있게 합니다.
실험으로서의 주장 행렬(claims-as-experiments matrix): ⟨주장, 지표, 기준선, 계측 도구, 단계⟩라는 사전 등록 형식입니다; 어느 필드든 빠진 주장은 아직 실험이 아닙니다.
장난감 규모에서 검증됨 / 인용-전용(toy-verified / cited-only): 커밋된 companion이 실제로 시연하는 것과 주변 문헌이 신뢰받는 근거로 쓰이는 것을 갈라놓는 주장 표의 열로, 행마다 그 이유가 진술됩니다.
인식론으로서의 결정론(determinism-as-epistemology): 시드가 붙은 실행, 두 실행 사이의 바이트 동등성, 의미론적 성질에 대한 단언, 타이밍의 제외입니다; 인용되는 모든 숫자를 상시 회귀 테스트로 만드는 관행입니다.
회귀 규율(regression discipline): 커밋된 모든 표제 값을 처음부터 다시 유도하고 매 실행마다 자릿수까지 동등성을 단언하는 것으로, 검사 집합 그 자체도 조용한 삭제로부터 지켜집니다(suite_harness.py).
적대적 자기 감사(adversarial self-audit): 출판 전에 여러분 자신의 시스템을 여러분 분야의 모든 이름 붙은 실패 모드에 맞서 돌려 보는 것으로, 각각이 그 커밋된 계측 도구에 대응됩니다.
정직한 장부(honest ledger): 비용이 이득과 동등한 지위를 지니고 그 인정들 자체가 단언으로 지켜지는, 사는 것 / 치르는 것 / 지키는 것의 출판 형식입니다.
계측 도구 준비성(instrument-readiness): 측정 도구가 이미 존재하는 공백을 선호하는 프로젝트 선정 발견법으로, 계측 도구를 짓는 일이야말로 연구의 숨은 예산이기 때문입니다.
사각지대 목록(blind-spot inventory): 어떤 방법이 체계적으로 경시하는 것에 대한 공개된 목록입니다; 진술된 한계는 범위가 정해진 주장이며, 범위가 정해진 주장은 참일 수 있습니다.

이 장이 이끄는 곳

활주로는 지어졌습니다: 공백은 지도로 그려졌고, 계측 도구는 커밋되었으며, 공백을 계측 도구에 연결하는 방법은 이제 한 페이지에 들어갑니다. 하나의 의무가 남아 있으며, 그것은 이 시리즈에서 가장 오래된 의무입니다. 1권은 기호와 벡터가 서로에게서 대체 무엇을 원할 수 있는지를 물으며 문을 열었습니다; 오라클과 경사와 회로와 커널과 감사로 채워진 다섯 권 뒤에, 이 질문은 마침내 입장이 아니라 증거로 답해질 수 있습니다. 솔직한 평결은 그것에 답함으로써 이 시리즈를 닫습니다: 커밋된 기록 위에서, 기호와 벡터가 실제로 서로에게 빚지고 있는 것은 무엇인가입니다.

Companion 코드: examples/frontier/suite_harness.py는 이 권의 지속적-검증 계측 도구입니다(다섯 개의 계측 도구를 하나의 시드가 붙은 프로토콜 아래 다시 실행하고, 커밋된 26개의 표제 값을 자릿수까지 다시 유도하고 단언하며, 지켜지는 인정들을 갖춘 설계 점검표를 인쇄합니다), 그리고 examples/frontier/satori_eval.py는 이 장에서 인용된 사전 등록된 C1 단언, 심어진-규칙 동일성 검사, 트레이스-대-MinA 교차 검사를 포함해 주장 행렬의 정직한 부분집합을 실행합니다. 위의 모든 숫자를 재현하려면 examples/frontier/에서 python3 suite_harness.py와 python3 satori_eval.py를 실행하십시오; 이름표가 붙은 타이밍 행을 제외하면, 두 실행 모두 실행할 때마다 바이트 단위로 동일합니다.

이 장에서 다루는 내용​

숨은 교과과정, 명시적으로 드러내기​

오라클 우선: 학습기보다 먼저 오는 참조​

실험으로서의 주장: 사전 등록된 행렬​

인식론으로서의 결정론: 스스로를 검사하는 논문​

적대적 자기 감사: 모든 실패 모드는 여러분이 실행한 검사에 대응됩니다​

정직한 장부: 아픈 열을 보고하기​

월요일 계획: G5를 처음부터 끝까지 공략하기​

사각지대 목록, 이 시리즈 자신에게 돌리기​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 장이 이끄는 곳​