회로: SDD, d-DNNF, 빠른 평가

📍 현재 위치: 2부 · 확률 논리와 회로 — 6장. 가중 모델 계수는 확률적 추론을 단 하나의 계수로 환원한 다음 #P의 벽에 부딪혔습니다; 이 장이 그 탈출로입니다: 한 번 컴파일하고, 영원히 계수하는 것입니다.

앞 장은 정직한 패배로 끝났습니다. 가중 모델 계수(weighted model counting, WMC)는 확률적-논리 추론의 올바른 화폐이지만, 임의의 논리식 위에서 그것을 계산하는 일은 #P-완전이고, 무차별 대입 계수기는 그 대가를 고스란히 치렀습니다. 동전 네 개가 추가되는 한 단계마다 열거되는 배정의 수는 정확히 16배로 불어났습니다. 그런데 그 패배를 주의 깊게 읽어 보면, 그 안에 스스로 빠져나갈 구멍이 들어 있습니다. 어려움의 결과가 말하는 것은 어떤 알고리즘도 모든 논리식을 빨리 셀 수는 없다는 것이지, 먼저 특별한 모양으로 다시 지어진 논리식에 대해서는 아무 말도 하지 않습니다. 지식 컴파일(knowledge compilation)이 정확히 그 일을 합니다. 논리식을 강한 구조적 보증을 갖춘 회로(circuit)로 번역하는, 어쩌면 값비쌀 수도 있는 일회성 노력을 들인 다음, 그 뒤로는 그 회로가 지원하는 질의들에 회로 크기에 다항인(이 책이 쓰는 질의들에서는 선형인) 시간으로 답하는 것입니다 [1]. 이 장은 목표 모양을 성질 하나씩 쌓아 올리고, 각 성질이 정확히 하나의 산술 연산을 건전하게 만드는 조건임을 증명하며, 자신의 보증을 스스로 검사하는 동작하는 컴파일러를 인용하고, 이 권의 나머지를 밀고 나가는 반전으로 끝을 맺습니다. 같은 회로를 다른 대수 아래에서 평가하면 다른 질문에 답한다는 것입니다.

쉽게 말하면

연장 코드와 멀티탭과 어댑터가 뒤엉킨 더미가 있고, 그 끝에서 얼마만큼의 전류가 흘러나오는지 알아야 한다고 상상해 보십시오. 누군가 물을 때마다 그 더미를 지나는 가능한 모든 경로를 처음부터 되짚어 볼 수도 있습니다. 느리고, 실수하기 쉬우며, 질문 하나마다 대가를 매번 고스란히 다시 치릅니다. 아니면 오후 한나절을 들여 그 더미를, 모든 접점에 이름표가 붙어 있고 어떤 전선도 다른 전선을 가로지르지 않는 깔끔한 배전반으로 다시 배선할 수도 있습니다. 그 재배선은 실제 노동이며, 때로는 많은 노동입니다. 하지만 그 뒤로는 어떤 질문이든(총 전류, 가장 센 단 하나의 경로, 살아 있는 경로가 하나라도 있는지) 배전반을 한 번 훑으며 각 접점을 한 번씩 읽는 것으로 답이 나옵니다. 지식 컴파일이 그 재배선이고, 회로가 그 배전반이며, 서로 다른 질문들은 접점에서 더하고 곱하는 서로 다른 방식입니다.

이 장에서 다루는 내용

• 분할 상환 논증: 열거는 질의마다 $2^n$($n$은 확률적 사실의 개수)을 지불하고, 컴파일은 일회성 비용을 치른 다음 이후의 모든 질의에 회로-크기 시간으로 답합니다. 회로 자체가 지수적으로 커질 수 있다는 정직한 단서가 붙습니다.
• 목표 언어, 성질 하나씩: 부정 정규형, 그다음 분해 가능성, 결정성, 매끄러움을 각각 정의하고, 각 성질이 하나의 세미링 연산을 올바르게 만든다는 짧은 증명으로 동기를 부여합니다.
• 실제 컴파일러: 고정된 변수 순서 위에서 캐시를 갖추고 하향식 섀넌 전개를 수행하며, circuit.py에서 그대로 인용하고, 그 OBDD(순서 이진 결정 다이어그램, ordered binary decision diagram) 혈통을 정직하게 밝힙니다.
• 검사 가능한 코드로서의 보증: 커밋된 함수들로 검증되는 세 가지 구조적 성질과, 실제 실행에서 나온 PASS 줄들입니다.
• 단 한 번의 상향 패스: OR을 $+$로, AND를 $\times$로 바꾸는 평가자는 무차별 대입 계수기와 소수점 열두 자리까지 일치하며, #P-벽 계열에 대한 회로 크기 대 $2^n$ 표가 함께합니다.
• 세미링 교체: 같은 회로 위에서 $(+, \times)$를 $(\max, \times)$로 바꾸면 최유력 설명이 계산되며, 이는 다음 장의 경사 세미링을 향한 첫걸음입니다.
• 컴파일 지도: d-DNNF(결정론적 분해 가능 부정 정규형), SDD(문장 결정 다이어그램), OBDD가 이 분야의 어디에 자리하는지, 그리고 각 언어가 어떤 질의를 다항 시간에 지원하는지입니다.

한 번 매끄러운 d-DNNF 회로로 컴파일하면, 그다음의 모든 질의는 한 번의 상향 패스입니다: 세미링이 질문을 고르고, 구조가 답을 보증합니다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

한 번 지불하고, 영원히 질의하기

앞 장이 측정한 정확한 비용을 떠올려 봅시다. 무차별 대입 계수기 wmc.wmc_counted는 논리식의 $n$개 변수에 대한 $2^n$개의 배정 전부를 훑는데, 여기서 $n$은 그 논리식이 언급하는 확률적 사실(동전)의 개수입니다. 합성 사슬 계열에서 그것은 $n = 20$에서 1,048,576개의 배정을 열거했고, 모든 질의는, 심지어 새 가중치로 같은 질의를 반복하는 경우조차, 청구서 전액을 다시 지불합니다.

컴파일은 이 장부를 재편성합니다. 작업을 두 단계로 나눕니다:

1. 컴파일(논리식마다 한 번): 명제 논리식 $\varphi$를 제한된 목표 언어 안의 동치인 회로 $C$로 번역합니다. 이 단계는 비쌀 수 있습니다. 최악의 경우 회로는 지수적으로 커지는데, 만약 컴파일이 언제나 값싸고 평가가 언제나 선형이라면 #P-완전 문제에 대한 다항 알고리즘을 갖게 되는 셈이고, 그런 것이 존재한다고 믿는 사람은 없기 때문입니다.
2. 질의(원하는 만큼 자주): $\varphi$에 관한 질문에 $C$의 단 한 번의 상향 훑기로, 회로 엣지 하나당 산술 연산 하나의 비용으로 답합니다.

