본문으로 건너뛰기

머리말 — 논리와 경사하강의 결혼

📍 Where we are: 4권 — 뉴로-심볼릭 통합의 문 앞에서. 3권은 짝을 이루는 두 가지 실패로 마무리되었습니다: 기하학은 적혀 있지 않은 모든 사실의 순위를 매기지만 아무것도 보장할 수 없고, 2권의 논리는 스스로 말하는 모든 것을 보장하지만 배울 수 없습니다. 이 권은 두 기둥이 더 이상 거래만 하지 않고 합주를 시작하는 곳입니다: 같은 학계 세계가 네 번째로 다시 읽히며, 이번에는 증명이 도함수를 갖는 곳으로서 말입니다.

프론티어를 앞둔 마지막 한 번, 다시 오신 것을 환영합니다. 2권은 모든 답이 정리인 추론기를 지었고, 3권은 모든 답이 순위인 임베딩을 지었습니다. 둘 다 결국 자기 자신의 상처를 측정하는 것으로 끝을 맺었습니다: 아무도 적어 두지 않은 사실을 물으면 추론기는 "표시된 바 없음"이라 답하고 멈춰 버리며, 보장을 요구받은 임베딩은 내놓을 것이 아무것도 없고, 그 훈련 안에는 자신이 어기고 있는 그 제약을 표상(represents)하는 것조차 없습니다. 서로를 보완하는 두 실패는 하나의 설계 과제이며, 이 권은 바로 그 과제를 수행합니다. 일곱 벌의 옷을 갈아입으며 반복되는 이 권의 단 하나의 기술적 조치는, 1권과 2권의 이산적 기계 장치(진리값, 논리곱, 증명, 모델 수, 규칙, 질의)를 가져다 그 각 조각을 미분 가능한(differentiable) 무언가로 다시 표현하는 것입니다: 신경망 출력의 작은 변화가 논리적 결론의 진리치에 작고 계산 가능한 변화를 만들어 내야 하며, 그리하여 경사 하강법이 논리 그 자체를 통과해 흐를 수 있어야 합니다.

쉽게 말하면

2권의 사서와 3권의 서점 주인이 마침내 동업을 시작한다고 상상해 보십시오. 그녀에게는 목록이 있습니다: 모든 카드가 정확하고, 모든 미지의 물음에는 담백한 "표시된 바 없음"으로 답합니다. 그에게는 현장 감각이 있습니다: 카드는 하나도 없지만, 무엇을 건네주어도 그는 아마 맞는 서가로 걸어갈 것입니다. 그들의 가게는 계약으로 돌아가며, 이 권의 각 부는 그 계약 하나하나입니다. 어떤 때는 그녀가 규칙을 정하고, 그의 진열이 그 규칙을 어길 때마다 그가 벌금을 냅니다(논리를 어긴 데 대한 손실입니다). 어떤 때는 그가 그녀의 서재 안에 책상 하나를 차지하고 앉아, 그녀는 해독하지 못하는 얼룩진 라벨을 읽어 주는 동안 그녀는 정리를 계속합니다(증명기 안에 들어앉은 신경 술어입니다). 어떤 때는 그들이 주장에 참 또는 거짓이라는 도장을 찍는 대신 정도에 따라 점수를 매기고(퍼지 진리), 어떤 때는 그녀가 가게가 취할 수 있는 모든 가능한 상태 하나하나에 한꺼번에 가격을 매깁니다(세계에 대한 확률). 이 권은 바로 그 깨알 같은 약관입니다: 계약 하나하나가 무엇을 대가로 치르는지, 무엇을 보장하는지, 그리고 그가 실제로 거기서 배울 수 있도록 벌금이 어떻게 계산되는지 말입니다.

이 권이 다루는 내용

4권은 진리를 하나의 숫자로 다시 정의하는 일에서 시작해 이 사업 전체를 심판하는 데까지 이르는, 일곱 부로 이루어진 하나의 연속된 오름길입니다. 각 부는 하나의 질문에 답합니다:

