완전성을 넘어선 일곱 난이도 축
📍 현재 위치: VI부 · 벤치마크와 평가 — 15장. 강화학습과 검증기 관문 추론은 표본추출된 사슬과 그 보상 사이에 검사기를 끼워 넣음으로써 V부를 닫았습니다; VI부는 바로 그 엄밀함을 우리 자신에게 돌려, 우리가 보고하는 점수가 실제로 무엇을 측정하는지를 묻는 것으로 문을 엽니다.
추론 문헌의 모든 리더보드는 결국 숫자 하나로 귀결됩니다: 시스템이 맞힌 질문의 비율입니다. 이 장은 그 숫자가 틀린 것은 아니지만 과소결정되어(underdetermined) 있다고 주장합니다. 질문 은행(question bank) 전체에 걸친 정확도는 그 은행에 숨어 있는 난이도 구성에 대한 가중 평균이며, 실패 양상이 정반대인 두 시스템이 오로지 은행이 어떻게 혼합되었는가 때문에 동점을 이루거나 순위가 뒤바뀔 수 있습니다. 그 보수책은 실험과학에서 가장 오래된 발상을 벤치마킹으로 들여온 것입니다: 한 사례를 어렵게 만드는 독립적인 손잡이(knob)들을 식별하고, 각 손잡이가 홀로 돌아가는 생성기를 만들고, 한 번에 한 요인씩만 바꾸어 시스템을 측정함으로써, 성능이 떨어질 때 어느 손잡이가 그것을 끌어내렸는지 말할 수 있게 하는 것입니다. companion 모듈 difficulty_axes.py는 모두가 이미 측정하는 것(완전성, 즉 하나의 유도 과정을 따라가는 재현율) 너머에 있는 이런 손잡이 일곱 개의 이름을 붙이고, 완전성 축을 의도적으로 고정한 채로도 장치 자신의 실패가 여전히 발생하고 집계되는 장치(gadget)로 각각을 실증합니다.
등산객 두 명을 "어떤 등산" 하나에 대한 평균 시간으로 평가한다고 상상해 보십시오. 등산로는 길이, 경사, 고도, 그리고 표지가 얼마나 잘 되어 있는지에 따라 다릅니다. 한 등산객은 체력이 강하지만 표지가 사라지면 속수무책이고, 다른 등산객은 길을 잃는 법이 없지만 긴 오르막에서 지칩니다. 마침 표본으로 뽑힌 등산로들이 짧고 표지가 잘 되어 있다면 첫 번째 등산객이 더 나아 보이고, 등산로를 길고 험하게 바꾸면 순위가 뒤집힙니다. 그 단일 평균은 등산객이 아니라 여러분이 뽑은 등산로 표본에 대해 말해 준 것입니다. 그 해법은 어떤 코치라도 할 법한 일입니다: 가파른 언덕, 긴 평지, 표지 없는 숲에서 각각 시간을 재되, 한 번에 한 가지만 바꾸는 것입니다. 이 장은 추론 시스템에 대해 정확히 이것을 합니다. 유도 깊이가 언덕 역할을 하고, 이 분야가 시간을 거의 재본 적 없는 여섯 가지 지형이 더 있습니다.
이 장에서 다루는 내용
- 교란 요인을 정확하게 만들기: 집계 정확도는 은행의 숨은 난이도 구성으로 가중된, 층위별 정확도의 가중 평균이며, companion의 실제 수치를 가지고 정반대인 두 시스템을 정확히 동점으로 만드는 혼합비를 유도합니다. 그 결과 "누가 더 나은가"는 시스템이 아니라 은행의 속성이 됩니다.
- 통제된 생성기:
ruletaker_lite.py가 (계층화된 어휘를 통해) 유도 깊이를 구조적으로 고정하고, 깊이별로 레이블을 균형 맞추며, 모든 무작위 선택에 시드를 주어 다른 모든 것이 정지해 있는 동안 손잡이 하나만 돌아가게 만드는 방법입니다. - 두 시스템, 두 가지 실패 기하: 커밋된 깊이별 표에서 통계적 추론기는 깊이를 따라 저하되는 반면, 번역-후-증명 파이프라인은 자신이 파싱한 것에 대해서는 깊이에 무관하게 평탄하되 표층 어휘가 흔들릴 때 대신 커버리지에서 대가를 치릅니다.
- 완전성 너머 일곱 축: 건전성, 종료성, 증명 너비, 질의 조인, 의미론 변화, 접지 신뢰, 공학적 규모를 각각 기계적으로 해독하고, 각각을 이 분야의 통제된 벤치마크 설계 계보 속에 놓으며, 각각을 완전성 축을 고정한 채 커밋된 장치로 실증합니다.
- 상호작용과 요인별 설계의 대가: 한 번에 한 요인씩 바꾸는 설계가 놓치는 것, 커밋된 계측기가 이미 드러내고 있는 상호작용, 그리고 아무도 일곱 방향 전체 격자를 돌리지 않는 이유에 대한 산술입니다.
- 진단으로서의 축들: 각 축을 이 시리즈 다른 곳에 있는 그 보수책으로 대응시켜, 저하 프로파일이 점수판이 아니라 보수 메뉴가 되게 합니다.
점수는 미지의 혼합에서 뽑은 표본 하나
평가 은행의 크기를 개의 질문으로 고정합니다. 여기서 은 은행의 크기이며, 각 질문은 숨겨진 난이도 좌표를 하나씩 지닌다고 합시다; 지금은 그것을 유도 깊이(derivation depth) , 즉 답의 증명이 필요로 하는 규칙 적용 횟수라고 둡니다. 를 깊이 에 있는 질문의 개수로, 를 주어진 시스템이 그중 맞게 답한 개수로 쓰고, 깊이별 정확도를 로 정의합니다. 집계 정확도는 맞힌 총 개수를 질문한 총 개수로 나눈 것이며, 그 합을 깊이별로 나누면 가중 평균이 됩니다:
여기서 (원주율이 아니라 아래 첨자가 붙은 그리스 문자 파이입니다)는 혼합 가중치(mixture weight)로, 은행에서 깊이 에 놓인 질문의 비율입니다. 그 대수 자체는 사소하지만, 그 귀결은 그렇지 않습니다. 벡터 는 시스템의 속성입니다. 벡터 는 은행을 만든 사람의 속성입니다. 보고된 점수 는 이 둘을 뒤엉키게 만들고, 만 읽어서는 누구도 이 둘을 풀어낼 수 없습니다. 어떤 모델은 무관한 사실을 무시하는 법을 배워 깊이 2에서의 역량을 사는 반면, 정반대로 하는 모델과 에서 똑같아 보일 수 있습니다; 그 집계는 아무도 적어 두지 않은, 가능한 은행들에 대한 어떤 분포에서 뽑은 표본 하나에 지나지 않습니다.
companion은 이것을 커밋된 수치로 구체화합니다. 4권의 두 계측기는 손대지 않은 채로 실행되어, 동일한 1,500개의 평가 질문에 대해 매우 다른 두 시스템을 채점하며, 그 깊이별 정확도는(소프트 추론기의 프로파일을 , 파이프라인의 프로파일을 라 부르며, 둘 다 아래에서 다시 인용하는 커밋된 표에서 그대로 옮긴 것입니다):
이는 깊이 부터 까지에 대한 값입니다. 커밋된 은행은 깊이를 로 섞으므로 이 되고, 두 집계는 , 으로 나와 파이프라인이 5점 차로 이깁니다. 이제 어떤 은행이라야 이 둘을 동점으로 만들지 물어봅시다. 혼합을 깊이 0과 1로 제한하여 으로 두고, 두 집계를 같게 놓습니다:
항을 한쪽으로 모으면:
커밋된 정확한 분수들을 대입하면, 이고 이므로:
깊이 0에서 31.7%, 깊이 1에서 68.3%를 뽑은 은행은 두 시스템 모두를 정확히 로 채점합니다. 순수하게 깊이 0 질문만으로 된 은행은 소프트 추론기를 1위로 매기고( 대 ), 깊이 2 위주의 은행은 파이프라인을 33점 차로 1위에 놓습니다( 대 ). 그 비교의 부호는 은행 구성의 자유 매개변수입니다. 이것이 바로 난이도 모델 없는 벤치마크 점수가 미지의 분포에서 뽑은 표본 하나에 불과하다는 말의 의미입니다: 그것은 평가자가 소리 없이 를 선택한 내적 (위 첨자 는 전치(transpose)로, 가중치 열벡터를 옆으로 눕혀 행 곱하기 열의 곱이 다시 합 가 되게 합니다)인 것입니다.
이 보수의 틀은 실험 설계(experimental design)에서 옵니다. 통제되지 않은 은행에 대한 집계는 관측적(observational) 점수입니다: 많은 난이도 요인이 한꺼번에 변하기 때문에 저하를 그 어느 하나의 탓으로 돌릴 수 없습니다. 한 번에 한 요인씩 바꾸는 설계(one-factor-at-a-time design)는 모든 요인을 기준선에 고정하고 손잡이 하나만 돌려, 정확도 하락이 그 원인의 이름을 대게 만듭니다. 이 방식의 이정표가 된 통제된 보수책, 곧 이 장이 일반화하는 계열은 깊이-층화 규칙 은행(rulebase) 설계입니다: 인공적인 이론을 생성하고, 모든 질문에 그 증명의 최소 깊이로 레이블을 붙이고, 각 층위 안에서 레이블을 균형 맞추어 클래스 사전확률이 새어 나가지 않게 하고, 집계가 아니라 깊이별 정확도를 보고하는 것입니다 [1]. 이 장의 모든 것은 그 방식을 일반화한 것입니다.
계측기: 구조적으로 깊이가 고정된 생성기
손잡이 하나를 돌리려면 그 손잡이가 통계적으로가 아니라 기계적으로 존재하는 생성기가 필요합니다. 4권의 소프트 추론기 장이 그런 생성기 하나를 지었고, VI부는 이제 그것을 실험 장치의 한 부품으로 읽습니다. 모듈 examples/integration/ruletaker_lite.py는 계층화된 술어 어휘(layered predicate vocabulary)에 걸쳐 통제된 영어로 이론을 표본추출합니다(92–98행): 명시된 4개의 계층-0 술어, 그리고 계층 1, 2, 3의 머리(head)들입니다. 규칙 표본추출기 자체가 바로 깊이 손잡이입니다(ruletaker_lite.py, 125–136행):
def _sample_rule(head: str, rng: np.random.Generator) -> tuple:
"""One rule for ``head``: a positive literal from the layer directly
below (this pins derivation depth to the layer index) plus, with
probability 1/2, one extra layer-0 literal, negated with probability
1/2 — the negation-as-failure ingredient."""
below = [p for p in PREDICATES if LAYER[p] == LAYER[head] - 1]
body = [(False, below[int(rng.integers(len(below)))])]
if rng.random() < 0.5:
extra = L0[int(rng.integers(len(L0)))]
if extra != body[0][1]:
body.append((bool(rng.random() < 0.5), extra))
return (head, body)
계층 의 모든 규칙 머리가 계층 에서 자신의 양의 본문 리터럴을 끌어오기 때문에, 어떤 원자(atom)의 최소 유도 깊이는 곧 그 계층 색인입니다: 깊이 레이블은 구조적으로 부여된 다음 독립적으로 확인됩니다. 레이블 부여기(labeler)는 1권의 1회전 결과 연산자(consequence operator)를 반복하며 첫 등장 회차에서 깊이를 읽어내고(label_with_depth, 182–200행), 모든 양성 레이블은 후방 연쇄기(backward chainer)에 의해 다시 결정됩니다(391–398행). 두 가지 균형 규율이 이 계측기를 완성합니다. 첫째, 유도 가능한 모든 원자는 같은 계층에서 시드로 뽑은 유도 불가능한 원자와 짝지어지고, 둘 다 긍정형과 부정형으로 물어집니다(225–247행). 이는 모든 깊이 층위를 정확히 참/거짓 50/50으로 강제하고 "not"이라는 단어가 레이블에 대해 정보를 전혀 담지 않게 만듭니다(379–386행에서 단언됩니다). 둘째, 모든 무작위성은 단일 시드에서 흘러나오므로 두 번 실행해도 바이트 단위로 동일한 출력이 찍힙니다. 커밋된 균형 점검은 다음과 같습니다:
[3] eval-question balance (per depth: True/False, asserted exactly 50/50)
depth 0: 402 True / 402 False
depth 1: 176 True / 176 False
depth 2: 140 True / 140 False
depth 3: 32 True / 32 False
이것이 균형 잡힌, 깊이-층화 질문 은행의 계보입니다 [1], 그리고 자연스러운 다음 단계는 요인별(factorial) 설계입니다: 첫 번째 손잡이에 맞서 두 번째 손잡이를 돌려 격자를 채우는 것입니다. 기술 논리(description-logic) 계열이 정확히 이것을 했습니다. 유도 깊이 대 언어적 복잡성이라는 두 요인 격자에 걸쳐 추론 문제를 생성하고, 훈련 셀을 넘어서는 일반화를 시험하기 위해 격자 수준의 일부를 떼어 두었습니다 [2]. companion의 두 번째 손잡이는 바로 그 두 번째 종류에 속합니다: translate_prove.py가 돌리는 표층 손잡이입니다.
두 시스템, 두 가지 실패 기하
두 번째 계측기인 4권의 번역 후 증명 파이프라인(examples/integration/translate_prove.py)은 동일한 커밋된 평가 분할을 소비하고 어휘 변이(lexical variation) 손잡이를 추가합니다: 술어가 다섯 단어짜리 동의어 표에 항목을 갖고 있는 모든 평가 질문은 시드로 고정된 확률 로 그 표를 통해 다시 쓰이고, 파이프라인의 엄격한 문법은 그 재작성 중 어느 것도 알지 못합니다(112–118행):
SYNONYM_CORRUPTION: dict[str, str] = {
"productive": "prolific",
"funded": "sponsored",
"published": "printed",
"cited": "referenced", # not in REPAIR_LEXICON: stays out-of-grammar
"senior": "veteran", # not in REPAIR_LEXICON: stays out-of-grammar
}
1,500개 질문 중 288개가 다시 쓰입니다; 1회전 보수 어휘집(repair lexicon)은 다섯 동의어 중 셋을 알고 있으며, 나머지 둘은 일부러 복구 불가능하게 남겨 둡니다. 그러면 커밋된 깊이별 표는 동일한 질문들 위에서 두 시스템을 나란히 놓습니다:
[3] the per-depth factorization table, beside the soft reasoner (same questions)
depth n coverage acc-on-parsed overall soft reasoner
0 804 0.9266 1.0000 0.9266 1.0000
1 352 1.0000 1.0000 1.0000 0.9659
2 280 0.8321 1.0000 0.8321 0.5000
3 64 1.0000 1.0000 1.0000 0.5000
두 기하를 열(column)에서 읽어냅시다. 소프트 추론기(국소 특징 모음(bag-of-local-features) 대역, 깊이 0–1에서 훈련됨)는 깊이 열을 따라 저하됩니다: , 답하기 위해 규칙 두 개를 합성해야 하는 깊이에서 정확히 무작위 확률 수준으로 붕괴합니다. 그리고 이 붕괴는 눈짐작이 아니라 단언됩니다: 모듈은 깊이-3 정확도가 이하이고 깊이 0으로부터 최소 25점 격차가 있을 것을 요구합니다(ruletaker_lite.py, 412–416행). 파이프라인은 자신이 파싱한 것에 대해서는 깊이에 무관하게 평탄합니다: acc-on-parsed 열은 모든 깊이에서 정확히 이며, 이 역시 질문 하나하나에 대해 단언됩니다(translate_prove.py, 298–309행). 파이프라인의 실패는 완전히 다른 열에 살고 있습니다: 커버리지(coverage)로, 어휘 손잡이가 물어뜯는 지점에서 정확히 떨어집니다. 엄격한 문법 아래서는 , 보수 회전 이후에는 입니다(엄격히 더 높아지고 엄격히 1 미만임이 단언됩니다, 311–316행). 파이프라인의 정확성은 로 분해됩니다. 여기서 는 질문 은행 위에서 괄호 안 사건이 일어날 확률을 뜻합니다: 정답의 확률은 파싱 성공의 확률에 정확히 1인 조건부 정확도를 곱한 것과 같습니다. 모든 종단 간 오류는 눈에 보이는 기권이지 결코 소리 없는 오답이 아닙니다. 그래서 파이프라인의 난이도 반응은 기권율인 반면, 소프트 추론기의 반응은 오류율입니다.
계측기가 돌리는 세 번째 손잡이는 부정(negation)입니다. RobustLR의 논리 변경 규칙 편집을 본뜬 [3] 반전 탐침(flip probe)은 규칙 본문 하나를 편집하여 조건 하나를 부정하고, 증명기로 다시 레이블을 매기며, 정답이 뒤집히는 질문만 남깁니다(ruletaker_lite.py, 327–366행):
[5] the RobustLR-style probe: flip one rule negation, relabel, remeasure
gold-flipped questions: 66 stand-in accuracy on them BEFORE the edit: 0.485
tracked after the edit: 54/66 = 0.818 (prover: 1.000 by construction)
소프트 추론기는 66개의 논리 반전 중 54개만 따라잡으며, 놓친 것은 모두 one_step 특징이 새로 부정된 조건을 무시하기 때문입니다. 편집된 이론으로부터 답을 다시 계산하는 파이프라인은 구조적으로 그 전부를 따라잡습니다.
그러므로: 두 시스템, 두 가지 실패 기하입니다. 하나는 깊이를 따라 무너지고 부정에서 비틀거리지만 표층 잡음은 대수롭지 않게 넘깁니다(통계적 판독기는 애초에 파싱하지 않으므로 동의어는 아무 비용도 들지 않습니다); 다른 하나는 깊이를 따라 증명 가능하게 평탄하고 부정 아래서도 정확하지만, 어휘가 흔들리는 순간 커버리지를 잃습니다. 집계값 대 은 5점 차로 벌어져 있으며 이 중 어느 것도 말해 주지 않습니다; 위 절에서는 이 둘을 정확히 같게 만드는 은행 구성을 보여주었습니다. 공개된 통제 생성기들은 같은 정신에서 더 많은 손잡이를 드러냅니다: 홉(hop)의 개수, 사실들의 순서, 그리고 교란(distractor) 가지, 즉 욕심 많은 판독기가 헤매어 들어가는 무관한 규칙 사슬로, 깊이가 고정되어 있어도 오류를 지배하는 것으로 밝혀집니다 [4]. 각 손잡이는 하나의 축이며, 축별 보고야말로 저하를 귀속시킬 수 있게 만드는 것입니다.
완전성 너머 일곱 축, 각각에 고정된 장치 하나
지금까지의 모든 손잡이는 여전히 하나의 사물 계열을 측정합니다: 단조로운 유도 과정을 따라가는 재현율입니다. 시스템이 깊이 에서, 표층 잡음을 뚫고, 함의된 답을 되찾았는가? 이것을 완전성 축(completeness axis)이라 부릅시다. 프론티어 companion examples/frontier/difficulty_axes.py는 이 장의 구조적 주장을 실행 가능하게 만듭니다: 완전성과 직교하는 최소 일곱 개의 추가 축이 추론기를 어렵게 만들며, 직교성은 경험적 주장이므로 각 축에는 엄격한 규율로 설계된 유한한 장치가 주어집니다. 모든 장치에서 완전성 축은 고정됩니다: 그 안의 추론기는 완전한 고정점까지 실행되거나, 재현율이 정확히 1로 측정되거나, 비교되는 조건들 사이에서 유도 깊이가 상수로 유지됩니다. 그러고 나서도 장치 자신의 실패는 여전히 발생하며 집계됩니다(run(), 412–435행은 일곱 장치를 모두 실행하는데, 각 장치는 자신의 고정 단언을 지니며, 건전성 고정과 대표 실패들을 다시 단언합니다). 깊이-완전한 추론기는 일곱 가지 방식 모두로 동시에 실패하며, 어떤 깊이 예산도 그중 어느 것도 고쳐 주지 못합니다.
고정된 완전성 허브에서 뻗어 나가는 일곱 개의 직교하는 난이도 축, 각 바퀴살은 그 장치의 커밋된 측정값을 담고 있다; 삽입된 띠는 두 계측기의 정반대 실패 기하를 보여준다.
저자가 AI의 도움을 받아 직접 제작한 원본 도해.
이 표는 모듈을 한 화면에서 읽어 냅니다; 이어지는 하위 절들은 각 축을 빠르게 다루며, (a) 그것이 기계적으로 무엇에 부담을 주는지, (b) 선험적으로(a priori) 어떤 시스템 부류가 타격을 입어야 하는지, (c) 커밋된 측정값을 제시합니다.
| # | 축 | 장치가 돌리는 것 | 고정된 통제 | 커밋된 측정값 |
|---|---|---|---|---|
| 1 | 건전성(soundness) | 실제 TBox 위의 과잉 일반화된 포섭 예측기 | 재현율 정확히 | 정밀도 , 22개의 날조된 쌍 |
| 2 | 종료성(termination) | 체이스(chase) 아래 하나의 존재 지도교수-역행(advisor-regress) 규칙 | 종료하는 통제 조건은 10개 원자에서 포화되어 그대로 머무름 | 크기 , 결코 포화되지 않음 |
| 3 | 증명 너비(proof width) | Horn 사다리 대 그 선언적(disjunctive) 쌍둥이 | 둘 다 가지당 깊이 20 | 잎 1개 대 1,024개 |
| 4 | 질의 조인(query joins) | 순환 질의(cycle query)의 변수 개수 | 동일한 6개 간선 그래프, 동일한 "예" 답 | 탐침 42 → 2,274 |
| 5 | 의미론(semantics) | 실패로서의 부정(negation-as-failure) 규칙 하나 | Horn 핵심부는 20개 후보 추가 전부에서 단조성이 검증됨 | 추가된 사실 하나가 결론을 철회시킴 |
| 6 | 신뢰(trust) | 레이블이 뒤바뀐 개념 추출기 | 두 추출기 모두 과제 정확도 | 개념 정확도 대 |
| 7 | 규모(scale) | 사슬 길이, 단순(naive) 대 준단순(semi-naive) 평가 | 동일한 폐쇄, 동일한 파동 깊이 | 탐침 비율 |
축 1: 건전성, 완전성이 볼 수 없는 오류
완전성은 여러분이 찾아낸 함의를 세고, 건전성은 여러분이 날조한 것을 셉니다. 이 장치는 2권의 완결된 학계 TBox(terminological box, 용어 상자: 온톨로지의 개념 수준 공리들) 분류에 대해 과잉 일반화하는 포섭 예측기를 실행합니다: 참이 그렇게 말할 때 또는 두 개념이 (최상위 개념, 모든 것을 포섭하는 보편 클래스로, 코드의 TOP) 이외의 어떤 포섭자(subsumer)를 공유할 때 (읽는 법: 모든 는 이다, 즉 개념 가 에 포섭된다)를 예측합니다(axis_soundness, 87–118행):
truth = {(a, b) for a in names for b in names
if a != b and b in S[a]}
pred = {(a, b) for a in names for b in names if a != b
and (b in S[a] or (S[a] & S[b]) - {TOP, a, b})}
예측 집합은 구조적으로 참의 초집합(superset)이므로, 진양성(true positive)을 라 하고 세로 막대 를 집합에 든 쌍의 개수를 세는 표기라 하면, 으로 정확히 나옵니다: 완전성이 고정된 것입니다. 그러나 입니다: 예측기는 22개의 포섭 관계를 날조하며, 그 대표 사례는 공유된 포섭자 Researcher로부터 주조된 Professor ⊑ Student입니다. 선험적으로 이 축은 기하학적 예측기를 가장 크게 다치게 합니다: 3권의 상자(box) 및 순서(order) 임베딩은 정확히 이런 완전하지만 건전하지 않은 태도를 기본값으로 삼는데, 겹치는 영역이 온톨로지가 결코 허가한 적 없는 관계를 주장하기 때문입니다. 재현율만 채점하는 벤치마크는 이 축에 대해 아무것도 증명하지 못하는데, 두 오류 방향이 서로 독립적이기 때문입니다.
축 2: 종료성, "마침내 완전함"이 결코 도래하지 않을 때
이 장치는 2권의 제한된 체이스(chase)에 존재 규칙 하나, 즉 지도교수 역행(advisor regress, 모든 연구자는 어떤 연구자에게 지도받았다) 규칙을 먹입니다. 이 규칙은 발화(firing)할 때마다 새로운 익명 개체를 하나씩 주조합니다. 단계 예산 10, 20, 40에서 인스턴스는 각각 21, 41, 81개 원자로 자라나며 매 상한에서 여전히 불포화 상태이고 그때마다 엄격히 더 커집니다; 종료하는 통제 규칙들은 3회 발화 후 10개 원자짜리 고정점에 도달하고 예산이 네 배가 되어도 움직이지 않습니다(axis_termination, 126–152행). 여기서 기계적으로 가해지는 부담은 완전함을 따질 고정점 자체가 없다는 것입니다: 재현율은 어떤 유한 예산에서도 정의되지 않으며, 그래서 완전성 축은 실패한 것이 아니라 성립 이전입니다. 이 장치는 계속 자라나는 실행을 보여줄 수는 있지만, 어떤 예산으로도 결코 충분해지지 않을 것이라고 증명할 수는 없습니다. 그리고 2권의 체이스 장은 이 질문을 일반적으로 결정하는 문제에 대한 고전적인 부정적 결과들을 담고 있습니다. 이 축은 자신의 평가가 유계 폐쇄(bounded closure)를 전제하는 모든 시스템을 다치게 합니다: 구체화(materialization) 엔진, 고정 깊이로 펼쳐진 네트워크, 그리고 어떤 규칙 은행의 "그" 폐쇄에서 수확된 모든 벤치마크가 그렇습니다.
축 3: 증명 너비, 같은 깊이에 의 청구서
깊이는 하나의 증명 가지를 따라가는 규칙 적용 횟수를 세고, 너비(width)는 가지의 개수를 셉니다. 이 장치는 개의 가로대(rung)를 가진 두 개의 명제 사다리를 만듭니다(ladder, 160–174행):
cl: list[tuple[frozenset, tuple]] = []
for i in range(k):
if disjunctive:
cl.append((frozenset({f"a{i}"}), (f"b{i}", f"c{i}")))
cl.append((frozenset({f"c{i}"}), (f"a{i + 1}",)))
else:
cl.append((frozenset({f"a{i}"}), (f"b{i}",)))
cl.append((frozenset({f"b{i}"}), (f"a{i + 1}",)))
return cl
Horn 쌍둥이는 단계를 밟고, 선언적 쌍둥이는 그 첫 단계를 (는 논리합, 즉 "또는")로 바꿉니다. 고전적인 경우 나누기(case-splitting) 증명기는 모든 선언지의 가지에서 목표를 확립해야 하므로, 가로대마다 증명 트리가 둘로 갈라집니다. 가로대 이후 열린 가지의 개수를 라 쓰면, 그 점화식은 일 때 이고, 이를 가로대 하나씩 풀어내면 가 됩니다. 어느 한 가지를 따라가도, 가로대마다 분기 하나와 확정적 발화 하나의 비용이 들므로, 두 사다리 모두에서 모든 가지는 정확히 깊이 에서 닫힙니다. 커밋된 실행은 두 수치 모두를 확인해 줍니다: 둘 다 가지당 깊이 20, 잎은 1개(Horn) 대 개(선언적), 그리고 그 깊이 동등성이 단언됩니다(axis_width, 210–227행). 너비는 어떤 깊이 예산으로도 치를 수 없는 두 번째의, 독립적인 청구서입니다. 이것은 Horn형 포화가 다항식인 EL과, 표(tableau)가 경우를 나누어 추론해야 하는 표현력 있는 논리들 사이에서 2권이 건넜던 절벽입니다. 선험적으로 이 축은 탐색 기반 증명기, 그리고 결코 끝나지 않는 트리의 한 가지를 자신의 추적(trace)으로 삼는 모든 사고 사슬(chain-of-thought)을 다치게 합니다.
축 4: 질의 조인, 질문 안에 사는 난이도
데이터를 완전히 얼려 놓아도 난이도는 여전히 자랄 수 있습니다. 질의 안에서 말입니다. 이 장치는 규칙이 전혀 없는 하나의 변하지 않는 6개 간선 그래프 위에서 불(Boolean) 순환 질의를 평가합니다: 이 질의는 변수 를 채울 노드들이 존재하는지(, 존재 한정사)를 묻되, 나열된 모든 간선이 동시에 성립하여(, 논리곱, 즉 "그리고") 순환을 닫도록 요구합니다. 적어 보면 이고, 여기서 는 변수의 개수입니다(axis_query, 239–260행):
[4] query joins — cycle queries over one 6-edge graph, no rules
k vars probes witnesses answer
2 42 6 yes
3 114 6 yes
4 258 18 yes
5 546 30 yes
6 1122 66 yes
7 2274 126 yes
data and entailment depth frozen; the bill is the query's alone
비용이 아닌 두 열은 손으로 유도할 수 있으며, 그렇게 해 볼 가치가 있습니다. 그것이 인스턴스가 결코 바뀌지 않았음을 증명해 주기 때문입니다. 그래프는 세 개의 노드 위에 있는 완전한, 루프 없는 유향 그래프이며, 인접 행렬은 입니다. 여기서 는 모든 성분이 1인 행렬이고 는 항등행렬입니다(관례적인 대신 이라 쓰는 이유는, 가 이미 이 장의 집계 점수를 가리키는 이름이기 때문입니다). 에 대한 증인(witness)은 에 노드를 배정하되 연속하는 모든 간선이 존재하게 하는 배정이며, 이는 정확히 길이 인 닫힌 보행(closed walk)입니다. 닫힌 -보행의 개수는 번째 행렬 거듭제곱의 대각합(trace, 대각 성분들의 합)인 입니다. 이 대각합에는 닫힌 형태가 있으며, 행렬 곱셈 이상의 어떤 도구도 없이 도달할 수 있습니다. 재료는 두 가지입니다. 첫째, 입니다: 의 각 성분은 1로 된 행과 1로 된 열의 곱, 즉 짜리 항 세 개의 합이므로 모든 성분이 입니다. 둘째, 꼴의 조합에 를 곱해 항별로 전개하면 가 됩니다: 여전히 와 의 조합입니다. 따라서 의 모든 거듭제곱은 이 꼴을 가지며, 에 대한 귀납법이 그 계수를 확정합니다:
일 때 이 주장은 이 되어 참입니다. 에서 성립한다고 가정하고 을 한 번 더 곱하되, 위의 전개를 , 에 적용합니다. 새 계수는 이고, 새 계수는 로, 정확히 에서의 주장입니다. 와 의 대각 성분은 모두 이므로, 각 행렬은 자신의 계수의 배를 대각합에 기여합니다:
계산해 보면: 는 , 은 , 는 , 그다음 , , 입니다. 커밋된 증인 열은 항목마다 정확히 일치합니다. 한편 확실한 불 답은 모든 에서 동일한 비트 하나이지만, 집계된 조인 탐침은 로 늘어나며, 연속 비율 은 변수 하나가 추가될 때마다 조인 전선(frontier)을 곱하는 외차수(out-degree)인 를 향해 떨어집니다. 이것은 데이터베이스 이론의 데이터 복잡도(data complexity)와 결합 복잡도(combined complexity) 사이의 구별을 증명이 아니라 실증하는 것입니다: 청구서는 오로지 질문의 구조만의 함수일 수 있습니다. 이 축은 질의를 공짜로 취급하고 데이터만을 유일한 크기 매개변수로 취급하는 모든 평가기를 다치게 하며, 이는 대부분의 지식 그래프 벤치마크에 해당합니다.
축 5: 의미론 변화, 사실을 추가하면 결론이 철회될 때
완전성 이야기는 단조 성장을 전제합니다: 입력이 많아지면 출력은 결코 줄어들지 않는다는 것입니다. 이 장치는 먼저 Horn 핵심부에 대해 그 전제를 검증합니다: Horn 프로그램의 사실들을 , 추가 후보 사실 하나를 , 1권 연쇄기(chainer)의 최소 고정점(least fixpoint)을 라 쓰면, 20개 후보 사실 추가 각각에 대해 , 즉 더 작은 프로그램의 모든 결론이 더 큰 프로그램의 결론에 담겨 있음(, 부분집합이라는 뜻)을 확인합니다. 그런 다음 실패로서의 부정(negation-as-failure) 규칙 하나를 추가합니다: "independent(X) if person(X) and not advised(X)"이며, 이는 계층화된(stratified) 방식으로 평가됩니다(_naf_independent 및 axis_semantics, 268–305행). 기본 학계 세계에서는 alice가 지도받지 않은 유일한 사람이므로 independent(alice)가 성립합니다; 단 하나의 사실 advises(bob, alice)를 추가하면 그 결론은 철회됩니다: 커밋된 실행은 before: ['alice'] after adding advises(bob, alice): {}를 출력합니다. 결과 연산자가 반단조(antimonotone)가 된 것입니다; 고정점의 대수가 바뀐 것이지 그 깊이가 바뀐 것이 아닙니다. 이것은 반전 탐침이 소프트 추론기에서 행동으로 포착했던 것과 같은 현상이며, 이제는 구조적으로 위치를 찾은 것입니다. 그리고 이 축은 훈련 분포가 결론이란 오직 쌓이기만 한다고 가르친 시스템을 정확히 다치게 합니다.
축 6: 신뢰, 엉뚱한 것에 대한 옳은 답
이 장치는 학계 세계의 다섯 사람에 대해 두 개의 개념 추출기를 만듭니다: 충실한 쪽은 참인 professor/student 개념을 읽어 내고, 뒤섞인 쪽은 그 둘을 맞바꿉니다. 하위 과제인 "researcher(x) = professor(x) or student(x)"는 두 개념에 대해 대칭적이므로, 두 추출기 모두 모든 사람에 대해 동일한 판정을 내립니다: 과제 정확도는 대 으로 구별이 불가능하지만, 개념 정확도는 대 입니다(axis_trust, 310–340행). 이는 추론 지름길이 헤아렸던 ( 계승(factorial), 개의 개념 레이블을 순열로 뒤바꾸는 경우의 수이며, 여기서 는 개념의 개수입니다)개의 잘못-접지된 최적점 중 경우이며, 여기서는 그 분류 체계 속의 한 좌표로서만 고정되어 있습니다: 시스템은 건전하고 완전하면서도 의미에 대해서는 틀릴 수 있으며, 어떤 혼합에서든 어떤 행동적 벤치마크 점수도 이를 볼 수 없습니다. 이 축은 특히 신경-기호 스택을 다치게 하는데, 그것들이야말로 자신의 중간 기호가 무언가를 의미한다고 주장하는 시스템이기 때문입니다.
축 7: 규모, 같은 논리에 불어나는 청구서
마지막 축은 순수한 공학입니다. 이 장치는 인용 사슬 개 간선에 대해 동일한 두 개의 이행적 폐쇄(transitive-closure) 규칙을 닫는데, 한 번은 단순(naive) 평가로(매 파동마다 모든 규칙을 전체 저장소에 대해 다시 조인함), 한 번은 준단순(semi-naive) 평가로(각 회차를 이전 회차의 델타로 시드하여 어떤 규칙 인스턴스도 다시 유도되지 않게 함) 닫으며, 모든 크기에서 두 폐쇄가 1권의 오라클과 같고 둘 다 동일한 파동 깊이를 지불한다는 것을 단언합니다(axis_scale 및 seminaive_lfp, 349–407행):
[7] scale — naive vs semi-naive on growing citation chains
m closure waves naive semi ratio
8 44 8 1,776 340 5.2x
16 152 16 24,480 2,344 10.4x
32 560 32 368,192 17,488 21.1x
폐쇄 크기는 정확히 입니다. 여기서 는 "개 중 2개 고르기"라 읽으며, 사슬의 개 노드 가운데 2개를 고르는 경우의 수, 곧 로서 사슬을 따라 있는 모든 순서쌍을 세고, 여기에 기본 간선 개를 더합니다: , , . 사슬은 번의 파동을 강제하고, 저장소는 차수의 원자로 자라나므로, 단순 평가의 청구서는 파동 곱하기 저장소, 즉 차수로 늘어나는 반면 준단순의 청구서는 차수입니다: 그 비율은 에 대해 선형으로 자라야 하며, 커밋된 비율 은 동일한 논리와 동일한 깊이 위에서 이 두 배가 될 때마다 두 배가 됩니다. 이것은 RDFox 같은 구체화 엔진이 생계를 꾸리는 축이며, GPU 추론은 이미 그 배치화된 사촌을 보여주었습니다; 데이터 크기를 고정하는 벤치마크는 이 손잡이를 전혀 돌리지 않습니다.
상호작용, 정직하게 한계 지어진
한 번에 한 요인씩 바꾸는 설계가 저렴한 이유는 그것이 불완전하기 때문입니다. 축마다 개의 수준이 있고(예컨대 : 꺼짐, 보통, 어려움) 축이 일곱 개라면, 요인별 설계는 기준선 셀 하나에 더해 각 축 하나씩만을 그 개의 비기준선 수준에서 측정합니다:
이 설계가 볼 수 없는 것은 상호작용(interaction)입니다: 정확도 곡면이 가산적이지 않은 경우, 즉 인 경우로, 두 손잡이를 함께 돌리면 각각 홀로 돌렸을 때의 비용의 합보다 더(또는 덜) 든다는 뜻입니다. 깊이와 교란(distractor)이 복합되는 것이 전형적인 우려 사항입니다: 깊이 1에서는 2점을 깎는 교란이 깊이 3에서는 20점을 깎을 수 있는데, 홉이 하나 늘어날 때마다 무관한 가지로 헤매어 들어갈 확률이 곱해지기 때문입니다.
커밋된 계측기들은 이미 하나의 상호작용을 드러내고 있으며, 이는 초대받지 않고 나타난 것이기에 주의 깊게 읽어 볼 가치가 있습니다. 파이프라인의 커버리지 열은 깊이에 걸쳐 상수가 아닙니다: . 어휘 손잡이는 균일하게 돌려졌는데, 왜 깊이 2가 가장 많이 대가를 치를까요? 동의어 표가 술어에 붙어 있고, 그 술어들이 계층에 묶여 있기 때문입니다: 복구 불가능한 "senior → veteran"은 깊이-2 머리에 부딪히므로 깊이 2가 커버리지를 잃고, 복구 불가능한 "cited → referenced"는 명시된 계층-0 술어에 부딪히므로 깊이 0이 잃습니다; 깊이-1과 깊이-3 술어는 복구 가능하거나 그 표에 아예 없으므로, 보수 회전 이후 그 커버리지는 정확히 으로 돌아옵니다. 어휘 축의 효과는 하나의 숫자가 아니라 깊이의 함수입니다. 요인별 보고였다면 이것을 커버리지 수치 하나로 평균 내어 그 지형을 잃어버렸을 것입니다.
정직한 해법은 전체 요인별(factorial) 설계일 것이며, 그 산술이 왜 이 분야가 그것을 돌리지 않는지를 설명해 줍니다. 일곱 축을 세 수준으로 하면 개의 셀이 됩니다. 어떤 셀의 정확도를 95% 신뢰 반폭(half-width) 로 분해하려면, 이항 분포 최악의 경우 일 때, 반폭 공식 를 셀당 표본 크기 에 대해 풀면 다음이 필요합니다:
그러므로 그 격자는 시스템당, 시드당 개의 레이블 붙은 질문을 필요로 하며, 모든 레이블은 증명으로 검증되어야 합니다. 그래서 프론티어 모듈은 어떤 요인별 격자도 커밋하지 않습니다; 그 일곱 장치는 선언된 정책에 따라 요인별 설계이며, 각각에서 완전성이 고정되어 있고, 위의 두-손잡이 상호작용은 설계된 셀이 아니라 계측기가 우연히 제공해 준 관측입니다. "난이도"를 통제한다고 주장하는 어떤 벤치마크 논문이든 이 산술에 비추어 읽어야 합니다: 일곱 축만 온전히 통제하는 데도 여섯 자리 숫자짜리 질문 은행이 필요합니다.
진단으로서의 축들: 보수 메뉴
귀속 가능한 저하의 요점은, 일단 이름이 붙고 나면 각 축을 겨냥한 문헌이 존재한다는 것입니다. 커밋된 표들을 진단으로 읽고, 이 시리즈를 약국으로 읽으십시오:
- 깊이는 상수-깊이 아키텍처가 순차적 유도를 시뮬레이션해야 할 때 떨어집니다; 그 완화책은 디코딩 시점의 순차 계산이며, 이는 사고 사슬과 그 천장을 다루는 트랜스포머 깊이의 천장의 주제입니다.
- 어휘 변이는 엄격한 파서로부터 커버리지를 굶깁니다; 그 완화책은 정확히 파이프라인 자신의 보수 루프(파싱 이전 정규화)와 더 풍부한 번역기이며, 커버리지 대 건전성의 거래는 기권에서 값매겨져 있습니다.
- 부정과 의미론 변화는 단조로운 데이터로 훈련된 시스템을 깨뜨립니다; 반전 탐침으로부터 얻은 4권의 교훈은 논리를 바꾸는 편집 아래서 평가하는 것, 그리고 비단조적 구성물을 학습기가 보기도 전에 계층화된 형태로 컴파일해 두는 것입니다. 여기서 레이블 부여기가 하는 일이 바로 그것입니다.
- 교란(distractor)은 주의(attention)와 검색(retrieval)의 문제입니다: 욕심 많은 판독기는 잘못된 가지를 따라가며 [4], 그 해법은 선택을 유도와 분리하여 채점하는 것입니다.
- 고정된 재현율에서 나타나는 건전성 실패는 보정된 신뢰도와 선택적 답변을 요구합니다: 보정과 이 권에서 앞서 지은 위험-커버리지 기구가 그것입니다.
- 종료성은 증명서가 딸린 예산을 요구합니다: 맨 점수가 아니라 포화됨 대 중단됨을 보고하는 규율이며, 이는 구체화 대 재작성이 공식화한 것입니다.
- 너비는 더 많은 깊이가 아니라 탐색 정책을 원합니다: 경우 예산, 절 순서, 그리고 앞 장의 검증기 관문 표본추출이 그것입니다.
- 신뢰는 개념 수준의 감사를 요구하는데, 어떤 과제 점수도 그 궤도(orbit)를 볼 수 없기 때문입니다; 추론 지름길과 식별 가능성이 바로 그 감사입니다.
- 규모는 공학적 답을 지닌 공학적 축입니다: GPU 추론에서처럼 준단순 델타와 배치화된 고정점이 그것입니다.
하나의 집계를 보고하는 리더보드는 순위를 매길 수 있을 뿐이지만, 축별 표는 처방할 수 있습니다. 그 차이가 이 장이 VI부의 나머지 부분에 수출하는 것입니다.
이 분야의 벤치마크가 통제하는 것
일곱 축 격자 위에 놓고 보면, 이 분야의 통제된 생성기들은 각각 몇 개의 축을 잘 고정하고 나머지는 느슨하게 둡니다. 아래 표는 그 조사를 압축한 것입니다; 각 행은 그 설계 의도가 정확히 이 장의 규율이었던 생성기 계열입니다.
| 생성기 계열 | 의도적으로 돌리는 축 | 홀드아웃 규율 | 느슨하게 남긴 것 |
|---|---|---|---|
| 깊이-층화 규칙 은행 (RuleTaker) [1] | 유도 깊이(층위), 폐쇄 세계 부정, 층위별 레이블 균형 | 훈련된 층위를 넘어선 시험 깊이 | 증명 너비(Horn만), 어휘 규모 |
| 깊이-대-언어적복잡성 격자 (ALCQ 계열) [2] | 깊이와 언어적 복잡성을 두 요인 격자로 | 홀드아웃 격자 수준 | 교란, 너비, 규모 |
| 허구 온톨로지 사슬 (PrOntoQA) [4] | 홉, 사실 순서, 교란 가지; 허구 어휘가 암기를 무력화함; 모든 단계가 점검 가능 | 홉 개수와 교차된 온톨로지 체제 | 너비, 데이터 규모 |
| 추상 도시 시뮬레이션 (LogiCity) [5] | 규칙 집합의 추상화 복잡성, 지평(horizon), 조합적 분할 | 보지 못한 규칙-에이전트 조합 | 건전성 귀속, 어휘 |
| 친족 합성 사슬 (CLUTRR) [6] | 일반화 축으로서의 사슬 길이, 등급화된 세 가지 잡음-사실 체제, 크라우드소싱된 바꿔쓰기(어휘) | 짧은 사슬로 훈련, 엄격히 더 긴 사슬로 시험 | 부정, 너비 |
일곱 중 두 열은 전체 행 집합에 걸쳐 연구가 부족하며, 이를 분명히 말해 둘 가치가 있습니다. 표 안의 어떤 생성기도 증명-너비 손잡이를 돌리지 않습니다: 모든 규칙 은행은 Horn 모양이거나 정책 모양이므로, 포화와 탐색을 가르는 축인 경우-나누기 비용은 이 분야의 통제된 증거에서 그냥 빠져 있습니다. 그리고 등급화된 암기-부담 손잡이로서의 어휘 크기는 허구화 트릭에 의해서만 통제되는데, 이는 그것을 훑는 것이 아니라 0으로 설정해 버리는 것입니다 [4]; 공개된 어떤 격자도 시스템이 서로 구별해 유지해야 하는 서로 다른 술어와 개체의 개수의 함수로 정확도를 측정하지 않습니다. 두 손잡이 모두 ruletaker_lite 종류의 생성기에 추가하기가 저렴하며, 이것이 이 권이 그런 생성기 하나를 담아 내보내는 이유의 일부입니다.
아직 풀리지 않은 부분
이 장의 규율과 추론 난이도에 대한 정착된 과학 사이에는 세 가지 간극이 있습니다. 첫째, 소프트 지식을 위한 축입니다. 위의 모든 장치는 명확한 세계에 살고 있습니다: 전제는 참이거나 부재하고, 난이도는 구조적입니다. 이 시리즈가 가중치와 확률을 붙여 둔 곳이라면 어디서나 그렇듯, 전제가 불확실성을 지닐 때, 난이도는 어떤 표준 축도 측정하지 못하는 요소를 얻게 됩니다: 보정 부담(calibration pressure), 즉 어떤 사례가 시스템의 답의 정체성이 아니라 그 신뢰도의 모양에 대해 시스템을 벌하는 정도입니다. 옳은 출력이 확률인 은행에는 합의된 층화 방식이 없으며, "깊어서 어려운 것"과 "사후확률이 정말로 0.6이라서 어려운 것"을 섞으면 정확히 깊이와 교란이 그랬던 것과 같은 방식으로 교란(confound)됩니다.
둘째, 생성적 증명을 위한 난이도입니다. 필요한 출력이 비트가 아니라 유도 과정일 때, 단계 수는 모두가 보고하는 축이지만 난이도에 대한 약한 대리 지표입니다: 길이가 동일한 두 증명이 사다리 장치의 만큼 너비가 다른 탐색 트리 위에 놓일 수 있으며, 보조정리(lemma)를 재사용하는 증명은 찾기는 더 쉽지만 쓰기는 더 짧지 않습니다. 증명 생성을 위한 난이도 모델은 그 산출물이 아니라 탐색 지형을 채점해야 할 것입니다.
셋째, 그리고 가장 중대한 것으로, 전이(transfer) 문제입니다. 이 구성 전체는 인공 생성기 위에서 측정된 축별 저하 프로파일이, 축이 통제되지 않고 상관된 채로 변하는 자연 말뭉치 위의 행동을 예측한다고 가정합니다. 이는 검증 가능한 주장입니다: 자연스러운 벤치마크의 난이도 혼합을 추정하고, 이 장의 첫 절에 나온 혼합 항등식을 통해 그 측정된 프로파일로부터 각 시스템의 집계를 예측한 다음, 그 예측을 확인해 보는 것입니다. 우리가 아는 한 그런 회귀를 대규모로 돌린 발표된 연구는 없습니다. 누군가 그렇게 하기 전까지, 이 축들은 계측기 자신의 영역 위에서만 검증된 도구입니다.
왜 중요한가
이 장은 VI부의 방법론적 경첩입니다. 이 권은 열네 개 장에 걸쳐 신뢰 기구(정당화, 보정, 기권)와 규모 기구(구체화, 배치화된 고정점, 깊이 예산)를 지어 왔습니다; "그것이 작동했는가?"라는 질문은 이제 벤치마크에 떨어지는데, 벤치마크는 그 저자가 인정하든 안 하든 실험입니다. 난이도 축은 벤치마크에 대해 실험에서의 통제 변수와 같은 관계에 있습니다: 그것 없이 점수는 관측이고, 그것과 함께라면 측정입니다. 독자 자신의 연구를 위한 수출품은 구체적입니다. 집계가 아니라 축별 표를 보고하십시오; 모든 커밋된 장치가 완전성을 고정했던 방식대로, 여러분이 연구하지 않는 축을 고정하십시오; 여러분의 생성기가 돌릴 수 없는 손잡이가 무엇인지 밝히십시오. 그리고 리더보드를 읽을 때, 이 장이 정밀하게 다듬어 놓은 그 하나의 질문을 던지십시오: 만약 이 시스템의 점수가 떨어졌다면, 누구든 어느 축이 그것을 끌어내렸는지 말할 수 있는가? 답할 수 없는 리더보드도 무언가는 측정하고 있습니다. 다만 그것은 추론이 아닙니다.
핵심 용어
- 완전성 축(completeness axis): 벤치마크가 보통 채점하는 난이도 차원으로, 단조로운 유도 과정을 따라가는 함의된 답의 재현율을 깊이별로 층화한 것입니다.
- 난이도 축(difficulty axis): 추론을 어렵게 만드는 인스턴스의 독립적인 기계적 속성입니다; 이 장이 다루는 완전성 너머의 일곱 축은 건전성, 종료성, 증명 너비, 질의 조인, 의미론 변화, 접지 신뢰, 규모입니다.
- 혼합 교란(mixture confound): 항등식 입니다: 집계 점수는 시스템의 층위별 정확도 를 은행의 구성 와 뒤엉키게 만들어, 혼합비가 바뀌면 순위도 뒤집힐 수 있습니다.
- 한 번에 한 요인씩 바꾸는 설계(one-factor-at-a-time design): 모든 난이도 요인을 기준선에 고정하고, 손잡이 하나를 돌리고, 그 하락을 귀속시킵니다; 저렴하지만(개의 셀) 상호작용에 대해서는 눈이 멉니다.
- 레이블 균형(label balance): 모든 난이도 층위를 참/거짓 50/50으로 강제하여 클래스 사전확률이 점수에 새어 들어가지 않게 하는 생성기의 규율입니다.
- 고정(pinning): 연구 대상이 아닌 축을 그 이상적인 값(재현율 정확히 1, 고정점 도달, 깊이 상수)에 붙들어 두도록 장치를 실행하여, 측정된 실패를 귀속 가능하게 만드는 것입니다.
- 증명 너비(proof width): 경우-나누기 증명이 필요로 하는 가지의 개수입니다; 선언적 사다리 위에서는 로 자라나는 반면 가지당 깊이는 로 유지됩니다.
- 결합 복잡도(combined complexity): 데이터가 고정된 상태에서 질의의 구조에 따라 자라는 비용으로, 순환-질의 장치의 탐침이 하나의 6개 간선 그래프 위에서 로 늘어나는 것으로 실증됩니다.
- 반단조성(antimonotonicity): 의미론-변화 실패입니다: 사실을 추가하면 결론이 철회되어, "입력이 늘면 출력은 결코 줄지 않는다"는 완전성 이야기의 전제를 깨뜨립니다.
- 저하 프로파일(degradation profile): 기준선으로부터의 축별 델타로 이루어진 시스템의 벡터입니다; 커밋된 표들이 보여주듯, 집계가 같은 두 시스템도 정반대의 프로파일을 가질 수 있습니다.
다음으로 이어지는 곳
이 장은 잣대들을 지었습니다; 다음 장은 그것들을 계기판 하나로 조립합니다. NeSy 벤치마크 스위트와 시뮬레이터는 이 권이 커밋한 다섯 계측기, 즉 깊이별 은행, 탐침, 보정 및 일관성 측정기를 가져다가, 그 커밋된 수치가 이 권의 회귀 시험을 겸하는 스위트 하니스로 용접하고, 그런 다음 같은 렌즈로 이 분야의 벤치마크 스위트(rsbench, KANDY, LTLZinc, NeSy4VRD와 그 동류)를 읽어 냅니다: 각 스위트가 어느 축을 고정하는지, 그래서 그 헤드라인 수치가 무엇을 귀속시킬 수 있는지를 말입니다.
Companion 코드: examples/frontier/difficulty_axes.py는 일곱 개의 고정된 장치를 구현하고, 여기서 인용된 모든 주장을 단언(assert)으로 지키며, 인용된 모든 숫자를 결정론적으로 재현합니다; examples/integration/ruletaker_lite.py와 examples/integration/translate_prove.py는 이 장이 다시 읽는 커밋된 표를 지닌 두 계측기입니다. 이 장의 모든 수치를 바이트 단위로 재현하려면 각각을 python3 <module>.py로 실행하십시오; 이 권의 인수 하니스(acceptance harness) examples/frontier/validate.py는 자신의 19개 검사짜리 원장(ledger)의 일부로서 이들을 다시 실행합니다.