번역 후 증명: Logic-LM과 LINC

📍 현재 위치: 6부 · 자연어 추론 — 20장. 소프트 추론기가 측정 도구를 만들어, 통계적 독해기가 학습된 깊이를 넘어서면 우연 수준으로 붕괴하는 모습을 지켜보았습니다; 이 장은 같은 도구를 거꾸로 통과합니다: 영어를 논리로 한 번 번역한 다음, 정리에 의해 건전한 증명기가 모든 추론 단계를 수행하게 합니다.

지난 장의 소프트 추론기는 하나의 덩어리였습니다: 영어가 들어가고 판결이 나오며, 그 사이의 모든 단계는 통계적이었습니다. 깊이 2에서 실패했을 때, 그 안의 무엇도 어느 부분이 실패했는지 말할 수 없었는데, 부분이라는 것이 애초에 없었기 때문입니다. 이 장은 부분을 일부러 만들어 내는 아키텍처를 연구합니다. 번역 후 증명(translate-then-prove) 파이프라인은 과제를 하나의 자연스러운 이음매에서 쪼갭니다: 번역기(translator)가 영어를 형식 프로그램으로 사상하고, 기호 엔진(symbolic engine)이 그 프로그램으로부터 답을 도출합니다. 신경망이 인증할 수 없는 모든 성질(건전성, 완전성, 종료성)은 정리에 의해 그것들을 갖는 요소 하나에 집중되며, 언어 이해가 보장할 수 없는 모든 성질은 번역기에 집중되는데, 그곳에서는 적어도 그것을 측정하거나 수리하거나 거부할 수 있습니다. 발표된 두 시스템, Logic-LM과 LINC(신경-기호 계산을 통한 논리적 추론, Logical Inference via Neurosymbolic Computation)는 대규모 언어 모델(large language model, LLM)을 번역기로 삼아 이 아키텍처를 구현하며, 정확히 그 실패 이음매에서 서로 갈립니다: 번역이 통하지 않을 때 무엇을 할 것인가. 동반 모듈 translate_prove.py는 소프트 추론기가 채점되었던 바로 그 평가 집합 위에서, 데스크 규모로 두 답을 모두 재구성합니다.

쉽게 말하면

판사는 흠 없이 완벽하지만 라틴어만 읽는 법정을 상상해 보십시오. 당신은 영어로 소를 제기하고, 서기가 그것을 번역합니다. 서기의 라틴어가 당신의 영어가 말한 바와 같다면, 판결은 반드시 옳으므로, 법정의 모든 오류 예산은 서기의 책상 위에 놓입니다. 모든 사건은 셋 중 하나로 끝납니다: 서기가 번역하고 판사가 판결한다(항상 옳음); 서기가 어떤 단어에서 막혀 법정이 추측하는 대신 사건을 기각한다; 아니면, 최악의 경우, 서기가 유창한 라틴어를 만들어 내지만 그것이 조용히 다른 것을 말하고, 판사는 잘못된 사건에 대해 흠 없이 판결합니다. 막힘에 대한 두 가지 해법이 있습니다. 한 법정은 문제 단어에 메모를 붙여 서류를 돌려보내고 서기가 다시 시도하게 합니다: Logic-LM의 수리 루프입니다. 다른 법정은 서기 열 명을 고용해, 파싱에 실패한 번역들을 버리고, 남은 것들의 다수결로 판결합니다: LINC의 투표입니다. 어느 해법도 세 번째, 조용한 실패에는 손을 대지 못하며, 그 사실을 붙들고 있는 것이 이 장의 절반입니다.

이 장에서 다루는 내용

인수분해된 아키텍처: 번역기 → 형식 프로그램 → 엔진 → 판결, 1권에서 다시 불러온 엔진의 건전성·완전성·종료성, 그리고 사건별로 유도된 정확성 인수분해 $P(\text{correct}) = P(\text{parse}) \times 1$ (일반적으로는 하한이지만 여기서는 등식).
인용된 번역기: translate_prove.py 안의 통제된 영어에 대한 결정론적 문법, 그리고 고정된 닫힌 문법이 표본 추출되는 LLM 번역이 줄 수 없는, 파싱된 것에 대한 100퍼센트 보증을 사들이는 이유.
커밋된 인수분해 예증: 깊이별 커버리지, 파싱된 것에 대한 정확도(정확히 1.0000, 단언됨), 그리고 전체 정확도를, 동일한 1,500개 질문에서의 소프트 추론기의 열 옆에 두고, 교차점을 양방향으로 정직하게 읽기.
축소된 자기 정련: 동의어 정규화 수리 패스와 그것의 커밋된 커버리지 상승 0.8080 → 0.9293을, 실제 시스템의 오류 메시지 루프, 그것이 보고한 실행 가능 비율 상승, 그리고 수리는 구문을 고칠 뿐 의미를 고치는 일은 드물다는 정직한 한계 옆에 두기.
인터페이스 계약으로서의 기권: LINC의 오류-필터링 다수결 투표를 분해하고, 동반 모듈의 커밋된 무소음-오류 단언, 그리고 삼중 실패-모드 대비표.
실제 규모의 솔버 메뉴: 논리 프로그래밍, 일차 논리 증명기, 그리고 SMT(충족 가능성 모듈로 이론, satisfiability modulo theories)를 그 레이블의 의미에 따라 벤치마크에 짝지으며, 다음 장을 위해 명명된 삼중 참/거짓/불확실 프로토콜.
발표된 헤드라인 대비: 파이프라인이 사고 사슬(chain-of-thought)을 압도하는 지점과 퇴보하는 지점 모두를 인용하고, 둘 다 같은 인수분해로 설명하기.
미해결 부분: 의미 번역 오류는 수리와 투표 모두에게 보이지 않는데, 파이프라인 안의 어떤 것도 그 수식이 문장을 뜻하는지 확인하지 않기 때문입니다.

파이프라인, 이음매에서 인수분해하기

발표된 아키텍처는 세 단계로 이루어집니다: 문제 형식화(problem formulation, 언어 모델이 몇 개의 예시로 프롬프트되어 영어 맥락과 질문을 솔버의 형식 구문으로 된 프로그램으로 번역), 기호 추론(symbolic reasoning, 결정론적 솔버가 프로그램을 실행), 그리고 결과 해석(result interpretation, 솔버의 판결이 답 레이블로 다시 사상됨) [1]. LINC는 목표 언어로 일차 논리를, 엔진으로 분해 증명기(resolution prover)를 사용해 동일한 골격을 구체화합니다 [2]. 두 경우 모두 언어 모델은 어떤 추론도 하지 않습니다: 그것의 임무 전체는 표현이며, 다단계 연역은 솔버 안에서 일어납니다. 동반 파이프라인은 각 슬롯을 이미 우리 책상 위에 있는 것으로 채웁니다: 번역기는 결정론적 문법이고(다음 절), 엔진은 1권의 후방 연쇄기(backward chainer) sld.provable이며, 이는 앞 장이 만든 계층화된 닫힌 세계 컴파일러 ruletaker_lite.ground_program이 만들어 낸 접지 프로그램 위에서 실행됩니다(translate_prove.py 200–208행):

