가중 모델 계수: #P의 벽

📍 현재 위치: 2부 · 확률 논리와 회로 — 5장. 분포 의미론은 질의의 확률을 2,048개의 가능 세계에 대한 합으로 정의했고, 각 세계는 고정점까지 전방 연쇄되었습니다; 이 장은 같은 숫자를 다른 화폐로, 즉 하나의 작은 논리식이 갖는 모델들의 가중 개수로 계산한 다음, 계수 그 자체를 어려운 부분으로 만드는 복잡도의 벽을 만납니다.

앞 장은 잔혹한 대가를 치르고 정확성을 사들였습니다. 어떤 질의에든 답하기 위해, 그것은 학술 세계의 열한 개 동전이 이루는 $2^{11}$가지 전체 선택(total choice) 전부를 실체화하고, 그 각각의 안에서 완전한 전방 연쇄 패스를 실행했습니다. 그 대가는 또한 질문 자체에는 기묘하게 무심합니다. 질의 grandAdvisor(alice, carol)은 정확히 두 개의 동전에만 의존하지만, 열거는 열한 개 전부를 뒤집어, 아홉 개의 무관한 동전을 2,048번의 고정점 계산 속으로 끌고 들어갑니다. 이 장은 표준적인 수리, 즉 진지한 확률적 논리 시스템이라면 어디든 그 위에 세워지는 환원을 수행합니다. 질의의 증명들을 모으고, 그것들을 오직 상관있는 동전들에 대한 하나의 명제 논리식으로 컴파일한 다음, 그 논리식으로부터 확률을 가중 모델 계수(weighted model count)로 읽어 내는 것입니다. 이 환원은 정확하며, 조건화를 두 계수의 비로 바꾸고, 모든 어려움을 정확히 이름 붙은 단 하나의 문제 속으로 집중시킵니다. 그것이 이 환원의 미덕이자 평결인데, 왜냐하면 모든 것이 집중되는 그 문제, 즉 논리식의 모델을 세는 일이 표준적인 가정 아래서 NP(비결정적 다항 시간, nondeterministic polynomial time)보다 더 어려운 #P-완전(#P-complete)이기 때문입니다 [1]. 이 장은 그 벽을 그저 인용하는 데 그치지 않고 실제로 측정하며 끝을 맺습니다.

쉽게 말하면

어느 마을 축제가 불꽃놀이를 열게 될 확률을 평가하는 보험 사무소를 상상해 보십시오. 앞 장의 꼼꼼한 사무원은 있을 수 있는 저녁 전부를 통째로 시뮬레이션합니다. 마을 전체에서 불확실한 모든 것의 모든 조합, 즉 수천 가지 시나리오 각각을 처음부터 다시 도출하는 것입니다. 더 영리한 사무원은 먼저 그 쇼가 실제로 무엇에 달려 있는지를 묻고, 단 하나의 체크리스트를 씁니다. 쇼는 (바지선이 도착한다 그리고 허가가 난다) 또는 (예비 부지가 말라 있다 그리고 허가가 난다)일 때 열립니다. 오직 세 개의 불확실한 항목만 등장하므로, 사무원은 그 세 항목이 나올 수 있는 여덟 가지 경우를 나열하고, 체크리스트가 충족되는 행만 남긴 다음, 남은 행들의 확률을 더합니다. 답은 같지만 행은 훨씬 적고, 체크리스트의 두 절반을 모두 충족하는 행이라도 여전히 단 한 행일 뿐이므로 아무것도 이중으로 계산되지 않습니다. 함정은 성장과 함께 찾아옵니다. 체크리스트에 불확실한 항목이 하나씩 늘어날 때마다 행의 수는 두 배가 되므로, 항목 스무 개짜리 체크리스트는 이미 약 백만 개의 행을 필요로 하며, 행을 나열하는 방법을 아무리 영리하게 바꾸어도 그 산술은 달라지지 않습니다. 이 장은 그 영리한 사무원의 방법과 그 정확성, 그리고 그 청구서를 다룹니다.

이 장에서 다루는 내용

• 접지, 처음부터 끝까지 상세히 다룹니다: 1권의 증명기가 모아 낸 질의의 SLD(한정 절을 위한 선택적 선형, Selective Linear Definite-clause) 리졸루션 증명들, 각 증명을 그것이 소비하는 동전들로 환원하는 과정, 그리고 커밋된 실행에서 그대로 인용한, 논리곱들의 논리합으로 조립된 질의 논리식 $\varphi_q$입니다.
• 정확성 보조정리, 양방향 모두: 어떤 세계가 $\varphi_q$를 충족하는 것은 정확히 그 세계에서 질의가 도출 가능할 때이며, 이를 신중하게 논증하면서 한정성(definiteness, 부정이 없음)이 증명을 떠받치는 지점을 짚어 냅니다.
• 재편성 대수: 세계에 대한 합을 충족 배정 기준으로 재편성하여, 질의의 확률이 그 논리식의 가중 모델 계수(weighted model count, WMC)와 같다는 $P(q) = \mathrm{WMC}(\varphi_q, w)$가 근사가 아니라 항등식이 되게 하는 과정입니다; 커밋된 표는 2,048개 세계 오라클과 단언된 1e-12까지, 그리고 측정된 0.0으로 일치합니다.
• 가중 모델 계수를 정의하고 해독합니다: 리터럴 가중치, 배정 가중치, 가중치 없는 특수 경우인 #SAT, 그리고 앞 장의 서로소-합 문제가 구성상 자연스럽게 사라지는 여덟 행짜리 손 계산 자취입니다.
• 두 계수의 비로서의 조건화: $P(q \mid e) = \mathrm{WMC}(\varphi_q \wedge \varphi_e, w) \,/\, \mathrm{WMC}(\varphi_e, w)$를 세계에 대한 조건부 확률로부터 유도하고, 커밋된 세 가지 증거 사례에서 소리 내어 읽어 봅니다.
• 벽을 신중하게 진술합니다: 부류 #P란 무엇인지, 완전성이 실무적으로 무엇을 의미하는지, 그리고 왜 이 파이프라인의 부정 없는 DNF(논리합 정규형, disjunctive normal form) 논리식들조차 정확한 계수에 있어서는 어려운 쪽에 놓이는지입니다.
• 벽을 측정합니다: $n = 8, 12, 16, 20$개의 동전에서 매개변수화된 계열에 대한 커밋된 시간 측정 표, 단언된 그대로 단계마다 열여섯 배씩 늘어나는 열거된 배정, 그리고 장난감 기계의 초 단위 측정치를 정직하게 읽어 낸 것입니다.
• 구조가 숨어 있는 곳: 컴파일된 논리식들은 대단히 반복적입니다; 서로 독립적인 사슬 부분 문제 열 개를 손으로 인수분해하여 평가하면 약 서른 번의 연산만 들지만 열거에는 백만 개의 배정이 필요합니다. 이 대조는 다음 장의 회로가 이용하게 될 간극을 드러내되, 최악의 경우를 이겨 내는 척하지 않습니다.

2,048개의 세계에서 하나의 논리식으로

앞 장의 표기법을 고정합시다. 확률적 사실(probabilistic fact, 동전)의 집합은 $\mathcal{F}$이며, 여기서는 열한 개의 원소를 갖습니다; $C$는 확실한 사실들의 집합이고, $R$은 혼 규칙(Horn rule)들이며, 전체 선택(total choice) $F \subseteq \mathcal{F}$(기호 $\subseteq$는 "의 부분집합이다"라고 읽습니다)는 하나의 가능 세계로, 확률 $P(F) = \prod_{f \in F} p_f \cdot \prod_{f \notin F} (1 - p_f)$를 가지며, 여기서 $\prod$는 그 항들을 서로 곱하고, $f \in F$는 선택된 집합에 든 동전들을 골라내며(기호 $\in$는 "의 원소이다"라고 읽고 $\notin$은 그 부정입니다), $p_f$는 동전 $f$에 매겨진 확률입니다. 성공 확률은 $P(q) = \sum_{F \,:\, F \cup C \cup R \,\vdash\, q} P(F)$, 즉 $q$를 도출하는 세계들의 총 가중치로 정의되었으며, 여기서 기호 $\cup$는 선택된 동전들과 확실한 사실들과 규칙들을 하나의 집합으로 합치고, 턴스타일 $\vdash$는 "1권의 전방 연쇄기에 의해 도출 가능하다"를 뜻합니다. 이 장의 환원은 오라클이 모든 세계 안에서 추론기를 실행하여 검사하는 조건 $F \cup C \cup R \vdash q$를, $F$만 보고서도 검사할 수 있는 명제 논리식으로 대체합니다.