이 내기는 분할 상환입니다. 지식 베이스는 드물게 바뀌고, 질의는 끊임없이 도착합니다. 학술 세계의 회로가 몇십 개의 노드로 컴파일된다면, 동전의 가중치를 다시 매기는 일, 증거에 조건화하는 일, 최유력 설명을 묻는 일은 각각 선형 패스의 비용만 들 뿐, 새로 지수적 열거를 치르지 않습니다. 컴파일 지도 [1]는 이 내기를 목표 언어들의 한 가족에 걸쳐 체계화하며, 서로 싸우는 두 축으로 각 언어를 채점합니다. 간결성(succinctness, 이 언어의 회로는 얼마나 작아질 수 있는가?)과 처리 가능한 질의(tractable queries, 이 언어는 어떤 질문에 다항 시간으로 답하는가?)입니다. 언어가 더 많은 질의를 지원할수록 그 회로는 더 많은 구조를 짊어져야 하고, 그만큼 더 커져야 할 수도 있습니다. 이 장이 짓는 언어는 그 절충의 달콤한 지점에 자리하며, 그 구조적 요구 사항 하나하나는 단언이 아니라 증명으로 획득될 것입니다. 한 가지 단서는 처음부터 밝혀 둡니다. 컴파일은 지수를 옮기는 것이지, 지우는 것이 아닙니다. #P의 벽은 질의 시간이 아니라 회로 크기에 관한 진술로 다시 나타나며, 마지막 절은 그것이 정확히 어디에 숨어 있는지로 되돌아갑니다.

목표 언어, 성질 하나씩

목표는 회로입니다. 잎이 리터럴이나 상수이고 내부 노드에 AND 또는 OR 이름표가 붙은 유향 비순환 그래프입니다. 요구되는 성질들을 한 번에 하나씩 쌓아 올리고, 각 성질마다 그것에 동기를 부여하는 산술적 사실을 증명합니다. 전체에 걸쳐, 리터럴(literal)은 변수 $x$ 또는 그 부정 $\neg x$이고, 배정(assignment) $\omega$는 모든 변수를 참 또는 거짓으로 사상하며, $\omega \models \varphi$("$\omega$가 $\varphi$를 충족한다"라고 읽고, 기호 $\models$는 "참으로 만든다"를 뜻합니다)는 그 배정 아래에서 논리식이 참으로 평가된다는 말입니다. 가중치 함수는 앞 장의 것입니다. 각 변수 $x$는 확률 $p_x$를 지니고, 리터럴 $x$의 가중치는 $w(x) = p_x$, 리터럴 $\neg x$의 가중치는 $w(\neg x) = 1 - p_x$이며, 배정의 가중치는 그 리터럴 가중치들의 곱입니다. WMC는 모델들에 대해 배정 가중치를 합산합니다:

$$\mathrm{WMC}(\varphi, w) \;=\; \sum_{\omega \,\models\, \varphi} \; \prod_{v \in V} w\bigl(v, \omega(v)\bigr),$$

여기서 $V$는 $\varphi$가 언급하는 변수들의 집합이고, 곱 기호 아래의 첨자 $v \in V$는 "집합 $V$의 각 변수 $v$"라고 읽으며, $w(v, \omega(v))$는 $\omega$가 $v$를 참으로 설정하면 $p_v$, 그렇지 않으면 $1 - p_v$입니다.

부정 정규형

회로가 부정 정규형(negation normal form, NNF)이라는 것은 부정이 오직 잎에서만 나타난다는 뜻입니다. 내부 노드는 AND와 OR뿐이고, 모든 $\neg$는 변수에 직접 붙어 있습니다. 어떤 명제 논리식이든 드 모르간 법칙($\neg(A \wedge B) = \neg A \vee \neg B$와 $\neg(A \vee B) = \neg A \wedge \neg B$)으로 부정을 안쪽으로 밀어 넣고 이중 부정을 소거하면, 모델 집합을 바꾸지 않은 채 NNF로 다시 쓸 수 있습니다. NNF만으로는 계산적으로 아무것도 사 오지 못합니다 [1]. 그것은 하중을 지는 두 성질이 그려질 캔버스입니다.

분해 가능성: ×를 올바르게 만드는 것

AND 노드가 분해 가능(decomposable)하다는 것은 그 자식들이 쌍마다 서로소인 변수 집합을 언급한다는 뜻입니다. 모든 AND 노드가 그러할 때 회로는 분해 가능하며, 이를 DNNF(분해 가능 부정 정규형, decomposable negation normal form)라고 부릅니다. 이 성질의 요점은 하나의 계수 보조정리이며, 평가자 전체가 그 위에 놓이므로 이 보조정리는 완전한 증명을 받을 자격이 있습니다.

보조정리(곱의 법칙). $A$와 $B$가 서로소인 변수 집합 $V_A$와 $V_B$ 위의 논리식이라 합시다. 즉 $V_A \cap V_B = \emptyset$(공유하는 변수가 없음)입니다. 그러면

$$\mathrm{WMC}(A \wedge B) \;=\; \mathrm{WMC}(A) \cdot \mathrm{WMC}(B).$$

증명. $V_A \cup V_B$(두 집합의 합집합: 어느 한쪽에라도 속하는 모든 변수) 위의 배정 $\omega$는 정확히 하나의 쌍 $(\omega_A, \omega_B)$입니다. $V_A$의 변수들로의 제한 $\omega_A$와 $V_B$의 변수들로의 제한 $\omega_B$입니다. 두 집합이 서로소이므로 이 짝짓기는 아무것도 잃지 않고 아무것도 중복하지 않습니다. $\omega$를 고르는 일은 $\omega_A$와 $\omega_B$를 독립적으로 고르는 일과 같은 행위입니다. $A$는 $V_A$의 변수만 언급하므로 $\omega \models A$인지는 오직 $\omega_A$에만 달려 있고, $B$도 마찬가지입니다. 따라서 $\omega \models A \wedge B$인 것은 정확히 $\omega_A \models A$이고 $\omega_B \models B$일 때입니다. $\omega$의 가중치도 같은 이음매를 따라 갈라지는데, $V_A \cup V_B$에 대한 곱은 두 부분 곱의 곱이기 때문입니다:

$$\prod_{v \in V_A \cup V_B} w\bigl(v, \omega(v)\bigr) \;=\; \underbrace{\prod_{v \in V_A} w\bigl(v, \omega_A(v)\bigr)}_{=\;W(\omega_A)} \;\cdot\; \underbrace{\prod_{v \in V_B} w\bigl(v, \omega_B(v)\bigr)}_{=\;W(\omega_B)}.$$

이제 계수를 계산합시다. 충족하는 $\omega$에 대한 합을 충족하는 쌍들에 대한 이중 합으로 바꾼 다음, 그 이중 합을 인수분해합니다(첫 번째 합의 각 항이 두 번째 합의 모든 항과 곱해지는데, 이는 정확히 두 합의 곱이 전개되는 방식입니다):

$$\mathrm{WMC}(A \wedge B) \;=\; \sum_{\omega_A \models A} \; \sum_{\omega_B \models B} W(\omega_A)\, W(\omega_B) \;=\; \sum_{\omega_A \models A} W(\omega_A) \sum_{\omega_B \models B} W(\omega_B) \;=\; \mathrm{WMC}(A) \cdot \mathrm{WMC}(B). \;\blacksquare$$

