분포 의미론: 논리와 확률의 만남
📍 현재 위치: 2부 · 확률 논리와 회로 — 4장. 퍼지에서 신경망으로는 각 논리식에 붙는 미분 가능한 정도로서의 진리로 1부를 마무리했습니다; 이 장은 다른 갈래를 택해, 그 대신 확률을 세계 전체에 붙입니다.
1부는 정직한 청구서로 끝났습니다. 퍼지 파이프라인은 어떤 논리식이든 값싼 한 번의 상향 패스로 진리 정도를 계산해 내지만, 그 결과 값은 어떤 t-노름을 골랐는지에 따라 달라지고, 어느 선택이 옳은지 알려 주는 것은 그 기계 장치 어디에도 없습니다. 이 장은 가지 않은 길을 택합니다. 논리는 완전히 명확한 채로 남습니다: 규칙은 정확히 1권의 혼 규칙(Horn rule)들이며, 어느 한 상황 안에서든 모든 원자는 명백히 참이거나 명백히 거짓입니다. 불확실성은 다른 곳으로 옮겨 갑니다: 몇몇 사실들이 더 이상 확실하지 않고, 각각이 참일 확률을 지니게 됩니다. 이것을 모든 질의에 대한 확률로 바꾸어 주는 정의가 분포 의미론(distribution semantics) [1]이며, 이는 이 권 전체의 정확성 닻입니다: 컴파일된 회로에서 신경 술어에 이르기까지, 앞으로 이어지는 장들의 모든 시스템은 결국 이 장이 정의하는 숫자를 재현하는지 혹은 근사하는지에 따라 평가받습니다. 학술 세계에서는 모든 것이 완전히 열거할 수 있을 만큼 작으며, 바로 그 점이 다음 장이 계산의 벽에 부딪히기 전에 이 정의를 감사할 수 있게 해 줍니다.
탐정의 코르크판을 상상해 보십시오. 핀은 사실이고, 실은 추론 규칙이며, 대부분의 핀은 확고합니다. 하지만 그중 열한 개는 불안정해서, 각각에 "90% 확실함" 또는 "55% 확실함"이라고 적힌 포스트잇이 붙어 있습니다. "그 결론이 성립할 가능성은 얼마나 되는가?"에 답하기 위한 정직한 절차는 철저한 것입니다: 불안정한 핀들이 나올 수 있는 모든 경우의 수를 하나하나 따져 보고(각 핀은 버티거나 떨어지므로, 2 × 2 × ⋯ × 2 = 2,048가지 시나리오가 나옵니다), 각 시나리오 안에서는 그것이 확정된 사실인 양 평범하고 명확한 탐정 작업을 다시 수행하며, 그 특정 핀들의 조합이 얼마나 그럴듯했는지에 따라 각 시나리오에 가중치를 매기고, 결론이 따라 나오는 시나리오들의 총 가중치를 보고하는 것입니다. 어느 시나리오 안에서도 "60% 참"인 것은 결코 없습니다; 모든 시나리오는 완전히 고전적입니다. 확률이 측정하는 것은 오직 여러분이 어느 시나리오에 있는지에 대한 무지뿐입니다.
이 장에서 다루는 내용
- 1부로부터의 갈래: "진리함수적"이 정확히 무엇을 뜻하는지, 확률은 진리함수적이지 않다는 두 줄짜리 증명, 그리고 그 차이가 이 부의 정확성 대 다루기 쉬움이라는 궤적을 어떻게 설정하는지입니다.
- 확률적 프로그램: 학술 세계의 열한 개 간선이
distsem.py에서 독립적인 동전이 되는 동안, 1권의 규칙들은 손대지 않은 채 그대로 가져옵니다. - 정의, 형식화하기: 전체 선택, 세계 가중치, 성공 확률을 모든 기호를 해독하고 독립성 가정을 검토하며 다룹니다.
- 정직한 무차별 대입으로서의 정확한 추론: 커밋된 2,048개 세계 열거 루프, 정규화 증명, 그리고 실제 출력 옆에서 손으로 풀어 본 단일 증명 정합성 검사입니다.
- 이 장의 중심, 서로소-합 문제: 두 개의 겹치는 증명을 가진 질의에서 증명 곱들을 순진하게 더하면 1.575가 나오고, 그 초과분은 정확히 이중으로 헤아려진 논리곱임이 밝혀지며, 포함-배제가 커밋된 1e-12 허용오차 안에서 열거된 값 0.8865를 되찾습니다.
- 실행 가능하게 만든 단조성: 확률적 사실을 추가해도 성공 확률이 결코 낮아질 수 없다는 증명, 그리고 그것을 실행하는 커밋된 전후 비교 표입니다.
- 미해결 부분: 동전들의 독립성은 모델링상의 허구이며, 이 의미론은 그것이 무시하는 상관관계를 학습할 고유한 방법을 제공하지 않습니다.
논리에 숫자를 붙이는 두 가지 방법
선택을 내리기 전에 그 갈래를 정확히 진술해 봅시다. 어떤 의미론이 진리함수적(truth-functional)이라는 것은, 어떤 복합 논리식의 값이 그 직접적인 부분들의 값만의 고정된 함수이고, 그 밖의 어떤 것에도 의존하지 않는다는 뜻입니다. 1부의 퍼지 논리는 구성상 진리함수적입니다: 평가 는 각 원자에 구간 안의 정도를 부여하고, 논리곱은 그 논리곱 항들로부터 계산되어, 고른 t-노름 가 무엇이든 가 되는데, 여기서 와 는 임의의 논리식을 나타내고 쐐기 는 "그리고"라고 읽습니다. 두 입력 정도를 아는 것으로 항상 충분합니다; 논리식의 내력이나 그 부분들이 서로 어떻게 관련되는지는 결코 중요하지 않습니다.
확률은 이것을 거부합니다. 확률은 논리식이 아니라 세계(world), 즉 사물이 어떨 수 있는지에 대한 완전한 고전적 기술에 숫자를 붙이며, 어떤 논리식은 그것이 고전적으로 참인 세계들의 총 가중치로서 자신의 확률을 물려받습니다. 이렇게 읽으면, 논리곱의 확률은 증명 가능하게 그 부분들의 확률의 함수가 아닙니다. 증명은 두 줄짜리 반례입니다. 를 "공정한 동전이 앞면이 나온다"라고 합시다. 그러면 입니다. 먼저 로 두면, 는 그저 이고, 입니다. 이제 대신 로 둡시다(기호 는 "아니다"라고 읽습니다). 그러면 이기도 하지만, 는 모순이어서 어떤 세계에서도 참이 아니므로 입니다. 두 경우 모두 입력 숫자 쌍은 로 같지만 출력은 다르므로, 를 만족하는 어떤 함수 도 존재할 수 없습니다.
두 한계값 숫자가 실제로 고정하는 것은 하나의 구간입니다. 를 충족하는 모든 세계는 를 충족하므로, 세계 가중치를 합하면 가 되고, 대칭적으로 가 되어, 결국 논리곱은 많아야 입니다. 아래쪽 한계에 대해서는, 두 사건의 합집합에서 각 세계는 의 왼쪽에서는 한 번만 헤아려지지만(기호 는 "또는"이라고 읽으며, 두 사건의 합집합을 뜻합니다) 오른쪽에서는 한 번 또는 두 번 헤아려지므로 이 부등식이 성립한다는 점을 눈여겨봅시다. 두 번의 다시 쓰기가 이것을 그 한계로 바꿉니다. 첫째, 어떤 세계가 를 거짓으로 만드는 것은 정확히 그것이 를 거짓으로 만들거나 를 거짓으로 만들 때이므로, 는 와 정확히 같은 세계 집합을 가리킵니다. 둘째, 어떤 논리식과 그 부정 사이에서는 모든 세계가 정확히 한 번만 헤아려지므로, 임의의 논리식 에 대해 입니다. , , 를 대입하면 부등식은 가 되고, 정리하면(양변에 를 더하면) 이 나옵니다. 참값이 그 구간 안 어디에 떨어지는지는 전적으로 두 사건이 세계들의 공간에서 어떻게 겹치는지에 달려 있습니다. 겹침이라는 그 단어가 바로 이 장의 엔진입니다: 아래의 서로소-합 전시물은 어떤 추론 방식이 그것을 잊었을 때 정확히 무슨 일이 일어나는지를 보여 줍니다.
그러므로 이 갈래는 하나의 거래입니다.
| 1부: 퍼지 | 2부: 확률적 | |
|---|---|---|
| 숫자가 사는 곳 | 각 논리식 | 각 세계(전체 선택) |
| 논리곱 | 계산됨, | 부분들로부터 계산 불가능; 겹침에 의존 |
| 하나의 평가 안 논리 | 다치 | 각 세계 안에서 고전적 |
| 순진한 평가 비용 | 한 번의 상향 패스 | 개의 세계, 즉 개의 불확실한 사실들의 조합마다 하나씩; 일반적으로 계수 문제 |
| 숫자의 의미 | 정도, t-노름에 의존 | 확률, 구성상 정합적 |
오른쪽 열의 의미는 정확하고 그 비용은 지수적이며, 왼쪽 열의 비용은 선형이고 그 의미는 흔들립니다. 이 권의 이 부는 오른쪽 열의 값을 영리하게 치르는 이야기이며, 이 장은 정확히 무엇을 위해 그 값을 치르는지를 확립합니다.
확률적 프로그램: 학술 세계 위의 열한 개 동전
컴패니언 모듈 distsem.py는 1권의 지식 베이스 바로 위에 이 권의 첫 번째 확률적 논리 프로그램을 짓습니다. 그 임포트는 아무것도 다시 입력하기를 거부합니다(distsem.py 58–59행):
from kb import FACTS, RULES, is_var # noqa: E402 (the academic world, Vol 1)
from forward_chain import least_fixpoint # noqa: E402 (⊢ = the least fixpoint)
RULES는 손대지 않은 1권의 규칙 집합입니다(kb.py 73–89행): 교수와 학생으로부터 나오는 researcher와 person, advises와 advises의 합성으로서의 grandAdvisor, 공유된 소속으로부터 나오는 colleague, 그리고 인용의 이행적 폐포입니다. 이 규칙들 중 어느 것도 숫자를 얻지 않습니다. 바뀌는 것은 스물세 개의 기본 사실 가운데 열한 개의 지위입니다(distsem.py 71–83행):
PROB_FACTS: dict[tuple, float] = {
("advises", "alice", "bob"): 0.90,
("advises", "bob", "carol"): 0.90,
("advises", "bob", "dave"): 0.85,
("advises", "carol", "erin"): 0.90,
("cites", "p2", "p1"): 0.80,
("cites", "p3", "p2"): 0.90,
("authored", "alice", "p1"): 0.95,
("authored", "bob", "p1"): 0.90,
("authored", "carol", "p2"): 0.90,
("authored", "dave", "p3"): 0.85,
("affiliated", "erin", "cmu"): 0.55,
}
이 숫자들을 있는 그대로, 즉 잡음 섞인 증거(noisy evidence)로 읽으십시오. alice가 bob을 지도한다고 말하는 학과 기록은 강력하지만 오류가 없지는 않으므로, 지도 간선들은 0.85에서 0.90 사이에 놓입니다. 인용 사슬은 2권의 주석 달린 추론기가 그 동일한 간선들에 붙였던 확신도(0.9와 0.8)를 정확히 그대로 지니고 있습니다. 한 기록만은 진짜로 불안정합니다: erin의 소속은 0.55로, 동전 던지기보다 거의 나을 것이 없습니다. kb.py의 나머지 모든 사실, 즉 모든 단항 유형, 나머지 소속들, 논문 주제들은 확실한 상태로 남으며, 이 모듈은 그것들을 PROB_FACTS에서 빼놓음으로써 그 사실을 부호화합니다(확실한 나머지는 distsem.py 86행에 모여 있습니다).
두 독립적인 연구 계열이 이런 프로그램에 대해 같은 해석에 이르렀습니다. 논리 프로그래밍 쪽에서는, 주석이 달린 각 사실이 하나의 무작위 스위치이며 프로그램은 자기 자신의 접지들에 대한 분포를 정의합니다 [1]; 에이전트 쪽에서는, 같은 대상이 독립 선택 논리(independent choice logic)로 나타나는데, 여기서 주석 달린 사실들은 자연이 내리는 독립적인 선택이고 명확한 규칙들은 각 선택의 귀결을 결정론적으로 펼쳐 냅니다 [2]. 표기법 p :: f는 ProbLog의 것이며, 위의 열한 개 동전짜리 프로그램은 축소판 ProbLog 프로그램입니다 [3]; 이 의미론 자체는 ProbLog가 이런 식으로 이 구성을 명명하기 십 년 전부터 이미 더 앞선 시스템들에서, 그중에서도 가장 먼저 Sato와 Kameya의 PRISM(PRogramming In Statistical Modeling)에서 돌아가고 있었습니다 [4].
여기 어떤 수식이 등장하기도 전에 해독된, 이 의미론의 전부가 있습니다. 열한 개의 동전을 모두 독립적으로 던집니다: 동전 는 자신의 확률 로 참이 나옵니다. 그 결과는 열한 개 사실 가운데 한 부분집합을 고르고, 그 부분집합은 열두 개의 확실한 사실과 함께 하나의 가능 세계(possible world), 즉 완전히 고전적인 하나의 상황을 이룹니다. 그 세계 안에서, 1권의 평범한 전방 연쇄기를 그 최소 고정점(least fixpoint)까지 돌립니다; 그 세계는 명확하게, 자신이 도출하는 것을 도출합니다. 어떤 질의의 확률은 그것이 도출 가능한 것으로 나오는 세계들의 총 가중치입니다. 그것이 정의의 전부입니다. 이 장의 나머지는 모두 신중하게 이루어지는 장부 정리일 뿐입니다.
정의, 형식화하기
이제 같은 정의를 기호로, 도착하는 즉시 하나하나 해독하며 표현해 봅시다. 확률적 사실(probabilistic fact)들의 집합을 로 쓰고(여기서는 PROB_FACTS의 열한 개 키입니다), 그 개수를 로 씁니다(막대 기호 는 집합의 크기를 나타내므로, 입니다). 각 사실 (기호 는 "의 원소이다"라고 읽습니다)는 확률 을 지닙니다. 확실한 사실들(나머지 열두 개의 kb.py 사실들)의 집합을 로, 규칙들의 집합을 로 씁니다. 전체 선택(total choice)이란 부분집합 (기호 는 "의 부분집합이다"라고 읽습니다)로, 참으로 나온 동전들의 집합입니다. 독립성은 전체 선택의 확률을 동전 하나당 인자 하나씩을 갖는 곱으로 만듭니다.
여기서 는 곱 기호이며(나열된 각 원소에 대해 인자 하나씩을 곱하는데, 이 나열된 각 원소에 대해 항 하나씩을 더하는 것과 같습니다), 는 집합 차, 즉 선택되지 않은 동전들입니다. 선택된 각 동전은 자신의 확률 를 기여하고, 탈락한 각 동전은 거짓이 나올 확률 를 기여합니다.
이 개의 가중치는 진짜 확률분포를 이룹니다: 그것들은 음이 아니고, 합이 1입니다. 그 증명은 한 번은 전체를 볼 만한 가치가 있는 곱 전개입니다. 동전 를 가진 인 경우를 봅시다. 네 개의 전체 선택은 다음의 가중치를 가집니다.
첫 번째 쌍과 두 번째 쌍을 공통 인자로 묶으면 다음이 나옵니다.
같은 묶음이 임의의 에 대해서도 통합니다: 곱 을 전개하면 정확히 부분집합 마다 하나씩의 항으로 분배되는데, 이는 각 에 대해 를, 각 에 대해 를 고르는 항입니다(기호 은 "의 원소가 아니다"라고 읽습니다). 이는 정확히 입니다. 따라서
두 개의 기호가 더 있으면 정의가 완성됩니다. "질의 가 선택된 사실들과 확실한 사실들과 규칙들로부터 도출 가능하다"를 로 씁니다: 기호 는 합집합으로, 그 세 집합을 하나의 사실-겸-규칙 베이스로 합치며, 턴스타일 는 "도출한다"라고 읽습니다. 이 권에서 도출 가능성은 곧 1권의 전방 연쇄기입니다: 가 도출 가능한 것은 정확히 그것이, 아무것도 새로 나타나지 않을 때까지 규칙을 발화시켜 least_fixpoint가 계산하는 최소 고정점에 속할 때입니다(forward_chain.py 52–63행). 의 성공 확률(success probability)은 그렇다면 도출하는 세계들의 총 가중치입니다 [1].
여기서 은 지시함수(indicator)로, 괄호 안의 진술이 성립하면 이고 성립하지 않으면 인 함수입니다. 두 번째 형태, 즉 세계들에 대한 지시함수의 기댓값으로서의 확률은 표현을 바꾼 것처럼 보이지만, 아래의 서로소-합 유도에서 실제로 일을 하게 됩니다. 이 정의가 아닌 것을 눈여겨보십시오: 이것은 부분 논리식 점수들을 결합하는 규칙이 아닙니다. 는 세계들을 거쳐 계산되는 프로그램 전체의 속성이며, 부분들의 어떤 지역적 결합도 그 값에 이른다는 보장이 없습니다. 그것이 바로 갈래 절의 비진리함수성이 하나의 정의로 구현된 것입니다.
이 정의를 떠받치는 가정은 독립성(independence)입니다: 동전들은 각각 따로 던져지므로, 동전 결과들의 어떤 조합의 확률이든 위의 곱으로 인수분해됩니다. 이것은 진짜 모델링상의 제약입니다. 이 언어는 "이 두 지도 기록은 같은 결함 있는 데이터베이스에서 나왔으므로 함께 실패한다"거나 "bob은 carol 또는 dave를 지도하지만, 둘 다는 아니다"를 직접적으로 말할 수 없습니다: 그런 결합은 독립적인 동전만으로는 아예 표현할 수 없습니다. 표준적인 탈출구는 주석 논리합(annotated disjunction)으로, 이는 여러 대안적 헤드가 하나의 선택을 공유하게 하여 그중 정확히 하나(또는 아무것도)가 발화하게 하는 구성입니다 [5]; 이것과 이를 일반화하는 신경 술어들은 DeepProbLog 장에 속합니다. 지금으로서는 이 프로그램이 독립성 안에서 정직하게 살아가며, 이 장은 그것이 무엇을 사 주는지를 검토합니다.
처음부터 끝까지의 분포 의미론: 명확한 규칙들 위의 열한 개 독립적인 동전, 자신의 고정점까지 전방 연쇄되고 가중치가 매겨지는 모든 전체 선택, 그리고 순진한 증명 합산이 공유된 동전의 겹침만큼 정확히 초과 계수하는 서로소-합 전시물.
저자가 AI의 도움을 받아 직접 제작한 원본 도해.
정직한 무차별 대입으로서의 정확한 추론
이 정의는 의 모든 부분집합에 걸쳐 양화하며, 학술 세계 규모에서 정직한 방법은 정확히 그것을 하는 것입니다: 개의 전체 선택 전부를 실체화하고, 각각을 전방 연쇄한 다음 합산합니다. 컴패니언은 이 정의를 문자 그대로 실행합니다(distsem.py 130–143행):
# Each integer 0 .. 2^n - 1 is one total choice: bit i decides coin i.
for bits in range(1 << n):
chosen: list[tuple] = []
# P(F) = Π_{f ∈ F} p_f · Π_{f ∉ F} (1 − p_f) (independent coins)
p_world = 1.0
for i in range(n):
if bits >> i & 1:
chosen.append(atoms[i])
p_world *= probs[i]
else:
p_world *= 1.0 - probs[i]
# model_F = lfp(T_{F ∪ C ∪ R}) — everything world F derives (Vol 1).
model = least_fixpoint(certain + chosen, RULES)
table.append((p_world, frozenset(model)))
부터 까지의 각 정수는 하나의 부분집합을 이진수로 부호화합니다: 비트 가 동전 를 결정하고, p_world는 곱 를 인자별로 누적하며, least_fixpoint는 그 세계가 무엇을 도출하는지 계산합니다. (가중치, 고정점) 쌍들로 이루어진 결과 표가 바로 분포 의미론을 풀어 쓴 것이며, 이 함수는 열두 개를 넘는 동전을 거부하는 단언으로 자신의 지수적 정직성을 지킵니다(distsem.py 125행). 그렇다면 어떤 질의의 확률은 그 표에 대한 필터링된 합이며(distsem.py 160–169행), math.fsum을 써서 개 항의 덧셈이 정확히 반올림되도록 함으로써 이 장의 1e-12 비교가 부동소수점 잡음이 아니라 의미론 자체를 검사하도록 합니다. 한 가지 미묘한 점은 자신만의 함수를 얻을 자격이 있습니다: 대문자 Z가 논리 변수인 grandAdvisor(alice, Z)와 같이 변수를 담은 질의는 존재 한정 질의(existential query)로, 어떤 도출된 원자가 그것과 단일화될 때 어느 한 세계에서 충족됩니다; holds가 이 성공 기준을 구현합니다(distsem.py 149–157행).
커밋된 실행은 정규화 증명이 약속했던 정합성 검사로 시작합니다.
[2] sanity: the 2048 world weights form a distribution
Σ_F P(F) = 1.000000000000 (must be exactly 1)
P(professor(alice)) = 1.000000000000 (a certain fact holds in every world)
확실한 사실은 모든 세계에서 성립하므로 그 성공 확률은 가중치 전체를 모으고, advises(erin, alice)처럼 어떤 세계도 도출하지 못하는 원자는 아무것도 모으지 못하며, 이 모듈은 둘 다를 단언합니다(distsem.py 233–236행).
첫 번째 실질적인 정리는 단일-증명 경우입니다. 질의 가 정확히 하나의 증명만을 가지며, 동전 를 소비한다고 합시다(증명 안의 확실한 사실은 어디서나 성립하므로 무시해도 됩니다). 그러면 가 세계 에서 도출 가능한 것은 정확히 개의 동전이 모두 안에 있을 때이며, 양쪽 방향 모두 한마디씩 살펴볼 가치가 있습니다. 개의 동전이 모두 안에 있다면, 그 증명이 소비하는 모든 사실이 존재하므로 그 규칙 발화가 하나하나 성립하여 고정점이 를 포함하게 됩니다; 가 우연히 담고 있는 다른 어떤 동전도 그 발화를 막을 수 없는데, 이는 두 절 아래에서 증명될 단조성의 특수한 경우입니다. 역으로, 를 도출하는 세계는 그 세계 안에 존재하는 사실들만으로 완전히 이루어진 의 증명을 적어도 하나 뒷받침하며, 가정에 의해 증명은 오직 하나뿐이므로 그 개의 동전이 모두 안에 있어야 합니다. 따라서 성공 확률은 그 증명이 고정하는 동전들과 그것이 결코 언급하지 않는 동전들로 나뉩니다. 언급되지 않은 동전들을 라고 씁시다; 도출하는 모든 세계는 고정된 부분과 자유로운 부분 의 서로소 합집합이며, 곱 는 그에 따라 인수분해됩니다.
여기서 마지막 단계는 언급되지 않은 동전들에 정규화 항등식을 적용한 것입니다: 그것들의 가중치는 합이 이 되므로 소거되어 사라집니다. 독립성은 논리곱을 곱셈으로 만들지만, 그것은 오직 무관한 모든 것에 대한 합이 무너져 사라지기 때문입니다. 커밋된 실행은 이를 증명이 유일한 세 질의에서 검사합니다.
[3] one-proof queries: P(q) = the product of the proof's coin probs
query enumeration product |diff|
grandAdvisor(alice, carol) 0.810000000000 = 0.90 · 0.90 0.0e+00
citesTransitively(p3, p1) 0.720000000000 = 0.90 · 0.80 0.0e+00
colleague(carol, erin) 0.550000000000 = 0.55 0.0e+00
첫 번째 줄을 손으로 풀어 봅시다. grandAdvisor(alice, carol)의 유일한 증명은 bob을 거쳐 예화된 규칙 grandAdvisor(X, Z) ← advises(X, Y), advises(Y, Z)이며(kb.py 79행), 이는 인 동전 advises(alice, bob)과 인 advises(bob, carol)을 소비합니다; 공식은 을 주고, 2,048개 세계 전부에 대한 열거는 0.810000000000을 돌려주어 차이가 전혀 없습니다. 세 번째 줄은 조용히 시사하는 바가 있습니다: colleague의 증명은 확실하여 인자 을 기여하는 affiliated(carol, cmu)와 불안정한 동전인 affiliated(erin, cmu)를 사용하므로, 그 곱은 그저 입니다.
서로소-합 문제
지금까지의 모든 것은 하나의 솔깃한 지름길을 시사합니다: 질의의 증명들을 찾고, 각 증명의 동전 확률들을 곱한 다음, 그 곱들을 더하는 것입니다. 증명이 하나일 때는 앞 절이 이것을 정확하다고 증명했습니다. 증명이 둘일 때는 틀리며, 커밋된 전시물은 그것이 최대한 시끄럽게 실패하는 모습을 보여 줍니다.
존재 한정 질의 grandAdvisor(alice, Z), 즉 "alice는 누군가의 grand-advisor이다"는 이 프로그램 아래에서 정확히 두 개의 접지 증명을 가집니다(distsem.py 207–209행). 둘 다 bob을 거쳐 내려갑니다.
- 증명 A, carol을 거침: 동전 advises(alice, bob)과 advises(bob, carol), 곱 .
- 증명 B, dave를 거침: 동전 advises(alice, bob)과 advises(bob, dave), 곱 .
증명 곱들의 순진한 합은 입니다. 이는 을 넘으므로 그저 부정확한 것이 아니라 아예 확률이 아닙니다. 그 진단은 갈래 절이 경고했던 바로 그 겹침입니다. 를 "증명 A의 동전이 모두 참으로 나왔다"는 사건이라 하고, 를 증명 B에 대한 그런 사건이라 합시다. 질의는 합집합 위에서 성공하지만, 이 두 사건은 결코 서로소가 아닙니다: 이들은 동전 advises(alice, bob)을 공유하므로, bob의 지도 기록 전체가 살아남아 두 증명이 모두 통과하는 세계들은 안에서 한 번, 안에서 또 한 번 헤아려집니다.
정확한 수정은 포함-배제(inclusion-exclusion)이며, 정의의 지시함수 형태는 그 증명을 네 줄짜리 진리표 확인으로 만듭니다. 임의의 두 사건에 대해, 지시함수들은 다음을 만족합니다.
이는 경우를 하나씩 짚어 확인됩니다: 둘 다 성립하지 않으면 양변 모두 이고, 정확히 하나만 성립하면 양변 모두 이며, 둘 다 성립하면 오른쪽은 로 왼쪽과 일치합니다. 양변에 세계 가중치 를 곱하고 모든 에 대해 합산하면, 각 지시함수의 합은 의 정의에 의해 확률이 됩니다.
다시 정리하면 입니다: 순진한 합은 진짜 값을 정확히 두 증명이 모두 통과할 확률, 즉 이중으로 헤아려진 영역만큼 초과합니다. 그 줄 위의 모든 양은 여기서 계산 가능합니다. 논리곱 는 두 증명의 동전 집합의 합집합 안에 있는 모든 동전이 참일 때 성립하며, 공유된 동전은 한 번만 헤아려지므로, 그 세 개짜리 동전 집합에 단일-증명 인수분해를 적용하면
이고, 포함-배제는 다음을 예측합니다.
컴패니언은 이 세 숫자를 모두 계산하여 정확한 열거와 대조합니다(distsem.py 248–262행):
p_a = proof_probability(DS_PROOF_A) # 0.9 · 0.9 = 0.81
p_b = proof_probability(DS_PROOF_B) # 0.9 · 0.85 = 0.765
naive = p_a + p_b # sum of proof products
# P(A ∧ B) = Π over the UNION of the two proofs' coins — the shared coin
# advises(alice, bob) is counted ONCE: 0.9 · 0.9 · 0.85 = 0.6885.
p_both = proof_probability(sorted(set(DS_PROOF_A) | set(DS_PROOF_B)))
# Inclusion–exclusion: P(A ∨ B) = P(A) + P(B) − P(A ∧ B).
incl_excl = naive - p_both
p_exact = P_query(DS_QUERY)
assert naive > 1.0, "the exhibit needs the naive sum to exceed 1"
assert naive - p_exact > 0.5, "naive sum should overcount by P(A ∧ B)"
assert abs((naive - p_exact) - p_both) < TOL, (
"the overcount must be exactly the doubly-counted P(A ∧ B)")
assert abs(incl_excl - p_exact) < TOL, (
f"inclusion-exclusion {incl_excl} != enumeration {p_exact}")
커밋된 출력은 단언들이 요구하는 1e-12 허용오차보다 훨씬 안쪽에서 열거와 일치합니다.
[4] the disjoint-sum problem: grandAdvisor(alice, Z) has two proofs
that SHARE the coin advises(alice, bob)
proof A {advises(alice,bob), advises(bob,carol)} product = 0.8100
proof B {advises(alice,bob), advises(bob,dave)} product = 0.7650
naive sum of proof products = 1.575000000000 <- exceeds 1: not a probability
P(A ∧ B), shared coin ONCE = 0.688500000000 = 0.90 · 0.90 · 0.85
inclusion-exclusion = 0.886500000000 = naive − P(A ∧ B)
exact enumeration = 0.886500000000 (agrees to 1.1e-16)
일반적인 교훈은 온전히 진술할 가치가 있습니다. 이 권의 절반이 그것에 답하기 때문입니다. 증명은 서로소 사건이 아닙니다. 증명들을 독립적으로 채점하여 더하는 어떤 추론 방식이든 그것들이 서로소라고 암묵적으로 가정하는 것이며, 그 겹침에 대해 해명해야 합니다. 증명이 둘일 때는 수리가 뺄셈 항 하나로 끝나지만, 증명이 개 겹칠 때는(문자 은 증명의 개수를 세며, 는 위에서 이미 증명 하나당 동전 개수를 세는 데 쓰였으므로 남겨 둡니다) 포함-배제가 그 개 증명의 공집합 아닌 부분집합마다 하나씩인 개의 부호 붙은 항으로 전개되어, 수리 자체가 지수적으로 커집니다. 체계적인 해법은 증명들에 대해 합산하는 일을 아예 그만두고, 대신 질의를 명제 논리식에 대한 가중 계수로 환원하는 것으로, 여기서는 어떤 세계가 몇 개의 증명을 뒷받침하든 상관없이 정확히 한 번만 헤아려집니다 [6]. 그 환원이 다음 장의 주제이며, 이 전시물이 바로 그것이 존재하는 이유입니다.
실행 가능하게 만든 단조성
이 의미론은 그 밑에 놓인 명확한 논리로부터 하나의 구조적 정리를 물려받습니다: 확률적 사실을 추가해도 어떤 성공 확률도 결코 낮아지지 않습니다. 증명에는 두 개의 층이 있습니다. 하나는 도출 가능성에 관한 것이고, 다른 하나는 가중치에 관한 것입니다.
도출 가능성 층은 1권의 고정점을 다시 읽은 것입니다. 여기의 프로그램들은 한정(definite)됩니다: 모든 규칙은 하나의 긍정 헤드와 긍정 원자들로 이루어진 몸체를 가지며, 도출된 사실이든 기본 사실이든 어디에도 부정이 없습니다. 그런 프로그램에서는 즉각-귀결 연산자가 자신의 사실 집합에 대해 단조적입니다: 더 작은 사실 집합에서 이용 가능한 어떤 규칙 발화든 더 큰 집합에서도 여전히 이용 가능한데, 더 작은 집합에 속함으로써 충족되는 몸체 원자는 그 초집합에서도 충족되기 때문입니다(forward_chain.py 42–49행). 몸체 원자 하나는 사실 조회가 아닙니다: colleague 규칙은 내장된 부등식 가드 neq(X, Y)를 지니고 있으며(kb.py 82–83행), 엔진이 이를 처리하는 방식(forward_chain.py 30–34행)은 정확히 그 두 접지된 인자가 서로 다를 때 성공하는데, 이 검사는 사실 집합을 전혀 참조하지 않으므로 사실이 추가될 때도 그 충족은 그대로 보존되고 논증은 아무 수정 없이 그대로 통합니다. 연쇄 라운드에 대한 귀납법에 의해, 더 작은 프로그램이 라운드 까지 도출하는 모든 원자는(라운드 계수는 새로운 글자를 씁니다. 는 이미 위에서 증명의 동전 개수를 세는 데 쓰였기 때문입니다), 더 큰 프로그램도 라운드 까지 도출합니다. 그러므로 임의의 두 사실 집합 (가 더 큰 집합)에 대해, 최소 고정점들은 을 만족합니다(화살표 는 "함의한다"라고 읽으며, 왼쪽이 성립할 때는 언제나 오른쪽도 성립한다는 뜻입니다). 사실을 추가하는 것은 오직 결론을 추가할 수 있을 뿐입니다.
가중치 층은 이것을 확률로 바꿉니다. 확률 을 가진 새 동전 을 프로그램에 추가합니다. 기존의 모든 전체 선택 는 정확히 두 개의 새로운 선택, 즉 가중치 를 갖는 자신과 가중치 를 갖는 로 나뉘며, 이 두 가중치는 다시 로 합쳐지므로 새 분포는 질량을 어디로도 옮기지 않은 채 기존 분포를 세분할 뿐입니다. 이제 이 쌍들끼리 새 세계들을 묶어 임의의 질의 의 새 성공 확률을 계산해 봅시다.
여기서 는 로부터의 도출 가능성을 줄여 쓴 것입니다. 도출 가능성 층에 의해 입니다: 확장된 세계는 원래 세계가 도출하는 모든 것을 도출합니다. 이 부등식을 항별로 대입하면
어떤 성공 확률도 떨어질 수 없습니다. 컴패니언은 이 정리를 그저 신뢰하는 대신 실제로 실행합니다(distsem.py 264–284행): 동전 0.5 :: cites(p3, p1)을 추가하는데, 이는 2권의 주석 달린 추론기가 확신도 0.5로 지니고 있던 바로 그 불확실한 직접 인용이며, 세계의 개수를 개로 두 배로 늘린 다음, 여섯 개의 질의를 다시 묻습니다(표에서 Δ 열은 변화량, 즉 이후에서 이전을 뺀 값입니다).
| 질의 | 이전 | 이후 | Δ |
|---|---|---|---|
| citesTransitively(p3, p1) | 0.720000000000 | 0.860000000000 | +0.1400 |
| citesTransitively(p2, p1) | 0.800000000000 | 0.800000000000 | +0.0000 |
| grandAdvisor(alice, Z) | 0.886500000000 | 0.886500000000 | +0.0000 |
| grandAdvisor(alice, carol) | 0.810000000000 | 0.810000000000 | +0.0000 |
| colleague(carol, erin) | 0.550000000000 | 0.550000000000 | +0.0000 |
| person(erin) | 1.000000000000 | 1.000000000000 | +0.0000 |
그 패턴은 정확히 두 증명 층이 예측하는 그대로입니다. 새 간선이 닿을 수 없는 다섯 개의 질의는 소수점 열두 자리까지 변하지 않습니다(이 모듈은 대표 사례 하나인 grandAdvisor(alice, Z)에 대해 1e-12 허용오차 안에서의 불변성을 단언하고, distsem.py 282–284행, 여섯 개 전부에 대해 감소하지 않음을 272행에서 단언합니다). 유관한 질의 하나는 상승하며, 그것도 계산 가능한 양만큼 상승합니다: citesTransitively(p3, p1)은 이제 두 개의 증명을 가지는데, 0.9와 0.8의 동전을 소비하는 p2를 거치는 기존 사슬과, 새로 생긴 0.5의 동전만을 소비하는 새 직접 간선입니다. 이 두 증명은 어떤 동전도 공유하지 않으므로, "사슬이 성공한다"와 "직접 간선이 성공한다"는 사건은 독립적이며, 독립성은 실패 확률들이 곱해지도록 허용합니다: 질의는 두 증명이 모두 실패할 때만 실패하므로,
이것은 두 증명의 노이즈-오어(noisy-or)로, 동전을 공유하지 않는 특수한 경우에는 포함-배제가 여집합의 곱으로 단순화됩니다(독립성 아래에서 성립하는 를 대입하면 가 되고, 이는 로 인수분해됩니다; 곱을 전개해 확인해 보십시오). 커밋된 실행은 숫자와 구조를 모두 확인해 줍니다.
relevant ct(p3,p1) rises as the noisy-or of its two now-disjoint
proofs: 1 − (1 − 0.72)(1 − 0.50) = 0.860000000000 = 0.860000000000
단조성은 정합성 정리이지만, 동시에 하나의 한계를 미리 보여 주기도 합니다: 명확한 확률적 프로그램은 오직 믿음을 축적할 수만 있을 뿐 결코 그것을 철회할 수 없으므로, 어떤 결론에 반하는 증거는 들어올 방법이 없습니다. 언어에 부정을 추가할 수는 있지만, 그 대가로 어떤 세계가 무엇을 도출하는지에 대한 훨씬 더 신중한 설명이 필요해집니다. 이 권은 그 정리가 깔끔하고 추론기가 1권 그대로인 명확한 핵심에 머무릅니다.
이 의미론이 사는 것, 그리고 미루는 것
갈래 절이 약속했던 거래를 따져 봅시다. 자산 쪽에서는, 숫자 가 어떤 알고리즘이 돌아가기도 전에 고정된 의미를 갖습니다: 그것은 모델링하는 사람이 사실 하나하나에 대해 진술한 분포 아래에서, 를 도출하는 세계들의 가중치입니다. 이것은 구성상 확률적으로 정합적이며(가중치는 음이 아니고 합이 1이며, 확실한 결론은 확률 1을, 불가능한 결론은 확률 0을 얻습니다), 논리가 단조로운 곳에서는 이것도 단조롭고, 어떤 세계 안에서든 논리는 정확히 고전적이므로 어떤 t-노름 선택도 답을 구부릴 수 없습니다. 1부가 "어떤 퍼지 논리곱이며, 애초에 0.72는 무엇을 뜻하는가?"를 물어야 했던 곳에서, 이 장의 0.8865는 단 하나의 해석만을 허용합니다: 진술된 증거 모델 아래에서, alice가 누군가를 grand-advise하는 세계들이 가중치의 88.65%를 차지한다는 것입니다. 부채 쪽은 이 장이 정중하게 계속 부딪혔던 벽입니다: 이 정의는 개의 세계에 대해 합산하며, 그 각각은 완전한 전방 연쇄 패스를 필요로 하는데, 여기서는 2,048행짜리 표였던 그 열거가 실제 지식 베이스 규모에서는 모든 물리적 계산을 넘어섭니다. 그래서 두 개의 유예가 예정되어 있습니다. 다루기 쉬움의 유예는 질의를 명제 논리식에 대한 가중 계수로 환원하여, 증명들 사이의 공유된 구조가 지수적으로 여러 번이 아니라 한 번만 처리되게 합니다 [6]; 이것이 다음 장의 주제입니다. 표현력의 유예, 즉 네트워크가 동전 확률을 공급하게 해 주는 주석 논리합과 신경 술어는 DeepProbLog 장의 몫입니다.
미해결 부분
독립성 가정은 엄청나게 크면서도 조용한 일을 하고 있으며, 그것은 모델링상의 허구입니다. 같은 교수에 관한 두 지도 기록은 현실에서 독립적이지 않습니다: bob의 학과 기록이 부실하게 관리되어 있다면, advises(bob, carol)과 advises(bob, dave)는 함께 의심스러우며, 하나를 확증하면 다른 하나에 대한 확신도 올라가야 합니다. 분포 의미론은 이것을 직접적으로 말할 수 없습니다; 그 동전들은 명령에 의해 하나씩 따로 실패합니다. 표준적인 임시방편은 잠재 구조를 손으로 설계하는 것입니다: reliable(bob) 같은 보조적인 확률적 사실을 도입하고, 두 지도 간선 모두를 그것을 참조하는 규칙을 거치도록 배선하여, 상관관계가 프로그램 안의 공유된 계보를 통해 흐르게 하는 것입니다. 이것은 통하지만, 누가 그 사고를 했는지 눈여겨보십시오: 모델링하는 사람이 그 잠재 사실과 그 확률과 그 배선을 선택했습니다. 이 의미론은 그 상관관계 구조를 데이터로부터 학습할 고유한 방법을 제공하지 않습니다. 이 권 후반부의 미분 가능한 규칙 학습기들은 이 문제의 학습 쪽 절반을 밀어붙여, 예제로부터 규칙과 확률을 복원합니다; 그곳에서조차, 어떤 숨은 공통 원인이 존재하는지 고르는 것은 여전히 추론이 아니라 모델링 행위로 남습니다. 학술 세계의 열한 개 동전은 그 허구를 눈에 보이면서도 무해하게 유지하지만, 지식 베이스 규모에서는 잘못 가정된 독립성이 상관된 증거에 닿는 모든 질의를 조용히 잘못 보정하며, 이 장의 어떤 커밋된 단언도 그것을 잡아낼 수 없습니다.
왜 중요한가
이 장은 문자 그대로, 실행 가능한 의미에서 이 권의 정확성 닻입니다: distsem.py는 이후 모듈들이 맞추어야 할 오라클입니다. 다음 장의 가중 모델 계수기는 오직 이 열거된 숫자들을 회로 평가로 재현해 내기 때문에 받아들여지며, DeepProbLog의 신경 술어를 훈련시키는 경사 세미링은 바로 이 동일한 의미론을 거쳐서 미분하고, Scallop의 유래 프레임워크는 이를 알면서도 완화하며 그것이 얼마나 벗어나는지로 평가받습니다. 먼저 의미를 감사할 수 있을 만큼 작은 형태로 고정한 다음, 확장 가능한 모든 근사가 그것에 답하게 하는 것입니다. 서로소-합 전시물은 또한 그럴듯해 보이는 지름길이 그저 부정확한 것이 아니라 의미론적으로 틀릴 수 있다는 이 권 최초의 시연이기도 합니다: 증명들을 독립적으로 채점하여 더하는 것은 여기서 0.6885만큼 틀리는데, 이는 어떤 훈련 데이터로도 고칠 수 없는 오류입니다. 계산되고 있는 양 자체를 잘못 정의하고 있기 때문입니다. 그리고 5권의 관심사에 있어서는, 이 장이 신뢰와 보정 탐침이 혼동해서는 안 될 두 속성을 분리합니다: 정합성(가중치의 합이 1이 되고, 확실한 결론이 확률 1을 갖는 것)은 이 의미론 아래에서 자동으로 성립하지만, 경험적 의미에서의 보정(예측된 확률이 관측된 빈도와 일치하는 것)은 오직 진술된 열한 개 동전 확률 자체가 옳은 만큼만 성립하며, 이 장의 어떤 것도 그것을 검사하지 않습니다; 5권의 탐침들은 정확히 그 둘 사이의 간극을 측정합니다.
핵심 용어
- 분포 의미론(Distribution semantics): 독립적인 확률적 사실들이 전체 선택들에 대한 분포를 유도하며, 질의의 확률은 그것을 도출하는 선택들의 총 가중치입니다.
- 확률적 사실(, Probabilistic fact): 독립적인 동전으로 취급되어 확률 로 참인 사실입니다;
PROB_FACTS의 열한 개 주석 달린 간선입니다. - 전체 선택 / 가능 세계(Total choice / possible world): 확률적 사실들의 부분집합 로, 가중치는 이며; 확실한 사실 및 규칙들과 함께 완전히 고전적인 하나의 상황을 이룹니다.
- 성공 확률(, Success probability): 이며, 도출 가능성은 1권의 전방 연쇄기가 결정합니다.
- 진리함수적(Truth-functional): 복합 논리식의 값이 그 부분들의 값의 고정된 함수인 의미론입니다; 퍼지 논리는 그렇고, 확률은 증명 가능하게 그렇지 않습니다.
- 서로소-합 문제(Disjoint-sum problem): 증명들은 겹치는 사건이므로 증명별 곱을 합산하면 그 논리곱을 초과 계수하게 됩니다; 여기서는 1.575 대 참값 0.8865입니다.
- 포함-배제(Inclusion-exclusion): 로, 두 증명에 대한 정확한 수리이며, 겹치는 증명의 수에 대해 지수적입니다.
- 단조성(Monotonicity): 명확한 프로그램에서는, 확률적 사실을 추가해도 어떤 성공 확률도 결코 낮아지지 않습니다.
- 노이즈-오어(Noisy-or): 규칙 로, 여기서 는 번째 증명의 동전 곱이며, 동전 집합이 쌍마다 서로소인 증명들에 대한 것입니다; 독립성은 실패들이 곱해지게 합니다.
- 주석 논리합(Annotated disjunction): 순수한 독립성으로부터의 탈출구로, 여러 대안적 헤드가 하나의 확률적 선택을 공유하게 합니다; DeepProbLog 장으로 미루어집니다.
이 장이 이끄는 곳
이 정의는 이제 정확하고, 감사되었으며, 지수적입니다. 이 장의 모든 숫자는 노트북이 몇 초 만에 끝내는 많아야 수천 번의 전방 연쇄 패스(2,048개의 세계, 그리고 열두-동전짜리 단조성 탐침을 위한 4,096개가 더)에서 나왔으며, 그중 어느 것도 만 개의 불확실한 간선을 가진 지식 베이스와의 접촉에서 살아남지 못합니다. 탈출로는 서로소-합 전시물에서 이미 보였습니다: 세계를 열거하는 일과 증명을 합산하는 일을 그만두는 것입니다; 대신, 질의가 동전들에 의존하는 방식을 하나의 명제 논리식으로 컴파일하고 그 논리식을 충족하는 배정들의 가중 계수를 계산하여, 각 세계가 구성상 한 번만 헤아려지게 하는 것입니다. 그 환원과 그것이 치르는 대가, 그리고 계수가 판정보다 어렵다는 것이 정확히 어떤 의미인지가 다음 장, 가중 모델 계수: #P의 벽의 주제입니다.
컴패니언 코드: examples/integration/distsem.py는 학술 세계 위에서 분포 의미론을 문자 그대로 실행하며, 1권의 kb.py와 forward_chain.py를 손대지 않고 그대로 가져와 2,048개의 세계 전부를 열거합니다; 그 단언들은 이 장의 모든 항등식(정규화, 단일-증명 곱들, 1e-12까지의 서로소-합 포함-배제, 단조성, 노이즈-오어)을 지킵니다. 위에서 인용한 모든 숫자를 재현하려면 python3 examples/integration/distsem.py를 실행하십시오.