주제답하는 질문
1부 · 퍼지·다치 논리K3와 Ł3; t-노름과 t-코노름; 소프트민과 경사진리가 [0, 1] 안의 숫자가 될 때 논리에는 무슨 일이 일어나며, 그 경사는 어떤 모습인가?
2부 · 확률 논리와 회로분포 의미론; 가중 모델 계수; d-DNNF 회로; DeepProbLog도출된 사실에 어떻게 올바른 확률을 매기며, 그 비용은 어떻게 감당하는가?
3부 · 미분 가능 프레임워크의미 손실; Scallop의 유래; 논리 텐서 네트워크; KLay와 Lobster두 경로는 어떻게 계층, 엔진, GPU 커널로 산업화되는가?
4부 · 미분 가능 규칙 학습Neural-LP와 DRUM; NTP와 CTP; RNNLogic과 AnyBURL경사 하강법은 규칙을 적용하는 데 그치지 않고 규칙 그 자체를 발견할 수 있는가?
5부 · 복합 논리 질의 응답계산 DAG; GQE, Query2Box, BetaE; CQD, GNN-QE, QTO; LMPNN, ULTRA임베딩은 한정사, 논리곱, 부정이 있는 논리 질의 전체에 답할 수 있는가?
6부 · 자연어 추론RuleTaker와 ProofWriter; Logic-LM과 LINC; FOLIO, LogicBench, PrOntoQA논리가 영어 문장으로 도착할 때, 추론은 누가 맡아야 하는가?
7부 · 평결결산통합은 언제 실제로 보상을 주며, 언제 한 기둥만으로 충분한 것이 정직한 선택인가?

이 권의 독자

이 권은 3권보다 한 걸음 더 나아간 독자, 대학원 진학을 향해 나아가는 4학년을 위해 쓰였습니다. 1권의 전방 연쇄기와 단일화, 2권의 EL++ TBox와 주석 달린 사실들, 3권의 임베딩과 필터링된 순위 매기기 프로토콜을 이미 알고 있다고 가정하며, 그 밖의 모든 것은 다시 유도합니다. 그 무엇도 블랙박스로 등장하지 않습니다. 모든 메커니즘은 동반 스위트 examples/integration/에 순수 NumPy로 구현되어 있고, 모든 경사는 본문에서 손으로 유도되며 그것을 계산하는 정확한 코드 줄 위의 주석에도 유도되어 있습니다. 그리고 선택적인 오라클 torch_check.py가 그 손으로 유도한 경사 가운데 세 가지를 torch.autograd로 다시 계산하여, 최악의 경우에도 1.3e-15까지 일치함을 확인해 줍니다. 이 스위트는 validate.py로 봉인되어 있습니다. 이는 커밋된 코드에 대해 21개의 역량 검사 중 21개가 모두 통과하는 인수 검증 하니스이며, 각 장에서 인용된 모든 숫자는 python3 <module>.py로 바이트 단위까지 동일하게 재현됩니다.

논지: 미분 가능한 논리로 가는 두 갈래 길

이 권 전체가 딛고 서 있는 확신은 다음과 같습니다. 논리를 미분 가능하게 만드는 원칙 있는 길은 정확히 두 가지이며, 이 둘은 같은 상품에 서로 다른 값을 매깁니다. 첫 번째 길은 진리를 완화합니다: 어떤 논리식을 정도 0.73만큼 참이라고 두고, ∧와 ∨를 정도 위의 연속 연산으로 바꾸면, 경사가 어디에나 값싸게 나타납니다. 그 대가는 왜곡입니다: 고전적인 세 t-노름 계열은 우리의 두 단계짜리 인용 사슬에 똑같은 입력으로부터 서로 다른 세 가지 확신도(괴델 0.80, 곱 0.72, 우카시에비치 0.70)를 매기며, 그중 어느 것이 "옳은지"는 정리가 아니라 모델링 결정입니다. 두 번째 길은 진리를 명확하게 남겨 두고 세계 위에 확률을 얹습니다: 각각의 불확실한 사실이 독립적인 동전이 되고, 어떤 질의의 확률은 그것을 함의하는 세계들의 총 무게가 되며, 그 의미론은 증명 가능할 만큼 정확합니다. 이 차이는 겉치레가 아닙니다: 어떤 질의의 두 증명이 지닌 확률을 순진하게 더하면 1.5750이 나오는데, 이는 확률조차 아닌 값이며, 분포 의미론은 정확한 값 0.8865를 돌려줍니다. 여기서의 대가는 계산량입니다: 정확한 추론은 가중 모델 계수이고, 이는 #P-난해 문제이며, 그 탈출구는 컴파일입니다. 질의를 한 번 회로로 바꾸어 두면, 그 뒤로는 모든 평가와 경사가 값싼 순전파 한 번으로 끝납니다. 값싸지만 왜곡된 것과 정확하지만 값비싼 것: 이 권의 모든 프레임워크는 바로 그 하나의 축 위의 한 위치이며, 이 권은 항상 그것이 어느 위치인지 말해 줄 것입니다.

실행 예제, 네 번째로 다시 읽기

