함의 벤치마크의 공백

📍 현재 위치: VI부 · 벤치마크와 평가 — 17장. NeSy 벤치마크 스위트와 시뮬레이터는 이 분야가 공유하는 시험대와 그 집계 점수들을 둘러보았습니다; 이 장은 그 집계들이 구조적으로 보지 못하는 성질을 측정합니다: 시스템의 답이 함의 자체가 따르는 닫힘들을 존중하는가 하는 것입니다.

앞 장의 모든 벤치마크는 너무나 보편적이어서 눈에 띄지 않는 하나의 설계 결정을 공유합니다: 시험 문항은 독립적으로 표본추출되고 독립적으로 채점되며, 보고되는 것은 맞힌 비율입니다. 그 프로토콜은 점별 성질을 측정하지만, 함의는 점별 성질이 아닙니다. 함의는 닫힘 성질(closure property)을 지닌 관계입니다: 어떤 질의를 함의하는 이론은 그 질의의 모든 바꿔 쓰기 역시 함의하고, 그 부정을 부인하며, 어떤 유도도 건드리지 않는 문장에는 흔들리지 않고, 재작성된 복합 문장에는 그 재작성이 요구하는 대로 정확히 답합니다. 함의를 계산하는 시스템은 그 모든 답을 하나의 닫힘에서 읽어 내므로 그 불변성들을 자동으로 물려받지만, 레이블을 예측하는 시스템은 그중 어느 것도 물려받지 않으며, 평범한 정확도는 이 둘을 구별하지 못합니다. 이 장은 그 공백을 학계 세계 위에서 실행 가능하게 만듭니다: companion은 동일한 시드가 붙은 이론들로부터 짝지어진 프로브 계열을 생성하고, 4권의 낯익은 두 시스템을 측정하며, 리더보드가 감추는 숫자를 게시합니다.

쉽게 말하면

지리 퀴즈를 보는 두 학생을 상상해 보십시오. 둘 다 99점을 받습니다. 그런데 첫 번째 학생에게 "파리는 마드리드보다 북쪽에 있는가?"라고 묻고, 열 문항 뒤에 "마드리드는 파리보다 북쪽에 있는가?"라고 물으면, 그녀는 태연히 둘 다 그렇다고 답합니다. 두 번째 학생은 결코 그러지 않는데, 사실을 더 많이 외웠기 때문이 아니라 모든 질문에 답할 때 머릿속 지도 하나만 들여다보기 때문이며, 지도 하나는 파리를 마드리드보다 북쪽에도 남쪽에도 동시에 둘 수 없기 때문입니다. 퀴즈 점수는 이 둘을 갈라내지 못하는데, 퀴즈가 각 문항을 따로따로 묻기 때문입니다. 고치는 데는 아무 비용도 들지 않습니다: 답이 서로 들어맞아야 하는 연결된 쌍으로 질문을 묻고, 그 들어맞음이 성립하는 빈도를 세면 됩니다. 각 쌍의 두 번째 답은 첫 번째 답이 결정하므로, 새로운 정답지도 필요 없습니다.

이 장에서 다루는 내용

• 공백의 정의: 변환 아래에서 닫혀 있는 불변성 성질로서의 함의와 점별 성질로서의 정확도를 대비시키고, 측정상의 귀결을 곧바로 도출합니다: 독립적인 사례가 아니라 논리로 연결된 계열을 시험해야 한다는 것입니다.
• 논리가 생성하는 네 가지 프로브 계열: 대우 쌍, 무관한 확장(단조성) 프로브, 바꿔 쓰기 프로브, 드모르간 재작성이며, 각각의 생성 규칙을 companion에서 그대로 인용하고, 사람의 새 레이블은 단 하나도 필요로 하지 않습니다.
• 커밋된 측정: 통계적 추론기의 98.96퍼센트 평범한 정확도를 두 계열의 71.6퍼센트, 48.6퍼센트 일관성 비율과 대비시키고, 어느 계열이 왜 다치는지를 기계적으로 읽어 냅니다.
• 구조적 대비: 번역-후-증명 파이프라인이 모든 계열의 파싱된 모든 프로브에서 정확히 1.0의 일관성을 내지만, 바꿔 쓰기 프로브에서의 24.55퍼센트 기권으로 그 값을 정직하게 치릅니다.
• 충분하지 않은 필요성: 일관성은 계열별로 훈련해 넣을 수 있고, 시스템은 일관되게 틀릴 수 있습니다; 불변성과 정답성 사이의 정확한 논리적 관계를 커밋된 숫자 위에서 진술하고 실증합니다.
• 리더보드 제안: (정확도, 계열별 일관성, 커버리지) 세 항목을 보고하며, 어느 열을 기준으로 정렬하느냐에 따라 이 권의 두 시스템 순위가 뒤바뀐다는 커밋된 전시물을 제시합니다.

정확도는 점별 성질, 함의는 닫힘 성질

두 성질을 하나의 이론 위에 나란히 놓아 봅시다. $T$를 학계 세계의 한 이론, 즉 4권의 생성된 말뭉치들과 같은 사실과 규칙의 집합이라 하고, $q$를 "alice is cited."(앨리스는 인용되었다)라는 질문이라 합시다. 앞선 모든 권이 써 온 폐쇄 세계 읽기 아래에서, $T$는 그 원자가 유도 가능할 때 정확히 $q$에 참으로 답하고, 그 짝인 질문 $\lnot q$, 곧 "alice is not cited."(앨리스는 인용되지 않았다)에는 그 여집합으로 답합니다; 이 쌍은 한 번의 사실을 두 번 묻는 것입니다:

	질문	함의의 답	레이블 예측기의 답
$q$	"alice is cited."	참 (그 원자가 유도 가능함)	그 점수가 말하는 대로 무엇이든
$\lnot q$	"alice is not cited."	거짓 (정의상 여집합)	그 점수가 말하는 대로 무엇이든, 독립적으로