(채워진 사각형 $\blacksquare$는 증명의 끝을 표시합니다.) 서로소성은 장식이 아닙니다. 그것을 떨어뜨리면 법칙은 즉시 무너집니다. $p_x = 0.9$인 $A = B = x$를 봅시다. 그러면 $A \wedge B$는 그냥 $x$이므로 $\mathrm{WMC}(A \wedge B) = 0.9$이지만, 곱은 $\mathrm{WMC}(A) \cdot \mathrm{WMC}(B) = 0.81$입니다. 곱셈은 $x$의 두 등장을 독립적인 동전으로 취급하지만, 그것들은 하나의 같은 동전입니다. 분해 가능성은 AND 노드에서의 곱셈이 그러한 이중 사용을 결코 저지르지 않게 되는 바로 그 구문적 조건입니다.

결정성: +를 올바르게 만드는 것

OR 노드가 결정적(deterministic)이라는 것은 그 자식들이 쌍마다 논리적으로 서로소라는 뜻입니다. 어떤 배정도 그중 둘을 동시에 충족하지 않습니다. OR이 모두 결정적인 분해 가능 회로는 결정론적 분해 가능 부정 정규형(deterministic decomposable negation normal form, d-DNNF)에 속합니다 [1]. 동기를 부여하는 보조정리는 곱의 법칙의 거울상입니다.

보조정리(합의 법칙). $A$와 $B$가 공통의 변수 집합 위의 논리식이고 $A \wedge B$가 충족 불가능하다고 합시다. 그러면

$$\mathrm{WMC}(A \vee B) \;=\; \mathrm{WMC}(A) + \mathrm{WMC}(B).$$

증명. $\varphi$를 충족하는 배정들의 집합을 $\mathrm{Mod}(\varphi)$라고 씁시다. OR의 진리표에 의해 언제나 $\mathrm{Mod}(A \vee B) = \mathrm{Mod}(A) \cup \mathrm{Mod}(B)$입니다. $A \wedge B$가 충족 불가능하므로 어떤 배정도 두 집합에 동시에 속하지 않습니다. 이 합집합은 서로소입니다. 서로소 합집합에 대한 합은 두 부분 합으로 갈라지며, 각 항은 정확히 한쪽에만 떨어집니다:

$$\mathrm{WMC}(A \vee B) \;=\; \sum_{\omega \in \mathrm{Mod}(A) \,\cup\, \mathrm{Mod}(B)} W(\omega) \;=\; \sum_{\omega \in \mathrm{Mod}(A)} W(\omega) \;+\; \sum_{\omega \in \mathrm{Mod}(B)} W(\omega) \;=\; \mathrm{WMC}(A) + \mathrm{WMC}(B). \;\blacksquare$$

결정성이 없으면 올바른 항등식은 포함-배제, 즉 $\mathrm{WMC}(A \vee B) = \mathrm{WMC}(A) + \mathrm{WMC}(B) - \mathrm{WMC}(A \wedge B)$이고, 순진하게 더하면 이중으로 충족하는 모든 배정을 초과 계수하게 됩니다. 이것이 분포 의미론 장이 서로소-합 문제(disjoint-sum problem)로 드러낸 함정입니다. grandAdvisor(alice, Z)는 동전 advises(alice, bob)을 공유하는 두 개의 증명을 가지며, 그 확률들을 더하면 터무니없는 "확률" $0.81 + 0.765 = 1.575$가 나왔는데, 참값은 $0.8865$입니다. 결정성은 그 함정의 구조적 치유책입니다. 겹침을 (증명의 개수와 함께 그 수가 폭발하는) 포함-배제 항들로 사후에 보정하는 대신, 컴파일러는 겹침이 아예 일어날 수 없도록 논리식을 다시 짓습니다. 출력의 모든 OR은 구성에 의해 "여기서 $x$는 참이다"와 "여기서 $x$는 거짓이다" 사이의 선택이고, 어떤 배정도 두 가지를 모두 탈 수 없습니다.

매끄러움: 장부 정리 성질

한 가지 성질이 더 있는데, 이것은 회로를 계수에-올바르게 만든다기보다 다루기 즐겁게 만들어 줍니다. OR 노드가 매끄럽다(smooth)는 것은 그 모든 자식이 정확히 같은 변수 집합을 언급한다는 뜻입니다. 왜 신경 쓸까요? 왼쪽 자식이 $\{x\}$를 언급하고 오른쪽 자식이 $\{x, y\}$를 언급하는 OR을 생각해 봅시다. 왼쪽 자식의 계수는 은연중에 $x$ 하나에 대한 배정들에 대한 계수이고, 오른쪽 자식의 계수는 둘 모두에 대한 배정들에 대한 것입니다. 이 둘을 더하는 것은 서로 다른 두 표본 공간을 섞는 일입니다. 확률 가중치에 대해서는 이 혼합이 공교롭게도 무해한데, 정확히 왜 그런지 볼 가치가 있습니다. 자식에서 빠진 변수 $y$는 자유롭게 참이거나 거짓일 수 있으므로, 전체-공간 계수에서 그 자식이 차지하는 몫에 대한 $y$의 기여는 인수

$$w(y) + w(\neg y) \;=\; p_y + (1 - p_y) \;=\; 1,$$

이고, 1을 곱하는 것은 아무것도 바꾸지 않습니다. 이 추론을 구조적으로 만드는 수리도 똑같이 간단합니다. 빠진 변수 $y$마다, 모자란 자식에 통과 노드(pass-through node) $\mathrm{pt}(y) = (y \vee \neg y)$를 곱하는 것입니다. 통과 노드는 그 자체로 결정적 OR이고(그 자식들은 $y$를 서로 반대로 결정합니다) 분해 가능한 AND-짝이므로(그것은 오직 빠져 있던 $y$만을 도입합니다) 이 수리는 d-DNNF를 보존합니다. 그리고 $(+, \times)$ 아래에서 그것은 방금 계산한 인수 1로 정확히 평가되므로 계수는 바뀌지 않습니다. 매끄러운 d-DNNF가 완전한 목표 언어입니다. 매끄러움이 제 밥값을 하는 이유는 다른 세미링들은 그렇게 관대하지 않기 때문입니다. $\max(p_y, 1 - p_y)$는 $p_y$가 정확히 $\tfrac12$가 아닌 한 1이 아니며, 아래의 데모는 매끄럽게 만들지 않은 회로가 확률 질의는 건드리지 않은 채 최유력-설명 질의를 조용히 오염시키는 모습을 보여 줍니다.

컴파일러: 캐시를 갖춘 섀넌 전개

이런 성질들을 갖춘 회로는 실제로 어떻게 만들어 낼까요? 컴패니언의 컴파일러 circuit.py는 책에서 가장 오래된 요령인 섀넌 전개(Shannon expansion)를 씁니다. 어떤 논리식 $\varphi$든 어떤 변수 $x$에 대해서든 다음과 같이 갈라집니다.

