자연어 추론 벤치마크: FOLIO, LogicBench, PrOntoQA
📍 현재 위치: 6부 · 자연어 추론 — 21장. 번역 후 증명은 모든 답변에 증명이 첨부되어 나오는 파이프라인을 구축했습니다; 이 장은 그러한 증명을 운 좋은 레이블과 구별할 수 있는 측정 도구를 구축하고, 6부의 두 시스템 모두를 그 도구에 통과시킵니다.
지난 두 장은 영어로 제기된 논리적 질문에 답하는 두 시스템을 만들었습니다: 항상 답하고 때로는 추측하는 소프트 추론기, 그리고 추측하기보다 기권하는 번역-후-증명 파이프라인입니다. 둘 중 하나를 고르려면 측정이 필요하며, 측정은 도구로 이루어집니다. 이 장은 추론 벤치마크를 정확히 그렇게, 즉 설계와 분해능과 특징적인 실패 양식을 가진 도구로 다룹니다. 발표된 세 가지 프로토콜은 각각 "참/거짓 질문에 대한 정확도"라는 소박한 도구의 한 가지 맹점을 고쳤으며, 동반 모듈 bench_lite.py는 그중 둘을 데스크 규모로 재구성하고 세 번째의 규율을 옮겨 심습니다. 그래서 이 장이 이름 붙이는 모든 함정은 일화가 아니라 확정된 숫자입니다.
최종 답만 확인해서 수학 시험을 채점한다고 상상해 보십시오. 모든 객관식 문제에 "(다)"라고 답하는 학생은 문제 하나 읽지 않고도 25퍼센트를 받으며, 정답지에서 "(다)"가 과대표되어 있다면 그보다 더 받습니다. 두 실수가 서로 상쇄되는 학생은 깔끔하게 계산한 학생과 같은 점수를 받습니다. 공정한 채점에는 세 가지 수리가 필요합니다: 추측이 알려진 낮은 보상만 얻는 정답지, 각 문제가 어떤 능력을 시험하는지에 따라 정렬된 문제(그래서 보고서가 학생이 어떤 능력을 갖췄는지 말할 수 있도록), 그리고 풀이 과정을 한 줄 한 줄 읽으며 각 줄이 이전 줄로부터 따라 나오는지, 또 그 줄들이 실제로 답에 도달하는지 확인하는 채점자입니다. 이 장의 세 벤치마크는 추론한다고 주장하는 기계를 위해 만들어진 바로 그 세 가지 수리입니다.
이 장에서 다루는 내용
- 도구로서의 관점: 벤치마크가 측정한다고 주장하는 것과 그 프로토콜이 실제로 구별할 수 있는 것의 차이; 소박한 프로토콜이 허용하는 세 가지 착시(동전 던지기 부풀림, 집계 흐림, 레이블 한정 관대함).
- 열린 세계에서의 삼항 함의: 이중 증명기 질의로 실행되는 FOLIO의 참/거짓/불확실 의미론과, 세 레이블이 깔끔하게 분할된다는 증명.
- 다수 클래스 함정, 측정됨: 최선의 추측 전략을 유도하고, 상수 추측기가 0.333의 무작위 하한에 맞서 0.500을 기록하는 확정된 표.
- 규칙별 분리: LogicBench의 항목당 하나의 추론 규칙 설계와, 패턴 매칭에 맞서는 짝지어진 변형 기법.
- PrOntoQA의 두 가지 설계 선택: 사전학습 지식이 답할 수 없는 가상 술어, 그리고 증명 단계와 일대일로 대응하는 정답 사고 사슬.
- 단계 검사기: 네 개의 플래그(parsed, valid, linear, connects)로 이루어진 검증기, 그리고 번역-후-증명 파이프라인이 단언된 100퍼센트로 그것을 통과하는 이유.
- 탐욕적 전시물: 모든 단계가 건전한 전건 긍정(modus ponens)이고 레이블 정확도는 파이프라인을 능가하지만 증명 정확도는 0.167로 붕괴하는 기준선, 그리고 유도되고 측정된 0.650의 그릇된-이유로-정답 비율.
- 지표 함정 표: 레이블 정확도, 증명 정확도, 기권을 나란히 놓고, 5권이 추론 지름길이라 이름 붙일 발산 열을 보여준다.
벤치마크가 볼 수 있는 것과 볼 수 없는 것
벤치마크는 프로토콜을 감싼 하나의 주장입니다. 그 주장은 대략 "이 데이터셋은 논리적 추론을 측정한다"는 식으로 말하며, 프로토콜은 예시 생성, 정답 레이블링, 채점의 기계 장치입니다. 그 주장은 프로토콜이 실제로 구별할 수 있는 것만큼만 훌륭하며, 소박한 프로토콜, 즉 레이블 정확도로 채점되는 이항 질문은 세 가지 뚜렷한 착시를 허용합니다. 동전 던지기 부풀림(coin-flip inflation): 레이블이 둘이면 동전은 0.5를 기록하며, 레이블 비율이 조금이라도 불균형하다면 가장 흔한 레이블을 항상 내뱉는 쪽이 그보다 더 높은 점수를 받는데, 둘 다 추론을 단 한 단계도 수행하지 않습니다. 집계 흐림(aggregate blur): 단 하나의 헤드라인 정확도는 데이터셋이 담은 모든 종류의 추론에 걸쳐 평균을 내므로, 하나의 추론 규칙은 통달했지만 다른 규칙에는 속수무책인 시스템도 정반대의 성향을 지닌 시스템과 똑같이 0.75를 기록합니다. 레이블 한정 관대함(label-only kindness): 레이블은 옳을 수 있지만 그것을 낳은 추론은 틀릴 수 있는데, 답 공간이 작으면 끊어진 단계들의 사슬도 정답에 도달할 수 있기 때문입니다; 레이블만 채점하는 것은 바로 이런 지름길 취하기를 용서하고, 그럼으로써 그것을 보상합니다.
이 장이 재구성하는 각 프로토콜은 그중 한 구멍을 막으며, 아래 표가 이 장의 지도입니다. FOLIO(자신이 담고 있는 일차 논리(First-Order Logic) 주석에서 이름을 딴 것)는 세 번째 레이블인 불확실을 더하는데, 그 의미론은 진정한 함의 검사를 강제하며, 정답 레이블은 증명기에 의해 감사됩니다 [1]. LogicBench는 항목마다 하나의 추론 규칙을 분리해 내므로, 역량은 뭉뚱그려서가 아니라 규칙별로 보고됩니다 [2]. PrOntoQA(증명과 온톨로지로 생성된 질의응답, Proof and Ontology-generated Question-Answering)는 추론 그 자체를 데이터의 일부로 만듭니다: 가상의 온톨로지는 사전학습된 지식이 발붙일 곳을 없애고, 정답 사고 사슬은 증명 단계와 일대일로 대응하며, 검사기가 생성된 각 단계를 검증하여 레이블 정확도와 증명 정확도를 갈라냅니다 [3].
| 착시 | 무엇이 빠져나가는가 | 그것을 막는 프로토콜 | 메커니즘 |
|---|---|---|---|
| 동전 던지기 부풀림 | 추측기와 사전 분포가 좋은 점수를 받는다 | FOLIO 방식의 삼항 레이블 | 불확실이 인식론적 무게를 지니며, 레이블별 분할과 기준선이 함께 보고된다 |
| 집계 흐림 | 숫자 하나가 고르지 못한 역량을 숨긴다 | LogicBench 방식의 규칙 분리 | 항목마다 추론 규칙 하나; 정확도가 규칙별로 보고된다 |
| 레이블 한정 관대함 | 끊어진 추론에서 나온 정답 | PrOntoQA 방식의 검사 가능한 사슬 | 정답 사고 사슬이 곧 증명이며, 단계 검사기가 레이블뿐 아니라 사슬을 채점한다 |
세 가지 착시, 세 가지 프로토콜 수리, 그리고 그것들이 마침내 이르는 도구: 레이블 정확도를 증명 정확도로부터 갈라내어 탐욕적 기준선의 0.650 그릇된-이유로-정답 비율을 드러내는 단계 검사기.
저자가 AI의 도움을 받아 직접 제작한 원본 도해.
아래의 모든 것은 실행 가능합니다. 모듈 bench_lite.py는 하나의 시드된 무작위 스트림으로부터 PrOntoQA 방식 코퍼스와 FOLIO 방식 코퍼스를 생성하고, 이전 장의 번역-후-증명 파이프라인과 의도적으로 탐욕적인 기준선을 PrOntoQA 방식 코퍼스에 대해 실행하고, 이중-질의 레이블 부여기와 닫힌-세계 전방 연쇄기와 다수 클래스 기준선을 FOLIO 방식 코퍼스에 대해 실행하며, 모든 주장을 assert로 지킵니다(bench_lite.py 586–616행). 두 번의 실행은 바이트 단위로 동일한 출력을 인쇄하므로, 이 장의 모든 숫자는 표집된 모델의 속성이 아니라 확정된 프로토콜의 속성입니다.
열린 세계에서의 삼항 함의
레이블 의미론에서 시작합시다. FOLIO의 전체 설계가 거기서 따라 나오기 때문입니다. (대문자 감마)는 전제 집합(premise set), 즉 하나의 예시가 단언하는 문장들을 가리키는 데 쓰고, 는 결론(conclusion), 즉 판정되어야 할 문장을 가리키는 데 씁니다. 기호 는 "함의한다"라고 읽습니다: 는 전체를 참으로 만드는 모든 상황이 도 참으로 만든다는 뜻입니다. 기호 은 "아니다"라고 읽으므로, 는 결론의 부정입니다. 세 레이블은 하나가 아니라 두 개의 함의 물음으로 정의됩니다 [1]:
이것은 2권에서 나온 열린 세계 가정(open-world assumption)이 이제 벤치마크의 임무를 수행하는 것입니다: 를 증명하는 데 실패했다고 해서 가 거짓이라는 증거는 아니며, 그것은 그저 증거의 부재일 뿐이고, 레이블 집합은 정확히 그 상태를 위한 부류 하나를 담고 있습니다. 불확실 부류는 설계의 인식론적 무게를 짊어집니다: 시스템은 오직 둘 중 어느 함의도 성립하지 않음을 알아차림으로써만 불확실 예시에서 점수를 얻는데, 이는 전제에 대고 결론을 패턴 매칭하는 것보다 엄연히 더 어려운 행위입니다.
세 경우는 가 일관될 경우 진정으로 분할을 이룹니다. 와 가 둘 다 성립한다고 가정해 봅시다. 의 모든 모델(모든 전제를 참으로 만드는 모든 상황)은 첫 번째 함의에 의해 를 참으로 만들어야 하고, 두 번째 함의에 의해 도 참으로 만들어야 할 것입니다; 어떤 상황도 둘 다를 만족할 수 없으므로, 는 모델을 하나도 갖지 못할 것이고, 이는 일관성과 모순됩니다. 코퍼스 생성기는 각 이론을 진술된 사례를 가진 충족 가능한 사슬을 중심으로 짓기 때문에, 구성상 그 이론들은 모델을 갖습니다(bench_lite.py 417–464행): 세 레이블은 서로 배타적이며 남김없이 모두를 포괄합니다.
의미론을 학계 세계의 삼중항 하나로 해독해 봅시다. 전제: 모든 교수는 연구자이다; 모든 교수는 학생이 아니다; Alice는 교수이다. 질의 "Alice는 연구자이다": 를 증명하는 것은 전건 긍정(modus ponens) 한 단계로 성공하며, 레이블은 참입니다. 질의 "Alice는 학생이다": 를 증명하는 것은 실패하지만, 를 증명하는 것은 부정 규칙을 통해 성공하며, 레이블은 거짓입니다. 질의 "Alice는 지원을 받는다": 전제는 지원을 전혀 건드리지 않으므로, 두 증명 모두 실패하며, 레이블은 불확실입니다. 예시마다 증명기를 두 번 호출하고, 레이블은 그 한 쌍이 도달하는 결과가 무엇이든 그것이 됩니다. 그것이 바로 확정된 레이블 부여기, folio_dual_query의 본체입니다(bench_lite.py 473–480행):
prog = _compile(ex["context"])
facts, rules = prog # FOLIO-lite text is never corrupted
a = ex["name"].lower()
if sld.prove((ex["query_concept"], a), facts, rules) is not None:
return "True"
if sld.prove(("not_" + ex["query_concept"], a), facts, rules) is not None:
return "False"
return "Unknown"
부정은 구체화(reification)로 처리됩니다: 규칙 "모든 는 가 아니다"(는 규칙의 몸체 개념, 즉 일반화되는 대상의 이름이고, 는 그 머리 개념, 즉 부정되는 대상의 이름입니다)는 머리가 새로운 술어 not_h인 규칙으로 컴파일되므로, not_h(alice)를 증명하는 것이 곧 그 부정을 증명하는 것입니다(bench_lite.py 349–372행). 이 생성기가 내놓는 이론들 위에서, SLD(선택적 선형 정형절, Selective Linear Definite-clause) 분해 위에 지어진 1권의 증명기는 건전하고 완전하므로, 이중 질의는 레이블 의미론의 근사가 아니라 그 자체로 실행된 레이블 의미론입니다. 정직하게 밝혀 둘 단서 하나: 이 구체화는 대우 추론(contrapositive reasoning)을 의도적으로 포기합니다. 고전 논리에서는 "모든 는 가 아니다"와 사실 "Alice는 이다"를 함께 놓으면 Alice가 가 아니라는 것이 함의되지만, not_b(alice)는 이 인코딩 아래에서 어떤 SLD 유도도 갖지 않습니다. 이 정확성은 부호 있는 단편 전체의 속성이 아니라 생성된 코퍼스의 속성입니다: 생성기는 부정 규칙의 머리를 결코 사실로 진술하지 않으며 규칙의 몸체 안에도 결코 두지 않으므로(bench_lite.py 417–464행), 생성기가 제기하는 어떤 질의도 대우를 필요로 하지 않으며, 확정된 assert는 바로 그 코퍼스 수준에서의 정확성을 인증합니다: dual_acc == 1.0이 정확히 성립합니다(bench_lite.py 612행).
이 구성은 원조 프로토콜에서 이름 붙일 가치가 있는 하나의 규율을 그대로 비춥니다. FOLIO는 전문가가 작성한 자연어와 손으로 작성된 일차 논리 주석을 짝지었는데, 그 프로토콜은 그 손을 신뢰하지 않았습니다: 일차 논리 주석은 추론 엔진을 통과했고, 그 판정이 정답을 감사했으며, 주석된 레이블이 기계 검사에 실패한 예시는 수리되었습니다 [1]. 증명기로 검증된 정답은 함의를 측정하는 것과 주석자와의 일치를 측정하는 것 사이의 차이입니다. 우리의 축소판은 애초에 구성상 그 속성을 물려받습니다: 레이블은 애초부터 증명기의 출력입니다.
다수 클래스 함정, 측정됨
삼항 레이블은 레이블 분포가 감시될 때만 동전 던지기라는 구멍을 막으며, FOLIO 자체의 구성비가 그 이유를 보여줍니다: 논문은 테스트 분할에 참 87개, 거짓 78개, 불확실 61개의 예시가 있어 다수 클래스 기준선이 38.5퍼센트라고 보고합니다 [1]; 공개된 훈련 분할에서 집계하면 그 개수는 388, 286, 330입니다. 축소판은 함정을 놓칠 수 없도록 불균형을 조금 더 밀어붙여, 45/22/33 구성비를 목표로 삼습니다(bench_lite.py 107행).
인용하기에 앞서 추측기의 보상을 유도해 봅시다. 은 레이블 을 갖는 예시의 비율을 가리키는 데 쓰고, 입력을 무시한 채 레이블 을 확률 로 내뱉는 시스템(고정된 어떤 추측 전략이든, 들의 합은 1입니다)을 생각해 봅시다. 는 기댓값, 즉 확률로 가중된 평균을 가리키는 데 쓰고, 기호 는 "세 레이블에 걸친 합"이라고 읽습니다. 추측기의 기대 정확도는 그 추측이 정답 레이블과 일치할 확률로, 모든 레이블 에 걸쳐 정답 레이블이 일 확률 과 추측이 일 확률 의 곱을 더한 것입니다:
여기서 그 부등식은 각 을 그중 가장 큰 것으로 대체한 것이며, 그 상계는 모든 추측 질량을 가장 흔한 레이블에 몰아줌으로써 달성됩니다(가 다수 클래스일 때 ). 따라서 최선의 입력 무관 전략은 다수 클래스 기준선(majority baseline)이며, 그 정확도는 다수 클래스 빈도 이고, 균등한 동전의 은 그저 이 추측 계열 위의 한 점, 즉 구성비에 무관한 유일한 점일 뿐입니다: 이 계열의 전체 범위는 (가장 드문 레이블에 모든 추측 질량을 몰아준 경우)부터 까지(아래에 진술되는 확정된 구성비에서는 부터 까지) 뻗어 있으므로, 도 다른 어떤 단일 숫자도 추측의 천장이 아닙니다. 헤드라인 숫자는 이 아니라 에 견주어 읽어야 합니다.
확정된 실행은 60개 중 참 30개, 거짓 11개, 불확실 19개로 목표 구성비를 실현하므로 이며, 레이블별 표는 세 시스템의 프로필을 한꺼번에 보여 줍니다:
[4] FOLIO-lite (3-way open-world, dual query), n=60, mix True/False/Unknown = 30/11/19
system True False Unknown overall
dual-query prover 1.00 1.00 1.00 1.000
greedy CWA 1.00 1.00 0.00 0.683
majority (True) 1.00 0.00 0.00 0.500
majority beats the 33.3% random floor at 50.0% (the imbalance trap);
never saying Unknown caps a system at 68.3% — greedy CWA sits exactly there.
이 표에는 두 가지 교훈이 담겨 있습니다. 첫째는 함정 그 자체입니다: 다수 클래스 행은 추론을 전혀 수행하지 않고도 0.500을 기록하는데, 이는 무작위 하한보다 16.7포인트나 높은 값입니다; "우리 시스템은 삼항 함의에서 55퍼센트에 도달한다"는 다수 클래스 기준선이 그 옆에 나란히 인쇄되기 전까지는 거의 아무것도 보고하지 않는 것입니다. 둘째는 불확실 열에 속합니다. 닫힌 세계 가정(closed-world assumption)을 줄인 greedy CWA 행은 질의 원자가 유도 가능하면 참으로, 그렇지 않으면 거짓으로 답하는 전방 연쇄기입니다(bench_lite.py 483–499행). 그것은 결코 불확실을 말할 수 없으므로 모든 불확실 예시에서 틀리며, 그 정확도는 으로 상한이 매겨집니다; 확정된 실행은 정확히 그 천장 위에 앉아 있는데, 그것이 말할 수 있는 두 레이블에서는 완벽하기 때문입니다. 시스템의 레이블 어휘는 추론에 관한 어떤 물음이 제기되기도 전에 이미 그 정확도의 상한을 정하며, 레이블별 분할이 그 상한을 드러냅니다. 이것은 3권의 순위 매김-프로토콜 규율이 자연어로 옮겨 심긴 것입니다: 그것이 어디서 나왔는지를 보여 주는 기준선과 분할 없이는 결코 헤드라인 숫자를 발표하지 마십시오.
항목당 규칙 하나: LogicBench의 규율
두 번째 착시인 집계 흐림은 균형 잡힌 레이블 아래에서도 살아남습니다. 두 시스템은 서로 겹치지 않는 추론 규칙 집합을 다루면서도 같은 집계 정확도를 공유할 수 있으며, 혼합된 데이터셋을 아무리 재가중해도 그 둘을 갈라놓지 못합니다. 그 수리는 구조적입니다: 각 항목이 정확히 하나의 추론 규칙 패턴(inference-rule pattern)을 다루도록 데이터셋을 짓고, 그다음 정확도를 규칙별로 보고하는 것입니다. 그것이 LogicBench의 설계입니다: 명제 논리, 일차 논리, 비단조 논리에 걸친 25개의 추론 패턴이 있으며, 각 항목은 전건 긍정, 후건 부정, 선언적 삼단논법 같은 이름 붙은 규칙 하나를 예화하므로, 평가는 스칼라 하나가 아니라 역량 프로필을 읽어 냅니다 [2]. 지름길 방지 장치가 하나 더 딸려 옵니다: 각 맥락은 여러 개의 예/아니오 질문 변형과 짝지어지는데, 결론을 체계적으로 부정하고 뒤바꿈으로써, 규칙이 아니라 표면적 겹침에 의존하는 시스템은 단일 맥락의 변형들에 걸쳐 스스로 모순되는 모습으로 포착됩니다 [2].
발표된 결과는 집계 흐림이라는 착시에 비추어 불편하게 읽힙니다: 규칙별로 평가하면, 프론티어 언어 모델들은 인간 기준선에 못 미쳤으며, 그 프로필은 일관된 방향으로 고르지 못했고, 부정을 포함하는 규칙이 가장 어려운 축에 들었으며, 모델은 추론에 필요한 맥락 정보를 때때로 간과했습니다 [2]. 집계 하나였다면 그 약한 규칙들을 그럴듯해 보이는 평균 속에 섞어 버렸을 것입니다; 규칙별 표는 그 실패를 국소화합니다.
우리의 축소판은 데스크 규모의 코퍼스가 허락하는 형태로 그 규율을 적용합니다. PrOntoQA-lite 생성기는 의도적으로 하나의 규칙 계열, 즉 양의 단항 규칙에 대한 전건 긍정만을 사용하므로(공유된 문법은 부호 있는 형태도 지원하지만, 이는 FOLIO-lite 생성기만 사용합니다), "규칙별"은 무너집니다; 대신 나누어 볼 수 있는 것은 깊이(depth, 정답 증명이 필요로 하는 규칙 적용 횟수)와 레이블이며, 확정된 출력은 둘 다 보고합니다: 아래의 깊이별 표, 위의 레이블별 FOLIO 표입니다. 축이 다를 뿐 규율은 동일합니다: 결코 뭉뚱그려서만이 아니라 고립된 능력마다 역량을 보고하십시오. 이 모듈은 또한 자연어는 변하지만 엄격한 패턴은 변하지 않는다는 LogicBench의 또 다른 교훈을, 예시당 확률 0.25(CORRUPT_FRAC, bench_lite.py 102행; 예시당 동전 던지기, 235–237행)로 적용되어 확정된 60개 예시 중 20개에서 실현되는 오염 연산자로 인코딩합니다(bench_lite.py 189–195행):
def corrupt_sentence(sign: int, body: str, head: str) -> str:
"""The out-of-grammar paraphrase (the LogicBench lesson: natural language
varies; a strict grammar does not). Pluralizing "Every b is a h." into
"All bs are hs." preserves the meaning exactly — a human or an LLM reads
straight through it — but the strict parser returns None."""
neg = "" if sign > 0 else "not "
return f"All {body}es are {neg}{head}es."
엄격한 파서를 무력화하는, 의미를 보존하는 의역은 언어적 변이를 데스크 규모에서 대신하는 장치이며, 그것이 바로 최종 표의 기권 열을 만들어 내는 것입니다.
가상의 세계와 검사 가능한 사슬: PrOntoQA의 두 가지 설계 선택
세 번째 프로토콜은 이 장의 중심이며, 그 두 가지 설계 선택은 각각 측정 타당성에 대한 특정한 위협에 답합니다.
선택 하나: 가상의 술어. 웹으로 사전학습된 모델은 이미 고양이가 포유류라는 것을 알고 있으므로, 진술된 전제로부터 그것을 "연역"하라고 요청하면 측정은 혼동됩니다. 정답이 전제에서 왔는지 매개변수적 기억에서 왔는지 알 수 없기 때문입니다. PrOntoQA는 wumpus, yumpus, zumpus 같은 지어낸 개념 명사에 대한 온톨로지를 생성하는데, 사전학습된 어떤 모델도 그것에 대해 아무것도 알 수 없으므로, 정답은 반드시 진술된 맥락을 거쳐 왔어야 합니다 [3]. 발표된 비교는 그 혼입이 실재함을 확인해 줍니다: 모델은 온톨로지가 상식 지식과 일치할 때 가장 좋은 점수를 받고, 가상의 온톨로지에서는 더 나쁘며, 온톨로지가 사전학습과 모순될 때는 조금 더 나쁩니다; 원 출처는 가상 설정과 모순 설정이 비슷하다는 것을 발견하며, 큰 간극은 일치하는 온톨로지와 그 둘 사이에 놓여 있는데, 그 간극이야말로 가상 어휘가 차단하는 바로 그 누출을 측정합니다 [3]. 축소판은 그 어휘를 통째로 채택하고(bench_lite.py 111–114행), 예시마다 개의 홉(hops, 규칙 적용)에 걸친 선형 하위류 사슬 를 생성하는데, 여기서 는 2권의 포섭 기호로 "~의 하위류이다"라고 읽습니다: 모든 는 이고, 모든 은 이며, 사슬을 따라 계속됩니다. 사슬과 나란히 홉마다 하나의 교란 규칙(distractor rule)이 놓이는데, 이는 각 홉 (부터 세는 홉 지표)에서 막다른 개념 로 갈라지는 갈래 이며, 아래에서 크게 중요해질 지름길 방지 장치입니다(bench_lite.py 200–255행).
선택 둘: 증명 단계와 일대일로 대응하는 정답 사고 사슬. 이것은 모델이 아니라 데이터에 대한 요구 사항입니다. 정답 설명이 자유로운 문단이라면, 어떤 기계적 방법도 시스템의 추론을 그것과 견줄 수 없습니다. PrOntoQA는 각 예시를 형식적 증명으로부터 생성하고, 전건 긍정 단계 하나당 문장 하나씩으로 언어화하므로, 정답 사고 사슬은 곧 증명이며, 뒤집을 수 있는 통제된 문법 안에 있습니다 [3]. 가역성(invertibility)이 그 하중을 떠받치는 속성입니다: 생성기와 검사기가 하나의 문법을 공유하므로, 생성된 모든 문장은 그것이 유래한 바로 그 원자나 규칙으로 다시 파싱되며, 같은 문법으로 된 예측된 사고 사슬도 의미론적으로 파싱되어 단계별로 검사될 수 있습니다. 검사 가능한 추론은 나중에 덧붙일 수 있는 것이 아닙니다; 그것은 생성기 안에 애초부터 설계되어 있어야 합니다. 축소판은 예시와 같은 호흡으로 정답 사슬을 짓는데, 사슬 개념마다 유도 순서대로 언어화된 사례 사실 하나씩입니다(bench_lite.py 253행). 그리고 시드된 동전이 사슬의 끝을 긍정으로("Sam은 jompus이다", 정답 참) 또는 부정으로("Sam은 jompus가 아니다", 정답 거짓) 묻는데, 두 극성 모두 같은 정답 증명을 공유하므로 극성 추측과 증명 산출은 서로 분리됩니다(bench_lite.py 233–251행).
단계 검사기: 이 장의 도구
이제 도구 그 자체를 봅시다. 예시 하나와 예측된 사고 사슬, 즉 생성된 문장들의 목록이 주어지면, 검사기 check_trace는 각 줄을 논리로 다시 파싱하여 네 가지 물음을 던지는데, 앞의 셋은 점점 더 강해지는 물음이고 넷째는 처음부터 끝까지 잇는 연결성 검사입니다(bench_lite.py 284–304행):
established = {ex["chain"][0]} # the instance axiom c_0(a)
prev = ex["chain"][0] # conclusion of the previous step
parsed = valid = linear = True
for line in cot:
p = parse_sentence(line)
if p is None or p[0] != "fact" or p[1] != entity:
parsed = valid = False
break
c = p[2]
# valid: ∃ rule (b → c) with b(a) established before this step.
if not any(b in established and h == c for b, h in pos_rules):
valid = False
# linear: the premise used must be the previous step's conclusion.
if not any(b == prev and h == c for b, h in pos_rules):
linear = False
established.add(c)
prev = c
connects = parsed and len(cot) > 0 and prev == ex["query_concept"]
return {"parsed": parsed, "valid": valid, "linear": linear,
"connects": connects,
"strict": parsed and valid and linear and connects}
네 개의 플래그를 해독해 봅시다. Parsed(파싱됨): 모든 줄이 공유된 문법을 통해 올바른 개체에 관한 원자로 뒤집히는지; 파싱할 수 없는 단계는 틀린 것으로 표시되며, 원 프로토콜도 그렇게 채점합니다 [3]. Valid(유효함): 각 단계가 올바른 규칙 예화(rule instantiation)인지, 즉 그 전제 가 사례 공리나 이전 단계에 의해 이미 확립되어 있는 어떤 맥락 규칙 (모든 개체 에 대해, 에서 가 성립하면 에서 도 성립한다는 뜻)가 있는지; 이것이 국소적 건전성입니다. Linear(선형임): 각 단계가 소비하는 전제는 반드시 바로 앞 단계의 결론이어야 합니다. 원 프로토콜은 정답 증명 자체의 연역 규칙(전건 긍정)으로 유도 가능한 엄격하게 유효한(strictly valid) 단계와, 규칙 두 개를 한 단계로 연쇄하는 것처럼 더 강한 증명 계산 아래에서만 유도 가능한 광의로 유효한 단계를 구별합니다 [3]; 연결 요구 사항은 분포 밖(out-of-distribution) 확장에서 온 한층 더 강화된 것으로, 증명 단계가 자신의 전제 중 하나를 곧바로 뒤따라야 함을 요구합니다 [4]. Connects(연결됨): 최종 결론이 질의된 원자여야 하므로, 받아들여진 단계들은 전제에서 목표까지 이어지는 경로를 이룹니다. 엄격 판정은 이 넷의 논리곱이며, 엄격한 단계 기준 아래에서 발표된 증명 정확도 지표의 축소판입니다 [4].
엄격/관대 구별은 현학적 트집이 아닙니다. 발표된 분석은 모델이 산출한 단계가 압도적으로 국소적으로 건전하다는 것을 발견했습니다: 5홉에서는 93.2퍼센트가 엄격하게 유효했습니다 [3]. 국소적 유효성이 기준이었다면 사고 사슬은 거의 해결된 것처럼 보였을 것입니다. 엄격한 기준이 존재하는 이유는 개별적으로 건전한 단계들의 더미가 증명은 아니기 때문입니다; 단계들은 연결되어야 하며, 연결성이야말로 시스템이 실패하는 지점입니다.
하나의 구조적 사실이 파이프라인과 이 검사기의 관계를 정확하게 만듭니다. 번역-후-증명 파이프라인은 질문과 맥락을 엄격하게 파싱하여 어떤 실패에서도 기권한 다음, 1권의 목표 지향적 SLD 증명기를 실행하는데(bench_lite.py 388–412행), 이는 이전 장 translate_prove.py의 아키텍처(translate_prove.py 211–228행)를 가상의 문법 위에 재구축한 것입니다. 후방 연쇄는 목표에서 시작해 전제를 향해 나아가므로, 그것이 내놓는 어떤 증명도 구성상 연결된 선형 사슬입니다; 문장으로 평탄화되면(bench_lite.py 375–385행), 그런 트레이스는 엄격한 검사기를 결코 통과하지 못하는 법이 없습니다. 확정된 assert는 이를 실행으로 검증된 정리로 진술합니다: 파이프라인이 내놓는 모든 트레이스는 통과하며, 트레이스 통과율은 정확히 1.0입니다(bench_lite.py 589행). 그 100퍼센트는 벤치마크 점수가 아니라, 모든 예시에서 검증된 목표 지향 증명 탐색의 구조적 속성입니다.
세 가지로 읽는 탐욕적 추론기
이 도구는 소박한 프로토콜을 속이도록 만들어진 시스템을 상대할 때 자신의 값어치를 증명합니다. 그것이 축소하는 발표된 결과는 이렇습니다: 사고 사슬을 위해 프롬프트된 언어 모델은 개별적으로 유효한 단계를 산출하지만 계획자로서는 실패하며, 여러 규칙이 적용될 수 있을 때 목표 경로 위에 있는 규칙이 아니라 눈에 띄는 아무 규칙이나 탐욕적으로 따라가므로, 특징적인 실패는 오도하는 단계이지 무효한 단계가 아닙니다 [3]. 이 모듈은 그 결과를 알고리즘으로 실행하는데, greedy_reason의 본체입니다(bench_lite.py 324–344행):
goal = ex["query_concept"]
established = {ex["chain"][0]}
lines: list[str] = []
for _ in range(cap):
fired = None
for s, b, h in ex["rules"]: # fixed listed order
if s > 0 and b in established and h not in established:
fired = (b, h)
break # FIRST applicable rule
if fired is None:
break
established.add(fired[1])
lines.append(verbalize_fact(ex["name"], fired[1]))
if fired[1] == goal:
break
reached = goal in established
if reached:
label = "True" if ex["polarity"] == 0 else "False"
else: # not derived within the cap
label = "False" if ex["polarity"] == 0 else "True"
return label, lines
사례 공리에서부터 전방 연쇄하며, 나열된 순서대로 첫 번째로 적용 가능한 규칙을 발화시키고, 목표에 도달하거나 9단계의 상한에 이르면 멈춥니다. 발화되는 모든 단계는 진정으로 유효한 전건 긍정이며, 어떤 단계도 결코 틀리지 않습니다. 이것은 또한 정답 기호 규칙을 직접 읽어 들이는데, 이는 어법이 결코 막히지 않는 모델을 대신하는 것이므로, 결코 기권하지 않습니다. 다음은 확정된 실습 예시로, 3홉 맥락이며, 두 시스템의 트레이스와 판정을 함께 보여 줍니다:
[1] worked example #20 (hops=3) — the greedy trap
Every wumpus is a rompus.
Every wumpus is a yumpus.
Every rompus is a brimpus.
Every rompus is a zumpus.
Every zumpus is a jompus.
Every zumpus is an impus.
Sam is a wumpus.
True or false: Sam is not a jompus. (gold label: False)
translate-then-prove answers False; its SLD proof chain:
rompus -> zumpus -> jompus
checker: parsed=yes valid=yes linear=yes connects=yes -> strict PASS
greedy reasoner answers False; its first-applicable trace:
rompus -> yumpus -> brimpus -> zumpus -> jompus
checker: parsed=yes valid=yes linear=NO connects=yes -> strict FAIL
두 시스템 모두 거짓으로 답하며, 거짓이 정답입니다. 파이프라인의 사슬은 세 단계짜리 증명입니다. 탐욕적 트레이스는 그 증명을 두 번의 교란 갈래 외출(yumpus, brimpus)과 뒤섞은 채 담고 있습니다: 다섯 단계 모두 파싱되고 맥락 규칙을 유효하게 예화하지만, 이미 두 번째 줄에서 발화된 규칙(모든 wumpus는 yumpus이다)이 이전 줄의 결론 rompus가 아니라 wumpus를 소비하며, 같은 이음매 실패가 세 번째와 네 번째 줄에서도 반복되므로(yumpus 다음의 brimpus, brimpus 다음의 zumpus), linear는 실패하고 그 트레이스는 증명이 아닙니다. 소박한 프로토콜은 여기서 이 두 시스템을 똑같이 채점합니다. 엄격한 검사기는 그렇지 않습니다.
이제 확정된 깊이별 표(홉 개수마다 스무 개 예시)를 세 가지로 읽어 봅시다:
[3] per-depth accuracy (label vs strict proof), 20 examples each
hops pipeline label/proof greedy label/proof
1 0.55 / 0.55 1.00 / 0.50
3 0.70 / 0.70 1.00 / 0.00
5 0.75 / 0.75 0.45 / 0.00
greedy right-for-wrong-reason rate: 0.65 (label correct, proof invalid or non-connecting)
깊이에 따라 정확도를 층화하는 것 자체가 물려받은 규율입니다: ProofWriter 배후의 연구 계열은 깊이별 평가와, 레이블뿐 아니라 생성된 증명의 채점을, 구성과 암기를 구별하는 방법으로 확립했습니다 [5]. 탐욕적 열을 메커니즘에 견주어 읽어 봅시다. 레이블 정확도는 아첨합니다. 1홉과 3홉에서는 완벽합니다: 목표 원자는 항상 유도 가능하고, 홉 맥락은 개의 규칙을 나열하며, 각 발화는 새 원자 하나를 더하므로, 최대 번의 발화면 맥락이 소진되는데, 이면 그것은 최대 6번의 발화로, 상한 9 안에 들어옵니다. 5홉에서는 산술이 뒤집힙니다. 첫-적용 스캔은 각 홉의 두 규칙을 그 홉이 동전으로 정한 순서대로 연이어 발화시키는데, 어떤 홉의 아직 발화되지 않은 규칙은 그보다 나중 홉의 어떤 규칙보다도 목록에서 앞자리에 있기 때문입니다; 그러므로 홉 의 쌍은 발화 번째와 번째를 차지하고(홉을 부터 셀 때), 목표 는 마지막 홉의 동전이 정답을 교란 규칙보다 앞에 나열했다면 발화 번째에, 그렇지 않다면 발화 번째에 도달합니다. 실행이 잘리는지 여부는 오직 마지막 홉의 순서 동전 하나로 결정됩니다: 정답이 먼저이면 목표는 발화 번째, 정확히 상한에 도달하고; 교란이 먼저이면 번째로 밀려나 상한을 하나 넘어섭니다(그 예산 산술은 bench_lite.py 96–101행에 그대로 적혀 있습니다). 이 예측은 성공 확률 2분의 1이며, 확정된 코퍼스는 20개 중 9개로 그것을 실현하는데, 이것이 위 깊이별 표의 0.45이고, 깊이-붕괴 assert가 정확히 그 하락을 지킵니다(bench_lite.py 606–608행): 얕은 깊이에서는 보이지 않다가 깊은 깊이에서는 파국적인, 계획 예산의 실패입니다. 단계 유효성은 구성상 높습니다: 발화되는 모든 단계는 건전하며, 이는 정확히 국소적으로 유효한 단계에 대해 발표된 프로필과 같습니다 [3]. 증명 정확도는 가혹합니다. 1홉에서는 시드된 동전이 정답 규칙을 교란 규칙보다 먼저 나열했을 때만 트레이스가 엄격한데, 확률 2분의 1이며 측정값은 0.50입니다. 3홉과 5홉에서는 정확히 0.00입니다: 모든 쌍이 정답을 먼저 나열하더라도, 첫-적용 스캔은 사슬을 진전시키기 전에 이전의 교란 규칙으로 되돌아가므로, 트레이스는 항상 뒤섞이고 linear는 항상 실패합니다.
첫 번째 읽기와 세 번째 읽기 사이의 간극에는 이름과 공식이 있습니다. 60개 예시에 걸쳐, 사건 (레이블이 옳음)과 (트레이스가 엄격한 검사기를 통과함), 그리고 그릇된-이유로-정답 비율(right-for-wrong-reason rate) (는 "그리고"라고 읽습니다)를 정의합니다: 이는 증명이 아닌 것이 실어 나른 정답 레이블의 확률입니다. 을 의 두 경우에 걸쳐 나누고, 아래의 겹화살표 를 "따라서"라고 읽으면:
탐욕적 추론기의 경우, 엄격한 통과는 정답 레이블을 함의합니다: 연결된 사슬은 질의된 원자에서 끝나므로, 목표가 도달되었고 극성 사상은 정답 레이블을 반환합니다. 따라서 이며(는 "~에 포함된다"라고 읽습니다), 엄격 통과 예시는 모두 정답 레이블 예시이기도 합니다. 그러므로 이고, 그 비율은 두 헤드라인 열의 차로 무너져 내립니다:
이는 정확히 확정된 rfwr=0.650입니다: 60개 중 39개 예시에서 탐욕적 추론기는 그릇된 이유로 옳으며, assert는 산문을 신뢰하는 대신 이 현상의 존재 자체를 지킵니다(bench_lite.py 597행). 레이블 정확도와 증명 정확도 사이의 발산은 두 지표 사이의 불일치가 아닙니다; 그것이 곧 값을 매기지 못한 정확함의 측정된 비율입니다.
지표 함정: 숫자 하나로는 부족하다
이 장의 유산이 되는 표는 세 측정치를 나란히 놓으며, 어느 시스템도 침묵 뒤에 숨을 수 없도록 기권을 오답으로 셉니다:
[5] metric-trap summary (PrOntoQA-lite, abstentions count wrong)
system label acc proof acc abstention
translate-then-prove 0.667 0.667 0.333
greedy heuristic 0.817 0.167 0.000
the trap: greedy WINS the label column (0.817 vs 0.667) while its proofs
collapse (0.167 vs 0.667); on answered examples the pipeline is at 100%/100%.
열 단위로 읽어 봅시다. 레이블 정확도만 놓고 보면 탐욕적 휴리스틱이 0.817 대 0.667로 이기며, assert는 그 순서를 의도적으로 고정합니다(bench_lite.py 600–601행): 이 함정은 가설이 아니라 확정된 것입니다. 파이프라인의 0.667은 순전히 커버리지 산술이며, 이전 장의 인수분해 이 다시 눈에 보이게 된 것입니다: 시드된 오염이 60개 예시 중 20개에서 문장 하나를 문법 밖으로 밀어냈고, 파이프라인은 정확히 그 20개에서 기권했으며(단언됨, bench_lite.py 593–595행), 답한 40개에서는 레이블 100퍼센트, 증명 100퍼센트입니다. 파이프라인의 깊이별 레이블 숫자와 증명 숫자가 같은 이유도 같습니다: 답한 모든 예시가 엄격한 증명을 지니므로, 두 열 모두 깊이별 커버리지, 즉 0.55, 0.70, 0.75로 환원됩니다. 증명 정확도 열 아래에서는 순서가 뒤집혀 0.667 대 0.167이 되는데, 그 격차는 assert가 최소 25포인트이기를 요구하는 격차입니다(bench_lite.py 602–603행).
이 표가 이 권의 측정 유산인 이유는 각 열이 서로 다른 물음에 답하기 때문입니다. 레이블 정확도: 출력이 얼마나 자주 옳은가. 증명 정확도: 그것이 얼마나 자주 진술된 이유 때문에 옳은가. 기권: 시스템이 답할 수 없음을 스스로 얼마나 자주 아는가. 어떤 열도 다른 열을 포섭하지 않으며, 첫 번째 열만 보고하는 평가는 체계적으로 건전하게 기권하는 시스템보다 자신만만하게 지름길을 취하는 시스템을 선호하게 됩니다. 발산 열, 즉 레이블 정확도에서 증명 정확도를 뺀 값은 5권이 추론 지름길(reasoning shortcut)이라는 이름으로 다룰 바로 그 양입니다: 승인된 함수를 계산하지 않고도 정답 출력에 도달하는 메커니즘으로, 훈련 분포 위에서는 무해하지만 그것을 벗어나면 실패할 준비가 되어 있으며, 탐욕적 추론기의 아첨하는 얕은-깊이 숫자가 그 5홉 붕괴를 감추었던 것과 정확히 같습니다.
"단계가 옳다면 추론도 옳다." 확정된 전시물은 지배적인 실패 양식이 그 반대임을 보여 줍니다: 탐욕적 추론기의 단계는 모두 개별적으로 옳지만, 그 사슬은 여전히 증명이 아닙니다. 단계 수준 타당성과 사슬 수준 타당성은 서로 다른 측정이며, 이 전시물이 축소하는 발표된 분석은 5홉에서 모델의 단계가 93.2퍼센트 엄격하게 유효했음에도 그 사슬이 계획으로서는 실패했음을 발견했습니다 [3]. 단계가 아니라 사슬을 채점하십시오.
미해결 부분
단계 검사기는 이 장에서 가장 강력한 도구이며, 그것의 도달 범위는 완화할 수 없는 하나의 요구 사항, 즉 단계가 파싱 가능해야 한다는 것에 의해 제한됩니다. 축소판의 검사기는 생성기 자신이 작성한 문법을 뒤집으므로 파싱은 구성상 정확합니다; 원 발표된 프로토콜도 마찬가지로 자신이 의미론적으로 파싱할 수 있는 통제된 문법에 기댑니다 [3]. 자유 형식의 사고 사슬은 이를 무력화합니다. 어떤 시스템이 한 단계를 "그러니까 Sam은 저 jompus 비슷한 것들 중 하나일 것이다"라고 표현하는 순간, 어떤 문법 역전도 원자를 복원하지 못하며, 검사기의 유일하게 정직한 판정은 "파싱 불가"(추론이 아니라 표현을 벌하는 것)이거나, 혹은 도구가 없애려던 바로 그 자리에 판단을 다시 들여오는 관대한 의미론적 매칭뿐입니다. 자연스러움과 검사 가능성 사이의 긴장은 실재합니다: 벤치마크가 받아들이는 언어가 자연스러울수록 그 검증은 덜 기계적일 수밖에 없으며, 현재 어떤 프로토콜도 그 밧줄의 양 끝을 동시에 붙들고 있지 못합니다.
이 장을 정직하게 지켜 주는 두 가지 단서가 더 있습니다. 가상의 세계는 연역을 고립시켜 시험하는데, 그것이 그 목적이지만, 실제 추론은 연역을 전제가 결코 진술하지 않는 지식과 뒤섞으며, 이 프로토콜의 어떤 것도 그 통합을 측정하지 않습니다. 그리고 모든 합성 생성기는 자신이 측정하는 것 속으로 자신의 문법을 누출시킵니다: 우리의 코퍼스는 공리 형태당 문장 템플릿 하나, 홉당 교란 규칙 하나, 오직 전건 긍정만을 가지므로, 시스템은 원칙적으로 논리가 아니라 생성기를 통달할 수도 있습니다. 프로토콜의 분포 밖 확장은 정확히 이 우려 때문에 존재하며, 시연보다 더 깊고, 더 넓고, 규칙 면에서 낯선 증명으로의 일반화를 시험합니다 [4]. bench_lite.py의 문서 문자열도 자신의 단순화를 스스로 소리 내어 진술합니다(bench_lite.py 53–60행). 벤치마크는 도구이며, 도구에는 그 자신의 오차 막대가 있습니다; 평결 장은 측정치와 이 단서들을 함께 물려받습니다.
왜 중요한가
이 장은 앞선 두 장이 스스로는 측정할 수 없었던 것을 내놓음으로써 6부를 마무리합니다. 소프트 추론기와 번역-후-증명 파이프라인은 각각 하나의 미덕, 즉 하나는 강건함을, 다른 하나는 건전함을 주장했습니다; 여기의 세 프로토콜은 그 주장들을 표의 열로 바꿉니다. 방법론적 보상은 데스크 규모를 훨씬 넘어 일반화됩니다: 모든 헤드라인 숫자와 함께 레이블별 분할과 다수 클래스 기준선을 보고하고, 능력을 분리하여 보고서가 시스템이 어떤 능력을 갖췄는지 말하게 하며, 출력이 추론 그 자체이어야 하는 곳이라면 어디서든 레이블을 신뢰하는 대신 검사기로 그 추론을 채점하십시오.
앞으로의 보상은 5권의 의제이며, 이 장 자신의 숫자로 진술되어 있습니다. 0.817의 레이블 열과 0.167의 증명 열 사이의 발산은 축소된 추론 지름길 현상입니다; 기권 열은 보정과 선택적 예측의 씨앗입니다; 단계 검사기는 5권이 짓는 검증기-게이트 추론의 선조입니다; 그리고 가상 온톨로지 장치는 매개변수적 지식과 맥락 내 추론을 갈라놓는 표준 통제로서 그곳에서 되돌아옵니다. 규모에서의 신뢰는 아첨할 수 없는 도구에서 시작하며, 이 장은 그런 도구를 세 개 지었습니다.
핵심 용어
- 벤치마크 프로토콜(Benchmark protocol): 벤치마크의 기계 장치, 즉 예시 생성, 정답 레이블링, 요구되는 출력, 채점입니다; 그것이 측정한다고 주장하는 것과 달리 그것이 실제로 구별할 수 있는 것입니다.
- 삼항 함의 레이블(Three-way entailment label): 전제가 결론을 함의하면 참, 그 부정을 함의하면 거짓, 어느 쪽도 아니면 불확실입니다; 열린 세계 아래에서 이중 증명기 질의로 결정됩니다.
- 다수 클래스 기준선(Majority baseline): 언제나 가장 흔한 레이블을 내뱉는 입력 무관 전략으로, 정확도는 입니다; 확정된 FOLIO-lite 구성비에서는 0.500입니다.
- 규칙별 분리(Per-rule isolation): 각 항목을 정확히 하나의 추론 규칙 패턴을 중심으로 지어, 정확도를 규칙별로 보고할 수 있게 하는 것입니다; LogicBench의 설계입니다.
- 가상 온톨로지(Fictional ontology): 사전학습된 지식이 답할 수 없는 지어낸 술어에 대한 이론으로, 맥락 내 연역을 매개변수적 기억으로부터 분리합니다; PrOntoQA의 설계입니다.
- 단계 검사기(Step checker): 사고 사슬의 각 줄을 파싱하여 규칙 예화(유효함), 즉각적인 전제 연결(선형임), 전제-목표 연결성(연결됨)을 검사하는 검증기입니다; 이 셋의 논리곱이 엄격한 증명 정확도입니다.
- 엄격한 단계 타당성 대 광의의 단계 타당성(Strict vs broad step validity): 원 프로토콜의 단계별 축입니다: 엄격하게 유효하다는 것은 정답 증명이 사용하는 연역 규칙(전건 긍정)으로 유도 가능하다는 뜻이고, 광의로 유효하다는 것은 규칙 두 개를 한 단계로 연쇄하는 것처럼 더 강한 계산 아래에서만 유도 가능하다는 뜻입니다; 별도의 연결 요구 사항(선형 플래그)은 분포 밖 확장에서 왔으며, 건전한 단계들의 더미를 증명과 갈라놓는 것입니다.
- 그릇된-이유로-정답 비율(Right-for-wrong-reason rate): 로, 증명이 아닌 것이 실어 나른 정답 레이블입니다; 엄격한 증명이 정답 레이블을 함의할 때는 레이블 정확도에서 증명 정확도를 뺀 값과 같습니다; 확정된 탐욕적 기준선에서는 0.650입니다.
- 지표 함정(Metric trap): 한 시스템이 레이블 정확도(0.817 대 0.667)에서는 이기지만 증명 정확도(0.167 대 0.667)에서는 지는, 확정된 역전입니다; 어떤 단일 열도 충분하지 않습니다.
다음으로 이어지는 것
6부가 완성되었습니다: 조용히 실패하는 단일체 독해기, 시끄럽게 실패하는 인수분해된 파이프라인, 그리고 이제 그 실패 양식들을 서로 구별하고 값을 매기는 도구들입니다. 남은 것은 결산입니다. 정직한 평결은 모든 부의 확정된 영수증을 하나의 원장으로 읽어 들여 이 권을 마무리합니다: 논리를 미분 가능하게 만드는 각 방식이 무엇을 샀는지, 무엇을 대가로 치렀는지, 어떤 assert가 각 주장을 지키는지, 그리고 어떤 빚(보정, 충실성, 추론 지름길, 규모에서의 신뢰)이 5권의 목차로 이월되는지를 말입니다.
동반 코드: examples/integration/bench_lite.py는 두 코퍼스를 모두 생성하고, 두 시스템을 모두 실행하며, 단계 검사기와 이중-질의 레이블 부여기를 적용하고, 확정된 모든 주장을 단언합니다: 100퍼센트 트레이스 통과율, 기권/오염의 일치, 0이 아닌 그릇된-이유로-정답 비율, 지표 함정의 역전, 탐욕적 깊이 붕괴, 그리고 다수결과 never-Unknown 상한입니다. 이 장의 모든 숫자를 재현하려면 python3 examples/integration/bench_lite.py를 실행하십시오; examples/integration/translate_prove.py는 벤치마크 시스템들이 물려받는 파이프라인 아키텍처를 담고 있습니다.