원재료는 증명들입니다. 1권의 SLD 증명기(sld.py)는 첫 번째 도출뿐 아니라 질의의 모든 도출을 열거할 수 있으며, 컴패니언은 그것을 끝까지 뽑아냅니다(wmc.py 69–76행):

def all_proofs(query: tuple) -> list[Proof]:
    """Every SLD derivation of ``query`` from the academic program, in the
    prover's deterministic rule/fact order.  ``sld.prove`` returns only the
    first proof; WMC needs the whole disjunction, so we drain the generator.
    Function-free and acyclic, so the enumeration terminates."""
    facts, rules = program()
    all_rules = [(fact, []) for fact in facts] + list(rules)
    return [proofs[0] for _sub, proofs in _solve([query], {}, all_rules, [0])]

각 증명은 유한한 트리입니다. 뿌리에는 질의가, 각 내부 노드에는 규칙 적용이, 그리고 잎에는 사실들이 있습니다. 확률에 있어서는 몇몇 잎만이 중요합니다. 확실한 사실은 모든 세계에서 성립하고, colleague 규칙의 neq 검사와 같은 내장 가드는 사실 집합을 아예 참조하지 않으므로, 둘 다 우리가 어느 세계에 있는지를 제약하지 않습니다; 실제로 그것을 제약하는 잎은 동전들입니다. 헬퍼 proof_coins(wmc.py 79–88행)는 트리를 훑어, 하나의 증명 $\pi$가 소비하는 확률적 사실들의 집합, 즉 그 $\mathrm{coins}(\pi)$를 정확히 그대로 반환합니다.

이제 동전 $f$마다 하나씩 불 변수(Boolean variable) $x_f$를 도입합니다. 이는 배정이 1(그 동전이 나왔다, $f \in F$) 또는 0(나오지 않았다)으로 설정할 기호입니다. 하나의 증명 $\pi$는, 그것이 소비하는 모든 동전이 나왔을 때 정확히 그 세계에서 통과하며, 이는 논리곱 $\bigwedge_{f \in \mathrm{coins}(\pi)} x_f$(큰 $\bigwedge$는 전체 집합에 걸쳐 "그리고"를 연쇄합니다)입니다. 질의는 어떤 증명이든 통과할 때 성공하며, 이는 증명들에 대한 논리합입니다. 따라서 질의 논리식은 다음과 같습니다.

$$\varphi_q \;=\; \bigvee_{\pi} \; \bigwedge_{f \in \mathrm{coins}(\pi)} x_f,$$

여기서 큰 $\bigvee$는 $q$의 모든 증명 $\pi$에 걸쳐 "또는"을 연쇄합니다. 변수들의 AND에 대한 OR로 이루어진 이런 모양의 논리식을 DNF(논리합 정규형, disjunctive normal form)라고 하며, 확률적 논리 문헌에서는 그 항들을 질의의 설명(explanation)이라고 부릅니다. 두 개의 경계 사례는 별도의 처리가 필요 없이 정의로부터 저절로 나옵니다. 동전을 하나도 소비하지 않는 증명은 공집합 논리곱을 기여하는데, 이는 항상 참인 논리식 ⊤이며, 그래서 $\varphi_q$는 항진식(tautology)이 됩니다. 즉 질의는 확실하며, 커밋된 실행은 동전 없는 질의 person(erin)에 대해 그 계수가 실행의 1e-12 허용오차 안에서 1과 같다고 단언합니다; 실제로 계수기가 계산하는 값은 정확히 1.0입니다(wmc.py 277–281행). 증명이 하나도 없는 질의는 공집합 논리합, 즉 항상 거짓인 ⊥을 산출하며, 정확히 0으로 계수됩니다. 컴파일러는 다섯 줄입니다(wmc.py 114–118행, query_dnf 내부):

    pf = PROB_FACTS if prob_facts is None else prob_facts
    terms = {proof_coins(proof, pf) for proof in all_proofs(query)}
    dnf = _absorb(terms)
    weights = {v: pf[v] for t in dnf for v in sorted(t)}
    return dnf, weights

_absorb 단계(wmc.py 92–99행)는 흡수 법칙(absorption law) $A \vee (A \wedge B) = A$를 적용합니다. 만약 어떤 항의 동전 집합이 다른 항의 동전 집합을 진부분집합으로 포함한다면, 그 큰 항은 불필요한데, $A \wedge B$를 충족하는 어떤 배정이든 이미 $A$를 충족하기 때문이며, 따라서 그 상위집합 항을 삭제해도 어떤 배정의 판정도 바뀌지 않고 그러므로 어떤 계수도 바뀌지 않습니다. 네 개의 커밋된 질의에 대해 컴파일러를 실행하면 실제 논리식들이 인쇄됩니다.

[1] queries compiled to weighted DNFs  φ_q = ∨_proofs ∧_coins x_f
    (a variable x_f per coin; certain facts contribute no variable)
      grandAdvisor(alice, carol)  1 proof(s) -> 1 term(s) over 2 var(s)
          φ = advises(alice, bob) ∧ advises(bob, carol)            w: 0.90, 0.90
      citesTransitively(p3, p1)   1 proof(s) -> 1 term(s) over 2 var(s)
          φ = cites(p2, p1) ∧ cites(p3, p2)                        w: 0.80, 0.90
      colleague(carol, erin)      1 proof(s) -> 1 term(s) over 1 var(s)
          φ = affiliated(erin, cmu)                                w: 0.55
      grandAdvisor(alice, Z)      2 proof(s) -> 2 term(s) over 3 var(s)
          φ = advises(alice, bob) ∧ advises(bob, carol)            w: 0.90, 0.90
            ∨ advises(alice, bob) ∧ advises(bob, dave)             w: 0.90, 0.85

프로그램에는 열한 개의 동전이 있지만, 어떤 논리식이든 많아야 세 개의 변수만을 가집니다. 그 축소야말로 핵심 전부이며, 앞 장의 열거로는 결코 볼 수 없었던 것입니다.

보조정리의 양방향

모든 것이 단 하나의 주장 위에 놓여 있으므로, 그것은 몸짓이 아니라 진짜 증명을 받을 자격이 있습니다. 전체 선택 $F$에 대해, 정확히 $f \in F$일 때 $x_f = 1$로 설정하는 배정을 $\omega_F$라고 쓰고, "그 배정이 논리식을 참으로 만든다"를 $\omega \models \varphi$(기호 $\models$는 "충족한다"라고 읽습니다)라고 씁니다.

보조정리. 모든 전체 선택 $F$에 대해: $\;F \cup C \cup R \vdash q\;$인 것과 $\;\omega_F \models \varphi_q$인 것은 동치입니다.

읽기 관례 하나를 먼저 짚어 둡니다. grandAdvisor(alice, Z)처럼 변수를 가진 질의의 경우, 턴스타일 $\vdash q$는 앞 장의 존재적 성공 의미론을 뜻합니다: 즉 $q$의 어떤 접지 인스턴스가 도출 가능하다는 것입니다. all_proofs가 모든 인스턴스의 증명들을 열거하므로, $\varphi_q$ 안의 증명들에 대한 논리합은 이미 모든 접지화에 걸쳐 있으며, 아래의 양방향 논증은 그대로 성립합니다.