$$\varphi \;=\; (x \wedge \varphi|_{x=1}) \;\vee\; (\neg x \wedge \varphi|_{x=0}),$$

여기서 $\varphi|_{x=1}$(코팩터(cofactor)라 하고, 잔여식(residual)이라고도 부릅니다)는 $x$를 참으로 바꿔 넣고 단순화한 $\varphi$이며, $\varphi|_{x=0}$은 그것을 거짓으로 바꿔 넣은 것입니다. 이 항등식은 경우 나누기로 읽습니다. 모든 배정은 $x$를 어느 한쪽으로 설정하며, 왼쪽 논리합 항은 정확히 $x$가 참인 모델들을, 오른쪽은 $x$가 거짓인 모델들을 모읍니다. 요구되는 두 성질 모두 이 갈라짐의 모양에서 저절로 나옵니다. OR은 결정적입니다. 그 자식들이 $x$를 서로 반대 값으로 강제하므로 어떤 배정도 둘 다 충족하지 못하기 때문입니다. 각 AND는 분해 가능합니다. 코팩터는 더 이상 $x$를 언급하지 않으므로(치환으로 사라졌습니다) 리터럴 자식과 잔여식 자식의 변수 집합이 서로소이기 때문입니다. 잔여식들에 대해 재귀하되, 언제나 잔여식이 아직 언급하는 변수 중 고정된 순서에서 첫 번째인 변수로 분기하고, 각 잔여식을 캐시하여 반복되는 부분 논리식이 하나의 공유 노드로 컴파일되게 하면, d-DNNF 회로가 나옵니다. 다음이 그 핵심을 그대로 옮긴 것입니다(circuit.py 266–282행):

    def build(residual: tuple) -> int:
        if residual == ():                 # no terms: unsatisfiable, φ = ⊥
            return b.add(("F",))
        if residual == (frozenset(),):     # empty term: satisfied, φ = ⊤
            return b.add(("T",))
        if residual in cache:
            return cache[residual]
        # Branch variable: the order-first variable the residual mentions.
        x = order[min(rank[v] for t in residual for v, _ in t)]
        # φ = (x ∧ φ|x=1) ∨ (¬x ∧ φ|x=0); builder simplification prunes the
        # ⊥ branch (AND with ⊥ = ⊥, dropped from the OR) and ⊤ conjuncts.
        hi = b.AND([b.lit(x, True), build(_cofactor(residual, x, True))])
        lo = b.AND([b.lit(x, False), build(_cofactor(residual, x, False))])
        cache[residual] = b.OR([hi, lo])
        return cache[residual]

    return _compact(b.nodes, build(dnf), order, dnf)

혈통에 관한 정직함: 고정된 변수 순서에 잔여식 캐시를 더한 것은 정확히 순서 이진 결정 다이어그램(ordered binary decision diagram, OBDD)의 조리법이며, 여기서는 그것을 회로로 읽은 것입니다. 이 장난감은 d-DNNF 옷을 입은 OBDD 컴파일러입니다. 산업용 컴파일러들은 훨씬 더 영리합니다. 문장 결정 다이어그램(sentential decision diagram, SDD)은 선형 변수 순서를 변수들 위의 이진 vtree로 일반화하고, 컴파일된 두 회로를 다항 시간에 결합하는 것을 지원하면서도 정준성을 유지합니다 [2]. ProbLog2 [3]와 ACE 시스템 뒤에 있는 것들과 같은, 논리곱 정규형(conjunctive normal form, CNF: OR-절들의 AND)을 d-DNNF로 바꾸는 컴파일러들은 성분 캐싱과 절 학습을 갖춘 소진적 DPLL(Davis–Putnam–Logemann–Loveland)-스타일 백트래킹 탐색의 자취로부터 회로를 추출합니다 [4]. 이 장난감이 그것들 모두와 공유하는 것은 공학이 아니라 계약입니다. 출력 언어와 그에 따르는 보증입니다. 섀넌 전개의 원시 출력에는 이미 예고된 결함 하나가 남아 있습니다. 매끄럽지 않다는 것입니다(⊤이 된 잔여식은 아무 변수도 언급하지 않습니다). 그래서 compile()(circuit.py 322–332행)은 전개 후에 smooth() 수리 패스를 실행하여, OR의 자식들이 범위(scope)에 대해 어긋나는 곳마다 통과 노드를 삽입합니다(circuit.py 307–317행):

        else:  # "O": pad every child up to the union scope of all children
            union: frozenset = frozenset()
            for c in rest[0]:
                union |= circuit.scope[c]
            kids = []
            for c in rest[0]:
                missing = sorted(union - circuit.scope[c], key=repr)
                inserted += len(missing)
                pts = [b.OR([b.lit(v, True), b.lit(v, False)]) for v in missing]
                kids.append(b.AND([new[c]] + pts))
            new.append(b.OR(kids))

이 컴파일러를 실행 예제 위에서 손으로 따라가 봅시다. 이 장의 기계 장치 전체가 그 안에 들어가기 때문입니다. 질의 grandAdvisor(alice, Z)는 (wmc.py에서) 두-증명 논리합 정규형(disjunctive normal form, DNF: AND-항들의 OR) $\varphi = (ab \wedge bc) \vee (ab \wedge bd)$로 컴파일되는데, 여기서 $ab$는 $p_{ab} = 0.9$인 동전 advises(alice, bob)의 줄임말이고, $bc$는 $p_{bc} = 0.9$인 advises(bob, carol), $bd$는 $p_{bd} = 0.85$인 advises(bob, dave)입니다. 정렬된 순서는 $ab$에 먼저 분기합니다. 코팩터 $\varphi|_{ab=0}$은 두 항을 모두 죽여(각 항은 $ab$를 요구합니다) 빈 DNF ⊥를 남기므로, $\neg ab$ 가지 전체가 가지치기됩니다. 코팩터 $\varphi|_{ab=1}$은 $bc \vee bd$이고, 이는 $bc$에 분기합니다. 참 가지의 잔여식은 ⊤이고(항 $\{bc\}$가 완전히 충족됩니다), 거짓 가지는 $bd$를 남깁니다. 따라서 원시 회로는

$$ab \;\wedge\; \bigl(\, bc \;\vee\; (\neg bc \wedge bd) \,\bigr),$$

노드 7개와 엣지 6개이며, 그 안쪽 OR은 매끄럽지 않습니다. 왼쪽 자식은 $\{bc\}$를 언급하고 오른쪽은 $\{bc, bd\}$를 언급합니다. 수리는 왼쪽 자식을 $bc \wedge (bd \vee \neg bd)$로 채워 넣고, 통과 노드 하나가 삽입되어, 노드 10개와 엣지 10개의 매끄러운 회로가 나옵니다. 이 크기들은 대충 얼버무린 것이 아닙니다. 커밋된 컴파일 표입니다:

[1] compile: top-down expansion, then the smoothness repair
      query                        vars terms |  raw nodes edges | smooth nodes edges  +pt
      grandAdvisor(alice, carol)      2     1 |          3     2 |           3     2    0
      citesTransitively(p3, p1)       2     1 |          3     2 |           3     2    0
      colleague(carol, erin)          1     1 |          1     0 |           1     0    0
      grandAdvisor(alice, Z)          3     2 |          7     6 |          10    10    1