우리는 세계를 마지막 한 가지 사실까지 그대로 유지하며, 오직 렌즈만 바꿉니다. 1권의 kb.py는 여전히 그 사실들과 혼 규칙을 담고 있으며, 그중에는 이 권이 닳도록 쓸 하나의 규칙, 곧 grandAdvisor는 advises와 advises를 합성한 것이라는 규칙도 있습니다. 2권의 온톨로지는 여전히 EL++ TBox와 엣지별 확신도를 담고 있고, 3권의 kg.py는 여전히 15/3 훈련·시험 분할과 필터링된 순위 매기기 심판을 담고 있습니다. distsem.py에 고정된 이 네 번째 읽기는 23개의 사실 가운데 11개를 독립적인 확률적 동전으로 승격시키고(0.85에서 0.95 사이의 지도 및 저술 기록들, 두 인용 엣지에 대한 2권의 확신도들, 0.55의 다소 불안한 소속 관계 하나), 나머지 12개는 확실한 채로 남겨 둡니다. 이 단 하나의 조치가 이 시리즈의 모든 숫자가 지닌 지위를 바꾸어 놓습니다: advises(alice, bob) 위의 0.90은 더 이상 증명과 함께 나란히 실려 다니는 주석이 아니라 하나의 매개변수가 되며, 여러분은 어떤 질의의 확률을 그것에 대해 미분할 수 있고, 따라서 신경망이 그것을 산출하도록 학습할 수 있습니다. 이 세계는 2^11 = 2048개의 가능한 상태를 가지며, 이 권이 할 일은 그 상태들을 다시는 하나하나 열거하지 않고도 그 위의 합을 계산하고, 컴파일하고, 미분하는 것입니다.

하나의 공유된 학계 세계 위에 세 개의 띠로 나뉜 폭넓은 다이어그램입니다. 왼쪽에는 2권의 기호 기둥이 있습니다: 두 개의 advises 사실로부터 alice와 carol의 grandAdvisor를 도출하는 작은 증명 트리가 인디고 색으로 그려져 있고, EL++ TBox 카드 한 장과 증명됨이라 적힌 도장이 함께 있습니다. 오른쪽에는 3권의 신경 기둥이 있습니다: 좌표 평면 위에 레이블 붙은 점들로 표시된 개체들이 이동 화살표 하나와 함께 있고, 순위 점수판 하나가 시안 색으로 그려져 있으며, 순위 매겨짐이라 적힌 도장이 함께 있습니다. 중앙에는 이 둘을 잇는 통합 기계 장치가 있습니다: 같은 증명이 산술 회로로 다시 그려져 있는데, 그 잎들은 동전 확률 0.90과 0.90을 지니고 있고 그 뿌리에는 P는 0.81과 같다고 적혀 있으며, 보라색 경사 화살표들이 뿌리에서부터 회로를 거슬러 흘러 잎 하나에 값을 공급하는 작은 신경망 아이콘 속으로 들어가고, 그 회로 위에는 퍼지 정도와 세계에 대한 확률이라는 두 위치짜리 다이얼이 놓여 있습니다. 세 개의 띠 아래로는 일곱 단짜리 사다리가 왼쪽에서 오른쪽으로 1부 퍼지·다치 논리, 2부 확률 논리와 회로, 3부 미분 가능 프레임워크, 4부 미분 가능 규칙 학습, 5부 복합 논리 질의 응답, 6부 자연어 추론, 7부 평결을 거쳐 오르며, 오른쪽 가장자리 너머로 점선 화살표가 뻗어 나가 남아 있는 질문들을 5권에 건네줍니다. 하나의 학계 세계가 네 번째로 다시 읽힙니다: 2권의 증명과 3권의 기하학이 한가운데서 만나 잎에 확률을 지니고 경사가 거슬러 흐르는 회로가 되며, 그 아래에는 이 권의 일곱 부에 걸친 오름길이 펼쳐져 있습니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

숫자가 된 진리: 퍼지 의미론과 그 경사

1부는 피해가 가장 적은 곳에서 시작합니다: 논리식은 그대로 두고 진리값만 바꾸는 것입니다. 3치 논리(K3와 Ł3)가 그 관문이며, 벌써 상처를 냅니다: 우리 세계가 시험하는 일곱 개의 고전적 항진명제 가운데 Ł3는 네 개를 보존하고 K3는 하나도 보존하지 못합니다. 그 뒤를 [0, 1] 연속체가 잇고, t-노름 계열(괴델, 곱, 우카시에비치)은 정도에 대해 AND를 말하는 세 가지 합법적 방식이며, 각각 자신의 t-코노름과 잉여(residuum)를 갖습니다. 1부는 이 권이 실제로 마음 쓰는 성질, 곧 경사에서 끝납니다: 괴델의 최솟값은 경사를 정확히 하나의 논리곱 항에만 넘겨주고 나머지는 굶기며(논리곱 항 쉰 개에서 희소도 0.980), 우카시에비치는 경사가 정확히 0이 되는 죽은 구간으로 잘려 나가고, 곱은 경사를 곱셈적으로 줄이며, 소프트민은 매끄러움을 편향의 대가로 사들입니다. 퍼지 논리는 값싼 길이고, 1부는 그 길의 정직한 가격표입니다.