def prove_statement(theory: dict, person: str, pred: str, neg: bool) -> bool:
    """The symbolic stage, exactly as the docstring factors it: compile the
    parsed theory with ruletaker_lite.ground_program (the stratified
    closed-world compiler resolves negation-as-failure against the stated
    facts), then ask Volume 1's BACKWARD chainer.  A positive question is
    True iff provable; a negated question is its closed-world complement."""
    facts, rules = rt.ground_program(theory)
    provable = sld.provable(("is", person, pred), sorted(facts), rules)
    return (not provable) if neg else provable

이 엔진을 전적으로 신뢰할 수 있는 이유를 세 문장으로 되짚어 보면, 각 문장은 1권의 정리 하나씩을 담고 있습니다. 그것은 건전합니다(sound): 모든 SLD(선택적 선형 정형절, Selective Linear Definite-clause) 유도는 분해 단계들의 사슬이며, 각 단계는 모든 모델에서 참을 보존하므로, 발견된 증명은 결코 거짓을 주장할 수 없습니다(귀결과 SLD). 그것은 이 프로그램들 위에서 완전합니다(complete): 접지 원자가 함수 없는 정형절 프로그램으로부터 따라 나온다면 SLD 분해가 반박을 찾아내므로, "증명을 찾지 못함"은 진정으로 "함의되지 않음"을 의미하며, 이를 닫힌 세계 평가는 거짓으로 읽습니다(추론과 증명). 그리고 그것은 여기서 1권이 정확히 밝힌 정초된 하강(well-founded descent) 이유로 종료됩니다(terminates): 모든 규칙의 몸체 술어는 그 머리보다 코퍼스 어휘의 엄격히 더 낮은 층에 자리하므로, 재귀는 호출마다 감소하는 척도를 가지며 탐색은 순환할 수 없습니다(고정점이 순방향 버전을 제공합니다; 여기서는 층 색인이 1권에서 비순환 인용 사슬이 했던 역할을 합니다).

이제 인수분해를 봅시다. 평가 분포에서 뽑은 질문 하나를 고정하고, 세 가지 사건을 정의합니다. $A$ 를 파싱 사건(parse event)이라 하겠습니다: 맥락의 모든 문장과 질문 자체가 번역기에 의해 받아들여지는 사건입니다. $B$ 를 충실성 사건(faithfulness event)이라 하겠습니다: 파싱이 주어졌을 때, 형식 프로그램이 영어가 뜻한 바를 뜻하는 사건입니다. $C$ 를 엔진 사건(engine event)이라 하겠습니다: 충실한 프로그램이 주어졌을 때, 엔진의 판결이 프로그램의 의미론적 귀결과 같은 사건입니다. 세 가지가 모두 일어나면 파이프라인은 옳게 답합니다. $P(A)$ 는 사건 $A$ 의 확률로 읽고, $P(B \mid A)$ 는(세로줄은 "주어졌을 때"라고 읽습니다) $A$ 가 이미 일어났을 때 $B$ 가 일어날 확률로 읽으십시오. 세 가지가 모두 일어나는 경로는 얼마나 그럴듯할까요? 조건부 확률의 정의에 의해 $P(B \mid A) = P(A \text{ and } B)/P(A)$ 이므로, 양변에 $P(A)$ 를 곱하면 $P(A \text{ and } B) = P(A)\cdot P(B \mid A)$ 를 얻습니다; 같은 정의를 한 번 더, 이번에는 결합 사건( $A$ 와 $B$ )과 $C$ 의 쌍에 적용하면 $P(A \text{ and } B \text{ and } C) = P(A \text{ and } B)\cdot P(C \mid A, B) = P(A)\cdot P(B \mid A)\cdot P(C \mid A, B)$ 가 됩니다. 이 항등식이 확률의 연쇄 법칙(chain rule of probability)이며(각 인자는 그 앞의 사건들에 조건화됩니다), 세 사건을 모두 거치는 정답 경로가 정확도에 정확히 $P(A)\cdot P(B \mid A)\cdot P(C \mid A, B)$ 를 기여한다고 말해 줍니다. 일반적으로 이것은 등식이 아니라 하한(lower bound)입니다:

P(\text{correct}) \;\ge\; P(A)\;\cdot\;P(B \mid A)\;\cdot\;P(C \mid A, B),

정답에 이르는 경로가 하나 더 있기 때문입니다: 충실하지 않은(unfaithful) 프로그램(사건 $B$ 없이 사건 $A$ 만 있는 경우)도 여전히 파싱되고 실행되며, 그 판결이 순전한 우연으로 정답 레이블과 일치할 수 있습니다. (완전히 일반적으로는 두 번째 여분의 경로도 있습니다: 엔진이 오류를 내는 충실한 프로그램, 즉 사건 $\lnot C$ (읽는 법: $C$ 가 아님, 곧 엔진 사건이 실패함)가 그럼에도 운으로 정답 레이블에 떨어지는 경우입니다; 이는 아래에서 $P(C \mid A, B) = 1$ 이 확립되는 순간 사라집니다.) 이진 레이블 벤치마크에서 그 우연 항은 일반적으로 0이 아닙니다: 의미가 틀린 프로그램 가운데 대략 절반은 그래도 옳은 레이블에 떨어집니다. 우연 경로가 비어 있을 때, 특히 $P(\lnot B \mid A) = 0$ 일 때 등식이 성립하는데, 여기서 $\lnot B$ (읽는 법: $B$ 가 아님)는 파싱은 성공했지만 충실성은 실패한 사건입니다.

앞 단락은 $P(C \mid A, B) = 1$ 을 확립합니다: 건전성과 완전성은 판결을 함의와 같게 만들고, 종료성은 판결이 존재하게 만들며, 닫힌 세계 여집합은 부정 질문을 처리합니다. 이것은 바람이 아니라 정리로 뒷받침된 인자입니다. 따라서 하한은 다음이 됩니다

P(\text{correct}) \;\ge\; P(A)\cdot P(B \mid A),