코드로 검사되는 계약

검사할 수 없는 보증은 소문일 뿐입니다. 앞 절의 성질들은 완성된 회로의 대상 성질로서 조사만으로 결정 가능하며, circuit.py는 컴파일러의 구성 논증을 믿는 대신 매 실행마다 그것들을 조사합니다. 분해 가능성은 집합 계산입니다. 모든 AND 노드에 대해 자식들의 변수 범위가 쌍마다 서로소여야 하는데, 이는 정확히 그것들의 합집합 크기가 크기들의 합과 같을 때 성립합니다(circuit.py 379–392행):

def check_decomposable(circuit: Circuit) -> int:
    """Decomposability: for every AND node the children's scopes are
    pairwise DISJOINT (sizes add up exactly).  Returns the number of AND
    nodes checked; raises AssertionError on any violation."""
    n_and = 0
    for i, (kind, *rest) in enumerate(circuit.nodes):
        if kind != "A":
            continue
        n_and += 1
        # |∪ scopes| = Σ |scope| ⇔ pairwise disjoint.
        assert len(circuit.scope[i]) == sum(len(circuit.scope[c])
                                            for c in rest[0]), (
            f"AND node {i} has overlapping child scopes")
    return n_and

결정성은 두 번 검사됩니다. 한 번은 구조적으로(모든 OR은 자식들이 한 변수를 서로 반대 값으로 강제하는 이진 결정입니다, circuit.py 395–419행), 그리고 한 번은 의미론적으로, 가능한 가장 무딘 도구로 검사합니다. 회로의 $n$개 변수에 대한 모든 $2^n$개 배정을 열거하고, 모든 노드를 불 세미링 아래에서 평가하며, 어떤 배정도 한 OR의 두 자식을 동시에 충족하는 일이 없기를 요구하는 것입니다(circuit.py 422–438행). 이 열거 검사는 장난감 규모에서만 감당할 수 있는데($n = 10$을 넘으면 코드가 거부합니다), 바로 그렇기 때문에 여기서는 값집니다. 이 규모에서 "OR들은 결정적이다"는 논증이 아니라 소진적으로 검증된 사실입니다. 매끄러움은 OR마다 자식들의 범위를 비교하여 검사합니다(circuit.py 441–452행). 커밋된 실행은 네 가지 모두에 도장을 찍습니다:

[2] the d-DNNF contract, checked as code (structure, never assumed)
      decomposability : 5 AND nodes across 4 circuits, child scopes pairwise disjoint            PASS
      determinism     : 2 OR nodes, each a decision x vs ¬x (structural)                         PASS
      determinism     : exhaustive, all 4+4+2+8 = 18 assignments, no OR children overlap         PASS
      smoothness      : raw circuits have 1 un-smooth OR; repaired with pt(v) = (v ∨ ¬v): 0 remain PASS

한 번의 패스, 소수점 열두 자리

이제 보상입니다. 매끄러운 d-DNNF 위에서 가중 모델 계수는 노드 목록에 대한 단 한 번의 상향 훑기입니다. 리터럴 잎은 자신의 가중치를 읽고, AND는 자식들의 값을 곱하며(컴파일러가 서로소 범위를 보증했으므로 곱의 법칙에 의해 건전합니다), OR은 자식들의 값을 더합니다(컴파일러가 서로소 모델을 보증했으므로 합의 법칙에 의해 건전합니다). 평가자는 짧은 루프 하나이고, 자신의 작업량을 스스로 셉니다. 정확히 회로 엣지 하나당 산술 연산 하나입니다(circuit.py 344–365행):

    for i, (kind, *rest) in enumerate(circuit.nodes):
        if kind == "F":
            vals[i] = sr.zero
        elif kind == "T":
            vals[i] = sr.one
        elif kind == "L":
            var, sign = rest
            vals[i] = weights[var][0] if sign else weights[var][1]
        elif kind == "A":
            # AND → ⊗ over children (decomposability makes this sound).
            v = sr.one
            for c in rest[0]:
                v = sr.times(v, vals[c])
                ops += 1
            vals[i] = v
        else:
            # OR → ⊕ over children (determinism makes this sound).
            v = sr.zero
            for c in rest[0]:
                v = sr.plus(v, vals[c])
                ops += 1
            vals[i] = v

매끄러운 grandAdvisor(alice, Z) 회로 위에서, 잎에서 위로, 손으로 실행해 봅시다. 통과 노드는 $0.85 + 0.15 = 1$로 평가됩니다. 채워 넣은 왼쪽 가지는 $0.9 \times 1 = 0.9$이고, 오른쪽 가지는 $0.1 \times 0.85 = 0.085$이며, OR은 이 둘을 더해 $0.9 + 0.085 = 0.985$가 되고, 루트 AND는 공유된 동전을 곱해 넣어 $0.9 \times 0.985 = 0.8865$입니다. 이는 앞 장이 $2^3$개의 배정 전부를 열거하여 얻은 정확히 그 값이며, 커밋된 실행은 네 개의 학술 질의 전부를 소수점 열두 자리에서 확인하고, 연산 횟수는 매번 엣지 수와 같습니다:

[3] ONE bottom-up (+, ×) pass == wmc.py's 2^n brute force, to 1e-12
      query                        circuit WMC      wmc.py brute     |diff|   ops = edges
      grandAdvisor(alice, carol)   0.810000000000   0.810000000000   0.0e+00     2 = 2
      citesTransitively(p3, p1)    0.720000000000   0.720000000000   0.0e+00     2 = 2
      colleague(carol, erin)       0.550000000000   0.550000000000   0.0e+00     0 = 0
      grandAdvisor(alice, Z)       0.886500000000   0.886500000000   1.1e-16    10 = 10

학술 회로들은 아주 작으므로, 분할 상환 논증이 실감 나게 다가오려면 스케일링 계열이 필요합니다. 앞 장의 #P-벽 계열($k$개의 독립적인 두-동전 사슬, $n = 2k$개의 변수, 닫힌 형식 $1 - 0.44^k$)은 노드 수가 $n$에 선형으로 자라는 회로로 컴파일됩니다. 사슬들은 변수를 공유하지 않으므로 각 사슬은 상수 크기의 장치 하나를 더할 뿐이고, 잔여식 캐시는 한 번 본 접미사를 결코 다시 전개하지 않습니다. 커밋된 표는 두 가격표를 나란히 놓습니다:

[6] the escape from the #P wall (wmc.py's chain family, compiled)
      n   k  2^n assignments   nodes  edges  ops    circuit WMC        1 − 0.44^k       |diff|
       8   4              256      41     64   64    0.962519040000   0.962519040000   0.0e+00
      12   6            4,096      65    114  114    0.992743686144   0.992743686144   0.0e+00
      16   8           65,536      89    172  172    0.998595177637   0.998595177637   0.0e+00
      20  10        1,048,576     113    238  238    0.999728026391   0.999728026391   0.0e+00
      growth per +4 coins: nodes +24 (LINEAR); edge increments [50, 58, 66]
      (quadratic — the smoothing price); brute-force assignments: exactly 16× per step
      at n = 20: 238 semiring ops vs 1,048,576 assignments — 4,405× fewer