도출 가능하면 충족한다. 세계 $F$가 $q$를 도출한다고 합시다. 전방 연쇄기가 도출하는 모든 것은 잎이 $F \cup C$ 안에 놓인 유한한 도출 트리를 가집니다. 라운드 $k$에서 추가되는 각 원자는, 몸체의 원자들이 모두 그 이전 라운드에 도착한 어떤 규칙의 머리이므로, 라운드에 대한 귀납법으로(앞 장이 단조성을 증명할 때 썼던 것과 같은 라운드별 귀납법으로) 그 원자들의 트리를 그 규칙 적용 아래에 이어 붙일 수 있습니다. 이 동일한 트리는 모든 동전을 이용할 수 있는 전체 프로그램으로부터의 타당한 도출이기도 한데, 왜냐하면 그 잎들이 거기서도 사실이기 때문입니다. $F \subseteq \mathcal{F}$이니까요. all_proofs가 실행하는 것처럼 철저하게 실행된 1권의 SLD 탐색은 전체 프로그램으로부터 나오는 $q$의 모든 도출을 열거합니다. 여기서 "모든"은 코드에 대한 관찰이 아니라 사용 중인 정리입니다: 한정 프로그램에 대한 SLD 리졸루션은 어떤 고정된 선택 규칙에 대해서도 완전하며, 따라서 이 증명기의 가장 왼쪽 우선 규칙에 대해서도 모든 도출 트리는 SLD 반박에 대응하고 SLD 탐색 트리를 남김없이 걸으면 반드시 그 반박을 방문합니다(1권의 리졸루션과 SLD 장은 이 반박 장치를 세우며, 이 프로그램들에서의 완전성은 추론과 증명에서 증명한 전방 연쇄 완전성의 후방 연쇄 쪽 얼굴입니다). 그 열거는 또한 유한합니다(프로그램은 함수 기호가 없고, 유일한 재귀 규칙은 비순환적인 인용 그래프를 따라 내려갑니다). 그러므로 우리의 트리는 열거된 어떤 증명 $\pi$로서 나타납니다. $\pi$의 잎 가운데 동전인 것은 모두 $F$ 안에 놓이는데, 그 트리가 세계 $F$에서 이용 가능한 사실들만을 사용했기 때문입니다; 따라서 $\mathrm{coins}(\pi) \subseteq F$이고, 그래서 $\omega_F$는 항 $\bigwedge_{f \in \mathrm{coins}(\pi)} x_f$의 모든 변수를 1로 설정하며, 그 항은 참이 되고, $\omega_F \models \varphi_q$입니다.

충족하면 도출 가능하다. $\omega_F \models \varphi_q$라고 합시다. DNF의 어떤 항이 $\omega_F$ 아래에서 참이며, 구성상 이는 어떤 열거된 증명 $\pi$에 대해 $\mathrm{coins}(\pi) \subseteq F$임을 뜻합니다. $\pi$가 세계 $F$ 내부에서 타당한 도출이 되려면 무엇이 필요한지 살펴봅시다. 그 잎들, 즉 $\mathrm{coins}(\pi)$에 확실한 사실들과 가드 검사들을 더한 것은 모두 $F \cup C$ 안에서 이용 가능합니다; 그리고 그 내부 노드들, 즉 각각의 규칙 적용은 그 타당성이 오직 규칙과 그 아래의 자식들에만 달려 있을 뿐, 다른 어떤 사실이 존재하는지에는 결코 달려 있지 않습니다. 따라서 동일한 트리가 세계 $F$에서의 도출이 되고, $F \cup C \cup R \vdash q$입니다. ∎

한정성이 무게를 떠받친 지점을 짚어 두어야 하는데, 그것이 정확히 두 번 그렇게 했기 때문입니다. 첫 번째 방향에서는, 작은 세계에서 타당했던 도출이 전체 프로그램에서도 그대로 타당하게 남았습니다; 그것은 앞 장이 한정 프로그램에 대해 증명한 단조성이며, 오직 전체 프로그램만을 보는 all_proofs가 여전히 모든 세계의 증명들을 아우른다는 것을 보장하는 것도 바로 그것입니다. 두 번째 방향에서는, 어떤 증명의 타당성이 오직 그 자신의 잎들이 존재하는지에만 달려 있었습니다. 부정이 끼어드는 순간 이 두 단계는 모두 무너집니다. 실패로서의 부정(negation as failure) 아래에서는 어떤 증명이 어떤 사실의 부재에 의존할 수 있으므로, 전체 프로그램의 증명이 더 작은 세계에서는 실패할 수 있고 그 반대도 가능하며, $\varphi_q$는 부정 리터럴을 담은 훨씬 더 신중한 번역을 필요로 하게 될 것입니다. 이 파이프라인은 이 권이 운용하는 한정적이고 비순환적인 프로그램들에 대해서만 충실하며, 그 이상은 주장하지 않습니다.

재편성: 세계에 대한 합에서 모델 계수로

보조정리는 하나의 치환을 허가하며, 그런 다음 평범한 대수가 환원을 마무리합니다. 정의에서 시작하여 보조정리의 조건을 대입합니다.

$$P(q) \;=\; \sum_{F \,:\, F \cup C \cup R \,\vdash\, q} P(F) \;=\; \sum_{F \,:\, \omega_F \models \varphi_q} P(F).$$

이제 $\varphi_q$가 실제로 볼 수 있는 것을 기준으로 합을 재편성합니다. $V$를 $\varphi_q$에 변수가 등장하는 동전들의 집합이라 하고(grandAdvisor(alice, Z)의 경우 열한 개 중 세 개입니다), 모든 전체 선택 $F$를 논리식이 읽는 부분과 무시하는 부분으로 나눕니다: $F$는 쌍 $(\omega, \rho)$로 결정되는데, 여기서 $\omega$는 $\omega_F$를 $V$의 변수들로 제한한 것이고 $\rho = F \setminus V$는 $V$ 바깥에서 선택된 동전들의 집합입니다(기호 $\setminus$는 "빼기", 즉 집합 차를 뜻합니다). 이 재편성이 성립하는 것은 두 가지 사실 때문입니다. 첫째, $P(F)$는 이 분할에 걸쳐 인수분해되는데, 그것이 동전 하나당 하나의 인자를 갖는 곱이기 때문입니다.