제대로 된 확률: 세계, 계수, 회로

2부는 정확한 길을 택합니다. 분포 의미론은 어떤 질의의 확률을 동전들의 2048가지 전체 선택지에 걸친 합으로 정의하며, 공유된 증명들에 대한 포함-배제가 바로 정확한 0.8865를 순진한 1.5750으로부터 갈라놓는 것입니다. 가중 모델 계수는 그다음의 단 하나의 인터페이스가 됩니다: 숫자 하나, 곧 충족시키는 배정의 가중 개수가 주변 확률, 조건부 확률, 최대 확률 상태를 모두 내어 주며, 이는 일반적으로 #P-난해입니다. 지식 컴파일은 정말로 중요한 질의들에서 이를 돌파합니다: d-DNNF 회로로 한 번 컴파일해 두면, 무차별 대입이 1,048,576개의 배정을 치르고 얻는 답을 238번의 연산으로 얻어 냅니다. 그리고 그 회로는 산술적이므로 미분 가능하며, 그리하여 질의에 답하는 바로 그 구조가 경사 세미링(gradient semiring)도 함께 실어 나릅니다. 이것이 DeepProbLog가 증명기 안에서 신경 술어를 훈련하는 방식입니다: 우리 세계에서, 소프트맥스 분류기는 논문 주제 레이블을 단 한 번도 직접 본 적 없이 오직 논리 질의의 하류 진리값만으로 논문 주제를 학습하여 정확도 1.00에 이릅니다.

프레임워크들: 두 경로를 산업화하기

3부는 두 경로가 인프라가 되는 곳입니다. 의미 손실은 가중 모델 계수를 통해 어떤 제약이 신경망 자신의 출력 분포 아래에서 얼마나 그럴듯한지를 물음으로써 굳은 제약을 하나의 훈련 신호로 바꿉니다. 우리의 태그 예측 과제에서 이는 정확도를 높이는 동시에 제약 위반을 20건에서 6건으로 줄입니다. Scallop은 2권의 변함없는 데이터로그 부동점 엔진 위에 유래 다이얼 하나를 얹습니다: 속도를 위한 max-prob, 조여드는 사다리를 위한 상위 k개 증명(0.7650 → 0.9344, 여섯 개의 증명에서 정확한 값), 경사를 위한 이중수(dual number)입니다. 논리 텐서 네트워크는 퍼지의 길을 끝까지 밀고 갑니다: 실수 논리는 상수, 함수, 술어를 텐서에 그라운딩하고 만족도를 최대화함으로써 훈련합니다(우리의 공리들에서 0.5295 → 0.9933). 그리고 KLay와 Lobster는 시스템의 물음에 답합니다. 회로를 배치된 GPU 네이티브 텐서 연산으로 평평하게 펴는데, tensor_ops.py는 이것이 루프 의미론과 비트 단위로 같음을 증명합니다.

경사로 학습한 규칙

4부는 다이얼을 규칙을 적용하는 일에서 규칙을 발견하는 일로 돌립니다. Neural-LP와 DRUM은 규칙 자체를, 즉 관계 행렬들의 가중 합성을 미분 가능한 대상으로 만들며, 합성 위의 주의는 우리의 정답 규칙 advises∘advises를 신뢰도 0.9990으로 복호화합니다. 신경 정리 증명기는 한 걸음 더 나아가 단일화(unification)를 미분합니다: 기호들은 임베딩 유사도로 매칭되고, 증명은 부드러운 점수가 되며, 훈련된 증명기는 grandAdvisor ← advises∘advises를 복호화하는 동시에 제외해 둔 엣지에 모든 오염된 엣지보다 0.7678의 여백만큼 더 높은 점수를 매깁니다. 4부는 신경망 방법들을 정직하게 유지해 주는 기호적 기준선들로 마무리됩니다: AnyBURL 방식의 채굴은 헤아림만으로 정답 규칙을 정확히 신뢰도 2/3로 복원하고, RNNLogic의 EM 루프는 같은 규칙에 대한 규칙 분포를 0.009에서 0.876으로 집중시킵니다. 경사와 헤아림이 일치할 때, 비로소 둘 다를 믿기 시작할 수 있습니다.