이 간극을 소리 내어 읽어 봅시다. 무차별 대입은 구성상 매 단계 작업량을 정확히 16배로 곱하고, 컴파일된 회로는 단계마다 노드 24개, 즉 상수만큼을 더합니다. $n = 20$에서 회로는 열거가 1,048,576개의 가중 배정으로 답하는 것을 238번의 세미링 연산으로 답하며, 이는 4,405배의 차이이고, 둘은 닫힌 형식과 기계 정밀도로 일치합니다. (엣지 수는 선형이 아니라 이차로 자랍니다. 그것이 매끄러움 수리의 대가인데, 나중 사슬들은 앞선 사슬들의 변수에 대한 통과 노드로 채워 넣어져야 하기 때문이며, 실행은 두 성장 법칙을 상수인 첫째 차분과 둘째 차분으로 단언합니다, circuit.py 644–648행.) 원시 열거가 증명 가능하게 $2^n$인 계열 위에서의 이 선형-대-지수 분리가 컴파일 기반 정확 추론의 사업 근거 전부입니다 [4].

세미링 교체: 같은 회로, 새로운 질문

평가자 발췌를 다시 봅시다. 그 안 어디에도 "확률"이라는 말이 없습니다. 그것은 OR 자식들을 sr.zero에서 시작해 sr.plus로 접고, AND 자식들을 sr.one에서 시작해 sr.times로 접는데, 여기서 sr은 교환 세미링(commutative semiring)입니다. 두 연산 $\oplus$와 $\otimes$, 그리고 두 개의 특별한 원소 $\bar 0$과 $\bar 1$을 갖춘 집합으로, $\oplus$는 항등원 $\bar 0$을 갖는 결합적이고 교환적인 연산이고, $\otimes$는 항등원 $\bar 1$을 갖는 결합적이고 교환적인 연산이며, $\otimes$는 $\oplus$에 분배되고, $\bar 0$은 $\otimes$ 아래에서 흡수합니다(무엇이든 $\bar 0$을 곱하면 $\bar 0$입니다). 이 장의 두 증명은 이 법칙들과, 구조가 보증하는 서로소성 사실들만을 썼습니다. 뺄셈도 나눗셈도 쓰지 않았습니다. 그러므로 다른 세미링의 $\oplus$와 $\otimes$를 같은 패스에 꽂아 넣을 때마다, 같은 컴파일된 회로가 다른 질문에 답합니다. 이것이 대수적 모델 계수(algebraic model counting)이며 [5], 2부의 나머지가 올라타는 추상화입니다.

첫 번째 교체는 $(\max, \times)$입니다. $\varphi$의 최유력 설명(most probable explanation, MPE)을 최대 가중치의 충족 배정으로, 그 값을 그 최댓값으로 정의합니다:

$$\mathrm{MPE}(\varphi, w) \;=\; \max_{\omega \,\models\, \varphi} \; \prod_{v \in V} w\bigl(v, \omega(v)\bigr).$$

합의 법칙은 최댓값의 법칙이 됩니다. 모델 집합들의 합집합에 대한 최댓값은 두 부분 최댓값 중 더 큰 것, 즉 $\max(\mathrm{MPE}(A), \mathrm{MPE}(B))$이고, 여기서는 결정성이 필요조차 없습니다. $+$와 달리 $\max$는 겹치는 집합에서 아무것도 두 번 세지 않기 때문입니다($\max$는 멱등입니다: $\max(a, a) = a$). 곱의 법칙은 글자 그대로 살아남습니다. 독립적인 선택들에 대한 최댓값은 인수분해되기 때문입니다. 최선의 쌍 $(\omega_A, \omega_B)$는 최선의 $\omega_A$와 최선의 $\omega_B$를 짝지은 것이므로, 모든 가중치가 음이 아니라는 사실을 써서 $\max_{(\omega_A,\omega_B)} W(\omega_A) W(\omega_B) = \bigl(\max_{\omega_A} W(\omega_A)\bigr)\bigl(\max_{\omega_B} W(\omega_B)\bigr)$입니다. 하지만 이제는 매끄러움이 하중을 짊어집니다. OR 자식에서 빠진 변수는 덧셈 아래에서는 무해한 인수 $p + (1-p) = 1$을 기여했지만, $\max$ 아래에서 통과 노드는 $\max(p, 1 - p)$, 즉 자유 변수의 더 나은 값을 선택하는 대가를 기여하며, 그 인수를 빠뜨리면 매끄럽게 만들지 않은 회로는 그 변수의 값을 1로 매기게 되어, $p \ne \tfrac12$일 때마다 과대평가가 됩니다. 커밋된 실행은 실행 예제 질의 위에서 정확히 이 실패와 그 수리를 보여 주는데, 원시 회로의 ⊤ 가지는 advises(bob, dave)를 결코 언급하지 않습니다:

[4] why smoothness matters: SAME circuit, (max, ×) semiring
      grandAdvisor(alice, Z): the raw circuit's ⊤ branch never mentions
      advises(bob, dave), so (max, ×) pays factor 1 instead of max(0.85, 0.15):
        un-smooth (max, ×) = 0.810000   OVERESTIMATE
        smooth    (max, ×) = 0.688500   = enumerated max (0.90 · 0.90 · 0.85)
      (+, ×) never notices: un-smooth WMC = 0.886500 is already exact,
      because a skipped variable contributes p + (1 − p) = 1 anyway

매끄러운 값을 손으로 확인해 봅시다. 통과 노드는 이제 $\max(0.85, 0.15) = 0.85$를 기여하고, 채워 넣은 왼쪽 가지는 $0.9 \times 0.85 = 0.765$, 오른쪽 가지는 $0.1 \times 0.85 = 0.085$이며, OR은 $\max(0.765, 0.085) = 0.765$를 취하고, 루트는 $0.9 \times 0.765 = 0.6885$, 즉 전부-참 배정 $ab \wedge bc \wedge bd$의 가중치를 내놓습니다. 최대화하는 배정 자체는 하향 argmax 패스(downward argmax pass)로 복원됩니다. 루트에서 시작하여, AND에서는 모든 자식으로 내려가되, OR에서는 그 값이 노드의 값과 같은 자식 하나로만 내려가고(노드의 $\max$는 어떤 자식에서 달성되므로 그런 자식은 존재합니다), 선택된 리터럴들을 잎에서 읽어 냅니다(circuit.py 456–480행). 여기서도 해독된 배정을 전체 배정으로 만들어 주는 것은 매끄러움입니다. OR 아래의 모든 변수가 모든 가지에 등장하므로 어떤 변수도 배정되지 않은 채 하강을 빠져나가지 못하며, 코드는 전체성을 명시적으로 단언합니다(circuit.py 478–479행). 소진적 열거와 대조하여 검증된 커밋된 해독:

      grandAdvisor(alice, Z)       MPE = 0.688500
        argmax: advises(alice, bob)=1, advises(bob, carol)=1, advises(bob, dave)=1