그리고 전체 공학적 질문은 남은 두 인자로 귀결됩니다: 커버리지(coverage, $P(A)$ , 번역기가 받아들이는 언어의 양)와 충실성(faithfulness, $P(B \mid A)$ , 받아들인 것을 참되게 표현하는가). 동반 번역기의 경우 두 번째 인자는 정확히 $1$ 인데, 그 이유는 다음 절이 정확히 밝힙니다: 문법의 생산 규칙당 하나의 읽기라는 고정된 설계가 충실성 사건을 확실하게 만들기 때문입니다(결정론은 같은 입력이 같은 읽기를 얻는다는 것만을 보장합니다; 그 읽기가 바로 의미라는 것은 닫힌 문법이 더하는 부분입니다). 그러므로 $P(\lnot B \mid A) = 0$ 이고, 우연 경로는 비어 있습니다; 그리고 파싱 실패는 아래의 채점에서 오답으로 간주되는 기권으로 끝나므로, $\lnot A$ 를 통해서도 정답이 도달할 수 없으며, 그리하여 부등식은 논지가 약속했던 등식으로 닫힙니다:

P(\text{correct}) \;=\; P(\text{parse}) \times 1 .

엔진이 신뢰되고 나면, 종단간 정확도는 곧 파싱 정확도입니다. 소프트 추론기와 대조해 보십시오: 텍스트에서 레이블로 가는 하나의 미분화된 함수일 뿐, 조건화할 사건도 없고, 정리에 의해 $1$ 과 같은 인자도 없으며, 따로 인증할 수 있는 구성 요소도 없습니다. 그것의 깊이 1에서의 0.9659와 깊이 3에서의 0.5000은 전체에 대한 사실일 뿐, 더 많은 측정으로만 설명될 수 있습니다. 파이프라인의 오류는 구조상 모두 한곳에 살고 있으며, 아래의 커밋된 숫자들이 그것이 그곳에 살고 있음을 보여 줍니다.

아키텍처를 이음매에서 인수분해한 모습: 번역기만이 오류를 일으킬 수 있는 유일한 단계이고, 엔진의 인자는 1권의 정리에 의해 1로 고정되며, 발표된 두 가지 해법(수리, 기권)은 오직 파싱 인자에만 작용한다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

인용된 번역기: 추측 대신 문법

동반 모듈의 번역기는 코퍼스 생성기가 내놓는 통제된 영어에 대한 결정론적 문법으로, 사람과 술어에 대한 닫힌 어휘집을 갖습니다; 그 명세 전체가 주석 하나에 들어맞습니다(translate_prove.py 89–94행):

# The parse table.  Three sentence forms, each anchored on closed lexicons:
#   fact/question:  "<person> is [not] <predicate>."
#   rule:           "If someone is <cond> [and <cond>]* then they are <pred>."
#                    with <cond> = "[not] <predicate>"
# Anything else — one unknown token suffices — is a ParseError, never a
# guess.  Same input, same parse, every time: the determinism is the point.

문장 파서는 문법의 첫 번째 행을 실행 코드로 옮긴 것입니다(translate_prove.py 131–145행): 공백으로 나누고, 두 번째 위치에 is가 있기를 요구하며, 선택적인 not을 벗겨내고, 코퍼스 모듈의 이름과 술어 목록으로 만든 고정 어휘집 PERSONS와 PREDS에 대해 두 개의 열린 슬롯을 모두 검사합니다(translate_prove.py 96–97행):

def parse_statement(sentence: str) -> tuple[str, str, bool]:
    """'<person> is [not] <predicate>.' -> (person, predicate, negated).
    Raises ParseError (with the offending token) on anything else."""
    toks = _tokens(sentence)
    if len(toks) < 3 or toks[1] != "is":
        raise ParseError(f"not a statement shape: {sentence!r}")
    person, rest = toks[0], toks[2:]
    neg = rest[0] == "not"
    if neg:
        rest = rest[1:]
    if person not in PERSONS:
        raise ParseError(f"unknown person {person!r}")
    if len(rest) != 1 or rest[0] not in PREDS:
        raise ParseError(f"unknown predicate {' '.join(rest)!r}")
    return person, rest[0], neg

parse_rule은 규칙 템플릿에 대해 같은 일을 하고, parse_theory는 사실을 먼저, 규칙을 나중에 두어 맥락 전체를 사상합니다(148–185행). 두 가지 설계 성질이 모든 하중을 짊어집니다. 첫째, 번역기는 판결에서 완전합니다(total in its verdicts): 모든 입력은 파싱되거나, 자리를 찾지 못한 것(문제 토큰 또는 잘못된 형태)의 이름을 담은 ParseError를 일으키며, 중간 상태는 없습니다. 둘째, 그것은 결정론적이고 합성적입니다(deterministic and compositional): 같은 입력은 항상 같은 파싱을 낳고, 각 문법 생산 규칙은 정확히 하나의 형식적 읽기를 가지며, 이는 코드 안에 한 번 고정되어 있습니다. 따라서 앞 절의 인자 $P(B \mid A)$ 인 충실성은 구성에 의해 $1$ 입니다: 파싱되는 문장은 그 생산 규칙이 지닌 유일한 읽기로 표현되며, 그 읽기는 바로 그 문장의 의미가 되도록 작성되었습니다.

이것이야말로 언어 모델 번역기가 줄 수 없는 바로 그 보증이며, 이 구분은 슬로건이 아니라 신중한 문장을 받을 자격이 있습니다. LLM의 번역은 텍스트에 조건화된 프로그램에 대한 학습된 분포로부터의 표본입니다: 온도가 0이더라도(표본 추출 온도는 모델의 출력 분포를 넓히거나 좁히는 손잡이인데, 0에서는 가장 좁아져 모델이 항상 확률이 가장 높은 토큰 하나만 고릅니다) 그것은 문법의 유일한 읽기가 아니라 그 분포로부터의 탐욕적 추출, 즉 토큰별 argmax(각 단계에서 확률이 가장 높은 토큰)일 뿐이며, 분포 전체가 가장 그럴듯하다고 평가하는 프로그램(그 최빈값)이 나온다는 보장조차 없고, 표본 추출된 프로그램의 의미론을 문장의 의미론에 묶어 주는 것은 아무것도 없습니다. LLM 파이프라인의 경우, $P(B \mid A)$ 는 엄격히 $1$ 보다 작은 경험적 양입니다: 프로그램은 형식이 올바르고 실행 가능하면서도 영어가 말한 바에 대해 틀릴 수 있습니다. 이 장의 장난감과 실제 시스템 사이의 정직한 다리는 바로 여기에 있습니다: 우리 문법은 $P(B \mid A) = 1$ 을 참으로 만듦으로써 그것을 눈에 보이게 하고, 그래서 아키텍처에 관한 나머지 모든 것(인수분해, 수리, 기권, 교차)을 커밋된 숫자로 연구할 수 있게 합니다; 실제 시스템들은 사라지지 않는 의미 오류 항과 함께 같은 대수를 물려받습니다 [1].