왼쪽 열은 제약되어 있습니다: 두 답은 두 면에서 본 하나의 결정이며, 둘 다를 단일한 닫힘에서 유도하는 어떤 계산도 결코 (참, 참)을 반환할 수 없습니다. 오른쪽 열은 제약되어 있지 않습니다: 각 질문을 학습된 점수를 통해 레이블로 사상하는 모델은 자유로이 (참, 참)이라 답할 수 있으며, 시험 집합이 마침 그 쌍의 한쪽 구성원만 담고 있다면, 그 비일관성은 아무 대가도 치르지 않습니다. 평범한 정확도는 점별 성질입니다: 각 (질문, 정답) 쌍을 따로 평가하므로, 그 값은 독립적인 지표항들의 합입니다. 이를 해독하면, $n$을 시험 문항의 개수, $\hat{y}_i$를 문항 $i$에 대한 시스템의 답, $y_i$를 그 정답 레이블이라 하고, $\mathbf{1}[\cdot]$을 대괄호 안 조건이 성립하면 $1$, 아니면 $0$인 지표라 할 때:

$$\text{acc} \;=\; \frac{1}{n}\sum_{i=1}^{n} \mathbf{1}[\hat{y}_i = y_i].$$

함의는 불변성 성질입니다: "모든 이론 $T$, 질의 $q$, 그리고 어떤 부류에 속한 변환 $\tau$에 대해, $\tau(T)$ 위에서의 $\tau(q)$에 대한 답은 $T$ 위에서의 $q$에 대한 답에 의해 결정된다"라는 형태의 진술들의 계열입니다. 그 변환은 질문을 재작성하거나(부정, 바꿔 쓰기, 드모르간) 이론을 확장할 수 있으며(무관한 문장 추가), 그것을 닫힘으로 만드는 것은 바로 그 결정 관계입니다. 일관성 비율(consistency rate)은 시스템이 하나의 닫힘을 얼마나 자주 지키는지를 측정합니다: $n_F$개의 프로브로 이루어진 계열 $F$에 대해, 각 프로브는 논리가 답을 상호 제약하는 짝지어진 질문들의 집합이며,