세미링 두 개, 회로 하나, 그리고 표에는 예고된 세 번째 행이 있습니다:

과제	$\oplus$	$\otimes$	$\bar 0$	$\bar 1$	결정성 필요?	매끄러움 필요?	읽어 내는 값
확률(WMC)	$+$	$\times$	$0$	$1$	예(합은 이중으로 셉니다)	아니요($p + (1-p) = 1$)	$P(q)$
최유력 설명	$\max$	$\times$	$0$	$1$	아니요($\max$는 멱등)	예($\max(p, 1-p) \ne 1$)	최선의 증명 세계
경사(다음 장)	쌍별 $+$	쌍에 대한 곱의 법칙	$(0,0)$	$(1,0)$	예	예	$\bigl(P(q),\ \partial P(q)/\partial p\bigr)$

세 번째 행이, 이 장이 미분 가능한 논리에 관한 권 안에 존재하는 이유입니다. 회로를 타고 운반되는 값이 하나의 숫자가 아니라 쌍(확률과, 어떤 사실의 가중치에 대한 그 확률의 도함수)이고, 둘째 성분이 미적분의 합의 법칙과 곱의 법칙을 따르도록 $\oplus$와 $\otimes$가 정의된다면, 같은 상향 패스가 질의 확률의 정확한 경사를 모든 확률적 사실에 대해 계산합니다. 그것이 경사 세미링이며, 다음 장에서 신경망이 정확한 논리 추론을 거쳐서 훈련되는 방식입니다.

컴파일이 이 분야에서 자리한 곳

이 장난감 컴파일러는 성숙한 생태계 속으로 들어갑니다. ProbLog2는 확률 논리 프로그램을 가중 불 논리식으로 접지하고, 그것을 d-DNNF 컴파일러로 또는 SDD로 컴파일하며, 그 결과 위에서 세미링을 평가합니다 [3]. 이 컴파일-후-평가 파이프라인은 정확한 확률-논리 추론의 표준 아키텍처입니다 [4]. 컴파일 지도는 가능한 목표 언어들을 포함 관계로 조직합니다. OBDD 회로는 SDD의 특수 경우이고 SDD는 d-DNNF이며 [2], d-DNNF는 DNNF이고, DNNF는 NNF이며, 사슬을 한 단계 오를 때마다 적어도 그만큼 간결해지면서(낮은 언어의 모든 회로는 이미 높은 언어에 속하므로, 가장 작은 높은-언어 회로는 더 작거나 같을 수밖에 없습니다) 다항 시간 질의는 더 적게 지원합니다 [1]. 이 책이 쓰는 질의들에 대한 절충의 요약은 다음과 같습니다:

언어	충족 가능성	가중 계수 $(+, \times)$	MPE $(\max, \times)$	모델 열거
NNF	다루기 어려움	다루기 어려움	다루기 어려움	다루기 어려움
DNNF(분해 가능)	다항 시간	다루기 어려움	다항 시간(매끄럽게 만든 뒤)	다항 시간
d-DNNF(+ 결정성)	다항 시간	다항 시간	다항 시간(매끄럽게 만든 뒤)	다항 시간
SDD	다항 시간	다항 시간	다항 시간(매끄럽게 만든 뒤)	다항 시간
OBDD	다항 시간	다항 시간	다항 시간(매끄럽게 만든 뒤)	다항 시간

("다루기 어려움"의 뜻은 다음과 같습니다. P가 NP와 같지 않은 한, 또는 다항 위계가 붕괴하지 않는 한, 다항 시간에 풀리지 않는다는 것으로, 지도의 조건부 결과들을 따릅니다 [1]. MPE 열은 위의 세미링 논증에서 따라 나오는데, 그 논증은 분해 가능성과 매끄러움을 필요로 하지만 비결정성은 견뎌 냅니다 [5].) 왜 굳이 더 약한 언어를 선호할까요? 간결성 때문입니다. 더 많은 다항 시간 질의를 요구하는 것은 회로 크기라는 대가를 치르며, 지도는 이웃한 행들 사이의 분리를 증명합니다. SDD가 산업적 역할을 얻은 것은 어떤 무제약 d-DNNF도 갖지 못한 것을 더했기 때문입니다. 정준형(vtree를 고정하면 회로가 고정됩니다)과, 컴파일된 두 SDD를 직접 논리곱하거나 논리합하는 다항 시간 apply 연산이며, 이는 논리식이 절 하나씩 자라날 때 증분 시스템이 필요로 하는 바로 그것입니다 [2]. 같은 분해 가능한-곱, 매끄러운-합 구조에(결정성은 선택적인 추가 성질입니다), 가중치를 리터럴 확률에서 학습된 분포로 일반화한 것이 확률 회로(probabilistic circuit)의 현대적 정의이며, 합-곱 네트워크와 그 친척들이 이제 그 우산 아래에 삽니다 [6]. 이 장이 논리를 위해 지은 기계 장치는, 거의 기호 하나하나까지, 처리 가능한 확률 모델링의 기계 장치입니다.

미해결 부분

지수는 죽지 않았습니다. 컴파일러 안으로 이사했고, 그 새 주소는 변수 순서(variable order)입니다. 사슬 계열이 선형 크기 회로로 컴파일된 것은, 부분적으로는 정렬된 순서가 우연히 각 사슬의 두 동전을 인접하게 유지해 준 덕분에 모든 잔여식이 작았고 캐시가 계속 적중했기 때문입니다. 일반적으로 순서는 엄청나게 중요합니다. OBDD-스타일 컴파일에는 어떤 순서 아래에서는 회로가 선형이고 다른 순서 아래에서는 지수적인 고전적 논리식 계열들이 있어(멀티플렉서류 함수들이 교과서적 사례입니다), 순서의 선택 하나만으로 컴파일이 하찮은 것에서 절망적인 것으로 요동칠 수 있습니다. 그리고 잘 고르는 일 자체가 어렵습니다. 주어진 OBDD의 순서를 개선하는 일조차 NP-완전이므로 [7], 실제 컴파일러들은 최적성 보증이 없는 휴리스틱(min-fill 순서, vtree를 위한 하이퍼그래프 분할, 동적 재순서화)으로 물러납니다 [2]. 이 장난감은 이 사다리에서 자신의 위치에 대해 정직합니다. 정렬된 변수 순서를 쓰고, 결코 탐색하지 않으며, 결코 재순서화하지 않습니다(circuit.py 45–49행이 이를 소리 내어 말합니다). 이 장의 의미론, 즉 두 정확성 증명과 두 세미링 평가는 빈틈이 없습니다. 풀리지 않은 것은 컴파일의 품질, 곧 여러분이 얻는 회로와 존재하는 가장 작은 회로 사이의 간극입니다. #P의 벽은 그대로 서 있습니다. 컴파일은 그것을 뚫지 않습니다. 요금소를 컴파일 시점으로 옮길 뿐이며, 드물게 바뀌는 지식 베이스라면 그 요금을 한 번쯤은 치를 만합니다.