여기 커밋된 코퍼스 위에서 한 번 실행되는 파이프라인 전체가 있습니다. 데모는 정답이 참인, 부정되지 않은 첫 번째 깊이-3 질문을 골라, 그것을 파싱하고, 맥락을 컴파일하며, 목표를 증명기에 건넵니다; 이는 python3 translate_prove.py의 실제 출력입니다:

[1] one worked pipeline pass: sentence -> program -> proof -> verdict
    question (as written):   'alice is influential.'
    parsed atom:             is(alice, influential)  negated=False
    SLD proof (Volume 1's backward chainer, on the compiled ground program):
         is(alice, influential)
           is(alice, senior)
             is(alice, visible)
               is(alice, cited)
             is(alice, cited)
    verdict: True   gold: True

증명 나무를 아래에서 위로 읽어 보십시오: cited는 진술된 사실이고, 규칙 하나가 그것을 visible로 끌어올리며, 다른 규칙이 (규칙의 두 번째 조건인) cited와 다시 함께 visible을 senior로 합성하고, 세 번째 규칙이 influential에 도달합니다. 이것이 바로 소프트 추론기가 0.5000에 머물렀던 깊이-3 합성이며, 세 번의 규칙 적용(사실 조회를 세면 다섯 번의 분해 단계)으로 실행되고 그 건전성은 정리입니다. 판결은 신뢰도가 아니라, 1권 이래로 sld.prove가 반환해 온 감사 가능한 증명 나무의 결론입니다(sld.py 63–75행).

커밋된 숫자로 본 인수분해

인수분해는 데이터와 맞닥뜨렸을 때도 살아남아야만 유도할 가치가 있으므로, 동반 모듈은 평가를 적대적으로 만들고 모든 인자를 측정합니다. 평가 집합은 새로운 것이 아닙니다: corrupted_corpus는 앞 장의 커밋된 분할을 그대로 임포트하므로, 두 아키텍처는 동일한 바탕 위에서 채점됩니다(translate_prove.py 240행):

    base = rt.run(verbose=False)              # the SAME split, deterministic

이는 소프트 추론기가 깊이별 열을 올렸던 바로 그 20개의 홀드아웃 이론과 1,500개의 질문입니다. 그 위에 하나의 씨앗 오염이 더해집니다: 술어에 "속어"(street name)가 있는 질문 문장 가운데 일부(SYN_FRAC = 0.35)가 엄격한 문법이 모르는 다섯 항목짜리 동의어 표를 통해 다시 쓰입니다(published는 printed가 되고, funded는 sponsored가, productive는 prolific이, cited는 referenced가, senior는 veteran이 됩니다; 112–118행). 이것은 모든 실제 파이프라인이 마주하는 간극, 즉 세상의 영어가 번역기의 영어보다 크다는 사실에 대한 데스크 규모의 대역입니다. 커밋된 실행에서는 1,500개 질문 가운데 288개가 다시 쓰입니다. 각 질문은 그런 다음 pipeline_answer(211–228행)를 통과하는데, 이는 아키텍처 전체를 한 화면에 담습니다:

def pipeline_answer(theory_sentences: list[str], question: str,
                    use_repair: bool) -> bool | None:
    """The whole translate-then-prove pipeline for one question.  Returns
    True/False, or None — the LINC-style Error/abstention — whenever any
    sentence fails the grammar (after the repair round, if enabled).
    Nothing here ever guesses: parse or be silent."""
    try:
        theory = parse_theory(theory_sentences)
        person, pred, neg = parse_statement(question)
    except ParseError:
        if not use_repair:
            return None
        try:
            theory = parse_theory([repair(s) for s in theory_sentences])
            person, pred, neg = parse_statement(repair(question))
        except ParseError:
            return None                      # abstain: visibly, not wrongly
    return prove_statement(theory, person, pred, neg)

채점은 가능한 한 가장 가혹합니다: 기권은 오답으로 간주되어, overall 열에서 어떤 부분 점수도 얻지 못하므로, 파이프라인은 어려운 모든 것을 거부함으로써 좋아 보일 수 없습니다. 다음은 수리가 활성화된 상태의 커밋된 깊이별 표로, 바로 같은 질문들에 대한 소프트 추론기의 정확도와 나란히 놓입니다(열 n은 각 깊이의 평가 질문 수를 셉니다; 실행의 [3]절, 실제 출력):

[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

acc-on-parsed 열은 인수분해를 눈에 보이게 만든 것입니다: 모든 깊이에서 정확히 $1.0000$ 이며, 이는 운 좋은 우연이 아니라 커밋된 단언으로, 수리 전후 매 실행마다 다시 확인됩니다; 파싱된 질문이 단 하나라도 정답과 어긋나게 답해지면 모듈은 실패합니다(translate_prove.py 298–301행):

    for tab in (before, after):
        for d, row in tab.items():
            assert row["acc_on_parsed"] == 1.0, \
                f"pipeline wrong on a parsed depth-{d} question ({row})"

그러므로 overall 열의 모든 숫자는 문자 그대로 coverage × 1.0이며, 모든 종단간 오류는 커버리지 오류입니다. 표의 모양조차 동의어 어휘집으로 설명됩니다: 깊이-3 질문은 속어가 없는 유일한 술어인 influential을 묻기 때문에 커버리지가 정확히 $1.0000$ 입니다; 깊이-1 질문은 productive 또는 visible을 묻는데, 오염될 수 있는 유일한 것(prolific)은 수리 가능하므로 수리 후 커버리지는 $1.0000$ 으로 돌아갑니다; 깊이 0과 2는 기권이 남는데, referenced와 veteran이 수리 어휘집이 일부러 모르는 두 동의어이기 때문입니다.

이제 교차점을 양방향으로 정직하게 읽어 봅시다. 깊이 0에서는 소프트 추론기가 1.0000 대 0.9266으로 이깁니다: 이것들은 답이 진술된 사실에서 곧바로 읽히는 질문들이고, 그것은 자신의 학습 분포이며, 소프트 추론기는 항상 답하는 반면 파이프라인은 수리되지 않은 모든 동의어에서 침묵합니다. 항상-답하기는 항상-답하는 쪽의 정확도가 정확한 시스템의 커버리지를 넘어서는 곳이면 어디서나 정확하지만-침묵하는 쪽을 이기며, 이 조건 $P_{\text{soft}}(\text{correct}) \gt P(\text{parse}) \times 1$ 은 깊이 0에서 $1.0000 \gt 0.9266$ 으로 구체화됩니다. 이미 깊이 1에서 부등식은 뒤집혀 $1.0000$ 대 $0.9659$ 가 되는데, 그곳에서는 수리가 이미 완전한 커버리지를 회복시켰기 때문입니다; 깊이 2와 3에서는 부등식이 격렬하게 뒤집힙니다: $0.8321$ 과 $1.0000$ 이 동전 던지기인 $0.5000$ 을 이기는데, 합성은 엔진의 안마당이고 아무리 항상 답해도 우연 수준으로 답하는 것을 보상할 수 없기 때문입니다. 질문 수로 가중하면, 총계는 파이프라인이 $0.9293$ , 소프트 추론기가 $0.8773$ 으로 나옵니다. 어느 숫자도 모든 깊이에서 압도하지 않습니다; 아키텍처 질문은 어떤 실패 프로파일을 배치가 감당할 수 있는가이며, 우승자를 선언하는 것이 아니라 그런 틀 짓기가 바로 커밋된 표가 가르치는 바입니다.

축소된 자기 정련: 파싱을 수리하고, 다시 시도하기

Logic-LM을 정의하는 견고성 메커니즘은 커버리지 인자를 직접 공략합니다. 솔버가 생성된 프로그램을 거부하면, 시스템은 오류가 있는 프로그램과 솔버 자체의 오류 메시지, 그리고 흔한 오류-수정 쌍의 시연을 함께 번역기에 다시 프롬프트하고, 이를 재시도하는데, 보고된 실험에서는 최대 세 라운드까지입니다 [1]. 이 루프의 효과는 실행 가능 비율(executable rate), 즉 프로그램이 어쨌든 실행되는 문제의 비율로 측정되며, GPT-3.5 백본에서 보고된 상승 폭은 상당합니다: FOLIO에서는 66.7에서 84.3퍼센트로; ProofWriter 부분집합에서는 87.3에서 95.6으로; 형식화하기 가장 어려운 목표인 AR-LSAT(로스쿨 입학시험, Law School Admission Test의 분석 추론 영역)에서는 11.3에서 겨우 21.8로 오르는데, 이는 수리가 애초에 가깝지도 않았던 커버리지를 마술처럼 불러낼 수는 없다는 것을 일깨워 줍니다 [1].

동반 모듈은 이 루프를 하나의 결정론적 라운드로 축소합니다: 알려진 문법 밖 동의어를 문법의 어휘로 다시 사상하는 정규화 어휘집으로, 수리 불가능한 나머지가 눈에 보이게 남도록 일부러 부분적입니다(translate_prove.py 103–107행 및 188–194행):

REPAIR_LEXICON: dict[str, str] = {
    "prolific": "productive",
    "sponsored": "funded",
    "printed": "published",
}

def repair(sentence: str) -> str:
    """The one-round self-refinement pass: normalize every token the repair
    lexicon knows, then hand the sentence back to the SAME strict parser.
    Deterministic, like everything else here (Logic-LM re-prompts an LLM
    with the solver's error message; the shape — error, rewrite, retry — is
    what this keeps)."""
    return " ".join(REPAIR_LEXICON.get(t, t) for t in sentence[:-1].split(" ")) + "."

그 모양은 발표된 루프의 모양과 같습니다: 기호 쪽에서 나온 실패 신호(여기서는 문제 토큰의 이름을 담은 ParseError, 저기서는 솔버의 오류 메시지)가 번역 쪽으로 되돌아가고, 번역 쪽은 다시 쓴 다음 같은 엄격한 검사기에 재제출합니다. 데모는 수리 하나가 성공하고 하나가 실패하는 모습을 그대로 보여 줍니다:

    the self-refinement round, where the strict grammar fails first:
    question (as written):   'bob is printed.'
    strict parse:            ParseError: unknown predicate 'printed'
    repair pass:             'bob is published.'  -> parses, proves, answers
    question (as written):   'alice is not referenced.'
    strict parse + repair:   ParseError both -> Error (abstain, stay silent)

그리고 커밋된 전/후 커버리지 표는 발표된 실행 가능 비율 표와 정확히 같은 모양을 가집니다:

[2] the parse-rate table: coverage before vs after the repair pass
    288 of 1500 eval questions were rewritten through 5 synonyms;
    the repair lexicon knows 3 of them (deliberately partial).
      pass            coverage
      strict only     0.8080
      + repair        0.9293   (strictly higher, asserted; Logic-LM's Table-3 shape)

그 상승의 양방향 모두가 단순히 출력되는 것이 아니라 단언됩니다: 하니스는 cov_after > cov_before(수리가 실제로 무언가를 회복했음)와 cov_after < 1.0(수리 불가능한 동의어들이 소리 없이 사라지지 않았음) 둘 다를 요구합니다(translate_prove.py 313–316행). 정직한 한계 하나가 함께 따라오는데, 발표된 절제 실험(ablation)도 이를 명시적으로 밝힙니다: 솔버 오류가 이끄는 정련은 구문(syntax)을 고칠 뿐, 의미론을 고치는 일은 드뭅니다. 실행 가능 비율은 라운드를 더할수록 계속 오르지만, 정확도는 발표된 절제 실험에서 첫 한두 라운드 이후로 정체되어 금세 고원에 도달하는데, 의미상으로는 틀렸지만 구문상으로는 멀쩡한 프로그램은 수리를 불러올 오류 메시지를 결코 촉발하지 않기 때문입니다 [1]. 우리의 축소판은 구성에 의해 같은 경계를 보여 줍니다: repair는 파서가 이미 거부한 문장에만 작용하므로, 잘못된 의미로 파싱된 문장(여기서는 불가능하지만, LLM에게는 얼마든지 가능함이 보장됩니다)은 그것을 그냥 지나쳐 버릴 것입니다.

인터페이스 계약으로서의 기권

실패 이음매에 대한 LINC의 답은 다릅니다: 수리하지 말고, 다양화하고 걸러내라는 것입니다. 번역기는 온도 0.8(번역기 절에서 풀이한 그 표본 추출 손잡이를 여기서는 넓게 열어 열 번의 추출이 서로 달라지게 만든 값)에서 같은 문제에 대한 후보 번역 $K = 10$ 개를 표집합니다; 각각은 증명기에 건네집니다; 파싱에 실패하거나 증명기를 충돌시키는 후보는 무엇이든 Error로 표시되어 투표에서 제외됩니다; 답은 생존자 가운데 다수결 레이블입니다; 그리고 $K$ 개 후보 모두가 오류를 내면, 그 예시는 추측되는 대신 오답으로 채점됩니다 [2]. 파싱 실패는 있는 그대로, 즉 답이 아닌 것으로 취급됩니다. 동반 모듈의 번역기는 결정론적이므로, 그것을 $K$ 번 표집해도 $K$ 개의 동일한 파싱이 나올 뿐입니다; 그것의 오류 필터 버전은 퇴화한 $K = 1$ 경우, 즉 명시적 기권(explicit abstention)입니다: 문법 밖 문장은 None을 산출하고, 파이프라인은 침묵을 지키며, 어떤 대체 답도 만들어 내지 않습니다. 이것을 하나의 행동에서 인터페이스 계약으로 끌어올리는 것은 동반 모듈이 질문 하나하나에 대해 그것을 단언한다는 사실입니다(translate_prove.py 305–309행):

    for q in eval_qs:
        v = pipeline_answer(theories[q["theory"]]["sentences"], q["text"],
                            use_repair=True)
        assert v is None or v == q["gold"], \
            f"a silent wrong answer slipped through on {q['text']!r}"

1,500개 질문 모두가 다시 실행되고 검사됩니다: 출력은 정답이거나 기권이며, 결코 소리 없는 오답이 아닙니다. 실행의 마지막 표는 그 보증이 사들이는 대비를 인쇄합니다:

[4] the failure-mode contrast (same evaluation set)
      system                       answers      silent errors      overall acc
      soft reasoner (always)       100.0%       yes (quietly wrong)   0.8773
      translate-then-prove         92.9%        never (asserted)     0.9293

이제 세 가지 설계가 같은 이음매에서 세 가지 계약으로 나란히 놓이며, 실패-양식 열이 정확도 열보다 더 중요합니다:

설계	파싱 실패 시	소리 없이 틀릴 수 있는가?	누가 실패를 소비하는가
소프트 추론기(단일 덩어리)	그런 사건 자체가 존재하지 않음; 항상 답함	그렇다, 보이지 않게 그리고 자신 있게	아무도 없음: 오류는 오직 정답 레이블에 맞서서만 드러남
Logic-LM 방식(수리한 다음 답하거나 대체)	오류를 되먹여 최대 3라운드까지 재시도; 그래도 고장 나 있으면 기본 답으로 대체함	그렇다, 대체 답과 의미상 틀린 프로그램을 통해	번역기가 오류 메시지를 소비함; 대체 답이 잔여물을 감춤 [1]
LINC 방식(투표하거나 기권)	오류가 난 표본을 투표에서 제외함; 전부 오류면 답 없음, 오답으로 채점됨	파싱 실패를 통해서는 아님(걸러짐), 하지만 충실해 보이는 오역을 통해서는 그렇다	투표가 그것을 소비함; 기권은 하류에서 눈에 보임 [2]

가운데 열의 비대칭에 주목하십시오: 두 해법 모두 소리 내어 나는 실패(실행되지 않는 프로그램)는 막지만, 어느 쪽도 조용한 실패(실행되면서 거짓말하는 프로그램)는 막지 못합니다. 그 비대칭이 미해결 부분의 주제입니다.

실제 규모의 솔버 메뉴

데스크 규모에서는 엔진 하나로 충분했습니다. 벤치마크 규모에서는 엔진을 골라야 하며, 원칙은 하나입니다: 엔진의 의미론을 벤치마크 레이블의 의미론에 맞추라는 것입니다. Logic-LM은 가장 명료한 발표된 예시인데, 하나의 보편 논리 대신 데이터셋별 솔버 표를 갖추고 있기 때문입니다 [1]:

벤치마크	레이블 공간	형식화	엔진
PrOntoQA	참 / 거짓	논리 프로그램(Horn 사실과 규칙)	Pyke, 논리 프로그래밍 엔진: 닫힌 세계 부정 아래에서의 연쇄
ProofWriter(열린 세계 가정, open-world assumption, OWA, 부분집합)	증명됨 / 반증됨 / 알 수 없음	명시적 진리값 인자를 가진 논리 프로그램	Pyke; 어떤 값도 바인딩하지 않는 질의가 알 수 없음 레이블을 회복함
FOLIO	참 / 거짓 / 불확실	일차 논리	Prover9, 분해 정리 증명기(resolution theorem prover): 열린 세계 함의
LogicalDeduction	다지선다(위치 단서 아래에서 객체 목록을 정렬)	제약 충족 문제	python-constraint: 유한 정의역 위에서 충족 대입 탐색
AR-LSAT	5지선다	SMT 명세	Z3: 제약 집합 아래에서 선택지별 충족 가능성

이 행들을 도구가 아니라 의미론으로 읽으십시오. 닫힌 세계 연쇄 엔진은 진술된 것으로부터의 증명 가능성을 결정하는데, 이는 거짓이 문자 그대로 "유도 불가능"을 뜻하는 코퍼스(우리 것과 PrOntoQA의 것)에 알맞은 의미입니다. 열린 세계 증명기는 함의(entailment)를 결정하며, 그 고유한 판결은 삼항입니다: 목표를 증명하면 참으로 답하고, 목표의 부정을 증명하면 거짓으로 답하며, 어느 쪽도 증명하지 못하면 불확실로 답합니다. 그 이중-질의 프로토콜이야말로 LINC가 두 결과짜리 증명기를 FOLIO와 열린 세계 ProofWriter가 요구하는 삼항 레이블 공간으로 바꾸는 방법이며 [2], 다음 장은 이를 일급 객체로 다룹니다. 답이 함의가 아니라 구성(configuration)인 퍼즐 벤치마크의 경우, 자연스러운 형식주의는 선언적 제약입니다: SatLM은 그 변형을 방법 전체로 삼아, 모델이 선언적 명세를 산출하도록 프롬프트하고 이를 SMT 솔버에 건네므로, 번역기는 반드시 참이어야 하는 것을 적어 내려가고 솔버는 그것을 충족하는 것을 탐색합니다 [3]. 아키텍처 공간은 심지어 이 장의 파이프라인을 뒤집은 것도 담고 있습니다: LAMBADA는 제어 흐름을 기호적으로 유지해, 목표로부터의 후방-연쇄 루프로 삼고, 각 단계 안에서 언어 모델을 추론의 기본 연산으로 사용합니다 [4]. 메뉴 전체에 걸쳐 하나의 불변량이 유지됩니다: 어떤 엔진이 그 슬롯을 채우든, 그 판결은 파이프라인보다 수십 년 앞선 보증으로 뒷받침되며, 표 안의 분해 증명기들에게 그것은 원조, 즉 분해 원리 자체의 건전성과 완전성으로, 1권의 스무 줄짜리 단일화기 위에 지어진 후방 연쇄기가 물려받는 것과 같은 정리입니다 [5].

파이프라인이 이기는 곳, 그리고 지는 곳

인수분해를 통해 읽으면, 발표된 헤드라인 숫자들은 더 이상 점수판이 아니라 진단이 됩니다. 파이프라인의 안마당은 번역기가 감당할 수 있는 언어에 대한 깊은 다단계 연역입니다. 우리의 깊이별 층화 표가 정확히 짚어 내는 영역인 ProofWriter 열린 세계 깊이-5 부분집합에서, Logic-LM은 같은 최강 백본 아래에서 사고 사슬(chain-of-thought, CoT) 프롬프팅의 68.11퍼센트에 맞서 79.66퍼센트를 보고하며, 더 약한 GPT-3.5 백본 아래에서는 48.33에 맞서 71.45를 보고하는데, 그 격차는 요구되는 깊이가 커질수록 벌어지는데, 연역이 깊이에 따라 저하되지 않는 엔진에 위임되기 때문입니다 [1]. LINC의 버전은 더 극명합니다: 균형 잡힌 열린 세계 ProofWriter 부분집합에서, 최강 백본은 사고 사슬의 72.2에 맞서 증명기와 함께 98.3점을 얻고, 155억 매개변수짜리 오픈 모델이 증명기와 함께(82.5) 자유 텍스트로 추론하는 최강 백본(72.2)을 이기는데, 이는 표현에 건전한 엔진을 더하면 연역에서 순전한 모델 규모를 능가할 수 있다는 가장 깔끔한 발표된 진술입니다 [2].

패배 또한 그만큼 시사하는 바가 큰데, 그것들이 추론의 패배가 아니라 커버리지와 충실성의 패배이기 때문입니다. 전제가 템플릿 문장이 아니라 사람이 쓴 영어인 FOLIO에서는, 최강 백본의 사고 사슬(75.3)이 같은 백본의 증명기 파이프라인(72.5)을 근소하게 앞서는데, 그 격차는 통계적으로 유의하지 않다고 보고됩니다: 언어가 번역기를 앞지르고, 엔진의 정확함으로는 번역이 잃은 것을 다시 사들일 수 없습니다 [2]. Logic-LM은 PrOntoQA에서 같은 역전을 보여 주는데, 그곳에서는 최강 백본의 사고 사슬이 이미 98.79에 도달해 있어서, 형식화 단계를 강제하면 15점을 잃습니다(83.20): 종단간 통계적 경로가 거의 완벽할 때, 번역 이음매는 순전히 추가된 위험일 뿐입니다 [1]. 두 퇴보 모두 다시 한번 인수분해이며, 이번에는 결정 규칙으로서입니다. 파이프라인은 적어도 다음일 때 이깁니다

P(\text{parse}) \cdot P(\text{faithful} \mid \text{parse}) \;\gt\; P_{\text{CoT}}(\text{correct}),

즉, 번역기가 내놓는 것에 엔진의 인자 $1$ 을 곱한 값이, 단일 덩어리의 인수분해되지 않은 숫자 하나에 맞선다는 뜻입니다. 이것은 정확한 기준이 아니라 충분 조건인데, 좌변은 파이프라인 정확도의 하한일 뿐이며, 운 좋은 불충실 프로그램이 거기에 더해질 수 있기 때문입니다. 깊은 합성은 우변을 낮추고 좌변은 그대로 두며; 어렵고 열린 영어는 좌변을 낮추고 우변은 그대로 둡니다. 우리의 커밋된 표는 데스크 규모에서의 바로 이 부등식이며, 교차점은 깊이 0과 깊이 1 사이에 놓여 있습니다.

아직 풀리지 않은 부분

발표된 두 해법 모두 같은 방아쇠에서 작동합니다: 눈에 보이는 실패입니다. 수리는 솔버가 오류를 낼 때 발동하고, 투표 필터는 표본이 파싱에 실패할 때 발동합니다. 어느 쪽도 가장 중요한 실패, 즉 파싱되고 실행되면서 잘못된 것을 뜻하는 번역에서는 발동할 수 없습니다. 뒤집힌 한정사, 반전된 조건문, 근접 동의어와 소리 없이 병합된 술어: 그 결과 프로그램은 구문적으로 흠이 없고, 솔버는 완벽한 건전성으로 그 귀결을 도출하며, 파이프라인은 유효한 증명을 두른 채 자신 있게 오답을 반환합니다. 인수분해에서 이것은 $P(\text{faithful} \mid \text{parse})$ 항이며, 불편한 사실은 파이프라인 안의 그 무엇도 그것을 측정하지 않는다는 것입니다. 엔진은 프로그램을 프로그램에 대해 검사할 뿐, 결코 프로그램을 문장에 대해 검사하지 않습니다. 수리는 도움이 될 수 없는데, 오류 메시지가 없기 때문입니다; 투표는 오역들이 서로 상관되어 있지 않을 때만 도움이 되며, 어떤 구문을 체계적으로 잘못 읽는 번역기는 $K$ 개의 표본 모두에서 그것을 잘못 읽습니다. 형식화 충실성에는 오라클이 없습니다: 파이프라인의 어떤 구성 요소도 수식이 영어 문장을 뜻하는지 결정할 수 없으며, 첫 번째 번역기를 검사하기 위해 채용된 두 번째 번역기는 자기 자신에 대해서도 같은 질문에 부딪힐 것입니다. 우리의 동반 모듈은 그 항을 구성에 의해 $1$ 과 같게 만들었는데, 바로 그 때문에 다른 모든 것을 깔끔하게 예증할 수 있었던 것이며, 이는 정확히 개방 어휘 번역기가 결코 할 수 없는 일입니다. 이 문제는 가상의 것도 아닙니다: 다음 장은 전문 주석자가 작성한 벤치마크의 골드 번역조차, 발표된 프로토콜이 자신의 레이블을 신뢰하기 전에 실패한 것들을 수리해야 했을 만큼 충분히 자주 증명기-루프-내 자가 점검에 실패한다는 것을 보여 줍니다.

왜 중요한가

번역 후 증명은 이 권에서 그 앞의 모든 것과 정반대의 모퉁이를 취합니다: 앞선 장들은 경사가 논리를 관통해 흐를 수 있도록 논리를 미분 가능하게 만들었지만, 이 장은 논리를 또렷하게 그대로 두고 모든 학습을 언어가 프로그램이 되는 경계로 옮깁니다. 그 보상은 이 권에서 가장 강한 정확성 진술, 즉 경계를 넘어서면 문자 그대로 $1$ 인 정확함의 인자이며; 그 대가는 측정되지 않은 양(충실성)에 눈에 보이는 거부 양식(기권)을 더한 것입니다. 5권을 위해, 이 장은 살아 있는 배치 질문을 커밋된 숫자로 넘겨줍니다: 같은 1,500개 질문에서, 한 시스템은 항상 답하며 12.3퍼센트의 시간 동안 조용히 틀리고, 다른 시스템은 92.9퍼센트의 시간 동안 답하며 단언에 의해 결코 소리 없이 틀리지 않습니다. 병원이나 법원, 또는 자율 실험실이 어떤 계약을 감당할 수 있는가는 벤치마크의 질문이 아니며, 보정과 기권과 검증기-게이트 생성을 다루는 5권의 장들이 이를 곧바로 물려받습니다. 두 기둥이 고리를 닫습니다: 엔진 쪽 절반은 1부가 기호 시스템이 할 수 있다고 약속한 것(자신의 언어 안에서 증명 가능하게 옳은 것)을 해내는 1권의 증명기이고, 번역기 쪽 절반은 3권의 교훈을 다시 진술한 것입니다(학습된 표현은 커버리지를 사들이고 그 대가는 보증으로 치릅니다). 파이프라인은 그 트레이드오프를 해소하지 않습니다; 그것에 값을 매길 뿐입니다.

핵심 용어

번역 후 증명(Translate-then-prove): 번역기가 자연어를 형식 프로그램으로 사상하고 기호 엔진이 답을 도출하는 아키텍처로, 모든 오류 가능성을 번역 단계 하나에 집중시킵니다.
정확성 인수분해(Correctness factorization): $P(\text{correct}) \ge P(\text{parse}) \cdot P(\text{faithful} \mid \text{parse}) \cdot 1$ 이며, 엔진 인자는 건전성·완전성·종료성으로 고정됩니다; 충실성이 확실할 때는 등식이 되는데, 그때는 어떤 불충실한 프로그램도 운으로 옳게 답할 수 없기 때문입니다.
커버리지(Coverage): 번역기가 입력을 받아들일 확률 $P(\text{parse})$ 입니다; 동반 모듈에서는 종단간 오류의 유일한 원천으로, 수리에 의해 0.8080에서 0.9293으로 상승합니다.
실행 가능 비율(Executable rate): 커버리지의 발표된 유사물로, 생성된 프로그램이 솔버 오류 없이 실행되는 문제의 비율입니다; 자기 정련은 이를 끌어올리지만(FOLIO 66.7 → 84.3) 정확도를 그에 비견될 만큼 끌어올리지는 못합니다.
자기 정련(Self-refinement): 솔버의 오류 메시지를 한정된 횟수의 수리 라운드 동안 번역기에 되먹이는 것입니다; 구문은 고치지만 의미론을 고치는 일은 드뭅니다.
오류-필터링 다수결 투표(Error-filtered majority vote): $K$ 개의 번역을 표집해, 파싱되지 않는 것들을 버리고, 생존자들의 다수결로 답하며, 전부 오류인 경우는 오답으로 셉니다.
기권(Abstention): 살아남는 번역이 하나도 없을 때 파이프라인이 명시적으로 답을 거부하는 것입니다; 동반 모듈의 단언은 기권이 결코 소리 없는 오답이 되지 않음을 인증합니다.
이중-질의 삼항 프로토콜(Dual-query three-way protocol): 증명기에게 목표와 그 부정을 모두 묻습니다; 앞의 것이 증명되면 참, 뒤의 것이 증명되면 거짓, 둘 다 아니면 불확실입니다.
의미 번역 오류(Semantic translation error): 파싱되고 실행되지만 원문 문장을 뜻하지는 않는 번역입니다; 수리와 투표 모두에게 보이지 않으며, $P(\text{faithful} \mid \text{parse})$ 에 오라클이 없는 이유입니다.

이 장이 이어지는 곳

이 장은 우리가 직접 생성한 코퍼스 위에서 두 아키텍처를 채점했는데, 그곳에서는 증명기가 골드 레이블을 작성해 주었으므로 레이블이 공짜였습니다. 이 분야의 실제 평가는 누군가가 구성하고, 균형을 맞추고, 검증해야 했던 레이블을 가진 벤치마크에 의존합니다. 다음 장 자연어 추론 벤치마크는 그 계측 도구 자체를 분해합니다: 생성된 코퍼스가 어떻게 깊이를 통제하는지, FOLIO의 사람이 쓴 전제가 레이블 신뢰성에서 어떤 대가를 치르는지(골드 번역조차 필요로 하는 증명기-루프-내 자가 점검을 포함해서), 그리고 불확실이 의미 있는 답이 되기 전에 삼항 프로토콜이 벤치마크에 무엇을 요구하는지입니다.

컴패니언 코드: examples/integration/translate_prove.py는 파이프라인 전체를 구현합니다: 문법과 어휘집(89–145행), 이론 파서와 수리 패스(148–194행), 1권의 후방 연쇄기 위에서의 증명 단계(200–208행), 기권(211–228행), 소프트 추론기의 커밋된 분할에서 임포트한 오염된 코퍼스(235–254행), 그리고 인수분해와 무소음-오류 계약과 커버리지 상승을 지키는 단언들(281–316행)입니다. 이 장의 모든 숫자를 바이트 단위까지 재현하려면 python3 examples/integration/translate_prove.py를 실행하십시오; 그 실행은 다음으로 끝납니다 SUMMARY translate_prove: corrupted=288/1500 coverage=0.8080->0.9293 acc_on_parsed=1.0000 overall=0.9293.

이 장에서 다루는 내용​

파이프라인, 이음매에서 인수분해하기​

인용된 번역기: 추측 대신 문법​

커밋된 숫자로 본 인수분해​

축소된 자기 정련: 파싱을 수리하고, 다시 시도하기​

인터페이스 계약으로서의 기권​

실제 규모의 솔버 메뉴​

파이프라인이 이기는 곳, 그리고 지는 곳​

아직 풀리지 않은 부분​

왜 중요한가​

핵심 용어​

이 장이 이어지는 곳​