$$\text{cons}_F \;=\; \frac{1}{n_F}\sum_{i=1}^{n_F} \mathbf{1}[\text{the answers to probe } i \text{ respect } F\text{'s closure}],$$

그리고 이 장의 중심 양은 공백(gap)입니다, $\text{gap}_F = \text{acc} - \text{cons}_F$, 곧 시스템이 옳은 빈도와 시스템이 그나마 일관된 빈도 사이의 거리입니다. 이 정의가 필요로 하지 않는 것을 눈여겨보십시오: $\text{cons}_F$에는 정답 레이블이 전혀 등장하지 않습니다. 일관성은 논리가 공급하는 제약 아래에서 시스템의 답들을 서로 비교할 뿐이며, 그래서 프로브는 값싸게 만들 수 있고, 이는 또한 아래에 나올 정직한 마무리의 씨앗이기도 합니다. 시스템은 모든 곳에서 틀리면서도 모든 제약을 만족시킬 수 있기 때문입니다.

측정상의 귀결은 곧바로 따라 나옵니다. 질문을 독립적으로 표본추출하는 시험 집합은 연결된 쌍의 두 구성원을 함께 담는 일이 거의 없으며, 설령 담더라도 채점은 결코 그 둘을 묶지 않습니다: 정확도는 지표들을 한 번에 한 문항씩 합산하므로, 대우 쌍에서의 비일관적인 (참, 참)은 오류 하나가 있는 일관된 쌍만큼이나, 혹은 그보다도 더 잘 점수를 받습니다. 닫힘을 조금이라도 보려면 벤치마크는 계열, 곧 함께 생성되고 함께 채점되는 짝지어진 집합을 표본추출해야 합니다. 그것이 companion이 구현하고 주류 리더보드가 생략하는 설계이며, 그 생략이 바로 이 장의 이름이 된 공백입니다.

같은 두 시스템이 두 프로토콜 아래 놓입니다: 독립적인 질문은 이들을 한 점 차이의 동점이라 부르고, 논리로 연결된 계열은 이들을 51점 차이로 갈라놓습니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

논리가 생성하는 네 가지 프로브 계열

companion entailment_gap.py는 문장 하나 다시 입력하지 않고 4권의 커밋된 말뭉치로부터 프로브 기반을 짓습니다: ruletaker_lite.run을 다시 실행하여(4권 자신의 assert들을 재실행하므로 말뭉치는 사전 감사를 마친 채 도착합니다) 깊이 1 이하의 평가-분할 질문들, 곧 소프트 추론기의 훈련된 체제(regime)를 유지합니다(entailment_gap.py 110–117행). 이 제한은 짐을 떠받치고 있습니다: 4권은 이미 특징-가방(bag-of-features) 모델이 자신의 훈련된 깊이를 넘어서면 실패한다는 것을 보였으며, 이 장은 그 결과를 다시 실행하는 것이어서는 안 됩니다. 프로브는 모델이 좋은 지점, 곧 98.96퍼센트의 평범한 정확도를 내는 1156개 질문에 머무르므로, 어떤 공백이 나타나든 그것은 외삽이 아니라 프로토콜의 성질입니다. 두 시스템은 각각 한 번씩 감싸인 4권의 그 쌍입니다: 소프트 추론기는 훈련된 가중치 벡터 $\mathbf{w}$, 곧 (이론, 질문) 쌍의 열 개 지역 특징 $\mathbf{x}$와 가중치의 내적이 $\mathbf{w}^\top \mathbf{x} \gt 0$일 때 정확히 참으로 답하고, 번역-후-증명 파이프라인은 엄격한 문법으로 각 문장을 파싱하고, 실패한 질문을 부분 어휘집을 통해 한 번 수선하며, 파싱된 이론의 최소 고정점 소속 여부로 폐쇄 세계 가정 아래에서 답하되, 문법이 감당하지 못할 때마다 None으로 기권합니다(entailment_gap.py 177–189행; 발췌문의 주석에서 CWA는 폐쇄 세계 가정(closed-world assumption)을, lfp는 최소 고정점(least fixpoint)을, "iff"는 "if and only if"(필요충분, 곧 "일 때 그리고 오직 그때만")를 줄인 것이고, XOR은 두 비트가 서로 다를 때 정확히 참이 되는 배타적 논리합(exclusive or)입니다):

    def answer(self, sentences: list[str], question: str) -> bool | None:
        """Parse (repairing once if the strict grammar objects), then decide
        by closed-world membership; None = abstention on a parse failure."""
        try:
            person, pred, neg = tp.parse_statement(question)
        except tp.ParseError:
            try:
                person, pred, neg = tp.parse_statement(tp.repair(question))
            except tp.ParseError:
                return None
        # CWA: True iff the atom is derivable, complemented for "not":
        #   answer = [ is(person, pred) in lfp ] XOR neg
        return (("is", person, pred) in self.closure(sentences)) ^ neg

각 프로브 계열은 하나의 닫힘을 예시하며, 각각은 이미 발표된 진단법의 축소판입니다. 대우 쌍(contraposition pairs)은 같은 이론에서 같은 원자의 두 극성을 모두 회수합니다(4권의 은행이 둘 다 내놓으므로 그 쌍들은 다시 표본추출되는 것이 아니라 묶이는 것입니다): 폐쇄 세계 아래에서의 닫힘은 $T$가 $q$에 참으로 답하는 것이 정확히 $\lnot q$에 거짓으로 답하는 것과 같다는 것이므로, 두 답은 반드시 불일치해야 합니다(entailment_gap.py 209–219행). 이는 RobustLR의 이론 쪽 부정 대비를 질문 수준으로 옮겨 놓은 것이며 [1], 그 이동은 이 장 자신의 각색입니다: RobustLR은 언제나 규칙 은행을 편집하고 시험 대상 진술은 고정해 두며, 그 규칙 수준 대우 편집은 우리의 폐쇄 세계 말뭉치가 지니지 않은 고전적 부정을 필요로 하므로, 여기서의 프로브는 질문 수준에 머무르며, 이는 명시적으로 진술된 축소입니다.

무관한 확장 프로브(irrelevant-expansion probes)는 증명 가능하게 아무것도 바꾸지 않는 추가 아래에서 답의 단조성을 시험합니다. 여기서 이 권의 가장 오래된 규율이 제 몫을 하는데, 말뭉치의 논리가 단조적이지 않기 때문입니다: 실패로서의 부정(negation as failure)은 삽입된 사실 하나가 본문에 "not c"라 적힌 규칙을 죽일 수 있다는 뜻이며, 이는 일곱 난이도 축이 자신의 의미론 장치로 실증했던 반단조성입니다(difficulty_axes.py 285–305행). 그러므로 "무관함"은 결코 가정되지 않습니다; 그것은 프로브가 지어지기 전에 4권 자신의 레이블 부여기에 맞서 양방향으로 검증됩니다(entailment_gap.py 243–265행):

    for person in rt.PEOPLE:
        for c in rt.L0:
            if (person, c) in stated:
                continue
            aug = {"facts": theory["facts"] + [(person, c)],
                   "rules": theory["rules"]}
            # lfp(T + f) = lfp(T) u {f}   (gain exactly the inserted atom)
            if set(rt.label_with_depth(aug)) == ref | {("is", person, c)}:
                found["facts"].append((person, c))

그 점검을 해독하면: 삽입된 사실 $f$는 확장된 이론의 최소 고정점(코드 주석의 lfp이며, u는 집합의 합집합을 나타냅니다)이 정확히 옛 고정점에 삽입된 원자만을 더한 것과 같을 때만 무관함이 인증됩니다. 곧 잃은 것도 없고(어떤 규칙도 죽지 않고) 더 얻은 것도 없다는(어떤 규칙도 새로 발화하지 않는다는) 뜻입니다. 두 번째 삽입 종류인 교란 규칙 "if c and not e then h"는 더 엄격한 등식 $\mathrm{lfp}(T + r) = \mathrm{lfp}(T)$로 인증됩니다: 이 규칙은 그 긍정 조건이 어떤 사람에 대해서는 충족될 수 있음에도 전혀 발화하지 않으며, 이는 정확히 유도를 추적하는 대신 규칙 본문에 패턴을 맞추는 추론기 앞에 교란 규칙(distractor rule)이 드리우는 미끼입니다. 프로브는 그런 다음 검증된 이웃 전체에 대한 불변성을 요구합니다: $q$에 대한 답은 모든 인증된 삽입에서 살아남아야 하며, 이는 전칭 양화된 닫힘을 정직하게 읽어낸 것입니다. 이 계열과 다음 계열은 모두 CheckList가 방법론으로 만든 바로 그런 의미의 불변성 시험, 곧 출력이 움직여서는 안 되는 교란입니다 [2].

바꿔 쓰기 프로브(paraphrase probes)는 4권이 커밋한 어휘 변이 손잡이를 재사용합니다: translate_prove.SYNONYM_CORRUPTION의 다섯 속칭 동의어("productive"에서 "prolific"로, "cited"에서 "referenced"로, 그리고 세 개 더; 파이프라인의 수선 어휘집은 다섯 중 셋만 압니다)입니다. 술어에 변형이 있는 각 기본 질문은 그 재작성된 자기 자신, 곧 속칭 아래의 같은 원자와 짝지어지므로, 정답은 변하지 않고 전달되며 일관된 추론기는 둘 다 똑같이 답하거나 정직하게 기권합니다(entailment_gap.py 280–294행). 드모르간 프로브(De Morgan probes)는 두 리터럴짜리 복합 문장으로 씨뿌려집니다: 논리곱 $C = A \wedge B$, 곧 $A$와 $B$가 두 리터럴("x is p"와 "y is q")의 이름이고 $\wedge$가 "그리고"의 기호인 이 논리곱은 "x is p and y is q."(x는 p이고 y는 q이다)로 표현되며, 드모르간 법칙에 따른 그 부정의 리터럴 재작성인 $\lnot(A \wedge B) = (\lnot A) \vee (\lnot B)$($\vee$는 "또는"의 기호), 곧 "x is not p or y is not q."(x는 p가 아니거나 y는 q가 아니다)와 짝지어집니다; 두 답은 반드시 불일치해야 합니다(entailment_gap.py 297–328행). 복합 문장은 정직한 모델링 결정을 강제하는데, 소프트 추론기가 연결사에 대한 표현을 아예 지니지 않기 때문입니다: companion은 지역 특징들의 가방이 할 수 있는 유일한 방식으로 복합 문장에 답합니다, 곧 두 리터럴의 특징 벡터를 평균하여 $\mathbf{x}_C = (\mathbf{x}_{l_1} + \mathbf{x}_{l_2})/2$를 얻고 평소처럼 문턱 값을 적용하는 것이며, 이는 허수아비가 아니라 선언된 해석입니다(entailment_gap.py 130–142행). 파이프라인은 조합적으로 답합니다: 각 리터럴을 증명하고, 연결사의 진리함수로 결합합니다.

생성 방식에 대한 두 가지 유의점이 있습니다. 첫째, 어떤 프로브도 새로운 주석을 필요로 하지 않았습니다: 모든 계열의 모든 구성원에 대한 정답은 말뭉치를 생성한 것과 같은 고정점 레이블 부여기에서 나옵니다. 논리가 레이블 부여기이며, 이는 이 시리즈가 1권 이래로 지켜 온 규율이자 FOLIO가 모든 정답 레이블을 1차 논리 증명기로 검증함으로써 분야 규모로 제도화한 규율입니다 [3]. 둘째, 폐쇄 세계는 단순함을 대가를 치르고 삽니다: DELTA는 참, 거짓, 모름의 열린 세계 삼원 레이블 아래에서 이와 똑같은 프로그램을 돌리며, 그곳에서는 일관성이 실패할 여지가 더 많습니다 [4]; 우리의 폐쇄 세계는 모름을 무너뜨리므로, 여기서의 일관성은 이원적이며, 이는 명시적으로 진술된 단순화입니다.

커밋된 측정

이 실험은 모든 계열에 대해 두 시스템을 측정하며 모든 주장을 assert로 지킵니다(entailment_gap.py 335–468행). 먼저, 리더보드가 발표할 관점입니다:

[1] the leaderboard view: plain label accuracy on the probe base
    base: 1156 eval questions of depth <= 1 (the soft reasoner's trained regime)
      system                 plain accuracy
      soft reasoner          0.9896
      translate-then-prove   1.0000
    delta: 1.04 points — a label-only leaderboard calls this a tie

그런 다음 프로브가 보는 관점, 이 장의 척추입니다:

[3] the committed table: consistency per probe family
      family           n     soft cons.   pipeline cons.   pipeline coverage
      contraposition   470     1.0000       1.0000           1.0000
      expansion       1156     0.7163       1.0000           1.0000
      paraphrase       782     0.4859       1.0000           0.7545
      de morgan        289     1.0000       1.0000           1.0000
    expansion sub-rates: facts only 0.9931, distractor rules 0.7197

그 공백들을 0.9896 평범한 정확도에 맞대어 읽어 보십시오. 이 모듈은 반올림되지 않은 비율로부터 $\text{gap}_F$를 계산하여 대우와 드모르간을 $-1.04$점(일관성이 정확도보다 높음)으로, 확장을 $+27.34$점으로, 바꿔 쓰기를 $+50.37$점으로 인쇄합니다: 두 계열은 _check가 단언하는 커밋된 10점 문턱을 훌쩍 넘어섭니다(entailment_gap.py 487–488행). 같은 모델이, 같은 이론들 위에서, 자신이 훈련받은 바로 그 깊이에서, 자신의 바꿔 쓰기 이웃의 겨우 절반에서만 일관됩니다. 그 숫자에 관한 그 무엇도 0.9896에는 보이지 않습니다.

어느 계열이 다치는지, 그리고 왜 다치는지는 신비롭다기보다는 기계적입니다; 커밋된 예시들이 그 원천을 지목합니다(entailment_gap.py 데모, [2] 절):

    expansion        add 'If someone is published and not cited then they are diligent.'
                     (verified never-firing; its positive half baits one_step, which
                     ignores 'not' — the soft answer to 'dave is diligent.' flips False -> True)
    paraphrase       'alice is cited.' -> 'alice is referenced.'  (soft flips True -> False)

확장 실패는 4권의 교란 메커니즘을 수량화한 것입니다. 소프트 추론기의 one_step 특징은 질의된 머리를 가진 어떤 규칙이 자신의 긍정 본문 원자를 모두 진술받았을 때 발화하며, 부정된 것들은 무시합니다(ruletaker_lite.py 286–302행). 인증된 발화하지 않는 규칙 "if published and not cited then diligent"는 고정점을 손대지 않고 두는데, dave가 인용되었고 실패로서의 부정이 그 규칙을 막기 때문입니다; 하지만 dave는 실제로 published이므로 긍정 절반이 들어맞고, one_step은 0에서 1로 뒤집히며, 점수는 문턱을 넘습니다. 하위 비율들은 그 원천을 고립시킵니다: 사실 삽입 아래에서는 99.3퍼센트가 불변이고, 교란 규칙 아래에서는 72.0퍼센트가 불변입니다. 바꿔 쓰기 실패는 더 노골적입니다: 술어 토큰에 키를 건 모든 증거 특징이 0을 읽는데, "referenced" 같은 속칭 술어는 어떤 진술된 사실에도 나타나지 않고 어떤 규칙의 머리도 되지 못하므로 stated, one_step, head_pred가 모두 사라지기 때문입니다; 재작성에서 살아남는 것은 사람에 키를 건 fact_frac 사전 성향과 편향 및 극성 특징들뿐이며, 커밋된 실행에서는 훈련된 가중치가 그 잔여분의 흔들림을 압도하므로 변형 질문의 답은 극성별로 상수가 되어, 정답이 무엇이든 모든 긍정 변형은 거짓으로, 모든 부정 변형은 참으로 답해집니다; 남는 것이 48.6퍼센트 일관성입니다. 두 실패 모두 일곱 난이도 축이 깊이와 직교한다고 도식화한 축들 위에 있습니다: 프로브는 깊이를 모델의 훈련된 체제에 고정했는데도, 비일관성은 교란 민감성과 어휘 이동을 통해 도착했을 뿐, 더 긴 유도를 통해서는 결코 도착하지 않았습니다.

구조적 대비: 정리 대 성취

파이프라인의 열은 네 번 1.0000을 기록하며, 그 숫자만큼이나 그 읽는 방식이 중요합니다: 이는 실행의 단언된 성질입니다, 어느 계열에서든 파싱된 프로브 하나라도 자신의 닫힘을 어기면 _check가 실패합니다(entailment_gap.py 506–509행), 하지만 이는 경험적인 놀라움이 아닙니다. 파이프라인이 내놓는 모든 답은 하나의 대상, 곧 파싱된 이론의 최소 고정점에서 읽어 낸 것이며, 그 닫힘들은 그 대상에 관한 정리들입니다. 대우가 성립하는 것은 answer가 소속 비트와 질문의 부정 플래그를 XOR한 것을 반환하기 때문이며, 그래서 $q$와 $\lnot q$는 말 그대로 하나의 비트를 반대 부호로 두 번 읽는 것입니다. 확장이 성립하는 것은 인증된 무관한 삽입이 (삽입된 원자 자체를 제외하고는) 고정점을 그대로 남겨 두기 때문이며, 동일한 고정점은 동일한 비트를 냅니다. 바꿔 쓰기는 문법이 배치할 수 있는 무엇에서든 성립하는데, 수선이 고정점을 참조하기 전에 변형된 토큰을 정경적 술어로 되돌려 사상하기 때문입니다. 드모르간이 성립하는 것은 각 리터럴이 증명되고 연결사의 진리표가 적용되며, $\lnot(A \wedge B)$와 $(\lnot A) \vee (\lnot B)$가 같은 진리표를 갖기 때문입니다. 이마저도 그냥 믿고 마는 것이 아닙니다: companion은 캐시된 닫힘 답들을 1권의 SLD(선택적 선형 정형절, Selective Linear Definite-clause resolution) 증명기에 맞서 200개의 시드가 붙은 표본에서 표본 감사하며, 컴파일된 그라운드 프로그램 위에서 sld.provable과의 일치를 매번 단언합니다(entailment_gap.py 364–374행).

그 대가는 세 번째 열입니다. 바꿔 쓰기 프로브에서 파이프라인의 커버리지는 0.7545입니다: 변형된 질문의 24.55퍼센트에서 기권하며, 정확히 그 속칭 술어가 자신의 수선 어휘집 밖에 있는 것들입니다("referenced"와 "veteran"은 문법 밖에 머무르고, 어휘집은 나머지 세 동의어를 복구합니다). 그 기권은 정직합니다, 추측이 아니라 None이며, III부의 기권 장치가 이미 그 정직함에 값을 매겼습니다; 하지만 이는 파이프라인의 완벽한 일관성이 더 작은 세계에 관한 진술이라는 뜻입니다. 프로브의 절반에서 기권하는 시스템은 자신이 답하는 절반에서는 자명하게 일관됩니다; 커버리지는 일관성 열을 정직하게 유지해 주는 열입니다. 이제 두 시스템의 그림이 완성됩니다: 통계적 일관성은 경험적 성취이며, 훈련이 그것을 심어 놓은 곳에는 있고 교란 하나만 지나면 없어지는 반면, 기호적 일관성은 정리이며, 커버리지로 값을 치릅니다. 바로 옆에서 시작하는 VII부의 사업인 하이브리드 설계는 커버리지 청구서 전액을 치르지 않고도 그 정리를 가지려는 시도입니다.

필요하지만 충분하지 않다: 일관성은 훈련해 넣을 수 있고, 거짓말할 수 있다

소프트 추론기가 1.0000을 기록하는 두 계열은 잡음이 아니며, 이 표에서 가장 교훈적인 행들입니다. 그곳의 일관성은 훈련해 넣어진 것이며, 그 메커니즘은 특징 집합으로부터 네 줄 만에 유도할 수 있습니다. 고정된 원자에 대한 질문의 열 개 특징(ruletaker_lite.py 286–302행)을 두 그룹으로 적어 봅시다: 극성-불변 증거와 극성-부호 붙은 사본입니다. 먼저 증거 특징들을 해독하면: $\text{stated}$는 질의된 원자가 진술된 사실임을 나타내고, $\text{one\_step}$은 위에서 정의한 규칙-미끼 지표이며, $\text{head\_pred}$는 어떤 규칙이 질의된 술어를 유도할 수 있음을 나타내고, $\text{fact\_frac}$은 질의된 사람에 대해 진술된 기본 술어의 비율입니다. 긍정 질문에는 $\text{pol} = +1$을, 부정된 질문에는 $\text{pol} = -1$을 두고, $\text{has\_not}$을 단어 "not"에 대한 0/1 플래그라 할 때, 코드가 커밋하는 순서 그대로 열 개의 특징은 다음과 같습니다: $1$로 고정된 상수 편향 특징(그 가중치가 $w_0$입니다), 다섯 개의 원시 양 $\text{stated}$, $\text{one\_step}$, $\text{has\_not}$, $\text{head\_pred}$, $\text{fact\_frac}$(가중치 $w_1$부터 $w_5$), 그리고 네 개의 극성-부호 사본 $\text{pol}\cdot\text{stated}$, $\text{pol}\cdot\text{one\_step}$, 맨몸의 플래그 $\text{pol}$ 자체, $\text{pol}\cdot\text{fact\_frac}$(가중치 $w_6$부터 $w_9$)입니다. 첫 번째 특징이 상수 $1$이고 아홉 번째가 $\text{pol}$ 단독이기 때문에, 아래에서 $w_0$과 $w_8$은 곁에 아무 특징 기호 없이 나타납니다. 점수 $s = \mathbf{w}^\top \mathbf{x}$는 다음과 같이 분해됩니다

$$s \;=\; \underbrace{w_0 + w_1\,\text{stated} + w_2\,\text{one\_step} + w_4\,\text{head\_pred} + w_5\,\text{fact\_frac}}_{u,\ \text{polarity-even}} \;+\; w_3\,\text{has\_not} \;+\; \text{pol}\cdot \underbrace{\left(w_6\,\text{stated} + w_7\,\text{one\_step} + w_8 + w_9\,\text{fact\_frac}\right)}_{v,\ \text{polarity-odd}}.$$

긍정 질문에 대해서는 $\text{has\_not} = 0$이고 $\text{pol} = +1$이므로 $s^{+} = u + v$입니다. 그 대우 짝에 대해서는 $\text{has\_not} = 1$이고 $\text{pol} = -1$이므로 $s^{-} = u + w_3 - v$입니다. 이제 $a = u + w_3/2$와 $b = v - w_3/2$를 대입하고 양방향을 확인해 봅시다: $a + b = u + w_3/2 + v - w_3/2 = u + v = s^{+}$이고, $a - b = u + w_3/2 - v + w_3/2 = u + w_3 - v = s^{-}$입니다. 그러므로 모든 대우 쌍의 두 점수는 정확히 다음 형태를 갖습니다

$$s^{+} = a + b, \qquad s^{-} = a - b,$$

여기서 $a$는 그 쌍의 극성-불변 점수이고 $b$는 그 극성-부호 점수입니다. 모델은 점수가 양수일 때 참으로 답하므로, 그 쌍은 $a+b$와 $a-b$ 중 하나는 양수이고 다른 하나는 그렇지 않을 때 정확히 일관됩니다(답이 불일치함). $\lvert b\rvert \gt \lvert a\rvert$이면 $b$가 지배적이고 두 식은 반대 부호를 취합니다: $b \gt 0$이면 $a + b \geq b - \lvert a\rvert \gt 0$이고 $a - b \leq \lvert a\rvert - b \lt 0$이며, $b \lt 0$일 때도 대칭적으로 그렇습니다. $\lvert b\rvert \lt \lvert a\rvert$이면 두 식 모두 $a$의 부호를 공유하고 그 쌍은 비일관되게 답해집니다. 따라서 그 쌍은 정확히 자신의 극성-부호 점수가 극성-불변 점수를 압도할 때 일관됩니다. 4권의 훈련 은행은 모든 원자를 두 극성 모두로, 상보적인 정답과 함께 물었으며, 극성-균형 은행은 정확히 그 불변 부분을 벌합니다: 오직 부호가 있는 특징들만 상보적인 레이블에 들어맞을 수 있으므로, 경사 하강은 훈련 분포 위에서 $\lvert b\rvert \gt \lvert a\rvert$가 될 때까지 $w_6$부터 $w_9$까지를 적재합니다. 470쌍에 걸친 커밋된 1.0000은 그것이 모든 평가 쌍에서도 성공했음을 말해 줍니다.

드모르간 행은 이제 공짜로 따라오며, 이 장에서 가장 예리한 전시물입니다. 복합 점수는 평균된 특징에 대해 선형이므로, 리터럴 점수의 평균입니다: $s_C = \mathbf{w}^\top (\mathbf{x}_1^{+} + \mathbf{x}_2^{+})/2 = (s_1^{+} + s_2^{+})/2 = \bar{a} + \bar{b}$이며, 여기서 $\bar{a}$와 $\bar{b}$는 두 리터럴의 불변 점수와 부호 점수를 평균한 것입니다. 재작성된 부정은 극성이 뒤집힌 같은 두 리터럴이므로, $s_{C'} = (s_1^{-} + s_2^{-})/2 = \bar{a} - \bar{b}$입니다. 같은 조건 $\lvert\bar{b}\rvert \gt \lvert\bar{a}\rvert$가 그 거울상을 내놓으므로, 모델은 연결사에 대한 표현을 아예 지니지 않고서도 드모르간의 법칙을 289쌍에 걸쳐 1.0000으로 완벽하게 따릅니다: 그 재작성은 오직 극성만을 뒤집을 뿐이며, 극성 반대칭이 훈련되어 들어갔습니다. 하지만 같은 계열의 정확도 열을 보십시오: 두 리터럴 점수의 평균은 논리곱도 논리합도 구현하지 않습니다. 확신을 갖고 참인 리터럴 하나와 거짓인 리터럴 하나로 이루어진 논리곱은 평균이 양수가 되어 정답이 거짓임에도 참으로 답합니다. 커밋된 실행은 그 발산을 정확하게 만듭니다: 소프트 모델의 드모르간 쌍은 1.0000으로 거울상을 이루지만 그 복합 답의 0.6055만이 정답이며, 파이프라인은 둘 다에서 1.0000을 기록하고, 이는 단언됩니다(entailment_gap.py 494–509행).

이것이 이 장이 갚아야 할 정확한 논리적 관계입니다. 불변성 프로브를 통과하는 것은 함의를 계산하기 위한 필요 조건입니다, 자신의 답을 단일한 닫힘에서 읽어 내는 모든 함수는 그 닫힘 성질을 정리로서 만족시키기 때문입니다; 그러므로 실패한 프로브는 시스템이 함의를 계산하고 있지 않다는 증거가 아니라 증명입니다. 이는 충분 조건이 아닙니다: 그 닫힘들은 답 함수의 형태만을 제약할 뿐 그 근거의 진실은 결코 제약하지 않으며, 닫힘을 존중하는 함수들의 집합은 정답인 함수 곁에 모든 일관된 사칭자를 나란히 담고 있습니다. 소프트 모델의 드모르간 행은 현행범으로 붙잡힌 하나의 사칭자이며, 복합 문장의 39.45퍼센트에서 일관되게 틀립니다; 추론 지름길은 더 깊은 종을 공급했습니다, 곧 체계적으로 잘못된 기호들 위에서 진짜 연역을 실행하는, 구성상 완벽히 일관되지만 세계에 대해서는 틀린, 잘못 접지된 모델입니다. 두 따름정리가 뒤따릅니다. $\text{cons}_F$는 어떤 정답 레이블도 참조하지 않으므로, 직접 최적화될 수 있습니다: 레이블 없는 프로브 계열에 대한 일관성 손실은 주석 없이도 닫힘을 강제하며, 극성-균형 은행은 그 강제가 계열별로 작동한다는 커밋된 실증이고, 이는 닫힘이 훈련 분포가 그에 정렬된 데이터를 실어 나른 곳에서만 나타나며 그때조차 확실하게 나타나지는 않는다는 진단 문헌의 발견과 일치합니다 [1]. 그리고 같은 이유로, 일관성 손실은 일관되게 잘못된 골짜기로 내려갈 수 있으므로, 이는 정답성 신호를 대신하는 것이 아니라 그 곁에 놓여야 합니다.

공백을 통해 읽는 이 분야

이 장의 출처 각각은 같은 원리, 곧 사례가 아니라 불변성을 벤치마크하라는 원리의 부분적 사례이며, 각각은 그 원리의 다른 면을 다룹니다. RobustLR은 연역적 규칙 은행에 논리적 편집, 곧 대우, 부정, 논리곱 재작성을 적용하고 모델의 답이 일관되게 움직이는지를 채점합니다: 트랜스포머 추론기에 대해 예시된, 규칙 쪽(이론 편집) 닫힘이며, 논리가 편집된 정답을 생성합니다; 그것이 값을 매기지 않는 것은 기권입니다, 모든 시스템이 모든 것에 답하기 때문입니다 [1]. CheckList는 일반적 형태의 방법론입니다: 최소-기능성, 불변성, 방향성-기대 시험을 정확도 너머의 일급 벤치마크 시민으로 삼습니다; 그 폭은 손으로 저술한 기대치로 사들여지므로, 그 목록들은 미적분처럼 조합되지 않으며, 어떤 템플릿의 정답도 인증하지 않습니다 [2]. FOLIO는 정확히 그 인증을 고칩니다: 그 삼원 함의 프로토콜의 모든 정답 레이블은 사람이 쓴 1차 논리 주석에 맞서 1차 논리 증명기로 점검되며, 그 구성상의 건전성은 사람이 수행한 자연어-논리 정렬의 한도 안에서 성립합니다; 다만 채점은 여전히 점별입니다, 연결된 계열이 아니라 사례별입니다 [3]. DELTA는 열린 세계 삼원 레이블과 통제된 구성적 분할을 지닌 기술 논리 함의 과제를 생성합니다, 계열 생성에 딱 맞는 기반이지만, 다시 사례별로 채점됩니다 [4]. 그리고 온톨로지 세계는 이 문제의 자기 버전을 이십 년 전에 풀었습니다: LUBM(리하이 대학교 벤치마크, Lehigh University Benchmark)은 지식 베이스 시스템을 질의당 완전성(모든 함의된 답을 돌려주었는가?)과 건전성(돌려준 모든 것이 함의되었는가?)으로 채점하며, 이는 표본추출된 레이블이 아니라 함의 관계 자체에 대한 지표입니다; 그것이 결코 필요로 하지 않았던 것은, 그 시스템들이 가정상 추론기였기 때문에, 통계적 예측기가 흉내 내는 것을 잡아내는 프로토콜입니다 [5]. 이 장의 이름이 된 공백은 어떤 주류 리더보드도 현재 조립하지 않는 그 부분들의 조합입니다: 논리로 생성된 연결된 계열, 증명기로 인증된 정답, 계열별 일관성, 그리고 커버리지를 함께 보고하는 것입니다.

리더보드 제안

VI부는 하나의 구체적인 수출품으로 마칩니다: (정확도, 계열별 일관성, 커버리지) 세 항목을 보고하는 것입니다. 커밋된 실행은 세 열 모두가 중복되지 않는 정보를 담고 있다는 논거입니다, 이 권의 두 시스템이 어느 열을 기준으로 정렬하느냐에 따라 순위가 뒤집히기 때문입니다:

정렬 기준	소프트 추론기	번역-후-증명	우위
평범한 정확도	0.9896	1.0000	통계적 동점, 1.04점
최악 계열 일관성	0.4859	1.0000	파이프라인, 51.41점 차
프로브 커버리지(바꿔 쓰기)	1.0000	0.7545	소프트 추론기, 24.55점 차

[5] the exhibit: what the leaderboard sees vs what the probes see
      plain-accuracy delta            1.04 points   (indistinguishable)
      worst-family consistency delta 51.41 points   (structural vs statistical)

두 델타 모두 단언됩니다, 평범한 정확도는 5점 이내이고 최악 계열 일관성은 최소 25점 차이 납니다(entailment_gap.py 519–522행), 그래서 이 전시물은 시드가 붙은 생성을 다시 실행해도 살아남습니다. 단일 숫자 리더보드는 이 세-열짜리 그림을 자신의 가장 정보가 적은 축 위로 투영합니다: 정확도로 정렬하면 두 시스템은 서로 바꿔 써도 되고, 일관성으로 정렬하면 파이프라인의 구조적 보증이 지배하며, 커버리지로 정렬하면 소프트 모델의 모든 것에 답하는 태도가 지배합니다. 의료 코딩 보조 도구를 위해 시스템을 고르는 실무자와 브레인스토밍 도구를 위해 고르는 실무자는 서로 다른 열을 기준으로 정렬해야 합니다; 정확도로 미리 정렬된 리더보드는 그 선택을 둘 다를 위해 조용히 내려 버렸고, 적어도 하나에 대해서는 잘못 내렸습니다. 추가 열들은 아무런 주석 비용도 들지 않고 이 권의 말뭉치에서 몇 초 만에 실행됩니다; 채택의 걸림돌은 비용이 아니라 관행입니다.

아직 풀리지 않은 부분

이 장의 프로브 목록은 하나의 논리에 속하며, 그 목록에 관한 질문은 세 방향으로 열려 있습니다. 첫째, 더 풍부한 논리들은 자신만의 목록을 필요로 하며, 이 목록의 번역이 아닙니다: 대우는 취소 가능 조건문에는 타당하지조차 않습니다("새는 대개 난다"는 "날지 못하는 것은 대개 새가 아니다"를 허용하지 않습니다), 그래서 오늘의 대우 프로브를 취소 가능 추론기에 그대로 수출한다면 옳은 행동을 벌하게 될 것입니다. 확률적, 취소 가능, 또는 파라일관적 추론기가 마땅히 따라야 할 닫힘이 무엇인지는, 벤치마크 질문을 제기하기 전에 먼저 해결되어야 할 의미론 질문입니다. 둘째, 불확실성 아래에서의 일관성은 거의 측정되지 않고 있습니다. 이 장은 굳은 레이블을 비교했지만, III부의 보정 장이 뜻하는 의미에서 보정된 시스템은 그 이상을 갚아야 합니다: 그 시스템의 확신은 바꿔 쓰기에 불변해야 하고, $q$와 $\lnot q$에 대한 그 확률들은 폐쇄 세계 아래에서 합이 1이 되어야 하며, 무관한 삽입은 그 사후 확률 전체를 손대지 않고 두어야 합니다. 어떤 모델은 동의어 하나 아래에서 확신이 20점 흔들리면서도 모든 레이블-수준 프로브를 통과할 수 있으며, 어떤 표준 프로토콜도 그것을 잡아내지 못합니다. 셋째, VI부가 계속 손짓해 온 인간에 관한 질문은 아직 쓰이지 않은 연구로 남아 있습니다: 사용자가 배치된 시스템에서 비일관성을 감지하는지, 비일관된 답이 명백히 틀린 답에 비해 얼마나 빨리 신뢰를 갉아먹는지, 그리고 일관성이 실제로 어떤 값을 요구하는지입니다. 리더보드 제안은 일관성이 누군가에게 중요하다고 가정합니다; 아직 없는 인간-컴퓨터 상호작용 실험이 얼마나, 그리고 누구에게 그러한지를 밝혀 줄 것입니다.

왜 중요한가

이 장은 VI부의 마무리 원리를 실행 가능한 형태로 담은 것입니다: 사례가 아니라 불변성을 벤치마크하라는 것입니다. 이 권은 단일한 답, 정당화, 충실성, 보정을 겨냥한 신뢰 도구들로 시작했습니다; 그런 다음 벤치마크 장들은 집계 점수가 그것들마저도 어떻게 흐리는지를 보였습니다. 함의 공백은 그 흐림의 가장 날카로운 판본인데, 그것이 관계를 계산하는 것과 그 출력을 흉내 내는 것 사이의 구조적 차이를, 1.04점짜리 정확도 델타 뒤에 숨기기 때문입니다. 독자 자신의 연구를 위한 수출품은 유별나게 값이 쌉니다: 이미 형식적 기반으로부터 데이터를 생성하는 어떤 평가든(논리를-레이블-부여기로-쓰는 네 권을 거친 뒤라면, 당신의 것도 그렇습니다) 아무 주석 비용 없이 독립적인 사례 대신 연결된 계열을 내놓을 수 있으며, 그런 계열 하나하나는 평범한 정확도가 재현할 수 없는 렌즈입니다. 시리즈 전체의 궤적을 두고 보면, 여기서 완성된 두-시스템 그림, 곧 성취로서의 일관성 대 정리로서의 일관성은 VII부가 지금 풀려고 하는 바로 그 긴장입니다.

핵심 용어

• 닫힘 성질(함의의)(closure property): 변환된 질의에 대한, 변환된 이론 위에서의 답이 원래 답에 의해 결정된다는 진술; 대우, 무관한 확장, 바꿔 쓰기 불변성, 드모르간 쌍대성이 여기서 예시된 네 가지입니다.
• 점별 성질(pointwise property): 평범한 정확도처럼 사례별 지표들의 평균인 벤치마크 양으로, 그래서 답들 사이의 관계를 볼 수 없습니다.
• 프로브 계열(probe family): 하나의 이론에서 생성되어 그 답이 논리에 의해 상호 제약되는 짝지어진 질문 집합; 일관성 채점의 단위입니다.
• 일관성 비율(consistency rate): 시스템의 답이 계열의 닫힘을 존중하는 프로브의 비율; 정답 레이블 없이도 계산 가능합니다.
• 공백(계열의)(gap): 평범한 정확도에서 계열의 일관성 비율을 뺀 것; 커밋된 실행은 확장에서 27.3점, 바꿔 쓰기에서 50.4점의 공백을 기록합니다.
• 무관한 확장(irrelevant expansion): 이론의 최소 고정점을 (삽입된 원자 자체를 제외하고는) 변화 없이 남긴다고 검증된 사실 하나 또는 발화하지 않는 교란 규칙 하나의 삽입; 실패로서의 부정이 논리를 비단조적으로 만들기 때문에 이 검증은 필수입니다.
• 커버리지(coverage): 시스템이 기권하지 않고 답하는 프로브의 비율; 완벽한 일관성 점수를 정직하게 유지해 주는 열입니다.
• 필요하지만 충분하지 않음(necessary, not sufficient): 불변성 프로브에 실패하는 것은 시스템이 함의를 계산하지 않는다는 것을 증명합니다; 모든 프로브를 통과하는 것은 그것을 증명하지 않는데, 잘못 접지된 추론기를 포함한 일관된 사칭자들이 존재하기 때문입니다.

이 장이 이끄는 곳

두-시스템 그림은 VI부를 그것이 풀 수 없는 긴장으로 마칩니다: 소프트 모델은 모든 것을 커버하지만 아무것도 보증하지 않고, 파이프라인은 자신이 답하는 모든 것을 보증하고 나머지는 기권합니다. VII부는 그 긴장이 근본적이지 않다는 건축적 내기로 문을 엽니다. 기호적 어텐션은 SATORI-lite 커널, 곧 그 가중치가 기호적 추론기에 의해 계산되는 어텐션 메커니즘을 지어서, 이 장이 바깥에서 측정했던 닫힘 성질들이 모델 안으로 옮겨가, 신경 성분이 무엇을 커버하도록 배우든 그 위에서 성립하게 만듭니다.

---

동반 코드: examples/frontier/entailment_gap.py는 4권의 커밋된 말뭉치로부터 네 가지 프로브 계열을 모두 생성하고, 두 시스템을 모두 측정하며, 파이프라인의 캐시된 닫힘을 SLD 증명기에 맞서 감사하고, 이 장에서 인용된 모든 숫자를 단언합니다; examples/frontier/difficulty_axes.py는 무관성 검증의 동기가 되는 반단조성 장치를 공급합니다. python3 examples/frontier/entailment_gap.py를 실행하십시오; 이 실행은 결정적이며 1분을 훌쩍 밑도는 시간 안에 끝납니다.