솔직한 평결: 뉴로-심볼릭 AI의 현주소
📍 현재 위치: IX부 · 평결 — 23장. 다음 연구 하기: 사각지대와 첫걸음은 공백 지도를 한 명의 연구자가 월요일에 시작할 수 있는 첫 실험들로 바꾸어 놓았습니다. 이 마지막 장은 다섯 권 전체의 장부를 소리 내어 읽으며, 모든 줄에 정착됨 또는 미해결이라는 도장을 찍고, 각 줄을 정직하게 지키는 커밋된 검사의 이름을 붙입니다.
이 시리즈의 모든 권은 하나의 평결로 끝났으며, 모든 평결은 같은 형태를 취했습니다: 순위표가 아니라, 줄은 주장이고 담보는 실행 가능한 코드인 장부입니다. 이 장은 그 형태의 시리즈 수준 사례이며, 이 시리즈가 정직하게 증언할 수 있는 만큼의 신경-기호 AI의 현주소를 다룹니다. 잘 알려진 하나의 분류법이 통합 패턴들을 공통 어휘로 조직했던 이 분야이자 [1], 학습하는 동시에 추론하는 시스템이라는 "제3의 물결"에 대한 논거를, 아래의 평결이 마침내 열정이 아니라 영수증으로 저울질하는 그 분야입니다 [2]. 이 장부를 앞선 세 권의 장부와 다르게 만드는 것은 범위입니다: 이 장의 줄들은 여러 장을 인용하며, 모든 줄은 다섯 개의 실행 가능한 companion 스위트 가운데 하나 안에서, 독자가 오늘 실행하여 그 줄이 아직 참인지를 검사할 수 있는 커밋된 검사의 이름을 답니다. 다시 말해 이 평결은 이 장이 하는 말이 아닙니다. 그것은 여러분이 그 코드를 실행할 때 일어나는 일입니다.
다섯 번의 건설 단계를 거친 건물의 최종 검사를 상상해 보십시오. 나쁜 검사는 연설입니다: 건축가가 여러분을 이끌고 다니며 자신을 믿으라고 말합니다. 좋은 검사는 스위치로 이루어진 벽입니다: 다섯 단계에 걸쳐 설치된 모든 하위 시스템에는 저마다의 시험용 스위치가 남아 있고, 보고서는 그 스위치를 하나하나 눌러 보며 불이 들어오는지 지켜본 기록일 뿐입니다. 이 장이 바로 다섯 권짜리 시리즈를 위한 그 스위치 벽입니다. 스위치 여든 개, 패널 다섯 개, 그것들을 전부 눌러 보는 데 걸리는 시간은 오후 한나절입니다. 정착됨이란 누르면 초록색으로 켜지는 것이고, 미해결이란 "아직 스위치가 설치되지 않았다"고 정직하게 이름표가 붙은 것이며, 보고서는 박수가 아니라 여러분 손에 쥐어진 공구함으로 끝납니다.
이 장에서 다루는 내용
- 장부의 형태, 마지막으로 한 번 더: 2권, 3권, 4권의 평결 장을 각각 한 문장으로 압축하고, 이 시리즈 수준의 반전, 즉 아래의 모든 주장 뒤에 놓인 심장박동으로 인용되는 다섯 개의 하니스 요약 줄을 다룹니다.
- 정착됨, 네 부분으로: 정확함은 프로그램화될 수 있다, 그래디언트는 알려진 값을 치르며 논리를 관통해 흐른다, 깊이에는 물리학이 있다, 신뢰에는 계측 도구가 있다는 것을 다루며, 각 부분은 그것을 다시 유도하는 모듈과 함께 커밋된 숫자들의 목록이고, "정착됨"이란 진술된 규모와 조각 안에서 그러하며, 나머지는 시스템 문헌이 짊어진다는 뜻입니다.
- 미해결, 움츠러들지 않고: 여덟 개의 공백을 계측 도구 준비성과 함께 한 줄씩 다루고, 가장 가까운 다루기 쉬운 프론티어로서의 상호작용 행렬을 다루며, 규모 각주를 남김없이 풀어씁니다.
- 상호 부채: 이 시리즈의 마지막 논증, 즉 기호는 학습에게서 그 구조를 빚지고 벡터는 추론에게서 그 보증을 빚진다는 것을 다루며, 이미 탁자 위에 놓인 영수증만으로 양쪽의 순수주의 모두에 맞서 그것을 방어합니다.
- 방법으로서의 평결: 네 가지 지상 명령(오라클 먼저, 실험으로서의 주장, 모델 곁의 계측 도구, 공개된 장부)과, 이 시리즈의 마지막 유물에 대한 정직한 이름 붙이기를 다룹니다.
장부, 마지막으로 한 번 더
이 평결에 앞서 세 개의 평결이 있었으며, 각각은 한 문장에 들어맞습니다. 2권은 기호가 여러분이 적어 두고 일관되게 유지해야 하는 지식 위에서, 신뢰하고 설명할 수 있는 정확함을 사들인다는 것을 발견했습니다. 3권은 그 거울상을 발견했습니다: 기하는 아무도 적어 두지 않은 지식 위에서 훈련 가능한 그럴듯함을 사들이지만, 그 값은 더는 가질 수 없는 확실함입니다. 4권은 둘 중 어느 쪽에도 왕관을 씌우기를 거부하고 대신 그 둘 사이의 모든 건너감에 값을 매겼습니다. 사는 것, 치르는 것, 지키는 것의 장부에서 "퍼지가 확률보다 나은가?"라는 질문은 "각각은 무엇을 사고, 어떤 커밋된 검사가 그 주장을 지키는가?"라는 질문으로 은퇴했습니다. 그 진행 자체가 이 분야의 설계 공간을 한 바퀴 걷는 것이며, 개관 문헌이 의미론과 추론의 위치와 학습 목표를 따라 지도로 그려 온 바로 그 공간입니다 [3]; 이 시리즈는 그저 하니스를 손에 들고 그 길을 걸었을 뿐입니다.
아래의 시리즈 수준 장부는 그것을 감사 가능하게 만드는 규율을 더합니다: 모든 줄은 그것을 가르친 장을 인용하며, 모든 장 뒤에는 다섯 개의 수락 하니스 가운데 하나가 서 있고, 그 종료 코드가 그 장이 단언한 모든 것에 대한 평결입니다. 그것들의 요약 줄이 이 시리즈의 심장박동이며, 커밋된 실행이 그대로 인쇄하는 그대로 정확히 인용됩니다(examples/logic/README.md 34번째 줄, examples/symbolic/README.md 39번째 줄, examples/neural/README.md 51번째 줄, examples/integration/README.md 62번째 줄, examples/frontier/README.md 67번째 줄):
logic companion: 12/12 competency checks passed
symbolic companion: 13/13 competency checks passed
neural companion: 15/15 competency checks passed (16s)
integration companion: 21/21 competency checks passed (19s)
frontier companion: 19/19 competency checks passed (56s)
여든 개의 검사, 다섯 개의 스위트, 그 전부를 관통하는 하나의 실행 예제: 1권이 소개했고 어떤 권도 결코 버리지 않은 열세 개체짜리 학계 세계입니다. 아래에서 정착됨이라 부르는 모든 것은 바로 이런 뜻에서 정착되어 있습니다: 주장 하나, 계측 도구 하나, 그리고 여러분이 다시 유도할 수 있는 초록 불빛입니다. 미해결이라 부르는 모든 것도 같은 뜻에서 열려 있습니다: 아직 어떤 계측 도구도 존재하지 않으며, 이 장은 그것을 있는 그대로 말합니다.
이 시리즈의 마지막 장부: 왼쪽에는 정착된 네 개의 행이 각각 그것을 참되게 지키는 하니스 심장박동에 연결되어 있고, 오른쪽에는 여덟 개의 미해결 공백과 그 상호작용 화살표가 있으며, 모든 것 아래에 규모 각주가 있고, 공구함이 손을 바꾸어 건네지고 있습니다.
저자가 AI의 도움을 받아 직접 제작한 원본 도해.
정착됨, 첫 번째 부분: 정확함은 프로그램화될 수 있다
첫 번째 정착된 줄은 이 시리즈에서 가장 오래된 것입니다: 추론 절차는 적어 둘 수 있고, 끝까지 실행할 수 있으며, 독립적인 구현과의 정확한 일치를 검사받을 수 있고, 이는 그 밑에 놓인 기계 장치가 아무리 바뀌어도 살아남습니다. 1권의 전방 연쇄기는 실행 예제의 혼 지식 베이스를 세 번의 파동으로 그 최소 고정점까지 닫아 47개의 원자 중 24개를 도출했고, 그 후방 증명기는 모든 소속 질의에서 그것과 일치했습니다. 2권의 EL 완성은 14개 공리짜리 학계 온톨로지를 분류하여 8개의 사소하지 않은 포섭과 2개의 충족 불가능한 개념을 찾아냈고, 전혀 다른 원리 위에 지어진 독립적인 태블로 추론기인 HermiT과 일치했습니다. 이 권은 적대적인 조건 아래에서 같은 고정점을 두 번 더 다시 지었고 같은 동등성을 요구했습니다: GPU 추론은 그 완성을 불 행렬 대수로 벡터화하여 2권의 오라클과 칸 하나하나까지 일치시키는 동시에 100개의 TBox(terminological box, 온톨로지의 공리 집합) 변형을 하나의 쌓인 텐서 패스로 닫았고, 구체화 대 재작성은 같은 질의들에 세 가지 방식으로 답했습니다: 47개의 저장된 사실에 대한 구체화된 조회, 23개에 대한 재작성, 그리고 SLD(선택적 선형 확정절 귀결, selective linear definite resolution) 오라클이며, 셋 모두 전체에 걸쳐 일치했고, DRed(삭제 후 재도출, delete-and-rederive) 삭제 유지보수는 정확히 2개의 사실을 과잉 삭제한 뒤 정확히 1개를 다시 도출했습니다. 네 개의 구현, 세 권의 책, 하나의 답 집합입니다: 정확함은 프로그램 하나의 속성이 아니라 얼마든지 많은 프로그램이 붙들려 있을 수 있는 하나의 계약입니다.
책임감 있게 말해 "정착됨"이 뜻하는 바는 이렇습니다: 진술된 규모와 조각 안에서라는 것입니다. 이 영수증들은 책상 크기의 세계 위의 혼 규칙과 EL 계열에 관한 것이며, 병원 규모의 OWL(Web Ontology Language) DL이나 수십억 개의 트리플에 대한 데이터로그를 인증하지는 않습니다. 그런 체제들은 실재하며, 그 증거는 이 시리즈가 재현하기보다 인용한 시스템 문헌 안에 삽니다: ELK와 CEL 계열의 EL 프로파일 추론기들, Konclude와 HermiT 계열의 표현력 높은 DL 추론기들, RDFox 계열의 병렬 구체화, LUBM, OWL2Bench, ORE 벤치마크 전통입니다. 정착된 주장은 정밀합니다: 의미론은 조각에 따라 달라지지만 규율은 그렇지 않으며, 그 문헌 안의 모든 규모 확장은 이 시리즈가 주머니 속에 지니고 다닌 것과 같은 종류의 오라클에 맞대어 검사될 수 있습니다.
정착됨, 두 번째 부분: 그래디언트는 알려진 값을 치르며 논리를 관통해 흐른다
두 번째 정착된 줄은 4권의 것이며, 그 21개 검사의 장부는 값 열을 눈에 보이게 유지한 세 개의 표제 영수증으로 압축됩니다. 첫째, 서로소-합 수리는 의미론이 가정되는 것이 아니라 선택되는 것이라는 영수증입니다: 실행 예제의 두 grandAdvisor 증명 확률을 마치 서로 배타적인 것처럼 더하면 이 나오는데, 이는 전혀 확률이 아닌 반면, 포함-배제는 이중으로 계산된 공유-사실 논리곱을 빼내어 를 내며, 이는 개의 가능 세계를 전부 열거하여 확인됩니다(분포 의미론이 모든 단계를 유도합니다). 둘째, DeepProbLog의 경사 세미링은 학습이 정확한 추론을 대체하는 대신 그 위에 올라탈 수 있다는 영수증입니다: 컴파일된 회로 위의 한 번의 상향 패스가 질의 확률을 모든 편미분과 함께 돌려주며, 손으로 유도한 그래디언트는 두 개의 독립적인 오라클, 즉 중앙 유한차분(커밋된 최대 불일치 )과 세 개의 도함수 파이프라인에 걸쳐 허용오차까지 일치하는 완전한 autograd 재구현에 답합니다. 셋째, 퍼지·무학습 CLQA의 무학습의 놀라움입니다: 사전 훈련된 1홉 예측기를 퍼지 논리곱과 논리합을 통해 합성하는 것만으로 다섯 가지 다중 홉 질의 유형에 답했으며, 종단간 훈련이 전혀 없었음에도 그래프 순회를 훨씬 웃돌았고, 쉬운 정답을 결코 놓치지 않았으며, 그 증명은 엣지 하나하나까지 검사 가능했습니다.
값 열이 이 줄을 정직하게 지켜 줍니다. 절단: 정확한 계수로부터의 상위- 탈출구(확률이 가장 높은 개의 증명만 남기고 나머지를 버리는 것)는 참값을 향해 오르는 하한이지만(, 커밋된 전시물에서), 자신이 참값으로부터 얼마나 떨어져 있는지는 결코 인증하지 못합니다. 보정 부채: 4권이 만들어 낸 확신 가운데 그 숫자가 뜻한 대로였던 것은 하나도 없었습니다. 개념 위험: 모델은 내부 기호가 잘못된 것을 뜻하면서도 모든 질의 수준 목표를 만족시킬 수 있으며, 이 부채는 이 권이 추론 지름길이라 이름 붙이고 세는 법을 배운 것입니다. 논리를 관통하는 그래디언트는 마치 서명 시점에 정착되는 담보 대출처럼 정착되어 있습니다: 조건은 알려져 있고, 상환은 실재합니다.
정착됨, 세 번째 부분: 깊이에는 물리학이 있다
세 번째 정착된 줄은 이 권이 새로 더한 것이며, 이 시리즈에서 가장 널리 옮겨 쓸 수 있는 교훈입니다: 병렬성, 깊이, 정확함은 소망 목록이 아니라 하나의 예산을 이룹니다. 네 개의 결과가 그것을 조립합니다. 첫째, 작업-깊이 트릴레마의 작업-깊이 장부는 연산 하나하나까지 세어 냅니다: 512개의 노드로 이루어진 관계 사슬을 닫는 데 준순진 엔진은 510번의 순차적 파동에 번의 기본 연산이 들지만, 반복된 불 행렬 제곱은 번의 병렬 단계에 번의 연산으로 그것을 닫으며, 이는 약 의 깊이 절감에 대해 측정된 의 작업 프리미엄입니다. 얕게 사들일 수는 있지만, 그 값은 작업으로 치릅니다.
둘째, 천장입니다. 그 배후의 정리는, 정밀하게 진술하되 여기서 증명하지는 않습니다: 순전파가 비트의 수치 정밀도를 나르는 모든 트랜스포머는(여기서 은 입력 길이이고 은 그 비트 예산이 오직 로그적으로만 자란다는 뜻입니다), 로그공간-균일 TC⁰ 회로족으로 시뮬레이션될 수 있습니다. 즉 상수 깊이, 다항 크기를 갖는 문턱 게이트(입력의 가중합이 문턱값을 넘으면 발화하는 게이트)들의 회로이며, 균일이란 하나의 로그공간 알고리즘이 각 입력 길이에 대해 그 회로를 적어 낸다는 뜻입니다 [4]. 그 귀결은 진짜 천장입니다: TC⁰ 밖에 있다고 증명 가능한 문제라면 무엇이든(그리고 치환군 , 곧 다섯 사물의 120가지 뒤섞임에서의 반복 합성은 Barrington의 정리에 의해 아마도 더 큰 부류인 NC¹, 곧 로그 깊이 회로로 풀리는 문제들의 부류에 대해 완전합니다), 그러한 트랜스포머가 모든 입력 길이에서 그것을 계산할 수 없습니다. 다만 두 부류가 무너지는 경우는 예외인데, 복잡도 이론은 그런 붕괴를 기대하지 않습니다. (companion 자신의 반복 과제는 TC⁰ 안에 머무릅니다; 깊이 천장 장은 그것을 분리의 증인이 아니라 메커니즘 시험대로 씁니다.) 증명은 이 권의 범위를 넘어섭니다. companion이 대신 시연하는 것은 그 물리학의 행동적 그림자입니다: 트랜스포머 깊이의 천장은 고정-깊이 네트워크들의 사다리를 훈련시켜, 깊이 1/2/3에 대해 패리티 일반화가 각각 입력 길이 3/6/6에서 절벽을 맞고, 절벽 너머의 정확도는 우연 수준인 0.506/0.500/0.500(우연선 0.500 대비)에 머무는 반면 깊이-확장 통제군은 계속 따라간다는 것을 지켜보았습니다. 장난감 MLP(multilayer perceptron, 다층 퍼셉트론)에서의 절벽은 메커니즘의 증거일 뿐, 결코 정리의 증명은 아닙니다.
셋째, 교환 비율입니다. 사고 사슬은 그 천장을 빌릴 수 있음을 보였습니다: 길이 5에서 절벽을 맞는(꼬리 정확도 0.159) 바로 그 고정-깊이 모델이, 중간 결과를 내놓고 다시 읽는 것이 허용될 때는 32단계까지 정확하게, 최소 정확도 1.000으로 남으며, 내놓은 단계 하나마다 잃어버린 깊이 한 층을 되사들입니다. 넷째, 빌린 깊이를 신뢰할 만하게 만드는 계약입니다: 강화학습과 검증기는 제안 정책을 증명 검사기 뒤에 게이트로 걸어, 재현율 에서 잘못된 도출의 비율을 에서 정확히 으로 낮추었고, 그런 다음 같은 검증기를 보상으로 써서 정책의 정확한-증명 비율을 에서 로 끌어올렸습니다. 건전함은 재현율을 대가로 사들여졌으며, 그 값은 곡선이 진술합니다. 네 개의 결과, 하나의 교훈이며, 독자가 앞으로 평가할 어떤 아키텍처로도 옮겨 쓸 수 있습니다: 깊이 예산이 무엇인지, 누가 작업 청구서를 치르는지, 그리고 잔여 오차가 정확함의 경계선 중 어느 쪽에 떨어지는지를 물으십시오.
정착됨, 네 번째 부분: 신뢰에는 계측 도구가 있다
네 번째 정착된 줄은 이 권의 무게 중심이며, IX부에 그 자리를 벌어 주는 이유를 한 문장으로 요약합니다: 계측 도구 없는 주장은 이제 필연이 아니라 선택입니다. 신뢰할 만한 추론의 다섯 가지 실패 양식은 저마다 하나의 측정 장치를 받았으며, 그것이 반드시 발동해야 하는 사례와 반드시 발동하지 말아야 하는 사례 양쪽에서 검증되었고, 그 숫자들은 실행할 때마다 그것을 다시 유도하는 하니스에 커밋되어 있습니다.
| 계측 도구 | 그것이 답하는 질문 | 커밋된 분리 | 모듈 |
|---|---|---|---|
| 정당화 열거 | 어떤 공리들이 이 함의를 실어 나르는가? | 4개의 함의에 걸친 7개의 MinA(최소 공리 집합), 개 부분집합 무차별 대입과 동일 | justifications.py |
| 소거 충실성 | 제시된 설명이 실제 이유인가? | 포괄성: 오클루전 0.3659, 어텐션 0.2497, 무작위 0.0789, 정확도 0.9609짜리 모델 하나 위에서 | faithfulness.py |
| 지름길 계수 | 개념이 옳은가, 아니면 레이블만 옳은가? | 레이블 정확도 AccY는 1.000 = 1.000인 반면 개념 정확도 AccC는 0.750 대 1.000으로 갈라짐 | rsbench_lite.py |
| 보정(ECE, 기대 보정 오차) | 확신도가 그 숫자를 뜻하는가? | ECE 0.0245 → 0.0167, 맞춰진 온도 에서; 정확도 0.9683과 AUC(ROC 곡선 아래 면적) 0.9136은 비트 단위로 동일 | calibration.py |
| 기권 곡선 | 시스템이 추측 대신 거절할 수 있는가? | 구조적(번역-증명) 커버리지 0.9293, 오답 0건에서 | abstention.py |
행들을 순서대로 읽으십시오. 정당화는 열거합니다: 각 MinA(최소 공리 집합, minimal axiom set)는 그 결과를 여전히 함의하는 온톨로지의 최소 부분집합이며, Reiter의 적중 집합 트리는 16,384개 공리 부분집합 전체에 대한 전수 탐색과 일치했고, 계산된 모든 보수는 증명 가능하게 그 함의를 무너뜨렸습니다. 충실성에는 소거가 있습니다: 정답을 맞히는 분류기 위의 의도적으로 불충실한 어텐션 패턴은, 그것이 가리키는 것을 지워도 예측이 거의 움직이지 않았기 때문에 붙잡혔습니다. 지름길에는 계수기가 있으며, 여기서 들여온 이론은 정밀한 진술을 받을 자격이 있습니다: 레이블이 개의 잠재 개념에 대한 알려진 불 함수인 과제에 대해(여기서 는 개념 비트의 개수를 셉니다), 레이블만 보는 훈련 목적 함수의 결정론적 최적점들은 정확히 과제 함수와의 합성이 모든 훈련 레이블을 재현하는 개념 사상들이며, 그런 최적점의 개수는 라 적고, 훈련 분포가 지지하는 서로 다른 입력들에 대해 세어진 닫힌 형식을 지닙니다 [5]. 그 유도는 이 권의 범위를 넘어섭니다. companion이 대신 시연하는 것은 그 개수 자체입니다: 전수 열거는 그 닫힌 형식을 정확히 재현하며, 지지집합이 줄어듦에 따라 개 개념의 XOR(exclusive or, 배타적 논리합)에 대해 개의 최적점을, 에 대해 개를 내놓고, 그런 다음 예측된 현상을 보여 줍니다: 완벽한 레이블 정확도, 개념 정확도 0.750, 개념 수준 ECE 0.2467을 지닌 모델이 개념의 단 10퍼센트만 지도받음으로써 1.000과 0.0013으로 수선됩니다. 보정에는 ECE가 있으며, 스칼라 하나로 수선됩니다: 유보된 데이터로 맞춘 온도 하나(표의 )가 정확도 계열 숫자는 전혀 건드리지 않은 채 보정 오차와 음의 로그가능도를 함께 낮추는데, 양의 상수로 점수를 나누는 것은 아무 순서도 바꾸지 않기 때문입니다. 그리고 기권에는 곡선이 있습니다: 하나의 표 안에 세 가지 정책이 있으며, 보정된 확신도 위의 Chow 규칙(커버리지 0.9841, 침묵 오류율 0.0159), 알 수 없는 영역을 거절하는 열린 세계 구간 읽기(커버리지 0.8651), 그리고 구성상 오답이 0건인 것이 그 답이 곧 증명이기 때문에 성립하는 구조적 번역-후-증명 정책입니다.
이 권은 그런 다음 다섯 개의 계측 도구 전부를 하나의 회귀 규율로 묶었습니다: suite_harness.py는 하나의 시드가 붙은 프로토콜 아래에서 모든 계측 도구를 처음부터 다시 실행하고, 커밋된 26개의 표제 숫자 각각이 파일 안에 얼려 둔 값과 자릿수까지 같다고 단언합니다(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}"
커밋된 실행은 이 스위트의 한 줄짜리 평결로 끝나며, 이는 평범한 정확도가 볼 수 없는 다섯 가지 분리이고, 각각은 단언된 마진으로 통과됩니다(suite_harness.py 444–450번째 줄):
SUMMARY suite_harness: checks=26/26 accC_gap=+0.250 ece_gap=-0.0078 comp_gap=+0.1162 cliff_gap=+3 cons_gap=+0.5141 checklist=4y/3n
마지막 필드는 정직성 조항입니다: 이 하니스는 자신의 미니 스위트를, 실제 벤치마크 세대인 rsbench, LogiCity, KANDY의 설계 원칙에 맞대어 채점하며, 책상이 가질 수 없는 세 가지 성질을 인정합니다. 이 점검표가 무엇이든 인정하기를 멈추면 실패하는 단언과 함께입니다(suite_harness.py 369–372번째 줄). 자기 자신을 고발할 수 없는 계측 도구는 마케팅입니다.
미해결, 움츠러들지 않고
공백 장은 여덟 개의 미해결 문제를 지도로 그렸습니다; 이 평결은 각각을 계측 도구 준비성과 함께 한 줄로 되짚어 봅니다. 준비된 계측 도구를 갖춘 미해결 문제는 그것을 갖지 못한 문제와는 다른 대상이기 때문입니다. G1, 정확/학습 가능 분할: 장난감 규모에서는 계측되어 있습니다(심어진 규칙 프로토콜은 라우터 질량 0.9718로 숨은 규칙을 복원하고, 크리스프 극한은 두 고전적 오라클 모두를 복원합니다), 어휘 규모에서는 미해결입니다. G2, 규칙-탐색 폭발: 여기서는 피했지만(25개 템플릿), 그것이 실제로 무는 곳, 곧 수천 개의 관계에서는 계측되어 있지 않습니다. G3, CPU에 묶인 기호 추론: 대리 계측 도구가 존재하지만(쌓인 텐서 패스, 벽시계 시간은 어디에서도 단언되지 않았다고 이름표가 붙어 있습니다), PyReason과 Scallop 계열 엔진에 맞선 초당 질의 수 비교는 여전히 인용-전용으로 남아 있습니다. G4, 온톨로지에 눈먼 규칙 학습: TBox로 지어진 커널 위에서는 절제 실험이 퇴화하므로, 기하학적 증거는 Box2EL과 TransBox 계열에 남아 있습니다. G5, 비전이성: 부분적으로 계측되어 있으며, 4권의 구조적 점수 매김기는 두 번째 장난감 세계로 제로샷 전이했지만(무작위 0.22에 맞선 평균 역순위, 곧 MRR 0.83), 두 번째 온톨로지는 여전히 빠져 있습니다. G6, 설명 충실성: 이 시리즈에서 가장 잘 계측된 공백이며, 소거에 더해 MinA 포함이, 캡스톤에서 포괄성 8/8과 충분성 4/4를 기록합니다. G7, 불확실성, 보정, 지름길: 처음부터 끝까지 계측되어 있으며, ECE, 계수기, 개입 프로브입니다. G8, 메타인지: 기권으로서 계측되어 있으며, 위험에 대비한 커버리지이고, 열린 세계 구간은 "나는 모른다"를 배짱의 실패가 아니라 데이터 모델 안의 값으로 만듭니다.
가장 가까운 미답의 땅은 어느 하나의 공백이 아니라 그것들의 상호작용이며, 그중 셋을 캡스톤은 책상 하나를 기다리는 실험으로 이름 붙였습니다: 라우팅 대 트레이스(학습된 라우터도 참된 최소 정당화를 담은 트레이스를 여전히 만들어 낼까요?), 배치화 대 구간(쌓인 고정점은 열린 세계 주석을 보존할까요, 아니면 벡터화가 조용히 세계를 닫아 버릴까요?), 그리고 훈련 대 보정(종단간 미세 조정은 얼려진 커널이 내거는 보정을 무너뜨릴까요?)입니다. 각각은 이 권이 이미 지은 두 개의 계측 도구를 짝짓습니다; 필요한 실험은 발명이 아니라 조합입니다.
그리고 이제 각주입니다. 위의 모든 정착된 줄 위에 서 있으므로 남김없이 풀어씁니다. 다섯 권에 걸쳐 커밋된 모든 숫자는 책상 위에서 측정되었습니다: 열세 개체, 47개의 원자, 46개의 포섭, 차원이 인 임베딩 모델, 수천 개 매개변수짜리 분류기, 수백 개 점짜리 프로브입니다. 데이터센터급 주장들, 즉 수십억 개의 트리플을 구체화하는 것, 수십만 개의 개념을 지닌 온톨로지를 몇 초 만에 분류하는 것, 실제 언어 모델 위에서 측정된 천장들은 인용에 실려 옵니다. 그리고 인용은 썩을 수 있습니다: 결과는 정정되고, 벤치마크는 포화되며, 코드 링크는 죽습니다. 독자의 감사 의무는 이렇게 따라옵니다: 이 시리즈가 숫자를 커밋한 곳에서는 하니스를 실행하십시오; 인용한 곳에서는 그 인용을 반감기가 줄어드는 주장으로 취급하고, 그것 위에 무언가를 짓기 전에 그 유물을 찾아 그 스위치를 눌러 보십시오.
상호 부채
이 시리즈의 마지막 논증은 정리처럼 생긴 하나의 문장이며, 이제는 그 절 하나하나가 영수증을 지니고 있습니다. 학습 없는 기호는 세계의 너비를 감당할 수 없습니다. 이것은 3권을 열었던, 적히지 않은 엣지의 교훈이자 실행 예제 자신의 역사입니다: 손으로 적은 규칙은 결코 적힌 적 없는 그 엣지를 상위권에 올려놓는 훈련된 기하에 자리를 내주었고(얼려진 무작위 0.1062에 맞선 필터링된 MRR 0.7778, 여기서 필터링이란 이미 알려진 참 엣지를 순위에서 제거하고 채점한다는 뜻이며, 정확한 순회는 정의상 모든 어려운 정답에서 0점을 받습니다), 그런 다음 라우팅된 규칙, 곧 오직 자신의 답만으로부터 숨은 grandAdvisor 규칙을 정확히 복원해 내는 템플릿에 대한 소프트맥스에 다시 자리를 내주었습니다. 누구든 적을 만한 여유가 있는 지식 베이스는 언제나 그 질의들이 필요로 하는 지식의 진부분집합일 뿐이며, 오직 학습만이 그 간극을 건넙니다. 기호 없는 학습은 자신의 약속을 지킬 수 없습니다. 이것은 3권 이래 모든 프로브의 건전성 교훈입니다: 지어졌을 때만 논리를 정확하게 실어 나르는 영역 기하, 자신의 시험 집합에서는 98.96퍼센트 정확하지만 바꿔 말하기 아래에서는 48.6퍼센트만 일관되는 소프트 추론기와 파싱된 모든 프로브에서 100을 유지하는 번역-후-증명 파이프라인, 그리고 그 답이 예측이 아니라 약속이 되기 전에는 여전히 검증기 게이트가 필요했던 보정된 확신도입니다. 그리고 세 번째 절, 중요한 아키텍처란 정확히 각 기둥이 다른 기둥에게 책임을 묻게 해 주는 아키텍처다는 소망이 아닙니다; 그것은 satori_eval.py가 인쇄하는 캡스톤의 커밋된 표입니다(625–651번째 줄):
[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
저 표를 이 분야의 축소판으로 읽으면, 두 순수주의 모두 이미 탁자 위에 놓인 영수증 앞에 무너집니다. 기호적 순수주의자에게: 여러분의 정확한 순회는 아무도 적어 두지 않은 모든 답에서 0점을 받아, 0.230이라는 우연의 바닥에도 못 미치는 MRR 0.1488에 그치는 반면, 같은 연산자의 신경망 절반은 건전성 닻을 그대로 유지한 채 0.568에 이릅니다. 연결주의적 순수주의자에게: 그 표 안의 모든 신경망 숫자는 오직 그 곁에 기호적 계측 도구가 서 있기 때문에, 즉 트레이스 뒤의 MinA, 기권 뒤의 구간, 커널 뒤의 크리스프 극한이 있기 때문에 신뢰할 만합니다. 통합 분류법은 이런 조합들에 이름을 주었고 [1], 제3의 물결 논증은 시스템이 학습하는 동시에 추론해야 한다고 말했으며 [2], 개관 논문들은 그 둘 사이의 설계 공간을 지도로 그렸습니다 [3]. 이 시리즈가 더하는 것은 감사입니다: 한 손에는 오라클을, 다른 손에는 계측 도구를 들고 그 공간을 걸을 수 있으며, 그 걸음에서 살아남는 아키텍처는 서로에게 책임을 묻는 아키텍처들이라는 다섯 권짜리 시연입니다.
마지막 페이지: 방법이 곧 평결이다
위의 모든 개별 숫자를 걷어 내면 남는 것은 하나의 방법이며, 이 시리즈가 첫 장부터 실천해 온 네 가지 지상 명령으로 다시 진술됩니다. 오라클 먼저: 아무리 작더라도 학습된 무엇이든 짓기 전에 그 과제의 정확한 버전을 짓고, 모든 실험 곁에 그것을 실행 가능하게 유지하십시오; 다섯 권에 걸친 모든 건전성 주장은 결국 누군가 수고롭게 적어 둔 오라클에 맞선 하나의 동등성으로 환원됩니다. 실험으로서의 주장: 시스템을 측정하기 전에 그것이 무엇을 해야 하는지를 검사 가능한 주장들의 행렬로 진술하고, 그 행렬이 이 숫자로 검증됨 또는 인용-전용, 그리고 그 이유라고 말하게 하십시오. 모델 곁의 계측 도구: 단언되는 모든 성질에 대해, 독립적이고 실패할 수 있는 측정 장치 하나를 두십시오; 논문이 광고하는 성질의 개수를 세고, 그 계측 도구의 개수를 세어, 그 차이를 홍보 문구로 읽으십시오. 공개된 장부: 숫자를 커밋하고, 무작위성에 시드를 부여하며, 하니스의 종료 코드를 평결로 삼아, "여전히 참이다"가 누군가 신뢰해야 할 평판이 아니라 누구든 실행할 수 있는 명령이 되게 하십시오.
이 시리즈가 정직하게 증언할 수 있는 신경-기호 AI의 현주소는, 이 학문 분야가 이제 처음부터 끝까지 가능하다는 것입니다: 혼 폐쇄에서 EL 오라클로, 훈련된 기하로, 미분 가능한 증명기로, 보정되고 기권하며 트레이스에 충실한 커널로 이어지며, 모든 이음매에 계측 도구가 있고 모든 주장 뒤에 초록불이 있습니다. 그것이 이 시리즈의 마지막 유물이 실제로 무엇인지를 확정합니다. 결론이 아닙니다; 결론은 문장이며, 문장은 다시 실행될 수 없습니다. 독자입니다: 이제 네 개의 작동하는 엔진, 다섯 개의 계측 도구 키트, 세 개의 표시된 상호작용을 지닌 여덟 개 공백의 정직한 지도, 월요일 계획을 소유하고, 이 분야의 다음 결과가 붙들려야 할 그 방법의 모든 단계를 몸소 실행해 본 독자입니다.
아직 풀리지 않은 부분
이 평결 자신의 방법에는 평결 스스로가 닫을 수 없는 미해결 질문이 하나 있습니다: 이 규율이 자신의 오라클을 잃고도 살아남을 것인가입니다. 여든 개의 검사 안의 모든 동등성 단언은, 오직 세계가 작기 때문에 존재하는 참값에 맞서 시스템을 비교합니다: 개 부분집합에 대한 무차별 대입, 전수 열거 가능한 최적점 공간, 두 번째 구현이 하룻밤 사이에 재현할 수 있는 고정점입니다. 이 분야의 진짜 주장들이 사는 규모에서는 오라클이 사라집니다: 어떤 무차별 대입도 십만 개 개념짜리 온톨로지의 정당화들을 열거하지 못하며, 어떤 정확한 계수도 지각 모델의 지름길 census를 인증하지 못합니다. 스위트 자신의 점검표가 정확히 이것을 인정하며, [ no] public scale: big OOD splits, (eps,delta)-guaranteed counting이라는 행을 인쇄합니다. 어떤 오라클도 메모리에 들어맞지 않을 때 오라클-동등성을 대신할 것이 무엇인지는 진정으로 미해결입니다: 명시적인 실패 확률을 지닌 통계적 인증서, 우아하게 저하되는 구간 경계, 시스템 전체가 아니라 개별 답을 인증하는 검증기 게이트입니다. 각 후보는 조각으로 존재합니다; 아직 어느 것도 이 시리즈가 책상 규모에서 실행한 종단간 장부로 조합되지는 못했습니다. 이 시리즈가 기록하는 마지막 미해결 문제는 자기 자신에 관한 것입니다: 방법의 규모를 확장하는 일은 그것이 측정하는 시스템들의 규모를 확장하는 일 못지않게 미해결입니다.
왜 중요한가
이 장은 이 시리즈의 다섯 권이 무엇을 위한 것이었는지에 대한 이 시리즈 자신의 주장입니다. 관광이 아니라 도제 수업입니다: 1권은 독자에게 오라클 짓는 법을 가르쳤고, 2권은 건전성과 완전성을 이름으로 요구하는 법을, 3권은 기하가 무엇을 지탱하는지 측정하고 무엇을 지탱하지 못하는지 고백하는 법을, 4권은 논리적 경계를 건너는 모든 그래디언트에 값을 매기는 법을, 5권은 신뢰를 계측하고 깊이를 세며 홍보 문구가 있어야 할 자리에 주장 행렬을 두는 법을 가르쳤습니다. 옮겨 지닐 수 있는 자산은 반사 신경입니다: 다음 아키텍처가 도착할 때, 그리고 그것은 광고와 함께 도착할 것인데, 질문들은 이미 장전되어 있습니다. 오라클은 어디에 있는가? 어떤 주장들이 실험인가? 그 성질이 가짜라면 어떤 계측 도구가 실패하는가? 장부는 어디에 있으며, 그것은 여전히 돌아가는가? 어떤 분야가 성숙하는 것은 그 시스템이 더는 틀리지 않게 될 때가 아니라, 그 틀림이 측정 가능하고, 귀속 가능하며, 값이 매겨지게 될 때입니다. 다섯 권의 증거는 신경-기호 AI가 책상 규모에서 그 선을 건넜다는 것이며, 다른 모든 규모에서 그 선을 건너는 일은 이제 이름 붙은 진영들 사이의 철학적 논쟁이 아니라 이름 붙은 공백들을 지닌 공학적 의제라는 것입니다.
핵심 용어
- 장부(ledger) — 이 시리즈가 순위표 대신 쓰는 평결 형식입니다: 줄은 주장이고, 열은 사는 것, 치르는 것, 지키는 것이며, 모든 줄은 그것을 참되게 지키는 커밋된 검사를 이름 붙입니다.
- 커밋된 검사(committed check) — 실행 가능한 하니스 안의 단언으로, 그 기댓값이 저장소에 얼려져 있어서 다시 실행하면 그 주장이 자릿수까지 그대로 재현되거나 시끄럽게 실패합니다.
- 오라클-동등성(oracle-equality) — 책상 규모에서 이용 가능한 가장 강력한 정착된-주장 표준입니다: 시스템과 독립적인 정확한 구현 사이의 정확한 일치입니다.
- 계측 도구(instrument) — 하나의 주장과 짝을 이루는 독립적이고 실패할 수 있는 측정 장치로, 반드시 발동해야 하는 사례와 반드시 발동하지 말아야 하는 사례에서 검증되며, 이 권에서 신뢰의 단위입니다.
- 심장박동(heartbeat) — 다섯 개의 스위트 요약 줄(12/12, 13/13, 15/15, 21/21, 19/19)이며, 이들이 함께 초록이라는 것은 이 시리즈 안의 커밋된 모든 숫자가 여전히 재현된다는 뜻입니다.
- 규모 각주(scale asterisk) — 모든 정착된 줄 위에 서 있는 상시 한정어입니다: 책상 위에서 측정되었으며, 데이터센터 규모의 증거는 독자가 반감기가 줄어드는 주장으로 취급해야 할 인용이 실어 나릅니다.
- 상호작용 행렬(interaction matrix) — 이미 계측된 성질들의 쌍(라우팅-트레이스, 배치화-구간, 훈련-보정)이며, 그 결합된 행동은 아직 어떤 커밋된 숫자도 측정하지 못합니다.
- 상호 부채(mutual debt) — 이 시리즈의 마지막 논증입니다: 기호는 학습에게서 적힌 지식 너머로의 도달 범위를 빚지고, 학습은 기호에게서 자신의 출력을 예측이 아니라 약속으로 만들어 주는 보증을 빚집니다.
- 주장 행렬(claims matrix) — 광고된 성질들의 사전 등록된 표로, 모든 행은 숫자를 지닌 장난감 규모에서 검증됨 또는 이유를 지닌 인용-전용으로 해소됩니다; 캡스톤의 C1–C8 표가 이 시리즈의 전시물입니다.
이 장이 이끄는 곳
어디로도 가지 않습니다. 그리고 그것이 바로 핵심입니다: 이것은 마지막 권의 마지막 장이므로, 넘겨받는 것은 다른 장이 아니라 독자입니다. 시리즈 — 이제 당신의 차례는 이 사다리 전체가 시작된 곳이며, 이제는 다르게 읽힙니다: 신입생의 첫 고정점은 여러분의 오라클 패턴이고, 방금 마친 프론티어의 장들은 여러분의 연구 활주로입니다. 이 기계 전체가 다시 조립되는 모습을 새로운 눈으로 다시 보고 싶다면, 이 시리즈가 자신의 깃발을 꽂았던 곳, 실행 예시: 하나의 지식 베이스, 다섯 권의 책에서 시작하여, 같은 열세 개체가 혼 사실에서 보정되고 기권하며 트레이스에 충실한 추론 커널에 이르는 과정을 따라가 보십시오. 이번에는 모든 단계에 여러분이 실행할 수 있는 검사가 있었다는 것을 알아차리면서 말입니다. 지금도 여전히 있습니다. 그것이 이 분야의 현주소이며, 이제 당신의 차례입니다.
컴패니언 코드: examples/frontier/suite_harness.py는 이 권의 회귀 계측 도구입니다(26개의 커밋된 표제 값을 다시 유도하여 자릿수까지 단언합니다); examples/frontier/satori_eval.py는 C1–C8 주장 표를 인쇄합니다; examples/frontier/validate.py는 이 장이 인용하는 19개 검사 전체짜리 장부를 실행하며, 네 개의 자매 하니스(examples/logic, examples/symbolic, examples/neural, examples/integration, 각각 validate.py를 통해)가 나머지 61개의 심장박동 검사를 공급합니다. 이들 가운데 어느 것이든 각자의 디렉터리에서 python3으로 실행하십시오; 이름표가 붙은 벽시계 시간 줄을 제외하면, 이 장의 모든 숫자는 그것들의 커밋된, 바이트 단위로 동일한 출력입니다.