$$P(F) \;=\; \underbrace{\prod_{f \in V,\, \omega(x_f)=1} p_f \prod_{f \in V,\, \omega(x_f)=0} (1-p_f)}_{W(\omega)} \;\cdot\; \underbrace{\prod_{f \notin V,\, f \in \rho} p_f \prod_{f \notin V,\, f \notin \rho} (1-p_f)}_{W'(\rho)}.$$

둘째, $\omega_F \models \varphi_q$인지 여부는 오직 $\omega$에만 달려 있는데, $\varphi_q$가 $V$ 바깥의 어떤 변수도 언급하지 않기 때문입니다. 그래서 $F$에 대한 하나의 합은 그 쌍들에 대한 이중 합이 되고, 충족 검사와 인자 $W(\omega)$는 안쪽 합의 바깥으로 빠져나오며, 안쪽 합은 무너져 접힙니다.

$$P(q) \;=\; \sum_{\omega \,:\, \omega \models \varphi_q} \; \sum_{\rho \subseteq \mathcal{F} \setminus V} W(\omega)\, W'(\rho) \;=\; \sum_{\omega \,:\, \omega \models \varphi_q} W(\omega) \cdot \sum_{\rho \subseteq \mathcal{F} \setminus V} W'(\rho).$$

남은 안쪽 합은 무시된 동전들의 모든 부분집합 $\rho$에 대한 것으로, 아무 조건도 붙어 있지 않으며, 이는 두 항짜리 합들의 곱과 같습니다: 곱 $\prod_{f \notin V} \big(p_f + (1 - p_f)\big)$을 분배 법칙으로 전개하면, 각 동전에 대해 $p_f$ 또는 $(1-p_f)$ 가운데 하나를 고르는 방법마다 하나의 항이 생기는데, 이는 정확히 부분집합 $\rho$마다 하나씩의 항 $W'(\rho)$이며, 각각 정확히 한 번씩 나타납니다. 따라서

$$\sum_{\rho \subseteq \mathcal{F} \setminus V} W'(\rho) \;=\; \prod_{f \notin V} \big(p_f + (1 - p_f)\big) \;=\; \prod_{f \notin V} 1 \;=\; 1,$$

그리고 무시된 동전들은 답에서 완전히 사라집니다.

$$P(q) \;=\; \sum_{\omega \,:\, \omega \models \varphi_q} W(\omega).$$

우변은 더 이상 세계도, 추론기도, 고정점도 언급하지 않습니다. 그것은 변수별 가중치들의 곱을, 하나의 논리식을 충족하는 배정들에 대해 합한 것이며, 이름을 갖고 있습니다.

가중 모델 계수, 정의하기

$\varphi$를 $n$개의 불 변수 $x_1, \ldots, x_n$에 대한 명제 논리식이라 하고, 여기서 $n$은 그 논리식이 언급하는 서로 다른 동전의 개수입니다. 배정(assignment) $\omega$는 각 변수에 $\lbrace 0, 1 \rbrace$ 안의 값을 부여하며, 그런 배정은 $2^n$개 있고, $\omega \models \varphi$인 배정을 $\varphi$의 모델(model)이라고 부릅니다. 모든 리터럴(literal, 변수 또는 그 부정, $\neg x_i$로 씁니다)에 가중치를 부여합니다: $w(x_i) = p_i$이고 $w(\neg x_i) = 1 - p_i$입니다. 어떤 배정의 가중치는 그것이 참으로 만드는 $n$개 리터럴의 가중치들의 곱이며, 가중 모델 계수(weighted model count)는 모델들의 총 가중치입니다.

$$\mathrm{WMC}(\varphi, w) \;=\; \sum_{\omega \,\models\, \varphi} \;\; \prod_{i \,:\, \omega(x_i)=1} w(x_i) \;\cdot\; \prod_{i \,:\, \omega(x_i)=0} w(\neg x_i).$$

앞 절의 재편성 항등식은 정확히 $w(x_f) = p_f$일 때 $P(q) = \mathrm{WMC}(\varphi_q, w)$라고 말하고 있습니다. 대신 모든 리터럴 가중치를 1로 설정하면 가중치 없는 특수 경우를 되찾습니다: 그러면 각 모델은 정확히 1을 기여하고, 합은 모델의 개수가 되는데, 이것이 #SAT(샤프-SAT라고 읽습니다)라고 불리는 문제입니다. 가중 모델 계수는 각 모델에 확률이 붙은 #SAT이며, 이 단 하나의 문제는 정확한 확률적 추론의 공통 화폐가 되었습니다: 그것을 한 번 잘 풀어내면, 그 위에 있는 여러 형식체계 전체가 그 덕을 봅니다 [2].

컴패니언은 그 정의를 문자 그대로 계산합니다(wmc.py 146–167행, wmc_counted 내부):

    variables = sorted({v for term in dnf for v in term})
    n = len(variables)
    index = {v: i for i, v in enumerate(variables)}
    # Each term as a bitmask: ω ⊨ ∧_{f∈t} x_f  ⇔  bits & mask_t == mask_t.
    masks = [sum(1 << index[v] for v in term) for term in dnf]
    # w(x_i) if bit i is 1, else 1 − w(x_i).
    p = [weights[v] for v in variables]
    q = [1.0 - weights[v] for v in variables]

    satisfied_weights: list[float] = []
    enumerated = 0
    # Integer bits = 0 .. 2^n − 1 IS the assignment ω: bit i gives ω(x_i).
    for bits in range(1 << n):
        enumerated += 1
        # P(ω) = Π_{ω(x_i)=1} p_i · Π_{ω(x_i)=0} (1 − p_i)  (independent coins)
        w = 1.0
        for i in range(n):
            w *= p[i] if bits >> i & 1 else q[i]
        # ω ⊨ φ  ⇔  some DNF term is fully true under ω.
        if any(bits & m == m for m in masks):
            satisfied_weights.append(w)
    return math.fsum(satisfied_weights), enumerated

$0$부터 $2^n - 1$까지의 모든 정수는 그 자체가 하나의 배정입니다(비트 $i$가 $x_i$의 값을 줍니다). 각각은 가중치가 매겨지고, 각각은 DNF에 대해 검사되며, math.fsum은 최종 덧셈을 정확히 반올림된 상태로 유지하여 아래의 1e-12 비교가 부동소수점 잡음이 아니라 의미론을 검사하도록 합니다. 정의가 grandAdvisor(alice, Z)에서 실제로 작동하는 모습을 지켜봅시다. 그 논리식은 세 개의 변수를 가집니다; $x_1$ = advises(alice, bob) (확률 $0.90$), $x_2$ = advises(bob, carol) (확률 $0.90$), $x_3$ = advises(bob, dave) (확률 $0.85$)로 줄여 쓰면, $\varphi = (x_1 \wedge x_2) \vee (x_1 \wedge x_3)$입니다. 여덟 개의 배정 전부를 손으로 계산하면 다음과 같습니다.

$\omega(x_1)$	$\omega(x_2)$	$\omega(x_3)$	$\omega$의 가중치	$\varphi$의 모델인가?	기여분
0	0	0	$0.10 \cdot 0.10 \cdot 0.15 = 0.0015$	아니요	—
1	0	0	$0.90 \cdot 0.10 \cdot 0.15 = 0.0135$	아니요	—
0	1	0	$0.10 \cdot 0.90 \cdot 0.15 = 0.0135$	아니요	—
0	0	1	$0.10 \cdot 0.10 \cdot 0.85 = 0.0085$	아니요	—
1	1	0	$0.90 \cdot 0.90 \cdot 0.15 = 0.1215$	예, 항 1	$0.1215$
1	0	1	$0.90 \cdot 0.10 \cdot 0.85 = 0.0765$	예, 항 2	$0.0765$
0	1	1	$0.10 \cdot 0.90 \cdot 0.85 = 0.0765$	아니요	—
1	1	1	$0.90 \cdot 0.90 \cdot 0.85 = 0.6885$	예, 두 항 모두, 한 번만 계수됨	$0.6885$

여덟 개의 가중치는 합이 $1$이 되며(그것들은 배정들에 대한 확률분포입니다), 세 개의 모델은 $0.1215 + 0.0765 + 0.6885 = 0.8865$를 기여합니다. 이를 앞 장의 서로소-합 전시물과 비교해 보십시오. 증명 곱들의 순진한 합 $0.81 + 0.765 = 1.575$는, 전부-참 배정이 두 항 모두를 충족하여 두 번 계수되기 때문에 실패했습니다; 포함-배제는 이중으로 계수된 $0.6885$를 손으로 빼서 그것을 고쳤습니다. WMC 정식화에서는 고쳐야 할 것이 아무것도 없습니다: 표의 맨 아래 행은 하나의 배정이고, if any(...) 줄은 그것이 몇 개의 항을 충족하든 상관없이 그 가중치를 한 번만 덧붙이며, 겹침 문제는 수정이 아니라 구성에 의해 애초에 사라져 있습니다. 커밋된 실행은 네 개의 질의 전부를 2,048개 세계 오라클과 대조하여 인증하고, 1e-12 이내의 일치를 단언하며(wmc.py 290–294행), 이 세계에서는 정확히 0인 차이를 측정합니다.

      query                        vars  assign   WMC(φ_q, w)      enumeration      |diff|
      grandAdvisor(alice, carol)      2       4   0.810000000000   0.810000000000   0.0e+00
      citesTransitively(p3, p1)       2       4   0.720000000000   0.720000000000   0.0e+00
      colleague(carol, erin)          1       2   0.550000000000   0.550000000000   0.0e+00
      grandAdvisor(alice, Z)          3       8   0.886500000000   0.886500000000   0.0e+00
      overlap handled free: grandAdvisor(alice, Z)'s two terms share
      advises(alice, bob); naive Σ term-products = 1.575000000000 (>1, not a
      probability) while WMC counts each assignment once: 0.886500000000

assign 열을 오라클의 상수 2,048과 견주어 읽어 보십시오: 이 환원은 답을 털끝만큼도 바꾸지 않았고, 작업량을 $2^{11}$번의 전방 연쇄 패스에서 많아야 $2^3$개의 가중치를 계산하고 검사하는 배정으로 바꾸었습니다(구조 절에서 값을 매기듯 곱셈 24번과 검사 8번입니다). 장난감 세계에서는 그 절약이 겉치레에 불과합니다. 이 장의 나머지는 일반적으로 왜 그것 역시 구원이 되지 못하는지에 관한 것입니다.

환원과 그 대가: 증명들은 세 변수짜리 DNF로 컴파일되고, 그 가중 모델들은 정확히 0.8865로 합해지며, 변수 개수가 늘어남에 따라 같은 계수 절차가 지수적인 벽으로 걸어 들어간다. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

조건화는 두 계수의 비다

증거를 관측하는 것은 확률적 지식 베이스를 쓸모 있게 만드는 연산이며, 이 환원은 새로운 기계 장치 없이 그것을 다룹니다. 계산해야 할 대상은 $P(q \mid e)$이며, 여기서 세로줄은 "주어졌을 때"라고 읽습니다: 즉 증거 $e$가 성립한다고 할 때 $q$가 성립할 확률입니다. 조건부 확률(conditional probability)의 정의에 따라, $P(e) \gt 0$인 사건들에 대해,

$$P(q \mid e) \;=\; \frac{P(q \wedge e)}{P(e)},$$

여기서, 가능 세계에 대해 결합 사건 $q \wedge e$는 "그 세계가 둘 다 도출한다"는 뜻이며, $P(q \wedge e) = \sum_{F \,:\, F \vdash q \text{ and } F \vdash e} P(F)$입니다(완전한 턴스타일을 줄여 썼습니다). 보조정리를 각 논리곱 항에 따로 적용합니다: $F$가 $q$를 도출하는 것은 $\omega_F \models \varphi_q$인 것과 동치이고, $F$가 $e$를 도출하는 것은 $\omega_F \models \varphi_e$인 것과 동치이므로, $F$가 둘 다 도출하는 것은 $\omega_F \models \varphi_q \wedge \varphi_e$인 것과 동치입니다. 그러면 재편성 논증은 앞서와 한 자 한 자 똑같이 진행되는데, 다만 이제 $V$는 두 논리식의 변수 집합들의 합집합이 되며, 분자와 분모 모두가 계수가 됩니다.

$$P(q \mid e) \;=\; \frac{\mathrm{WMC}(\varphi_q \wedge \varphi_e,\, w)}{\mathrm{WMC}(\varphi_e,\, w)}.$$

작은 구문상의 잡일 하나가 남아 있습니다: $\varphi_q \wedge \varphi_e$는 두 DNF의 논리곱이지, 그 자체로 DNF는 아니므로, 계수기가 그것을 곧바로 처리할 수 없습니다. 분배 법칙이 그것을 다시 씁니다. $(\bigvee_i A_i) \wedge (\bigvee_j B_j) = \bigvee_{i,j} (A_i \cup B_j)$로, 쌍마다 하나의 결합된 항을 만든 다음 흡수를 적용합니다(wmc.py 121–129행, dnf_and). 그러면 그 비 자체는 같은 계수기에 대한 두 번의 호출이 되고, 세 번째 호출은 표시용 사전 확률을 계산합니다(wmc.py 186–193행, conditional 내부):

    dnf_q, w_q = query_dnf(query)
    dnf_e, w_e = query_dnf(evidence)
    w = {**w_q, **w_e}
    prior = wmc(dnf_q, w_q)
    joint = wmc(dnf_and(dnf_q, dnf_e), w)
    p_e = wmc(dnf_e, w_e)
    assert p_e > 0.0, f"evidence {evidence} has probability 0; cannot condition"
    return prior, joint, joint / p_e

이 두-계수의-비는 논리 프로그램에만 국한된 요령이 아닙니다; 그것은 완전한 베이즈 네트워크 추론이 가중 모델 계수로 옮겨진 것과 같은 환원으로, 각 조건부 확률 표 항목이 가중 리터럴로 부호화되고 증거가 질의 논리식에 논리곱으로 덧붙습니다 [3]. 커밋된 실행은 학술 세계 위에서 이를 세 가지 방식으로 시연하며, 각각은 세계-열거 오라클과 대조하여 1e-12까지 검사됩니다(wmc.py 313–329행):

[3] conditioning = two counts: P(q | e) = WMC(φ_q ∧ φ_e, w) / WMC(φ_e, w)
      q = grandAdvisor(alice, dave)    e = grandAdvisor(alice, carol)
        P(q) = 0.765000000000   P(q ∧ e) = 0.688500000000   P(q | e) = 0.850000000000
        (e entails the proofs' shared coin advises(alice, bob), so only the
         remaining coin advises(bob, dave) = 0.85 is left standing)
      q = citesTransitively(p3, p1)    e = cites(p2, p1)
        P(q) = 0.720000000000   P(q ∧ e) = 0.720000000000   P(q | e) = 0.900000000000
        (e observes one chain link; exactly the other link cites(p3, p2) is left
         standing: posterior = 0.90)
      q = grandAdvisor(alice, carol)   e = colleague(carol, erin)
        P(q) = 0.810000000000   P(q ∧ e) = 0.445500000000   P(q | e) = 0.810000000000
        (e shares NO coin with q, so conditioning changes nothing at all
         the posterior equals the prior, to 1e-12)

사례 (a)를 소리 내어 읽어 봅시다. 논리식들이 눈에 보이고 나면 숫자들이 스스로를 설명하기 때문입니다. 질의는 "alice가 dave를 grand-advise한다"이며, 앞서의 축약으로 $\varphi_q = x_1 \wedge x_3$이고 사전 확률은 $0.90 \cdot 0.85 = 0.765$입니다; 증거는 "alice가 carol을 grand-advise한다"이며, $\varphi_e = x_1 \wedge x_2$입니다. 이 둘의 논리곱은 $x_1 \wedge x_2 \wedge x_3$이고, 계수는 $0.90 \cdot 0.90 \cdot 0.85 = 0.6885$이며, 사후 확률은

$$P(q \mid e) \;=\; \frac{p_1\, p_2\, p_3}{p_1\, p_2} \;=\; p_3 \;=\; 0.85 .$$

carol에 대한 grand-advising을 관측하는 것은 두 질의가 공유하는 동전, 즉 alice에서 bob으로 가는 지도 엣지를 확증하므로, dave에 대해 남아 있는 유일한 의심은 증거가 건드리지 않는 그 하나의 동전뿐이며, 사후 확률은 정확히 그 동전의 가중치 위에 내려앉아, 사전 확률 $0.765$보다 올라갑니다. 사례 (b)는 멱등성이 추론 노릇을 하는 경우입니다: $\varphi_e$의 단일 논리곱 항인 동전 cites(p2, p1)은 이미 $\varphi_q$의 항들 가운데 있으므로, 분배가 만들어 내는 그 하나의 항은 $\varphi_q$ 자신의 항이 바뀌지 않은 것이며(동전 집합 수준에서는 $x \wedge x = x$입니다), $\varphi_q \wedge \varphi_e$는 다시 $\varphi_q$로 무너지고, 결합 확률은 사전 확률 $0.72$와 같으며, 사후 확률은 $0.72 / 0.80 = 0.90$, 즉 다른 사슬 고리입니다. 사례 (c)는 무관성이 정리 모양을 갖춘 경우입니다: 두 논리식은 어떤 변수도 공유하지 않으므로, 재편성 논증에서와 같은 인수분해에 의해 결합 계수는 곱 $0.81 \cdot 0.55 = 0.4455$이며, 그 비는 사전 확률을 손대지 않은 채 그대로 돌려줍니다. erin의 소속에 관한 증거는 지도에 관한 질의를 움직일 수 없으며, 이는 이제 직관이 아니라 변수-서로소 논리식들에 관한 항등식입니다.

벽, 신중하게 진술하기

이제 대가를 따져 봅시다. 지금까지의 모든 것은 추론을 계수로 환원했습니다; 정직한 질문은 계수가 우리가 출발했던 것보다 더 쉬운가입니다. 그 답은 이름 붙은 정리이며, 먼저 하나의 정의가 필요합니다. 많은 결정 문제는 "적어도 하나의 증인이 존재하는가"라는 모양을 하고 있습니다: 인스턴스 $x$(논리식 하나), 다항 시간 검사 $R(x, y)$("$y$가 $x$의 충족 배정인가?"), 그리고 $x$의 크기에 대한 다항식보다 길지 않은 증인 $y$입니다. 그런 문제들의 부류가 NP입니다. 부류 #P(샤프-P라고 읽습니다)는 그런 관계마다, $x$를 $R(x, y)$를 만족하는 증인 $y$의 개수로 보내는 함수를 담고 있습니다. 계수는 판정보다 엄밀히 더 많은 것에 답합니다: 그 개수로부터 그것이 0인지 아닌지를 읽어 낼 수 있으므로, 계수 오라클은 결정 문제를 공짜로 해결하며, 그 역이 바로 전체 질문입니다.

	판정	계수
증인에 관한 질문	적어도 하나 존재하는가?	몇 개나 존재하는가?
명제 논리식에 대해	SAT: $\varphi$가 충족 가능한가? (NP-완전)	#SAT: $\varphi$의 모델은 몇 개인가? (#P-완전)
$\varphi_q$와 같은 단조 DNF에 대해	자명함: 어느 한 항의 변수들을 참으로 만들면 된다	여전히 #P-완전
이 장의 파이프라인에서	$P(q) \gt 0$인가? 증명 하나면 충분하다	$P(q)$ 그 자체: 모든 모델의 무게를 단다

그 토대가 되는 결과들은 Valiant에게서 나왔습니다 [1]: #SAT는 #P-완전이며, 이는 #P에 속한 모든 계수 문제가 다항 시간 안에 그것으로 변환된다는 뜻이고, 따라서 효율적인 정확한 #SAT 알고리즘이 있다면 그것은 곧 #P 전체에 대한 효율적인 정확한 알고리즘이 되리라는 뜻입니다. 가중 모델 계수는 그 난해함을 즉시 물려받는데, 모든 리터럴 가중치를 1로 설정하면 WMC 오라클이 #SAT 오라클로 바뀌기 때문입니다. 표의 세 번째 행은 우리의 특정 논리식들에 대해 희망 섞인 생각을 품는 것을 금지하는 부분입니다. 이 파이프라인이 컴파일하는 DNF들은 단조(monotone)입니다(부정된 변수가 결코 등장하지 않으며, 한정 프로그램은 그런 것을 만들어 낼 수 없습니다), 그리고 그것들의 충족가능성을 판정하는 일은 자명합니다. 그러나 단조 DNF의 모델을 세는 일은, 모든 항이 단 두 개의 변수만 갖는 경우에도 이미 #P-완전입니다 [1]. 여기서 부류와 인스턴스를 분리해서 봐야 합니다: 그 결과는 사슬 계열의 부류, 즉 단조 2-DNF를 다루지만, 그 특정 인스턴스들을 다루지는 않습니다. 그 인스턴스들의 항들은 일부러 어떤 변수도 공유하지 않으며, 측정 절이 보여 주듯 쉽습니다; 어려운 단조 2-DNF는 서로 겹치는 항들을 필요로 하며, 아래의 벽 표는 열거기의 비용을 매기는 것이지, 인스턴스들의 본질적인 난해함을 매기는 것이 아닙니다. 난해함은 부정이나 판정 안에 있는 것이 아니라, 정확한 계수 그 자체 안에 있으며, 정확한 계수에 있어서는 우리의 친절해 보이는 설명 논리식들도 정본적인 어려운 부류 바깥이 아니라 안쪽에 놓여 있습니다. (근사 계수는 DNF 위에서는 다른 이야기이며, 마무리 절에서 그것으로 돌아옵니다.)

그 벽은 얼마나 높이 닿아 있을까요? 증명 없이 진술하는 정직한 맥락 한 문장은 이렇습니다: #SAT 오라클에 질의할 수 있는 다항 시간 기계는 다항 계층(polynomial hierarchy) 전체, 즉 NP 위에 쌓인 복잡도 부류들의 무한한 탑에 속한 모든 문제를 풀 수 있으며, 그래서 그 계층은 $\mathrm{P}^{\#\mathrm{P}}$ 안에 들어갑니다 [4]. 그러므로 실무적으로 완전성이 뜻하는 바는 이렇습니다: 일반적인 다항 시간 가중 모델 계수기가 있다면, 그것은 영리한 자료구조가 아니라 우리가 지금 이해하고 있는 복잡도 이론 전체를 무너뜨리는 것이 될 것입니다. 이 권이 정확한 추론을 값비싼 것으로 다룰 때, 바로 이 정리가 그 뒤로 미뤄지고 있는 것입니다.

벽, 측정하기

최악의 경우에 관한 정리는 측정을 받을 자격이 있으므로, 컴패니언은 지수적 증가가 눈에 보이고 답을 독립적으로 검사할 수 있는 논리식 계열을 만듭니다. grandAdvisor 패턴의 독립적인 복사본 $k$개를 취합니다: 사슬 $i$는 그 두 동전이 모두 나올 때 연결되며, $a_i$는 $0.8$, $b_i$는 $0.7$이고, 질의는 적어도 하나의 사슬이 연결되는지를 묻습니다. 그 논리식은 $n = 2k$개의 변수에 대한 단조 2-DNF $\varphi_n = \bigvee_{i} (a_i \wedge b_i)$입니다(wmc.py 220–227행, chain_family 내부):

    assert n % 2 == 0, "the family needs n = 2k coins"
    dnf: list[frozenset] = []
    weights: dict[tuple, float] = {}
    for i in range(n // 2):
        a, b = ("chain", str(i), "a"), ("chain", str(i), "b")
        weights[a], weights[b] = CHAIN_P
        dnf.append(frozenset({a, b}))
    return tuple(dnf), weights

사슬들이 어떤 동전도 공유하지 않으므로, 정확한 답은 계수기를 견주어 볼 닫힌 형태를 갖습니다. 한 사슬이 연결될 확률은 $0.8 \cdot 0.7 = 0.56$이고 실패할 확률은 $1 - 0.56 = 0.44$입니다; 사슬들은 독립적이므로, $k$개 모두가 함께 실패할 확률은 $0.44^k$이고, "적어도 하나가 연결된다"는 그 여사건입니다:

$$P \;=\; 1 - 0.44^{\,k}.$$

커밋된 실행은 $n = 8, 12, 16, 20$에서 무차별 대입 계수기의 시간을 잽니다:

    φ = ∨_i (a_i ∧ b_i) with w(a_i) = 0.8, w(b_i) = 0.7 — brute force
    touches ALL 2^n assignments; +4 coins = 16× the work, every time
      n    k  assignments   WMC(φ, w)        1 − 0.44^k       |diff|    seconds*
       8   4          256   0.962519040000   0.962519040000   1.1e-16     0.000
      12   6        4,096   0.992743686144   0.992743686144   1.1e-16     0.004
      16   8       65,536   0.998595177637   0.998595177637   1.1e-16     0.071
      20  10    1,048,576   0.999728026391   0.999728026391   1.1e-16     1.380
      *measured wall-clock, shown for scale only, asserted nowhere;
       the assignment COUNT (exactly 2^n, ratio 16 per step) is asserted

열들을 정직하게 읽어야 하는데, 그것들이 서로 다른 종류의 것을 말해 주기 때문입니다. assignments 열은 기계와 무관한 산술입니다: 계수기는 정확히 $2^n$개의 배정을 열거했으며, 이 실행은 네 개의 동전이 늘어날 때마다 그 개수가 정확히 $2^4 = 16$배가 된다고 단언합니다(wmc.py 344–346행). |diff| 열은 $1.1 \times 10^{-16}$으로, 이는 배정밀도 부동소수점의 최하위 자리 한 단위입니다: 열거와 닫힌 형태는 기계 정밀도까지 일치합니다. seconds 열은 파이썬 루프에 대한 노트북 측정치로, 규모 감각을 위해 제시될 뿐 어디서도 단언되지 않습니다; 실행할 때마다 그 숫자는 흔들리지만, 인터프리터 오버헤드를 지나고 나면 그 추세는 배정 개수를 따라갑니다(마지막 두 단계는 정확한 16배에 견주어 약 18배와 19배로 늘어났습니다). 그 장난감 측정치라는 단서를 붙여 두고 추세를 외삽해 보면, 그리고 안쪽의 가중치 루프가 배정 하나당 $n$번의 곱셈을 치른다는 것을 기억하면: $n = 40$에서 이 루프는 $2^{20} \approx$ 백만 배 더 많은 배정을 열거하며, 각각은 폭이 두 배이므로, 대략 $n = 20$ 비용의 이백만 배, 즉 약 한 달이 걸립니다; $n = 60$에서는 배정의 폭이 세 배가 되어, 대략 15만 년 규모가 됩니다. 한편 answer 열은 $0.9625$에서 $1$을 향해 서서히 기어가며, $n = 20$에 이르면 수치적으로는 지루해집니다. 계산되고 있는 값은 거의 상수인데, 그것을 열거로 계산하는 비용은 동전 하나마다 아랑곳없이 두 배가 됩니다. 그 불일치, 즉 쉬워 보이는 숫자에 지수적인 작업의 값이 매겨진다는 것이야말로, #P의 벽 뒤에서 살아간다는 것이 안에서 볼 때 어떤 느낌인지입니다.

구조가 숨어 있는 곳

무차별 대입 열은 문제가 아니라 알고리즘을 측정하며, 이 논리식들 위에서는 그 둘 사이의 간극이 어마어마합니다. grandAdvisor(alice, Z)를 다시 살펴봅시다: 두 항은 동전 $x_1$을 공유하므로, 분배 법칙이 그것을 인수로 빼낼 수 있습니다,

$$(x_1 \wedge x_2) \vee (x_1 \wedge x_3) \;=\; x_1 \wedge (x_2 \vee x_3),$$

그리고 그 인수분해된 형태는 열거가 아니라 평가될 수 있습니다. 논리합 $x_2 \vee x_3$는 확률 $1 - (1 - 0.90)(1 - 0.85) = 1 - 0.015 = 0.985$를 가지며(그 두 변수는 서로 다른 동전이므로 실패 확률들이 곱해집니다), 독립적인 $x_1$을 논리곱으로 결합하면 $0.90$을 곱하게 되어, $0.90 \cdot 0.985 = 0.8865$가 나옵니다: 다섯 번의 산술 연산, 즉 두 번의 여사건, 한 번의 곱, 한 번의 여사건, 한 번의 곱으로 얻은 정확한 답이며, 이는 표의 여덟 개 가중 행이 치르는 스물네 번의 곱셈과 여덟 번의 검사와 대조됩니다. 사슬 계열은 더 극명합니다. 그 인수분해된 평가는 사슬마다 하나의 곱과 하나의 여사건, $k$개의 여사건들에 걸친 하나의 누적 곱, 그리고 마지막 여사건 하나를 필요로 합니다: 대략 $3k$번의 연산이며, $n = 20$에서는 약 서른 번인데, 이는 각각 스무 번의 곱셈을 치르는 $2^{20} = 1{,}048{,}576$개의 열거된 배정, 즉 도합 약 2천1백만 번과 대조됩니다. 서른 개의 서로 다른 부분 문제가 백만 행짜리 열거 속에 숨어 있었던 것인데, 그 열거가 그 사슬 바깥의 열여덟 개 동전의 배정마다 매번 각 사슬의 작은 계산을 다시 도출하기 때문입니다.

두 지름길 모두 정당했으며, 정확히 왜 그런지가 중요합니다. $x_1$을 인수로 빼낸 것은 순수한 불 대수였습니다; $\vee$를 곱들의 여사건으로, $\wedge$를 곱으로 바꾼 것이 건전했던 것은 오직, 각 단계에서 양쪽이 어떤 변수도 공유하지 않아 그 사건들이 독립적이었고 확률들을 곱할 수 있었기 때문입니다. 컴파일된 회로는 다르고 더 일반적인 경로로 같은 수치에 도달합니다: 그것은 논리합을 서로 배타적인 가지들로 다시 씁니다, $x_2 \vee (\neg x_2 \wedge x_3)$로, 그 사건들은 결코 둘 다 발화할 수 없으므로, 가지별 계수를 그냥 더하는 것이 건전하며, $0.90 + 0.10 \cdot 0.85 = 0.985$로 다시 같은 값이 나옵니다; 그 상호 배타성이 바로 결정성(determinism) 속성이며, 위에서 쓴 곱들의 여사건 지름길은 그 재작성의 독립성 특수 경우입니다. 그 두 조건, 즉 두 가지가 결코 함께 발화하지 않는 논리합, 그리고 양쪽이 어떤 변수도 공유하지 않는 논리곱은, 정확히 다음 장이 이름 붙일(결정성과 분해 가능성) 그리고 하나의 논리식 안으로 의도적으로 컴파일해 넣을 구조적 성질들입니다. 그것이 탈출로입니다: 더 빠른 열거기가 아니라, 단 한 번의 재구조화이며 그 이후로는 계수가 그 구조 위의 한 번의 패스만큼의 비용만 듭니다. 그리고 그 정직한 경계는 앞 절의 정리에 의해 정해집니다. 재구조화가 성공하는 것은 논리식의 변수 상호작용이 충분히 국소적일 때, 즉 논리식의 트리너비(treewidth)와 비슷한 너비 매개변수가 작게 유지될 때이며, 학술 세계의 논리식들은 논리식이 국소적일 수 있는 만큼 국소적입니다. 상호작용이 전역적으로 얽혀 있는 곳에서는, 알려진 어떤 컴파일된 형태든 지수적으로 폭발하며(다음 장은 그 회로 언어들에 걸쳐 정확히 이 간결성 절충을 값매기고, 변수 순서 하나의 선택만으로 회로가 선형에서 지수로 널뛰는 논리식 계열들을 보여 줍니다), #P-완전성은 $\mathrm{FP} = \#\mathrm{P}$가 아닌 한 현재든 미래든 어떤 다항 시간 컴파일-후-계수 파이프라인도 최악의 경우를 피할 수 없는 항구적인 이유입니다. 여기서 $\mathrm{FP}$는 다항 시간에 계산 가능한 함수들의 부류, 즉 판정 부류 P에 대응하는 함수-부류 짝입니다. 다음 장은 열거를 이겨 냅니다. 그 무엇도 벽을 이기지는 못합니다.

모두를 다스리는 하나의 계수 문제

왜 한 분야 전체가 자신의 추론을 이 하나의 어려운 문제로 깔때기처럼 몰아넣는 데 동의했을까요? 집중 그 자체가 전략이기 때문입니다. 이 환원은 그 위에 있는 모든 형식체계에 같은 표적을 제공합니다: 베이즈 네트워크는 자신의 조건부 확률 표를 가중 절로 부호화함으로써 도착하고, 확률적 논리 프로그램은 정확히 이 장이 축소판으로 재연한 파이프라인, 즉 프로그램을 질의와 상관있는 부분으로 접지하고, 그 접지된 프로그램을 가중 불 논리식으로 번역하고, 계수하는 파이프라인을 거쳐 도착합니다 [5]. (실전 파이프라인들은 CNF, 즉 부정 리터럴을 담을 수 있는 OR-절들의 AND인 논리곱 정규형으로 번역합니다; 그것들은 더 신중한 부호화로 순환과 부정을 다루고, 논리식을 열거하는 대신 컴파일합니다; 우리의 설명-DNF는 한정적이고 비순환적인 특수 경우이며, 컴파일러의 자리는 일부러 비워 둔 것입니다.) 이 공유된 표적이 주는 보상은, 계수기와 컴파일러에 대한 모든 개선이 논리 프로그램, 베이즈 네트워크, 그리고 스스로를 가중 논리식으로 부호화할 수 있는 그 밖의 모든 것에 동시에 상속된다는 점입니다. 진술할 문제 하나, 최적화할 자리 하나입니다. 그리고 이 권에게 결정적인 것으로, 미분할 자리도 하나입니다: $\mathrm{WMC}$의 합-곱 모양은 실수의 대수 $(+, \times)$ 위에서의 평가이며, 그 대수를 다른 세미링(semiring, 합-곱 모양이 필요로 하는 분배 법칙을 지키는 자신만의 "덧셈"과 "곱셈"을 갖춘 수 체계)으로 바꾸면 같은 구조로 다른 질문에 다시 답하게 되는데, 여기에는 경사 세미링과 함께, DeepProbLog 장이 그것을 통해 신경망을 훈련시킬, 동전 확률들에 대한 계수의 도함수도 포함됩니다.

아직 풀리지 않은 부분

정확성은 이 장이 포기하기를 거부한 것이므로, 정직한 질문은 그것을 내어 줌으로써 무엇을 얻는가이며, 그 답은 논리식의 크기보다 그 모양에 더 많이 달려 있습니다. 이 장이 실제로 컴파일하는 단조 DNF들에 대해서는, 소식이 정말로 좋습니다: 정확한 계수는 여전히 #P-완전이지만, 근사 계수는 다루기 쉽습니다. 고전적인 무작위 스킴은 항 단위로 배정을 표집하여 DNF의 계수를 추정하며, 이는 완전 다항 무작위 근사 스킴(fully polynomial randomized approximation scheme, FPRAS)입니다: 어떤 정확도 $\varepsilon \gt 0$과 실패 확률 $\delta \gt 0$에 대해서든, 그것은 적어도 $1-\delta$의 확률로, 논리식 크기와 $1/\varepsilon$과 $\log(1/\delta)$에 대해 다항 시간 안에, 참값의 인수 $(1+\varepsilon)$ 이내의 값을 반환하며, 이 추정기는 가중치가 있는 경우로도 확장됩니다 [6]. 그것은 어디서도 SAT 솔버를 참조하지 않는데, DNF의 모델 하나를 만들어 내는 일이 자명하기 때문입니다. 그러므로 이 장의 벽은 설명 DNF에 대한 값싼 정확한 답을 금지하지만, 그것들에 대한 값싸고 보장된 근사까지 금지하지는 않습니다. 그 어려운 경계는 부호화 한 걸음 떨어진 곳, 즉 실전 파이프라인들이 살아가는 CNF 쪽에 있습니다: CNF의 모델 개수를 근사하는 일은, 상당히 거칠게 하더라도, 최악의 경우 NP-난해이며, 그 난해함은 추론이 만들어 내는 것들에 가까운 제한된 CNF 부류들, 그중에서도 단조 절들에 대해서까지 지속됩니다 [7]. 그곳에서 최신 기술은, 무작위 패리티 제약으로 모델들의 공간을 조각내고 각 조각에서 SAT 솔버를 오라클로 호출하는 해싱 기반 계수기들입니다 [8]; 그 보장은 같은 $(\varepsilon, \delta)$ 형태를 갖지만, 그것은 최악의 경우 시간이 그 자체로 지수적인 SAT 호출들로 값을 치르므로, 벽은 제거되는 것이 아니라 오라클 속으로 옮겨질 뿐이며, 달성 가능한 시간 예산은 인스턴스마다 다릅니다. 근사는 진짜 연구의 프론티어이지만, 그것은 무조건적인 보장을 확률적인 보장과 맞바꾸며, CNF 쪽에서는 고정된 비용을 어려운 인스턴스가 소진할 수 있는 예산과 맞바꿉니다. 이 권은 할 수 있는 동안에는 그 반대의 거래를 합니다: 학술 세계 규모에서는 정확한 채로 남아 숫자들을 1e-12까지 단언하며, 이 입장이 규모에서는 통하지 않는다는 것을 소리 내어 말합니다. 이 권의 5부는 그 반대 극단, 즉 세계를 아예 세지 않는 질의 응답 시스템들을 만날 것이며, 그것들이 건전성에서 치르는 대가는 이 권 전체에서 되풀이되는 주제입니다.

왜 중요한가

가중 모델 계수는 이 권의 두 기둥이 실제로 맞닿는 지점입니다. 논리식 $\varphi_q$는 순수한 기호입니다: 그것은 증명들로부터 왔고, 그 모양이 바로 질의가 갖는 설명들의 논리적 구조입니다. 가중치들은 순수한 양입니다: 열한 개의 엣지 위의 열한 개의 숫자입니다. $\mathrm{WMC}(\varphi_q, w)$는 양쪽 모두가 동의하는 하나의 스칼라이며, 그 틀이야말로 이후의 모든 장이 구체화하는 것입니다: 다음 장의 회로는 같은 양을 더 빠르게 평가하고, 경사 세미링은 그것을 미분하여(손실이 논리를 거쳐 신경망 속으로 흐르게 하고), 의미 손실 장은 사실상 제약의 가중 개수를 네트워크 자신의 출력 확률 아래에서 평가한 것으로 네트워크에 벌점을 부과하며, Scallop의 유래 세미링(provenance semiring)들은 알면서도 같은 합을 완화합니다. #P의 벽은 그 반대 방향으로도 똑같이 무게를 떠받칩니다: 이 분야의 메뉴가 정확하지만 작은 것과 규모는 되지만 건전하지 않은 것으로 갈라지는 것은, 누군가 내년에 고칠 공학적 사고가 아니라, 정리로 뒷받침되는 이유 때문입니다. 5권이 신뢰와 보정을 감사할 때, 정확한 계수를 보여 줄 수 있는 시스템들은 영수증을 가진 시스템들이 될 것이고, 규모가 되는 시스템들은 그럴 수 없기에 경험적으로 캐물어져야 하는 시스템들이 될 것입니다. 이 장은 바로 그 갈림길에 값이 매겨지는 곳입니다.

핵심 용어

• 접지(Grounding): 어떤 세계 안에서의 도출 가능성을 질의와 상관있는 동전들에 대한 명제 논리식으로 대체하는 것입니다; 여기서는 모든 SLD 증명을 모으고 각 증명의 동전 집합을 간직하는 것입니다.
• 질의 논리식 / 설명들의 DNF($\varphi_q$): 증명들에 대해, 각 증명의 동전들의 논리곱을 논리합한 것입니다; 어떤 세계가 그것을 충족하는 것은 정확히 그 세계에서 질의가 도출 가능할 때입니다.
• 흡수(Absorption): 법칙 $A \vee (A \wedge B) = A$입니다; 상위집합 항을 삭제해도 어떤 배정의 판정도, 어떤 계수도 바뀌지 않습니다.
• 모델 / 충족 배정: 논리식을 참으로 만드는, 모든 변수에 대한 0/1 배정입니다.
• 가중 모델 계수(Weighted model counting, WMC): $\mathrm{WMC}(\varphi, w) = \sum_{\omega \models \varphi} \prod_{\omega(x_i)=1} w(x_i) \prod_{\omega(x_i)=0} w(\neg x_i)$입니다; $w(x_f) = p_f$일 때 이는 성공 확률과 같습니다, $P(q) = \mathrm{WMC}(\varphi_q, w)$.
• #SAT: 논리식의 모델을 세는, 가중치 없는 특수 경우입니다; SAT의 계수 유사물입니다.
• #P와 #P-완전성: NP 관계들에 대한 증인-계수 함수들의 부류입니다; #SAT는 그것에 대해 완전하며, 단조 2-DNF 계수도 포함됩니다, 그리고 다항 계층은 $\mathrm{P}^{\#\mathrm{P}}$ 안에 들어가므로, 효율적인 정확한 계수는 그것을 무너뜨리게 될 것입니다.
• FPRAS(완전 다항 무작위 근사 스킴, fully polynomial randomized approximation scheme): 적어도 $1-\delta$의 확률로, 입력 크기와 $1/\varepsilon$과 $\log(1/\delta)$에 대해 다항 시간 안에, 참값의 인수 $(1+\varepsilon)$ 이내의 답을 반환하는 알고리즘입니다; DNF 계수는 이를 가지고 있고, CNF 계수는 표준적인 가정이 무너지지 않는 한 갖지 못합니다.
• 두 계수로서의 조건화: $P(q \mid e) = \mathrm{WMC}(\varphi_q \wedge \varphi_e, w) / \mathrm{WMC}(\varphi_e, w)$이며, 그 논리곱은 분배와 흡수에 의해 DNF로 재구성됩니다.
• 사슬 계열: $k$개의 독립적인 두-동전 사슬, $\varphi_n = \bigvee_i (a_i \wedge b_i)$입니다; 닫힌 형태는 $1 - 0.44^k$이고, 무차별 대입 비용은 정확히 $2^n$개의 배정입니다.

이 장이 이어지는 곳

이 장은 의도적인 불균형으로 끝을 맺습니다: 무차별 대입이 백만 번의 배정을 치르고 얻는 것과 같은 $n = 20$ 논리식이, 손으로는 약 서른 번의 연산만으로 평가되었는데, 그 이유는 그것의 논리합들이 결코 이중으로 계수되지 않았고 그것의 논리곱들이 결코 변수를 공유하지 않았기 때문입니다. 다음 장인 회로: SDD, d-DNNF, 그리고 빠른 평가는 그 관찰을 지식 컴파일(knowledge compilation)이라는 공학적 규율로 바꿉니다: 한 번 비용을 치러 논리식을 OR-노드가 결정론적이고 AND-노드가 분해 가능한 회로로 재구조화한 다음, 회로의 크기에 선형인 단 한 번의 상향 패스로 답하는 것입니다. 이 장이 인증한 논리식들에 대해, 커밋된 컴파일러는 모든 계수를 기계 정밀도까지 재현하며, $n = 20$ 사슬 계열을 1,048,576개의 배정이 아니라 238번의 회로 연산으로 처리합니다. 그것은 열거를 확실하게 이겨 냅니다. 그것이 남겨 두는 최악의 경우는, 정확히 이 장이 그래야만 한다고 증명한 바로 그곳입니다.

---

컴패니언 코드: examples/integration/wmc.py는 1권의 sld.py 증명기로 질의들을 가중 DNF로 컴파일하고, 리터럴 열거로 계수하며, 두 계수로 조건화하고, 학술 세계의 모든 숫자를 distsem.py의 2,048개 세계 오라클과 대조하여 1e-12 이내로 인증하며, 벽 표의 값들은 닫힌 형태 $1 - 0.44^k$와 대조하여 1e-9 이내로 인증합니다; 그 단언문들은 또한 겹침 전시물, 세 가지 조건화 사례 전부, 그리고 벽 표의 정확한 $2^n$ 배정 개수도 고정합니다(시간 측정치만은 결코 단언되지 않습니다). 위에 인용된 단언된 모든 숫자를 재현하려면 python3 examples/integration/wmc.py를 실행하십시오(초 단위 열은 기계에 따라 달라집니다).