모양을 갖춘 질의: 계산 DAG

5부는 목표를 하나의 빠진 엣지(3권 전체의 게임이었던 것)에서 온전한 논리 질의로 키웁니다: "alice가 지도하는 누군가에게 지도받지만, carol에게는 지도받지 않는 사람은 누구인가?" 이러한 모든 질의는 사영, 교집합, 합집합, 부정으로 이루어진 계산 DAG이며, 이 스위트는 14가지 질의 유형과 36개의 구체적 질의를 정답으로 삼는 기호 실행기로 고정해 둡니다. 3권의 임베딩 계보가 부담 아래에서 다시 등장합니다: GQE의 점, Query2Box의 박스, BetaE의 분포는 각각 연산자 메뉴의 서로 다른 부분만을 지원하며, 커버리지 표의 빈칸들은 공학적 결함이 아니라 정리입니다. 그다음 이 분야를 재편한 반전이 나옵니다: CQD와 QTO는 사전 훈련된 링크 예측기의 퍼지 점수 위에서 빔 탐색이나 부동점 최적화로 질의에 무학습으로 답하며(불완전한 그래프를 순진하게 순회하면 0.1465에 그치는 곳에서 MRR 0.8000을 냅니다), ULTRA 방식의 구조적 채점기는 개체 어휘를 통째로 버려서, 한 번도 본 적 없는 병원 세계로 제로샷 전이하여 무작위 기준선 0.2198에 맞서 MRR 0.8333을 냅니다.

논리가 영어로 적혀 있을 때

6부는 인터페이스를 트리플에서 문장으로 옮깁니다. 소프트 추론기(RuleTaker와 ProofWriter 계열)는 자연어 규칙에 대한 연역을 흉내 내도록 언어 모델을 훈련하며, 이 스위트의 대역은 정말로 중요한 발견을 재현합니다: 훈련된 증명 깊이에서는 거의 완벽한 정확도(1.000, 0.966)를 보이다가, 한두 홉 더 깊어지면 동전 던지기 수준인 0.500으로 무너지는 반면, 기호적 증명기는 모든 깊이에서 100%를 유지합니다. 번역 후 증명(Logic-LM과 LINC 패턴)은 대신 일을 나눕니다: 영어를 형식 논리로 파싱하고, 그 논리를 증명기에 넘긴 다음, 파싱이 실패하면 기권합니다. 우리가 생성한 말뭉치에서 파싱에 성공한 입력에 대한 정확도는 정확히 1.0000이며, 자가 수리는 커버리지를 0.8080에서 0.9293으로 끌어올리면서도 기권을 오류로 바꾸는 일은 결코 없습니다. 그다음 벤치마크 장은 레이블 정확도와 증명 정확도를 갈라내는 계측기를 짓습니다: 우리의 탐욕적 추론기는 레이블에서는 이기고(0.817) 증명에서는 집니다(0.167). 이는 틀린 이유로 옳았던 경우의 실측된 모습입니다.

미리 약속된 평결

7부는 이 모든 것을 하나의 결산 위에서 저울질합니다. 얻은 것들은 주장되는 것이 아니라 측정됩니다: 증명들의 합이 거짓말했던 곳에서의 정확한 확률, 훈련을 통해 강제된 제약, 경사로 복원되고 헤아림으로 확인된 규칙, 열네 가지 유형 폭넓게 답해진 질의, 결코 허풍 떨지 않는 증명으로 파싱된 영어. 대가들도 측정됩니다: 유도되지 않고 선택된 t-노름 왜곡, 컴파일로 치른 #P 복잡도, 죽은 경사, 깊이의 절벽. 통합은 그 구조가 문제의 구조와 맞아떨어지는 바로 그곳에서 보상을 주며, 평결 장은 숫자로 그것을 말한 다음, 살아남은 질문들, 곧 신뢰, 보정, 충실성, 규모를 5권에 건네줍니다.

이 길이 이르는 곳

오름길은 1권의 논리에 가할 수 있는 가장 작은 변화, 곧 세 번째 진리값을 더하는 일에서 시작합니다. 첫 장인 다치 논리: 참과 거짓을 넘어는 미지이거나 부분적일 수 있는 진리를 가지고 명제 의미론을 다시 지으며, 학계 세계 위에서 K3와 Ł3의 진리표를 항목 하나하나 풀어내고, 이 모든 작업의 첫 번째 희생을 측정합니다: 진리가 더 이상 이진적이지 않게 될 때 어떤 고전적 법칙이 살아남고, 미분 가능해지는 길목에서 어떤 법칙이 조용히 죽는지 말입니다.