왜 중요한가

이 장은 이 권이 다음에 짓는 모든 것의 하중을 받치는 바닥입니다. DeepProbLog는 정확한 확률적 추론을 거쳐 신경망을 훈련시키는데, 그것이 감당 가능한 것은 오직 그 추론이 열거가 아니라 미분 가능한 회로 패스이기 때문입니다. 의미 손실(3부)은 논리 제약을 회로로 한 번 컴파일한 다음 모든 훈련 스텝마다 그것을 거슬러 역전파합니다. 분할 상환 논증이 문자 그대로 그 훈련 루프입니다. Scallop의 유래 세미링과 다음 장의 경사 세미링은 이 장의 세미링 표에 새로 붙는 행들이며, 같은 원-패스 평가자로 평가됩니다. 더 멀리, 5권의 신뢰 이야기는 회로 평가가 정확하다는 사실에 기댑니다. 확률 추정치가 d-DNNF 패스에서 나올 때, 의미론과 $10^{-12}$까지 일치한다는 것은 희망이 아니라 검사 가능한 속성이며, 그것이 바로 추론 프론티어에 모자란 종류의 보증입니다. 두 기둥은 여기서 보기 드문 대칭으로 만납니다. 기호 기둥은 논리식과 건전성 증명을 내놓고, 신경 기둥은 가중치를 내놓을 것이며, 회로는 그 둘이 거래하는 방입니다.

핵심 용어

• 지식 컴파일(knowledge compilation): 논리식을 구조적 보증을 갖춘 목표 언어로 한 번 번역한 다음, 그 언어가 지원하는 질의들에 컴파일된 회로 크기에 다항인(이 장의 질의들에서는 선형인) 시간으로 답하는 것입니다; 컴파일 지도의 간결성-대-질의 절충으로 체계화되었습니다 [1].
• NNF(부정 정규형, negation normal form): 내부 노드는 AND와 OR뿐이고, 부정은 잎에 갇혀 있습니다; 그 자체의 처리 가능성은 없는 캔버스 언어입니다.
• 분해 가능성(decomposability): 모든 AND의 자식들이 쌍마다 서로소인 변수 집합을 언급합니다; $\mathrm{WMC}(A \wedge B) = \mathrm{WMC}(A)\,\mathrm{WMC}(B)$가 성립하는 바로 그 조건입니다.
• 결정성(determinism): 모든 OR의 자식들이 쌍마다 논리적으로 서로소입니다; $\mathrm{WMC}(A \vee B) = \mathrm{WMC}(A) + \mathrm{WMC}(B)$에 포함-배제 보정이 전혀 필요 없게 되는 바로 그 조건이며, 서로소-합 문제의 구조적 치유책입니다.
• 매끄러움(smoothness): 모든 OR의 자식들이 같은 변수 집합을 언급하며, 통과 노드 $\mathrm{pt}(v) = (v \vee \neg v)$로 복원할 수 있습니다; $p + (1-p) = 1$이므로 $(+, \times)$ 아래에서는 무연산이지만, $(\max, \times)$ 아래에서는 하중을 지는데, 그곳에서 통과 노드는 자유 변수의 값을 $\max(p, 1-p)$로 매깁니다.
• d-DNNF(결정론적 분해 가능 부정 정규형, deterministic decomposable negation normal form): 위의 모든 것을 결합한 목표 언어입니다; 계수, MPE, 열거가 각각 한 번의 상향 패스로 실행됩니다.
• 섀넌 전개(Shannon expansion): $\varphi = (x \wedge \varphi|_{x=1}) \vee (\neg x \wedge \varphi|_{x=0})$; 고정된 순서 위에서 잔여식 캐시와 함께 재귀적으로 적용하면, 구성에 의해 결정적이고 분해 가능한 OBDD-스타일 d-DNNF가 나옵니다.
• SDD(문장 결정 다이어그램, sentential decision diagram): OBDD의 변수 순서를 vtree로 일반화한 산업용 목표 언어입니다; 정준적이며, 다항 시간 apply 연산을 갖습니다 [2].
• 교환 세미링(commutative semiring): 평가자가 그 위에서 범용적으로 동작하는 대수 $(\oplus, \otimes, \bar 0, \bar 1)$입니다; $(+, \times)$는 확률을, $(\max, \times)$는 MPE를, 경사 세미링(다음 장)은 도함수를, 전부 하나의 회로에서 읽어 냅니다 [5].
• MPE(최유력 설명, most probable explanation): 최대 가중치의 충족 배정입니다; $(\max, \times)$ 패스로 계산되고, 각 OR에서 그 노드의 값을 달성하는 자식으로 내려가며 해독됩니다.
• 확률 회로(probabilistic circuit): 분해 가능한 곱과 매끄러운(선택적으로 결정적인) 합을 갖춘 계산 그래프들의 우산 용어로, 컴파일된 논리 회로와 학습된 처리 가능 모델을 똑같이 아우릅니다 [6].

이 장이 이끄는 곳

세미링 표는 하나의 예고와 함께 끝났습니다. 운반되는 값이 쌍, 즉 확률과 그 도함수인 행입니다. 다음 장 DeepProbLog: 신경 술어와 경사 반환이 그 예고를 현금으로 바꿉니다. 신경망의 소프트맥스 출력이 리터럴 잎의 확률 이름표가 되고, 회로 패스는 질의 확률을 정확하게 계산하며, 경사 세미링은 같은 패스를 (값, 도함수) 쌍 위에서 실행하여, 논리 질의의 확률이 네트워크 자신의 가중치에 대해 갖는 참된 경사를 네트워크에 건네줍니다. 논리는 네트워크에 덧붙여진 후처리기이기를 멈추고 그 안의 미분 가능한 층이 되며, 이 장의 증명들이 바로 그 층의 순방향 패스를 근사가 아니라 정확한 것으로 만들어 주는 것입니다.

---

컴패니언 코드: examples/integration/circuit.py는 이 장 전체를 구현합니다. 세미링 객체(71–90행), 잔여식 캐시를 갖춘 섀넌-전개 컴파일러(247–282행), 매끄러움 수리(285–319행), 엣지당 연산 하나를 세는 원-패스 평가자(336–374행), 세 가지 구조 검사(379–452행), argmax 해독을 갖춘 MPE(456–480행), 무차별 대입 오라클(485–510행), 그리고 여기 인용된 모든 숫자를 단언하는 실행(519–661행)이며, examples/integration/wmc.py의 인증된 DNF들을 export_for_circuit()(wmc.py 240–252행)을 통해 소비합니다. 모든 표를 바이트 단위로 재현하려면 python3 examples/integration/circuit.py를 실행하십시오. 실행은 다음으로 끝납니다. SUMMARY circuit: queries=4 max|circuit-brute|=1.1e-16 unsmooth_mpe=0.8100 true_mpe=0.6885 wall_n=20 ops=238 assignments=1048576 max|circuit-closed|=0.0e+00