논리 텐서 네트워크: 실수 논리
📍 현재 위치: 3부 · 미분 가능 프레임워크 — 10장. Scallop은 각 접지 사실의 최상위 증명만을 남겨 두는 방식으로 확률적 기둥을 확장했습니다; 이 장은 기둥 자체를 완전히 바꿉니다: 1부의 퍼지 연산자들을 완전한 1차 언어로 조립하고, 그 언어의 한정된 공리들이 손실 함수 자체가 되도록 만듭니다.
2부의 모든 확률적 시스템은 그 의미론이 아무리 정교했더라도, 실제 작업은 언제나 접지된(ground) 논리식 위에서 수행되었습니다: 규칙은 사례로 예화되었고, 증명은 열거되었으며, 가능 세계는 세어졌습니다. 이 장은 동일한 통합 문제에 대한 퍼지 기둥의 성숙한 답을 제시합니다. 논리 텐서 네트워크(Logic Tensor Networks, LTN)라 불리는 이 프레임워크의 언어인 실수 논리(Real Logic)는 한정사를 미분 가능한 1급 객체로 그대로 유지합니다. 전칭 한정된 공리는 확장되어 계수기에 넘겨지는 것이 아니라, 모든 사례를 한꺼번에 다루는 하나의 매끄러운 함수로서 평가되어, 0과 1 사이의 진리도(truth degree)로 귀결됩니다. 지식 베이스 전체가 하나의 숫자가 되며, 학습이란 경사 하강법으로 그 숫자를 1을 향해 밀어붙이는 것을 뜻합니다. 동반 모듈 ltn.py는 학술 세계 위에서 이 기계 전체를 손으로 조립합니다: 2권의 실제 공리들, 306개의 학습 가능한 매개변수, 주석 안에서 유도되고 유한 차분법에 맞서 인증된 모든 그래디언트, 그리고 훈련된 모델을 의도적인 의심을 품고 읽어 내는 일련의 보류된 탐침들입니다.
큰 결혼식의 좌석 배치를 여러 제약 조건의 목록에 맞추어 정한다고 상상해 보십시오: 신부 측 가족 모두는 신랑 측 가족의 누군가와 가까이 앉아야 하고, 누구도 3번 테이블과 7번 테이블 양쪽에 동시에 속해서는 안 되며, 밴드 옆에 앉은 사람은 누구든 춤을 출 줄 알아야 합니다. 작업을 진행하는 동안에는 예/아니오만 판정하는 검사기는 쓸모가 없습니다. 거의 모든 초안 배치가 어딘가에서 실패하기 때문입니다. 여러분에게 필요한 것은 만족도 계기판입니다: 예를 들어 0.53을 가리키는 다이얼로, "규칙집 전체가 대략 절반쯤 지켜지고 있으며, 가장 심하게 위반된 규칙들이 바늘을 가장 세게 끌어내리고 있다"는 뜻입니다. 그런 다음 다이얼이 올라가는 방향으로 한 번에 1센티미터씩 의자를 옮겨, 계기판이 0.99를 가리킬 때까지 반복합니다. 실수 논리는 바로 1차 논리를 위해 만들어진 그런 계기판입니다: 개체는 움직일 수 있는 점이 되고, 술어는 조정 가능한 경계가 되며, (한정사를 포함한) 모든 공리는 0과 1 사이의 숫자가 되고, 학습이란 규칙집 전체가 거의 1을 가리킬 때까지 모든 것을 밀어 옮기는 일입니다.
이 장에서 다루는 내용
- 2부 이후의 공백: 가중 모델 계수(weighted model counting)의 확률적 기계 장치가 정확하면서도 근본적으로 명제 논리적인 이유, 그리고 한정된 1차 논리 구조를 유지하면서 정확성을 미분 가능성과 맞바꾼다는 것이 무엇을 뜻하는지입니다.
- 그라운딩 : 시그니처의 모든 기호를 텐서 계산으로 바꾸는 매핑을, 학술 세계 위에서 조각조각 풀어낸 것과 완전한 기호-텐서 대응표, 306개 매개변수 예산입니다.
- 안정적 곱(stable product) 설정: 어떤 퍼지 연산자가 각 논리 결합자를 맡는지, 각 선택이 왜 그래디언트 품질에서 이기는지, 그리고 안정성 클램프 과 이 어디서 제 몫을 하는지입니다.
- 일반화 평균으로서의 한정사: 이 장의 핵심 유도로, ∃("존재한다"로 읽습니다)에 대한 -평균 과 ∀("모든 것에 대하여"로 읽습니다)에 대한 -평균-오차 , 그 그래디언트를 단계별로 풀어낸 것, 그리고 커지는 가 왜 "모든 것에 대하여"를 최악의 사례들에 대한 커리큘럼으로 바꾸는지입니다.
- 하나의 손실로서의 지식 베이스: 그라운딩된 2권의 실제 공리 23개, 집계 SatAgg와 그 그래디언트, 0.5295에서 0.9933까지 이어지는 커밋된 훈련 기록, 그리고 한 행씩 읽어 내는 공리 그룹별 표입니다.
- 정직함을 지키는 탐침들: 공리별 훈련 목표였던 적이 없는 질의들, 모든 개체에서 0에 가까운 분리 논리곱, 그리고 실수 논리가 고전 논리로 정확히 붕괴하는 명확한 입력 복원 검사입니다.
- 만족도가 아닌 것: SatAgg가 1에 가깝다는 것이 왜 증명이 아닌지, 진리도가 왜 보정된 확률이 아닌지, 그리고 이 분야가 왜 대규모에서의 보장을 위해 다시 회로로 돌아가는지입니다.
세계를 세는 일에서 세계를 채점하는 일로
이 장을 이 권의 지도 위에 놓아 봅시다. 2부는 확률적 기둥을 최고 높이까지 쌓아 올렸습니다: 분포 의미론(distribution semantics)은 확률적 사실에 정확한 의미를 부여했고, 가중 모델 계수는 가능 세계 전체에 대한 합산으로 질의 확률을 계산했으며, 컴파일된 회로는 그 합산을 다룰 만하게 만들었고, DeepProbLog는 그것을 통해 신경 술어를 훈련시켰습니다. 이 모든 기계 장치는 정확하며, 근본적으로는 명제 논리적입니다. 한정된 규칙은 그라운딩을 거친 뒤에야 이 시스템들에 들어옵니다: 유한한 정의역 위에서 예화되어, 그 사례들이 명제 논리식이 되고, 계수는 접지 원자에 대한 진리 할당 전체에 걸쳐 이루어집니다. 한정사 자체는 미분 가능한 대상으로 살아남지 못합니다; 수학이 시작되기도 전에 컴파일되어 사라져 버립니다.
실수 논리는 정반대의 거래를 합니다 [1]. 정확성을 포기하고(가능 세계도, 확률도, 계수도 없습니다) 그 대가로 완전한 1차 논리 구문을 미분 가능한 계산 내부에 살아 있는 채로 유지합니다: 상수, 함수 없는 항, 임의의 항수를 가진 술어, 모든 논리 결합자, 그리고 두 한정사 모두가 각각 실수에 대한 매끄러운 연산으로 매핑됩니다. ∀x Prof(x) → Res(x)의 진리값은 전칭 진술로서 계산되며, 그라운딩된 사례들에 대한 집계 자체가 미분 가능하고, 그 그래디언트는 모든 사례에 동시에 흘러들어 갑니다. 이 아이디어는 처음에 "데이터와 지식으로부터의 딥러닝과 논리적 추론"을 위한 제안으로 등장했으며 [2], 이 장이 해부하는 프레임워크로 성숙했습니다: 논리 결합자가 정확히 1부의 연산자들인 퍼지 1차 의미론으로, 그래디언트를 위해 선택된 것들입니다.
이 계보는 중요합니다. t-노름 장은 그 대수를 확립했고, 퍼지-신경 다리 장은 논리식이 손실이 되었을 때 각 연산자가 그래디언트에 무엇을 하는지 측정했습니다. LTN은 이 두 장이 결실을 맺는 지점입니다: 퍼지 기둥의 성숙한 프레임워크가, 검증된 연산자들을 조립하여 2권의 온톨로지가 말하는 모든 것을 말할 수 있을 만큼 큰 언어를 만들고, 그것에 맞서 훈련시킵니다.
그라운딩 : 모든 기호가 텐서가 되다
실수 논리의 핵심 대상은 그라운딩(grounding)이며, 로 표기됩니다: 1차 논리 시그니처의 모든 기호를 구체적인 수치 대상으로 보내는 매핑으로, 그 기호들로 구성된 모든 논리식이 합성을 통해 안의 실수로 평가되도록 합니다 [1]. 고전적 해석이 기호를 집합과 관계로 매핑하는 자리에서, 그라운딩은 기호를 텐서와 미분 가능한 함수로 매핑합니다. 학술 세계는 모든 조각에 얼굴을 부여합니다: 시그니처는 13개의 상수(alice부터 erin까지의 개인들, 논문들, 기관들, 주제들로, 2권의 ontology.py에서 읽어 온 것이며 다시 타이핑되지 않습니다, ltn.py 75–96행), 일곱 개의 단항 술어(Professor, Student, Researcher, Person, Paper, Institution, Topic), 그리고 이항 술어 하나(advises)를 가집니다.
상수는 학습 가능한 벡터가 됩니다. 각 개인 는 벡터 , 즉 두 개의 실수로 이루어진 목록으로 그라운딩되며, 임베딩 행렬의 한 행으로 저장됩니다(ltn.py 232행). 여기서 임베딩 차원은 2인데, 이는 의도적인 선택입니다: 이 작은 세계에 대해서는 두 좌표만으로 충분하고, 학습된 배치를 문자 그대로 그림으로 그릴 수 있게 해 주며, 그것이 바로 이 장의 그림이 보여 주는 것입니다. 결정적으로, 이 임베딩은 입력이 아니라 매개변수입니다: carol을 옮기는 것이 만족도를 높인다면 경사 하강법은 자유롭게 carol을 옮길 수 있습니다.
단항 술어는 작은 신경망 분류기가 됩니다. 각 개념 는 미분 가능한 함수 로 그라운딩되며, 유닛들이 tanh(하이퍼볼릭 탄젠트, 위로 값을 눌러 담는 S자형 압착 함수)를 적용하는 폭 8의 은닉층 하나와 시그모이드 출력을 가진 다층 퍼셉트론(multi-layer perceptron, MLP, 작은 순전파 신경망)으로 구현됩니다. 이는 ltn.py 196–206행의 2-8-1 구조입니다:
def mlp_forward(p: dict, X: np.ndarray) -> tuple[np.ndarray, tuple]:
"""Batched forward over the rows of X (n, din) → truth values a (n,)."""
# z = W₁x + b₁ (row-wise: Z = X W₁ᵀ + b₁)
Z = X @ p["W1"].T + p["b1"]
# h = tanh(z)
H = np.tanh(Z)
# s = w₂·h + b₂
S = H @ p["w2"] + p["b2"][0]
# a = σ(s)
A = sigmoid(S)
return A, (X, H, A)
마지막 시그모이드 는, 여기서 는 지수 함수(오일러 수 을 부호가 뒤집힌 점수 만큼 거듭제곱한 것)인데, 신경망의 점수를 안으로 눌러 담기 때문에, 그 출력은 곧 진리도입니다. 원자 논리식 Professor(carol)는 그런 다음 1차 논리 의미론이 지시하는 그대로 합성적으로 평가됩니다: , 즉 carol의 현재 임베딩에 Professor 신경망을 적용한 것입니다.
이항 술어는 연결(concatenation)에 대한 MLP가 됩니다. 역할 advises는 로 그라운딩됩니다: 쌍 는 두 개의 2차원 임베딩을 하나의 4차원 벡터로 연결하여 표현되며, 동일한 시그모이드 헤드를 가진 4-8-1 MLP가 그것을 채점합니다(ltn.py 304–307행은 개의 쌍 행을 한 배치로 만듭니다). 각 블록의 매개변수 개수와 함께, 기호-텐서 대응 규약 전체를 표 하나로 정리하면 다음과 같습니다(ltn.py 229–234행):
| 기호 종류 | 예시 | 그라운딩 | 매개변수 |
|---|---|---|---|
| 상수 | carol | 안의 학습 가능한 벡터 | |
| 단항 술어 | Professor | MLP (2-8-1 + ) | |
| 이항 술어 | advises | 연결된 쌍에 대한 MLP (4-8-1 + ) | |
| 논리 결합자 ∧ ∨ ¬ → | 다음 절 참고 | 고정된 대수 연산자, 매개변수 없음 | |
| 한정사 ∀ ∃ | 유도 참고 | 사례에 대한 일반화 -평균, 매개변수 없음 |
각 2-8-1 MLP는 개의 첫 층 가중치, 8개의 첫 층 편향, 8개의 출력 가중치, 1개의 출력 편향을 가지므로 33개의 매개변수이며, 4-8-1 advises 신경망은 개를 가집니다. 총합은 개의 학습 가능한 숫자이며, 커밋된 실행은 훈련이 시작되기 전에 전체 손실의 손으로 작성한 그래디언트를 그 306개 전부에 대해 중심 유한 차분법에 맞서 인증합니다(ltn.py 419–435행). 표의 아래 두 행만이 고정되어 있고, 그 위의 모든 것은 훈련이 움직이는 대상입니다.
그라운딩은 모든 기호를 텐서 계산으로 매핑하고(왼쪽), 학습된 2차원 평면은 움직이는 임베딩 주위에 분리된 Professor 영역과 Student 영역을 조각해 내며(가운데), 23개의 그라운딩된 공리는 훈련이 0.5295에서 0.9933까지 밀어 올리는 단 하나의 미분 가능한 숫자 SatAgg로 집계됩니다(오른쪽).
저자가 AI의 도움을 받아 직접 제작한 원본 도해.
논리 결합자: 안정적 곱 설정
원자들이 그라운딩되고 나면 복합 논리식에는 논리 결합자가 필요하며, 1부는 그 메뉴를 만들었습니다. 실수 논리의 참조 정식화는 하나의 구체적인 선택, 안정적 곱 설정(stable product configuration)을 권장하며 [1], 미분 가능 퍼지 논리에 대한 체계적인 연산자 분석은 그것이 왜 이기는지를 설명합니다: 이 설정의 그래디언트는 단위 정사각형 내부 어디에서나 두 인자 모두에 대해 0이 아니며, 이는 시그모이드와 클램프가 모든 진리값을 유지하는 영역입니다. 이와 대조적으로 괴델 연산자는 그래디언트 전체를 한 인자에만 보내며, 우카시에비치 쌍은 그 클리핑이 그래디언트가 0이 되는 사각지대를 만듭니다 [3]. 네 가지 선택과, 경사 하강법이 실제로 사용하는 편도함수를 함께 표로 정리하면 다음과 같습니다:
| 논리 결합자 | 연산자 | 공식 | ||
|---|---|---|---|---|
| 곱 t-노름 | ||||
| 확률적 합 | ||||
| 표준 부정 | — | |||
| 라이헨바흐 함의 |
각 행은 기본값이 아니라 근거 있는 선택입니다. 곱 t-노름은 퍼지-신경 장에서 조밀한 그래디언트의 승자였습니다: 괴델 최솟값이 그래디언트 전체를 가장 약한 하나의 논리곱 항에만 보내고 나머지를 굶주리게 하는 것과 달리, 곱의 나머지-하나-빼기(leave-one-out) 편미분 는 모든 논리곱 항이 계속 학습하도록 유지합니다. 확률적 합은 아래에서 그것의 드모르간 쌍대입니다: tnorms.py의 닫힌 형식 s_probsum(128–130행)은, 그 모듈에서 쌍대 구성 에 맞서 검증되며 편차는 정확히 0입니다. 라이헨바흐 함의는 곱의 고겐(Goguen) 잉여(residuum)가 아닙니다(그 화살표는 후건을 전건으로 나눈 몫 를 담고 있어서, 전건 에서 그래디언트가 특이해집니다); 그것은 안정적 쌍으로부터 만들어진 실질적 화살표이며, 그 항등식은 대수 한 줄의 값어치가 있습니다. 이 설정 자체의 부정과 논리합 아래에서 로 정의해 봅시다:
가운데 단계는 에서 를 전개합니다; 와 가 서로 상쇄되어, 경우 분기도 몫도 꺾임점도 없이 어디서나 매끄러운 다항식이 남습니다. 동반 코드는 이 항등식을 그저 믿고 넘어가지 않습니다: ltn.py 507–511행은 tnorms.py의 이진 격자(모든 값이 정확한 이진 부동소수점인 곳) 위에서 가 정확히 의 편차로 성립함을 단언합니다. 편도함수는 함의를 통한 학습의 의미론을 담고 있습니다: 는 후건으로 흘러드는 그래디언트가 전건의 진리값에 의해 조절된다는 것을 말하며(전건이 참인 곳에서만 규칙이 그 머리 부분을 가르친다는, 전건 긍정식의 퍼지적 그림자입니다), 은 후건이 이미 완전히 참이 아닌 이상 전건을 높이는 것이 함의를 낮출 수만 있다는 것을 말합니다. 구현은 단 두 줄입니다(ltn.py 120–125행):
def implies(a, b):
# Reichenbach implication I_R(a, b) = 1 - a + a·b.
...
return 1.0 - a + a * b
1부에서 온 재료가 하나 더 있는데, 이번 것은 대가가 붙어 있습니다. 안정적(stable)이라는 단어는 두 개의 클램핑 사영, 와 를 가리키며, 이는 정확히 0이나 정확히 1에서 특이점을 갖는 어떤 연산에라도 들어가기 전에 진리값을 그 지점들로부터 멀리 묶어 둡니다 [1]; 논문은 을 작다는 것 외에는 명시하지 않은 채로 남겨 두며, 동반 코드는 (참조 구현의 기본값을 따라) 로 설정합니다. 퍼지-신경 장은 논증이 아니라 실증 사례를 남겼습니다: fuzzy_grad.py(310–343행)에서, 정확히 거짓인 그라운딩 하나가 로그-곱 손실을 문자 그대로 무한대인 inf로 만들고 그래디언트도 무한대가 되는 반면, 클램핑된 버전은 항당 과 그래디언트 크기 로 유계입니다. 이 장은 그 모듈에서 , , 을 임포트하며(ltn.py 79행) 정확히 한 곳, 즉 한정사 집계기 내부에서만 그것들을 적용하는데, 다음 절은 바로 그곳에서 동일한 폭발이 기다리고 있음을 보여 줍니다.
일반화 평균으로서의 한정사
여기 실수 논리를 2부의 모든 것과 갈라놓는 구성이 있습니다. 한정된 논리식 는 를 모든 개인에 대해 평가하여 사례 진리값의 벡터 을 만들어 냄으로써 그라운딩되며, 여기서 은 그라운딩된 사례의 개수입니다(변수 하나가 개인들에 대해 범위를 가질 때는 , 두 개일 때는 입니다). 그러면 한정사는 하나의 집계기(aggregator)입니다: 그 개의 숫자를 하나로 접는 미분 가능한 함수입니다. 실수 논리는 지수 를 갖는 일반화 평균(generalized mean)의 계열을 사용하는데, 는 이상치 민감도 다이얼 역할을 하는 1 이상의 실수입니다 [1]. 존재 한정사 ∃는 -평균입니다(수식은 이렇게 읽습니다: 각 사례 진리값 를 제곱하고, 합 기호 으로 개의 거듭제곱된 진리값을 사례 마다 하나씩 더해 평균을 낸 뒤, 제곱근을 취합니다),
그리고 전칭 한정사 ∀는 -평균-오차(p-mean-error)로, 참으로부터의 편차 를 평균 낸 뒤 그 결과를 1에서 빼는 것입니다:
유도에 앞서 다이얼을 먼저 읽어 봅시다. 에서는 둘 다 단순한 산술 평균으로 환원됩니다: 모든 사례가 동등하게 취급되어, 전칭 공리가 어느 한 사례가 0에 있어도 0.9를 기록할 수 있습니다. 가 커질수록 거듭제곱 합은 그 가장 큰 항들에 의해 지배됩니다: 에서는 가장 큰 (가장 좋은 증거에 기대는 낙관주의자), 에서는 가장 큰 오차 (가장 심한 위반에 기대는 비관주의자)입니다. 극한에서 이 평균들은 괴델 한정사가 됩니다. 에 대해 이를 확인하려면, 오차를 로, 그 최댓값을 로 쓰고, 안쪽 항을 다음과 같이 조여 봅니다:
아래쪽 경계는 합의 가장 큰 항 하나만을 남기고, 위쪽 경계는 모든 항을 그것으로 대체합니다. 일 때 이므로(고정된 분수의 제곱근은 1로 수렴합니다), 두 경계 모두 로 수렴하고, 따라서 가 됩니다: 오직 최악의 사례 하나만이 결정하며, 이는 정확히 괴델의 "모든 것에 대하여"이자 정확히 퍼지-신경 장이 경고했던 희소 그래디언트입니다. 동반 코드는 로 고정하는데(ltn.py 101행), 이는 명시적인 타협입니다: 이미 가장 거짓인 사례 쪽으로 기울어 있으면서도, 아직 나머지를 굶주리게 하지는 않는 지점입니다.
이제 이 장의 핵심 유도입니다: 하나의 사례 진리값 에 대한 의 그래디언트를, 모든 단계를 보이면서 구합니다. 안쪽의 거듭제곱 평균을 이라 이름 붙이면, 계산은 세 고리로 이어진 연쇄가 됩니다:
첫째 고리, 거듭제곱 평균을 통한 집계. 를 에 대해 거듭제곱 법칙으로 미분하면:
둘째 고리, 오차를 통한 거듭제곱 평균. 합 중에서 인 항만이 에 의존하며, 를 미분하면 이 나옵니다:
셋째 고리, 사례를 통한 오차. 로부터 단순히 입니다. 세 고리를 곱하면, 둘째 고리의 가 첫째 고리의 를 상쇄하고, 두 개의 음의 부호가 서로 상쇄됩니다:
살아남은 두 인자를 읽어 봅시다. 인자 은 사례별입니다: 각 사례는 자기 자신의 위반 정도의 제곱에 비례하는 그래디언트를 받습니다. 에서 이는 단순히 이며, 그래디언트는 그 사례가 현재 얼마나 거짓인지에 비례합니다; 두 사례 사이의 그래디언트 비율은 이므로, 가 커질수록 집계기는 학습 신호 전체를 가장 심하게 위반된 사례들에 집중시킵니다. "모든 것에 대하여"의 의미론은 커리큘럼이 됩니다: 최적화기는 언제나 그 공리에 대한 최악의 반례들에 가장 열심히 매달리며, 다이얼 는 그 집중이 얼마나 외골수인지를 정합니다 [1]. 인자 는 전역적이며, 이것이 함정입니다: 공리가 완전한 만족에 가까워질수록 모든 이 되어 이 되고, (에서는 )는 발산합니다. 이것은 로그 폭발의 한정사 수준 버전이며, 안정 변형들이 거듭제곱 평균 이전에 로 그 입력을 클램핑하는 이유입니다: 이므로 평균은 를 만족하고, 따라서 폭발하는 인자는 로 유계이며 연쇄는 로부터 추가로 하나의 을 얻습니다. 구현은 유도를 한 줄 한 줄 그대로 따릅니다(ltn.py 141–149행):
def agg_forall(a: np.ndarray, p: int = P) -> tuple[float, np.ndarray]:
"""Stable A'_pME and its gradient ∂A/∂a_i (derivation above)."""
n = a.size
e = 1.0 - pi_1(a) # e_i = 1 - (1-ε)a_i ∈ [ε, 1]
m = float(np.mean(e ** p)) # M = (1/n) Σ e_i^p ≥ ε^p
val = 1.0 - m ** (1.0 / p) # A_pME = 1 - M^{1/p}
# ∂A/∂a_i = (1-ε)/n · e_i^{p-1} · M^{(1-p)/p}
grad = (1.0 - EPS) / n * e ** (p - 1) * m ** ((1.0 - p) / p)
return val, grad
존재 한정사의 거울상인 agg_exists(ltn.py 160–168행)는 마지막의 뒤집기 없이 에 대해 동일한 연쇄를 실행하여, 를 내놓습니다: 그래디언트는 가장 참에 가까운 증거들, 즉 이미 존재 한정사를 만족하는 데 가장 가까이 다가간 사례들에 기댑니다.
하나의 미분 가능한 숫자로서의 지식 베이스
실수 논리 이론은 닫힌 논리식들의 집합이며, 그 훈련 목표는 이들의 집계된 진리값인 SatAgg입니다. 동반 코드는 장난감 모방이 아니라 2권의 실제 공리들을 그라운딩합니다: 14개 공리로 이루어진 TBox(용어 상자, 스키마 수준의 공리들)는 ontology.py 125–174행에 있으며, ltn.py는 모델이 그라운딩한 시그니처, 즉 일곱 개의 개념과 advises 역할만을 언급하는 모든 공리를 1차 논리 형태로 옮깁니다; grandAdvisor 역할 연쇄, Dean, TenuredStudent, TenuredStudentAdvisor 공리들, 그리고 저작(authored) 역할과 관련된 두 공리는 이 시그니처 밖에 있어 그라운딩되지 않습니다. 커밋된 실행은 그 목록을 인쇄합니다:
[1] the grounded theory: 23 axioms from Volume 2's ontology.py, 306 parameters
abox 13 axiom(s) ABox typings C(a)
disjoint 1 axiom(s) ∀x ¬(Prof(x) ∧ Stud(x)) [TBox 6]
subsume 3 axiom(s) the ladder ∀x C(x) → D(x) [TBox 1-3]
dom/rng 2 axiom(s) adv domain ∀ + range-∃ [TBox 5, 4]
facts 4 axiom(s) asserted advises(a, b) atoms
ABox(단언 상자, 온톨로지의 접지 사실들)에서 온 13개의 타입 지정과 4개의 advises 사실은 접지 원자이므로, 그 진리값은 단일 술어 평가입니다. 분리성 공리 Professor ⊓ Student ⊑ ⊥(ontology.py 143행)는 가 되며, 사례 진리값은 로 에 의해 집계됩니다(ltn.py 325–334행). 포섭 사다리 Professor ⊑ Researcher, Student ⊑ Researcher, Researcher ⊑ Person은 세 개의 전칭 한정된 라이헨바흐 함의가 됩니다. advises 정의역 공리 ∃advises.⊤ ⊑ Researcher(ontology.py 138행)는 가 되며, 이는 사례 격자입니다. 그리고 ∃를 사용하는 유일한 공리인 Professor ⊑ ∃advises.Student(ontology.py 133행)는 한정사를 중첩시킵니다:
이는 의미론이 합성되는 그대로 안에서 바깥으로 계산됩니다(ltn.py 359–379행): 안쪽 논리곱은 격자 를 채우고, 각 행은 을 통해 존재 점수 로 집계되며, 각 는 화살표를 적용하고, 가 전칭 한정사를 마무리합니다. 이 파이프라인의 모든 연산자는 위 두 절에서 나온 것 중 하나이므로, 손으로 작성한 역방향 패스는 그저 그 편도함수들을 역순으로 연쇄한 것에 지나지 않습니다.
SatAgg 자체도 후일 생각이 아니라 그래디언트를 가진 하나의 선택입니다. 동반 코드는 프레임워크의 실용적 권고를 따라 동일한 에서 를 재사용하며, 이를 23개의 공리별 진리값 에 적용하고 [1], 다음을 최소화합니다
동일한 유도에 의해, 바깥쪽의 로 부호만 뒤집힌 채로 말입니다. 두 가지 귀결이 곧바로 따라옵니다. 그래디언트는 결코 양수가 아닙니다: 어떤 공리의 진리값을 높이든 언제나 손실을 낮춥니다. 그리고 가장 심하게 위반된 공리가 가장 큰 밀어붙임을 받습니다, 왜냐하면 공리별 인자가 다시 한번 위반 정도의 제곱이기 때문입니다; SatAgg는 각 전칭 한정사가 사례들에 걸쳐 실행하는 것과 동일한 최악-우선 커리큘럼을 공리들에 걸쳐 실행합니다. 순전파와 역전파를 합친 것은 ltn.py 388–396행이며, 훈련 루프는 순수한 완전 배치 경사 하강법 로, 매개변수 벡터 는 306개의 학습 가능한 숫자 전체를 모은 것이고 학습률 은 각 단계의 크기를 조정하며, 3000 에폭 동안 실행됩니다(ltn.py 443–447행). 무엇이든 실행되기 전에, 이 모듈은 손으로 조립한 전체를 인증합니다: 306개의 매개변수 전부에 걸쳐, 해석적 그래디언트와 중심 유한 차분법 사이의 최대 간극은 이며(출력 블록 [3]), 이는 올바르게 연쇄된 유도의 수치적 특징입니다. 커밋된 기록은 다음과 같습니다:
[4] training: full-batch GD on L = 1 − SatAgg (η = 2.0, 3000 epochs)
epoch : SatAgg 1 − SatAgg
1 : 0.5295 0.4705
10 : 0.7425 0.2575
100 : 0.9564 0.0436
500 : 0.9890 0.0110
1000 : 0.9931 0.0069
2000 : 0.9933 0.0067
3000 : 0.9933 0.0067
공리 그룹별 만족도가 훈련 전과 후로 정리된 표는, 이론이 이 특정한 세계와 만나는 지점입니다. 커밋된 표를 한 행씩 읽어 봅시다:
| 그룹 | 공리 수 | 이전 | 이후 | 이 행이 말하는 것 |
|---|---|---|---|---|
| abox | 13 | 0.4670 | 0.9991 | 무작위로 초기화된 MLP들은 모든 것에 대해 0.5 근방으로 답한다; 타입 지정은 가장 쉬운 공리로, 1을 향한 순수한 지도 학습적 끌림이다 |
| disjoint | 1 | 0.7301 | 0.9986 | 무지 때문에 훈련 이전에도 높다: 두 술어가 0.5 근방이면 논리곱은 0.25 근방, 부정은 0.75 근방이 된다; 진짜 작업은 나중에 온다 |
| subsume | 3 | 0.7545 | 0.9987 | 전건이 0.5에 가까운 함의는 근방에서 시작한다; ABox가 전건을 1로 밀어붙이는 동안 훈련은 이들을 계속 참으로 유지해야 한다 |
| dom/rng | 2 | 0.6669 | 0.9776 | 가장 어려운 그룹이며 가장 낮게 마무리된다: 중첩된 ∃ 공리는 169개의 쌍에 걸쳐 한꺼번에 세 개의 술어를 조율해야 한다 |
| facts | 4 | 0.5200 | 0.9995 | 네 개의 접지 원자가 1로 끌려간다, ABox 행의 이항 유사물이다 |
분리성 행은 좀 더 자세히 살펴볼 가치가 있는데, 이것이 부정 압력(negative pressure)을 공급하는 유일한 공리이기 때문입니다. 다른 모든 공리는 상향 단조적입니다: 어딘가에서 어떤 술어를 더 참으로 만듦으로써 만족되며, 게으른 최적화기라면 모든 개인에 대해 모든 술어를 1로 밀어붙이는 것만으로 이들 모두를 한꺼번에 만족시킬 수 있습니다. 분리성만이 이를 벌합니다: ABox가 Stud(carol)을 1을 향해 밀어붙일 때, 사례 진리값 이 높게 유지되려면 Prof(carol)이 0을 향해 밀려나는 수밖에 없습니다. 그 그래디언트 는 술어를 아래로 누르며, 함의들의 부정적 전건 압력(후건이 1로 포화되면 사라지는 편미분)과 달리, 이 압력은 포화 상태에서도 지속됩니다: 분리성은 만족을 위해 술어를 0을 향해 밀어붙여야 하는 유일한 공리이며, 이것이 바로 학습된 평면에서 Professor 영역과 Student 영역을 갈라 조각해 내는 것이지, 그렇지 않으면 둘 다 보편적 진리라는 하나의 덩어리로 녹아 버렸을 것입니다.
정직함을 지키는 탐침들
0.9933이라는 만족도 점수는 훈련이 작동했음을 말해 줄 뿐, 모델이 조회 테이블이 아니라 논리를 학습했음을 말해 주지는 않습니다. 그래서 커밋된 실행은 공리별 훈련 목표였던 적이 없는 질의들로 훈련된 그라운딩을 심문하며, 모든 판정을 단언합니다(ltn.py 540–557행):
[6] the learned world — truth values for the five people
(Researcher and Person are NEVER asserted: the subsumption
ladder alone entails them — gradient descent as inference)
individual Prof Stud Researcher Person
alice 0.9991 0.0014 0.9988 0.9979
bob 0.9990 0.0014 0.9985 0.9976
carol 0.0008 0.9999 0.9990 0.9987
dave 0.0004 0.9999 0.9983 0.9980
erin 0.0005 0.9999 0.9986 0.9984
entailed minima over the five: Researcher ≥ 0.9983, Person ≥ 0.9976
held-out probes:
Professor(carol) = 0.0008 (< 0.3 asserted; carol is typed Student)
max_x Prof(x)·Stud(x) = 0.0018 at x = p3 (< 0.25 asserted: disjointness holds everywhere)
the 4 asserted advises facts:
advises(alice,bob) 0.9995
advises(bob,carol) 0.9999
advises(bob,dave) 0.9998
advises(carol,erin) 0.9993
세 가지를 읽어 낼 수 있습니다. 첫째, Researcher 열과 Person 열은 창발적 함의(emergent entailment)입니다: 어떤 ABox 공리도 Researcher(alice)나 Person(carol)을 단언한 적이 없지만, 다섯 사람 모두 두 열에서 0.9976 이상으로 끝나는데, 이는 ABox가 그 전건들을 1로 유지하는 동안 사다리 함의들을 만족시킬 유일한 방법이 후건들을 참으로 만드는 것이기 때문입니다. 경사 하강법은 2권의 완성 알고리즘이 기호적으로 수행했던 추론을 수치적으로 수행한 것입니다. 둘째, Professor(carol)은 무지의 상태인 0.5가 아니라 0.0008에 자리 잡습니다: 그것이 거짓이라고 단언한 것은 아무것도 없지만, 분리성 공리가 Stud(carol) = 0.9999를 Prof(carol)에 대한 하향 압력으로 전달했습니다. 셋째, 2권에서 증명 가능하게 충족 불가능한 TenuredStudent 개념의 퍼지적 표현인 논리곱 는 13개 개인 전체에서 최대 0.0018을 기록하며, 이 탐침은 훈련이 그랬던 것보다 더 엄격하게 훈련된 값들을 읽어 냅니다: 분리성 공리의 훈련된 사례별 -평균을 엄격한 최댓값으로 대체하는 것입니다. 명확한 추론기는 그 개념이 비어 있음을 증명했고, 훈련된 그라운딩은 그것을 거의 비워 둡니다. 이것이 바로 성공이면서 동시에 그 간극의 정확한 척도입니다.
마지막 탐침은 퍼지 기둥 전체가 기대고 있는 주장, 즉 실수 논리가 고전 논리를 대체하는 것이 아니라 일반화한다는 주장을 검사합니다. 안의 값인 명확한 입력에서, 안정적 곱 논리 결합자들은 대수적으로 불 연산자와 같습니다: 는 AND이고, 는 OR이며, 는 NOT이고, 는 실질 조건문입니다. 동반 코드는 네 진리표의 모든 모서리를 오차 허용 없이 정확한 동등성으로 단언하며(ltn.py 467–472행), 그런 다음 명확한 지시 벡터 위에서 완전한 한정된 공리 하나를 평가합니다(ltn.py 474–498행). Researcher를 그 고전적 폐포(교수들과 학생들 위에서 정확히 1인 명확한 지시 벡터로, 포섭 사다리가 함의하는 바로 그 집합입니다)로 취한 의 경우, 모든 사례가 정확히 1이므로 오차 평균은 정확히 0이고 클램핑되지 않은 는 정확히 을 반환합니다. 이는 참인 전칭 명제의 고전적 진리값입니다(클램프는 훈련 가능성을 위한 장치이며 여기서는 꺼져 있습니다, 이 명확한 1을 으로 옮겨 버릴 것이기 때문입니다). 고전적으로 거짓인 공리 가 더 유익한 흔적을 남기며, 인쇄된 0.6078은 손으로 재현할 수 있습니다. 사례 벡터는 두 명의 교수 alice와 bob에서 을, 나머지 열한 명의 개인에서 을 가지므로, 열세 명의 개인에 걸쳐 오차 벡터는 1이 두 개, 0이 열한 개입니다:
이 판정은 퍼지화 이후에도 살아남지만(참인 공리는 정확히 1에, 거짓인 공리는 1보다 엄격히 아래에, 위반하는 사례 자체는 정확히 0에 자리합니다), 그 값 0.6078은 등급이 매겨진 것이지 고전적인 딱딱한 0이 아닙니다; 그것을 회복하려면 위에서 유도한 괴델 극한인 가 필요할 것입니다. 이것이 바로 퍼지 논리와 고전 논리 사이의 연속성 주장을 검사 가능하게 만든 것입니다: 산문 속의 주장이 아니라 커밋된 코드 안의 assert 문에 의해 지탱됩니다.
만족을 넘어서: 훈련된 그라운딩은 무엇에 쓰이는가
SatAgg를 극대화하는 것은 학습이지만, 훈련된 그라운딩은 자기 자신의 훈련 목표 이상을 지원합니다 [1]. 질의는 즉각적입니다: 훈련 중에 전혀 본 적 없는 것을 포함하여 이 언어의 어떤 닫힌 논리식이든 최종 매개변수 아래에서 진리도로 평가됩니다; 위의 보류된 탐침들이 정확히 이것입니다. 반박에 의한 추론(reasoning by refutation)은 그 기계 장치를 뒤집습니다: 이론이 를 함의하는지 묻기 위해, 를 추가하고 만족도를 극대화하려고 시도합니다; 만약 어떤 매개변수 설정도 증강된 이론을 높은 정도로 충족 가능하게 유지하지 못한다면, 그 실패한 탐색 자체가 함의에 대한 증거가 되며, 반대로 그 탐색이 성공한다면, 그렇게 찾아낸 그라운딩은 이론은 만족시키면서도 는 거짓으로 만드는 것이고, 그 자체가 함의를 반박하는 반례가 됩니다. 그리고 이 프레임워크의 초기 대표 응용은 의미론적 이미지 해석(semantic image interpretation)으로, 여기서 개인은 학습 가능한 임베딩이 아니라 탐지된 객체들의 특징 벡터로 그라운딩되어, 공리들이 지각 신경망의 출력을 논리적 일관성 쪽으로 정규화합니다 [4]; 그 설계는 임베딩 행렬을 시각 모델의 출력으로 바꾼 ltn.py입니다.
정직한 비용은 계산의 형태 안에 쓰여 있습니다. 논리식을 그라운딩하는 것은 사례를 열거하는 일입니다: 한정된 변수 하나가 개의 개인에 걸쳐 있으면 번의 평가가 들고, 개의 서로 다른 한정 변수는 번, 즉 에 대해 지수적으로 듭니다. 우리의 중첩된 공리는 이미 에 대해 짜리 격자를 채웁니다; 같은 공리를 개의 개체를 가진 지식 그래프에 적용하면 에폭당 개의 쌍 평가가 필요할 것입니다. 이 프레임워크는 그 탈출구들의 이름을 제시합니다: 대각 한정화(diagonal quantification)는 전체 곱집합 격자 대신 공유된 하나의 인덱스를 따라가는 쌍을 이룬 튜플에 대해 한정하며, 보호된 한정화(guarded quantification)는 신경망 평가가 실행되기 전에 값싼 기호적 조건을 만족하는 사례들로만 제한하여 를 그 보호 조건의 지지집합으로 줄입니다 [1]. 둘 다 컴파일러가 찾아 주는 최적화가 아니라 모델러가 선택해야 하는 정의역 제한입니다.
해결되지 않은 부분
실행이 끝맺는 숫자, SatAgg = 0.9933은 그 무엇의 증명도 아니며, 집계 수학은 정확히 왜 그런지를 말해 줍니다. 유한한 에서 는 평균이며, 평균은 국소적인 위반을 흡수합니다: 두 변수 전칭 명제의 169-사례 격자에서, 완벽한 168개 중 진리값이 0인 사례 하나만 있어도 가 되고 만족도는 이 됩니다. 하나의 공리가 격자 안에 구체적인 반례를 그대로 품은 채, 고전적으로는 그저 거짓이면서도 "92% 만족"으로 읽힐 수 있습니다. 2권의 추론기는 결코 이럴 수 없었습니다; 그 함의들은 모두-혹은-전무였고 유도를 동반했습니다. 둘째, 진리도는 보정된 확률이 아닙니다. 훈련된 모델이 advises(alice, bob)에 부여하는 0.9995는 그 무엇에 대한 99.95%의 확률도 아닙니다: 그것은 손실 압력에 의해 형성된 시그모이드 출력이며, 퍼지 논리 전통 자체가 진리도와 신뢰도가 서로 다른 법칙을 따르는 서로 다른 양이라고 명시적으로 말합니다 [5]. 2권의 숫자는 정확한, 모델-계수적 의미에서의 확률이었습니다; 실수 논리의 숫자는 만족도 다이얼 위의 위치이며, 그것들을 임계값으로 자르거나 술어들 사이에서 비교하는 데에는 의미론적 허가가 없습니다. 셋째, 기하학적 우연에 의한 만족을 막는 것은 아무것도 없습니다: 목표 함수는 13개의 점에서 평가된 23개의 공리를 통해 306개의 매개변수를 제약하며, MLP들은 거기서 잘 채점되는 한 어떤 방식으로든 평면을 조각할 자유가 있는데, 여기에는 훈련된 지점에서 조금만 벗어난 임베딩에서 공리를 심하게 위반하게 될 방식들도 포함됩니다. 보류된 탐침들은 실패할 수도 있었기 때문에 선택된 것입니다; 그것을 통과했다는 것은 증거이지 인증이 아닙니다. 만족도 극대화에 인증서(숨겨진 위반에 대한 경계, 그 등급의 보정, 훈련 격자 밖에서의 보장)를 부여할 수 있는지는 열려 있으며, 보장이 필요한 응용에 대한 이 분야의 실용적인 답은 기둥을 다시 바꾸는 것입니다: 2권의 회로가 지닌 정확성을 유지하고 대신 그 비용을 공략하는 것이며, 이것이 정확히 다음 장이 향하는 곳입니다.
왜 중요한가
이 장은 이 권의 두 번째 기둥을 완성합니다. DeepProbLog는 훈련 가능한 논리로 가는 확률적 경로를 보여 주었습니다: 정확한 의미론, 명제 논리적 핵심, 모델 계수를 통한 그래디언트입니다. 논리 텐서 네트워크는 퍼지 경로를 보여 줍니다: 한정된 1차 구문은 온전히 유지되고, 정확성은 포기되며, 일반화 평균을 통해 그래디언트가 흐릅니다. 이 권의 나머지 모든 통합 시스템은 이 두 극단이 정의하는 축 위 어딘가에 자리 잡으며, 이제 그 거래는 수사적인 것이 아니라 정량화된 것입니다: 여기서는 최악-우선 그래디언트 스케줄링을 동반한 0.9933의 집계값, 저기서는 컴파일 비용을 치른 정확한 질의 확률입니다. 여기서 기록된 실패 양상들은 5권에도 그대로 부담이 됩니다: 보정되지 않은 신뢰도와 평균으로 뭉개진 위반은 정확히 5권의 충실성(faithfulness) 및 보정(calibration) 장들이 캐묻는 신뢰 문제들이며, 안의 최악-사례 커리큘럼은 프론티어의 검증자-유도 훈련 루프를 미리 보여 줍니다.
핵심 용어
- 실수 논리(Real Logic): 논리 텐서 네트워크의 완전히 미분 가능한 1차 논리 언어; 1차 논리 구문, 안의 의미론, 그래디언트를 실어 나르도록 선택된 모든 연산자입니다.
- 그라운딩 : 기호에서 텐서로의 매핑; 상수는 학습 가능한 벡터로, 술어는 로 가는 미분 가능한 함수로, 논리식은 둘의 합성으로 갑니다.
- 안정적 곱 설정(stable product configuration): 권장되는 연산자 메뉴; 곱 t-노름, 확률적 합, 표준 부정, 라이헨바흐 함의 , 그리고 집계기에서의 클램프 입니다.
- 일반화 -평균(, ): 한정사 집계기; 는 이상치 민감도를 조절하고, 는 (의 경우) 최댓값을, (의 경우) 최솟값을 회복하며, 그래디언트 는 가장 심하게 위반된 사례들에 집중됩니다.
- SatAgg: 이론 전체의 집계된 진리값으로, 여기서는 공리별 진리값들에 대한 입니다; 훈련 손실은 입니다.
- 부정 압력(negative pressure): 부정된 공리(여기서는 분리성)가 진리값을 아래로 밀어내는 힘으로, 이것이 없으면 만족도 극대화는 "모든 것이 참이다"로 퇴화합니다.
- 명확한 복원(crisp recovery): 입력에서 실수 논리가 고전 논리로 붕괴하는 것으로, 동반 코드에서 정확히 단언됩니다.
- 대각/보호된 한정화(diagonal / guarded quantification): 개의 한정 변수가 갖는 그라운딩 비용에서 벗어나는 탈출구; 공유된 인덱스를 갖는 튜플이거나, 사례 격자에 대한 기호적 사전 필터입니다.
이 장이 이어지는 곳
실수 논리는 보장을 포기하는 대가로 1차 논리 구문을 얻었습니다; 2부의 회로는 보장을 유지했지만 컴파일과 CPU 위주의, 포인터를 따라가는 평가에서 그 대가를 치렀습니다. 그 비용에 대한 프론티어의 답은 새로운 의미론이 아니라 새로운 하드웨어 원칙입니다: 컴파일된 회로를 조밀한 텐서 층으로 평평하게 펴고, 신경 술어를 훈련시키는 것과 동일한 가속기 위에서 수백만 개의 세계-가중치 곱을 배치 처리하여, 정확한 추론이 대규모 훈련 루프 안에 들어갈 만큼 빠르게 만드는 것입니다. 그것이 다음 장인 GPU 네이티브 NeSy의 주제이며, 그곳에서 두 기둥은 우아함을 두고 경쟁하는 것을 멈추고 처리량(throughput)을 두고 경쟁하기 시작합니다.
동반 코드: examples/integration/ltn.py는 2권의 공리들을 306개 매개변수를 가진 실수 논리 모델로 그라운딩하고, 모든 그래디언트를 손으로 유도하며(중심 유한 차분법에 맞서 까지 인증됨), SatAgg를 0.5295에서 0.9933까지 훈련시키고, 이 장에서 인용된 모든 탐침을 단언합니다. 그 논리 결합자는 tnorms.py에서, 클램프는 fuzzy_grad.py에서, 공리는 examples/symbolic/ontology.py에서 임포트합니다. python3 examples/integration/ltn.py를 실행하면 모든 숫자를 재현할 수 있으며, 두 번의 실행은 바이트 단위로 동일한 출력을 인쇄합니다.