Scallop: 유래를 갖춘 미분 가능 데이터로그

📍 현재 위치: 3부 · 미분 가능 프레임워크 — 9장. 의미 손실과 제약 계층은 고정된 명제 제약을 미분 가능한 벌점으로 컴파일했습니다; 이 장은 재귀적인 규칙 엔진 전체를 미분 가능하게 만드는데, 그러면서도 새 엔진은 하나도 새로 쓰지 않습니다.

2권은 자신의 기호 이야기를 조용한 일반화 하나로 마무리했습니다: 데이터로그의 고정점을 맨 사실이 아니라 어떤 대수에서 온 태그를 실은 사실들 위에서 돌리면, "이것이 도출 가능한가?"에 답하던 바로 그 루프가 "어느 출처로부터?", "어떤 대안적 도출을 거쳐?", "얼마의 확신으로?"에 답하기 시작합니다. 그 장은 태그를 장부 정리로 다루었습니다. Scallop의 통찰은 그 장부 정리가 곧 뉴로-심볼릭 통합이라는 것입니다: 태그가 확률인 세미링을 고르면 루프는 확률적 추론을 수행하고, 태그가 많아야 $k$개의 증명으로 이루어진 집합인 세미링을 고르면 루프는 조절 가능한 정확성 다이얼을 갖춘 근사 확률적 추론을 수행하며, 태그가 경사를 실어 나르는 세미링을 고르면 루프는 끝에서 끝까지 미분 가능해집니다 [1]. NeurIPS(신경 정보 처리 시스템 학회, Conference on Neural Information Processing Systems)에서 발표된 시스템으로 시작한 것은 교체 가능한 유래 구조의 라이브러리와 PyTorch 인터페이스를 갖춘 온전한 뉴로심볼릭 프로그래밍 언어로 자라났습니다 [2]. 짝이 되는 모듈 provenance.py는 이것을 학술 세계 위에 소형으로 다시 짓습니다: 2권의 엔진을 바꾸지 않고 그대로 들여오고, 정확히 세 개의 새 세미링을 더하며, 모든 주장은 assert로 지키고 모든 숫자는 커밋되어 있습니다.

쉽게 말하면

소포 분류 창고를 상상해 보십시오. 컨베이어 벨트는 고정된 라우팅 규칙에 따라 합쳐지고 갈라지며, 모든 소포에는 스티커가 붙어 있습니다. 스티커가 체크 표시라면, 창고는 어느 목적지에 도달할 수 있는지를 계산합니다. 스티커가 소포가 거쳐 온 공급처의 목록이라면, 창고는 유래를 계산합니다. 스티커가 가격이고, 벨트가 합류할 때는 가장 싼 스티커를 남기고 벨트가 맞물릴 때는 가격이 더해진다면, 창고는 최적 경로를 계산합니다. 이 세 가지 작업 사이에 벨트 하나 다시 짓는 사람은 없습니다: 기계 장치는 동일하고, 스티커 산술만 바뀝니다. Scallop의 창고는 데이터로그이고, 스티커는 세미링 태그이며, 발견이란 어느 특정한 스티커 산술(경사를 함께 실은, $k$개의 최선 증명 집합)이 창고 전체를 신경망의 학습 가능한 계층으로 바꾸어 놓는다는 것입니다.

이 장에서 다루는 내용

• 물려받은 엔진: 2권의 Semiring 클래스와 provenance_lfp 고정점을 실제 줄 번호 그대로 인용하고 재구현하는 대신 들여오며, 그것들을 뉴로-심볼릭 기반 시설로 읽는 Scallop의 틀을 소개합니다.
• 최댓값-확률, 가장 온순한 새 세미링: $\oplus = \max$와 $\otimes = \times$를 갖춘 $[0,1]$ 안의 태그, 고정점이 각 사실의 최선 증명이 갖는 확률을 계산한다는 유도, 그리고 그 답이 1권의 SLD 증명기와 일치한다는 커밋된 검사입니다.
• 상위 k개 증명, 대표 세미링: 태그는 많아야 $k$개의 증명으로 이루어진 집합이고, $\vee_k$는 합집합에서 가장 그럴듯한 $k$개의 증명을, $\wedge_k$는 가장 그럴듯한 $k$개의 쌍별 합집합을 유지하며, $k$를 참 증명 개수 이상으로 두면 정확한 추론이 복원됩니다.
• 수렴 표: 커밋된 사다리 $k = 1, 2, 4, 8$이 $0.765$에서 정확한 분포-의미론 값 $0.934360942$까지 단조 증가하며, $k = 2$ 항목은 포함-배제를 통해 손으로 다시 유도합니다.
• 같은 루프 위의 경사 세미링: 이중수 태그 $(p, \nabla p)$, $\otimes$ 안의 곱의 법칙, 그리고 대표 도함수들(단일-증명 질의의 두 동전, 여섯-증명 질의의 세 동전)을 $10^{-6}$에서 중심 유한 차분과 대조하는 커밋된 표본 검사입니다.
• 실제 Scallop이 더하는 것: 층화 아래의 부정과 집계, 18개의 내장 유래 구조, PyTorch 모듈 경계, 그리고 DeepProbLog와 견준 속도-대-정확성 이야기의 정직한 인용입니다.
• 왜 데이터로그인가: 종료성, 집합 의미론, 층화가 데이터로그를 근사 태그에 맞는 올바른 기반으로 만드는 이유, 그리고 깊은 재귀와 값싼 클램프 세미링이 나쁘게 상호작용하는 지점에 대한 정직한 문단 하나입니다.

엔진은 물려받은 그대로, 새것은 세미링뿐

대수를 되짚어 봅시다. 가환 세미링(commutative semiring)은 가능한 태그들의 집합 $K$에 두 개의 이항 연산과 두 개의 특별한 원소를 갖춘 것으로, $(K, \oplus, \otimes, 0, 1)$로 씁니다: "덧셈" $\oplus$는 항등원 $0$을 갖는 결합적이고 가환적인 연산이고, "곱셈" $\otimes$는 항등원 $1$을 갖는 결합적이고 가환적인 연산이며, 원소 $0$은 소멸시키고($a \otimes 0 = 0$), $\otimes$는 $\oplus$ 위로 분배됩니다. 즉 $a \otimes (b \oplus c) = (a \otimes b) \oplus (a \otimes c)$입니다. 분배 법칙이 하중을 떠받치는 법칙입니다: 엔진이 온전한 증명들을 통째로 열거하는 대신 공유된 부분 도출을 인수분해하며 태그를 점진적으로 결합할 수 있게 해 주는 것이 바로 이 법칙이며, 이 장의 모든 세미링이 스스로 얻어 내야 할 공리이기도 합니다. 읽는 방식은 2권에서 한 번 고정된 뒤로 바뀐 적이 없는 유래-세미링 읽기입니다: 모든 사실은 태그를 실어 나르고, 규칙 몸체는 논리곱이므로 대응된 사실들의 태그는 $\otimes$로 결합되며, 같은 머리에 대한 대안적 도출들은 논리합이므로 그 태그들은 $\oplus$로 결합됩니다 [3].

2권은 그 읽기를 두 개의 작은 조각으로 구현했고, 이 장은 둘 다 한 글자도 바꾸지 않고 다시 씁니다. 첫째는 자료 구조로서의 대수, annotated.py 38–46행입니다:

class Semiring:
    """A commutative semiring (K, ⊕, ⊗, 0, 1) as four operations + two constants."""

    def __init__(self, zero, one, plus, times, name=""):
        self.zero = zero
        self.one = one
        self.plus = plus
        self.times = times
        self.name = name

둘째는 엔진입니다: provenance_lfp(annotated.py 79–96행)는 세미링으로 주석된 직접 귀결 연산자의 최소 고정점(least fixpoint)을 계산합니다. 각 라운드는 도출 가능한 모든 사실의 태그를, 모든 한 걸음 도출에 걸친, 몸체 태그들의 $\otimes$-곱의 $\oplus$-합으로 다시 계산하는데, 태그가 붙은 기본 사실들(주어진 사실들의 외연 데이터베이스, 즉 EDB; 라운드마다 다시 계산되는 파생 사실들은 내포 데이터베이스, 즉 IDB를 이룹니다)에서 시작하여 한 라운드 전체가 아무것도 바꾸지 않을 때 멈추고, max_iter 라운드가 지나도록 안정화되지 않으면 값을 돌려주는 대신 예외를 일으킵니다:

def provenance_lfp(edb_annot, rules, sr: Semiring, max_iter: int = 100):
    """Least fixpoint of the semiring-annotated immediate-consequence operator.

    Each round recomputes every fact's annotation as the ⊕-sum, over all one-step
    derivations, of the ⊗-product of the body annotations — starting from the EDB
    tokens, which persist. Converges for any ω-continuous semiring on an acyclic
    program (all five below, on the DAG example)."""
    ann = dict(edb_annot)
    for _ in range(max_iter):
        new = dict(edb_annot)          # base tokens persist; IDB is recomputed
        for head, body in rules:
            for sub, prod in _match_body(body, ann, sr, {}, sr.one):
                h = _apply(head, sub)
                new[h] = sr.plus(new.get(h, sr.zero), prod)
        if new == ann:
            return ann
        ann = new
    raise RuntimeError("annotated fixpoint did not converge (cyclic provenance?)")

2권은 이 루프를 다섯 개의 세미링으로 인스턴스화했습니다: 불리언 세미링(평범한 도출 가능성), which-유래(결과가 닿는 기본 사실들의 집합), why-유래(어느 대안적 증인 집합들인가), 다항식 세미링 $\mathbb{N}[X]$(온전한 유래 다항식), 그리고 확신 세미링입니다(annotated.py 100–132행). 짝이 되는 모듈 provenance.py는 클래스와 루프를 곧바로 들여오고(provenance.py 69–73행) 엔진에는 아무것도 더하지 않습니다. 이 장에서 새로운 모든 것은 태그 안에 삽니다. 그것이 정확하게 서술한 Scallop의 틀입니다: 확률적-데이터로그 사실은 태그 붙은 사실이고, 추론은 provenance_lfp이며, 세미링의 선택이 추론이 무엇을 뜻하는지와 무엇을 치르는지를 결정합니다 [1]. 정직한 단순화 하나를 앞머리에 밝혀 둡니다: 실제 Scallop의 유래 프레임워크는 부정도 다루고("이 사실이 부재한다"에 대한 태그 연산) 근사 태그 아래의 재귀가 증명 가능하게 종료되도록 포화 조건도 부과합니다 [2]; 우리 프로그램은 확정적(definite)이어서(어디에도 부정이 없습니다) 두 메커니즘 모두 여기서는 작동하지 않으며, 그 단순화가 시스템 그 자체인 척하는 대신 그렇다고 밝혀 둡니다.

프로그램: 동전 열두 개, 규칙 일곱 개, 증명 여섯 개

이 확률적 프로그램은 실행 예제를 전력으로 가동한 것입니다. 열두 개의 독립적인 동전은 distsem.extended_prob_facts()입니다(distsem.py 95–100행): 분포 의미론 장의 열한 개 확률적 간선에 흔들리는 직접 인용 $0.5 :: \text{cites}(\text{p3}, \text{p1})$("cites(p3, p1)은 확률 $0.5$로 성립한다"라고 읽습니다)을 더한 것입니다. 분포 의미론 아래에서 동전 집합 $\mathcal{F}$의 각 부분집합 $F$(기호 $\subseteq$는 "부분집합이다"라고 읽습니다)는 확률 $P(F) = \prod_{f \in F} p_f \cdot \prod_{f \notin F} (1 - p_f)$를 갖는 가능 세계입니다: 곱 기호 $\prod$는 동전마다 인자 하나씩을 곱하는데, 첫째 곱은 참으로 나온 동전들 $f \in F$($\in$은 "원소이다"라고 읽습니다) 위를 달리며 각 동전이 자기 확률 $p_f$를 기여하고, 둘째 곱은 빠진 동전들 $f \notin F$("원소가 아니다") 위를 달리며 각 동전이 $1 - p_f$를 기여합니다. 질의의 성공 확률은 그것을 도출하는 세계들의 총 질량, 곧 $P(q) = \sum_{F \subseteq \mathcal{F}\,:\, F \cup C \cup R \,\vdash\, q} P(F)$입니다. 여기서 $C$는 확실한 사실들, $R$은 규칙들이며, $F \cup C \cup R$(기호 $\cup$은 "합집합"이라고 읽습니다)은 참으로 나온 동전들을 확실한 사실들 및 규칙들과 한데 모은 것이고, $\vdash$("도출한다")는 1권의 전방 연쇄기입니다. 규칙들은(provenance.py 100–110행) 1권의 grandAdvisor와 citesTransitively를 그대로 유지하고 새 관계 하나를 더합니다: 영향 간선(influence edge) iedge(X, Y)는 $X$가 $Y$를 지도하거나 $X$의 논문이 $Y$의 논문에 인용될 때 성립하며, influences는 iedge의 추이 폐쇄입니다. 실행 질의는 influences(alice, dave)이고, 이것이 선택된 이유는 이 권에서 진짜 조합적 결을 가진 첫 질의이기 때문입니다: 전수 SLD(Selective Linear Definite-clause resolution, 한정절에 대한 선택적 선형 귀결, 1권의 후방 연쇄 전략) 열거는 정확히 여섯 개의 최소 증명을 찾아내는데, 지도 사슬을 통해, 직접 인용을 통해, 그리고 서로 동전을 공유하는 두 홉 인용 경로들을 통해 dave에 도달합니다.

정확성은 어떤 근사가 등장하기도 전에 이미 닻을 갖습니다. 모듈의 exact_P(provenance.py 146–162행)는 1권의 least_fixpoint로 $2^{12} = 4096$개의 세계 전부를 실체화하고 성공하는 세계들의 질량을 math.fsum으로 합산합니다; 이것은 공유 질의 위에서 distsem.P_query(distsem.py 160–169행)에 고정핀으로 묶여 있으며, 실행은 두 열거기가 $10^{-12}$까지 일치함을 단언합니다. 자취의 커밋된 머리말은 다음과 같습니다:

[1] the program: Volume 2's engine, Scallop's semirings
    12 coins (distsem.extended_prob_facts), 12 certain facts, 7 rules
    running query  influences(alice, dave)   exact P = 0.934360942  (2^12 worlds, Volume 1 chainer)
    enumerator pinned to distsem.P_query on citesTransitively(p3, p1): both 0.860000

$P = 0.934360942$를 붙들어 두십시오: 이 장의 모든 근사가 이 숫자에 대고 재어집니다.

최댓값-확률: 최선 증명의 확률

가장 온순한 새 세미링은 연산 하나만 바꿉니다. $[0,1]$ 위에서 $\otimes = \times$는 그대로 두되(한 증명을 따라 놓인 독립 동전들은 곱해집니다) 논리합의 합을 최댓값으로 바꿉니다:

$$\text{MaxProb} \;=\; \big([0,1],\; \max,\; \times,\; 0,\; 1\big),$$

코드로는 한 줄입니다(provenance.py 221행): MAXPROB = Semiring(0.0, 1.0, max, lambda a, b: a * b, "max-prob"). 먼저, 이것이 정말 세미링인지부터 확인합니다. 이 검사는 해 볼 가치가 있는데, 분배 법칙이야말로 고정점이 기대는 바로 그것이기 때문입니다. 임의의 $a, b, c \in [0,1]$에 대해, 음이 아닌 수 $c$를 곱하는 것은 순서를 보존합니다: $a \le b$이면 $ac \le bc$입니다. 이를 $a, b$ 중 더 큰 쪽에 적용하면 다음을 얻습니다:

$$\max(a, b) \times c \;=\; \max(a \times c,\; b \times c),$$

이것이 $\times$의 $\max$ 위로의 분배 법칙입니다. 남은 공리들은 $[0,1]$ 위에서 한 줄짜리 검사입니다: 모든 태그가 $a \ge 0$을 만족하므로 $\max(a, 0) = a$이고(따라서 $0$은 $\oplus$의 항등원입니다), $a \times 1 = a$이며(따라서 $1$은 $\otimes$의 항등원입니다), $a \times 0 = 0$이 소멸입니다.

이제 의미론입니다. 사실의 증명(proof)을 어떤 도출이 소비하는 동전들의 집합으로 정의하고(확실한 사실들은 인자 $1$을 기여하므로 떨어뜨립니다), 증명의 확률을 그 동전들에 대한 $\prod_{f} p_f$로 정의합니다. 고정점을 풀어헤쳐 보면 태그가 무엇을 계산하는지 드러납니다: 기본 동전의 태그는 $p_f$이고, 규칙 한 번의 적용은 몸체 태그들을 $\otimes$-곱하므로, 귀납에 의해 단일 도출은 정확히 자기 증명의 곱을 기여합니다; 같은 머리에 대한 대안적 도출들은 $\oplus = \max$에서 만나므로, 분배 법칙 덕분에 엔진이 결과를 바꾸지 않고 공유된 접두부를 인수분해할 수 있었던 터라, 살아남는 태그는

$$\mathrm{tag}(q) \;=\; \max_{\pi \,\in\, \mathrm{proofs}(q)} \;\prod_{f \in \pi} p_f,$$

즉 최선의 단일 증명이 갖는 확률입니다. 이것이 데이터로그의 비터비(Viterbi) 읽기입니다: 곱이 합이 되고 $\max$는 $\max$로 남는 로그 공간에서 보면 트로피컬(tropical) 최단 경로 세미링의 $[0,1]$ 사촌이며, 고정점 루프는 도출들에 대한 동적 계획법을 수행하고 있는 것입니다.

커밋된 실행은 이 주장을 두 권 전의 기계 장치와 대조하여 검사합니다. sld_proofs(provenance.py 180–190행)는 1권의 SLD 증명기를 몰아 질의의 모든 증명을 열거하고, 동전 집합의 중복을 제거하고, 초집합을 떨어뜨립니다; 이어서 실행은 최댓값-확률 태그가 열거된 최선 증명의 곱과 $10^{-12}$까지 같음을, 그리고 (다음에 소개할 세미링에서 온) 상위 1개 증명이 바로 그 동일한 증명임을 단언합니다(provenance.py 364–370행):

    proofs = sld_proofs(QUERY)                       # minimal, sorted by prob
    best_sld = proof_prob(proofs[0])
    mp = tag_of(QUERY, MAXPROB)
    assert abs(mp - best_sld) < 1e-12, f"max-prob {mp} != best proof {best_sld}"
    top1 = tag_of(QUERY, topk_semiring(1))
    assert len(top1) == 1 and top1[0] == proofs[0], \
        "top-1 proof differs from the SLD-enumerated best proof"

[2] max-prob semiring ([0,1], max, x): the best proof's probability
    tag(influences(alice, dave)) = 0.765000
    == max over all 6 SLD proofs (Volume 1 prover), whose best is
    {adv(a,b), adv(b,d)}  p = 0.765000

최선의 증명은 순수한 지도 사슬, 곧 alice가 bob을 지도하고 bob이 dave를 지도하는 경로이며, 확률은 $0.90 \times 0.85 = 0.765$입니다. 세 권에 걸친 기계 장치가 하나의 대상 위에서 일치합니다: 1권의 후방 연쇄 증명 탐색, 2권의 주석된 고정점, 그리고 이 권의 확률적 읽기가 모두 같은 두 동전을 지목합니다. 그러나 $0.765$가 정확한 값 $0.934$에서 얼마나 멀리 떨어져 있는지 눈여겨보십시오: 최선의 증명이 이야기의 전부가 아닌 것은, 나머지 다섯 증명이 저마다의 질량을 지니기 때문입니다. 온전한 지수적 비용을 치르지 않고 그 간극을 닫는 것이 바로 대표 세미링이 하는 일입니다.

상위 k개 증명: 정확성 다이얼

Scallop의 대표 유래는 최선의 증명 하나가 아니라 최선의 $k$개를 유지하는데, 여기서 $k$는 사용자가 고르는 작은 양의 정수입니다 [1]. 태그는 이제 많아야 $k$개의 증명으로 이루어진 집합이고, 각 증명은 동전 식별자들의 집합입니다. 증명 집합 $A$를 받아, 다른 증명의 초집합인 증명을 버리고(이에 대해서는 곧 다시 말합니다), 확률 $\prod_{f \in \pi} p_f$가 가장 높은 $k$개의 남은 증명을 유지하는 연산을 $\mathrm{top}_k(A)$로 씁시다. 두 세미링 연산은 그러면 다음과 같습니다.

$$A \vee_k B \;=\; \mathrm{top}_k(A \cup B), \qquad A \wedge_k B \;=\; \mathrm{top}_k\big(\lbrace\, a \cup b \;:\; a \in A,\; b \in B \,\rbrace\big).$$

유래의 목소리로 읽어 봅시다. 논리합은 양쪽의 증명들을 한데 모아 가장 그럴듯한 $k$개를 유지합니다: 대안적 도출은 후보 증명을 더할 뿐, 기존 증명을 고치지 않습니다. 논리곱은 왼쪽 항의 모든 증명을 오른쪽 항의 모든 증명과 짝지어 두 동전 집합의 합집합을 취하는데, "$A$ 그리고 $B$"의 증명에는 양쪽의 동전이 모두 필요하고, 양쪽이 공유하는 동전은 한 번만 나타나야 하며, 이것이 정확히 집합 합집합이 하는 일이기 때문입니다. 부정을 가진 실제 시스템에서 $\wedge_k$는 합집합에 어떤 리터럴과 그 보수가 함께 들어 있는 쌍(충돌)을 추가로 떨어뜨립니다; 우리 프로그램은 확정적이므로, 그 필터는 언어 논문의 정의에는 존재하지만 여기서는 결코 발화하지 않습니다 [2]. 영 태그는 빈 집합(증명 없음)이고 일 태그는 빈 증명 하나를 담은 집합(공짜로 참, 확률 $1$)입니다. 구현은 정규화기 _norm_topk를 거느린 topk_semiring입니다(provenance.py 229–249행):

def topk_semiring(k: int) -> Semiring:
    """Scallop's top-k-proofs provenance:
         ⊕: top-k of the union of the two proof sets,
         ⊗: top-k of all pairwise unions a ∪ b (a proof of the conjunction
            needs both conjuncts' coins; a shared coin merges — frozenset ∪).
    Our program is definite, so the language paper's conflict filtering (drop
    a ∪ b when it holds a literal and its negation) never fires."""
    return Semiring(
        (),                      # 0: no proof
        (frozenset(),),          # 1: the empty proof (certainly true)
        lambda a, b: _norm_topk(set(a) | set(b), k),
        lambda a, b: _norm_topk({x | y for x in a for y in b}, k),
        f"top-{k} proofs")

초집합을 떨어뜨리는 단계가 흡수(absorption), 곧 법칙 $a \vee (a \wedge b) = a$입니다: 다른 증명의 동전들의 진부분 초집합을 쓰는 증명은 더 작은 증명의 사건 안에 포함되는 사건을 기술하므로, 결코 확률 질량을 더할 수 없고 버려도 됩니다. 흡수는 또한 고정점을 재귀 규칙 위에서 안전하게 돌릴 수 있게 해 주는 것이기도 합니다: 흡수적 세미링에서는 태그가 무한히 자랄 수 없는데, 도출을 재귀 규칙에 한 바퀴 더 통과시키는 것은 증명에 동전을 더하기만 하여 흡수가(또는 실제 시스템의 논증에서는 상위-$k$ 절단 자체가) 내다 버리는 초집합만 만들기 때문이며, 따라서 주석 사상은 안정화되고 provenance_lfp의 종료 검사 new == ann은 결국 성공합니다; 고정점 유래가 흡수적이어야 한다는 요구가 정확히 언어 논문의 포화 조건입니다 [2].

이제 다이얼이 대수 안에서 눈에 보입니다. $k = 1$이면 태그는 단일 최선 증명이고 세미링은 최댓값-확률의 정보 내용으로 무너집니다. $k$가 질의의 참 최소 증명 개수 이상이면 아무것도 버려지지 않으며, 태그가 완전한 최소-증명 집합 그 자체입니다: 아래로부터 복원된 정확한 추론입니다. 그 사이에서 $k$는 충실도와 비용을 맞바꾸는데, 태그는 결코 $k$개를 넘는 증명을 담지 않고 $\wedge_k$는 결코 $k^2$개를 넘는 쌍을 살피지 않으므로, 질의가 아무리 조합적이어도 라운드당 작업량은 유계입니다.

한 걸음만 더 가면 증명 집합이 확률로 바뀝니다. "증명 $\pi_i$의 동전들이 모두 참이다"라는 사건들은 서로 겹치므로, 증명 곱들을 그냥 합하면 과대 계수가 됩니다(분포 의미론 장의 서로소-합 문제입니다). 이 규모에서 모듈은 합집합을 포함-배제(inclusion-exclusion)로 정확히 해소합니다(provenance.py 201–212행): $m$개의 증명이 이루는 사건 $A_1, \ldots, A_m$에 대해(여기서 $m$은 증명의 개수를, $A_i$는 증명 $\pi_i$의 동전들이 모두 참인 사건을, $\lvert S \rvert$는 인덱스 집합 $S$의 원소 개수를 나타냅니다), 아래의 합은 인덱스 집합 $\lbrace 1, \ldots, m \rbrace$의 공집합이 아닌 부분집합 $S$마다 항 하나씩을 갖고(기호 $\emptyset$은 공집합을 나타내므로 $\emptyset \neq S$가 공집합을 배제합니다), 부호는 부분집합의 크기에 따라 교대합니다:

$$P\Big(\bigcup_{i=1}^{m} A_i\Big) \;=\; \sum_{\emptyset \neq S \subseteq \lbrace 1..m \rbrace} (-1)^{\lvert S \rvert + 1} \prod_{f \,\in\, \bigcup_{i \in S} \pi_i} p_f,$$

여기서 각 항의 곱은 선택된 증명들의 동전들의 합집합 위를 달리며, 공유된 동전은 한 번만 셉니다. 정직성 노트: 이 교대합에는 $2^m - 1$개의 항이 있어, 책상 규모의 $m \le 8$개 증명에는 괜찮습니다; 실제 Scallop은 그 대신 상위-$k$ 증명 집합을 논리합 정규형(disjunctive normal form, DNF)의 논리식으로 읽어 가중 모델 계수(weighted model counting, WMC)에 넘기는데, 이는 회로 장과 같은 기계 장치입니다 [1].

수렴 표

이 장의 중심 전시물을 위한 준비가 모두 끝났습니다. 실행 질의에 대해 모듈은 K_LADDER = (1, 2, 4, 8)(provenance.py 117행)의 각 단에서 상위-$k$ 태그를 계산하고, 각 태그를 포함-배제로 확률 $P_k$로 변환하며, 정확한 값 $0.934360942$와 비교합니다. 커밋된 표는 다음과 같습니다:

[3] top-k proofs: the exactness dial (query has 6 minimal proofs)
      k   #proofs kept   P_k (incl-excl)    |exact - P_k|
      1              1   0.765000000      0.169360942
      2              2   0.848652750      0.085708192
      4              4   0.908377371      0.025983571
      8              6   0.934360942      0.000000000
    monotone nondecreasing; exact once k >= #proofs (asserted)

$k$	유지된 증명 수	$P_k$	정확값과의 간극	읽기
1	1	$0.765000000$	$0.169360942$	최댓값-확률의 답: 단일 최선 증명
2	2	$0.848652750$	$0.085708192$	증명 하나를 더해 간극의 절반이 닫힘
4	4	$0.908377371$	$0.025983571$	무거운 증명들은 들어왔고, 꼬리가 남음
8	6	$0.934360942$	$0.000000000$	$k \ge 6$개 증명: 정확한 추론 복원

$k = 2$ 행은 손으로 다시 계산해 볼 가치가 있는데, 모든 정의를 한꺼번에 시험하기 때문입니다. 가장 그럴듯한 두 증명은 지도 사슬 $\pi_1 =$ {adv(a,b), adv(b,d)}($p(\pi_1) = 0.90 \times 0.85 = 0.765$)와 지도-후-인용 경로 $\pi_2 =$ {adv(a,b), adv(b,c), au(c,p2), cit(p3,p2), au(d,p3)}($p(\pi_2) = 0.90 \times 0.90 \times 0.90 \times 0.90 \times 0.85 = 0.557685$)입니다. 둘은 동전 adv(a,b)를 공유하므로 합집합 $\pi_1 \cup \pi_2$는 일곱이 아니라 여섯 개의 동전을 가지며, 그 곱은 $p(\pi_1 \cup \pi_2) = 0.90 \times 0.90 \times 0.85 \times 0.90 \times 0.90 \times 0.85 = 0.474032250$입니다. 두 사건에 대한 포함-배제는 그러면 다음을 줍니다:

$$P_2 \;=\; p(\pi_1) + p(\pi_2) - p(\pi_1 \cup \pi_2) \;=\; 0.765 + 0.557685 - 0.474032250 \;=\; 0.848652750,$$

표의 둘째 행과 마지막 자리까지 일치하는 값입니다. 실행은 표가 내보이는 두 구조적 주장을 단언합니다: 단조성은 $k$를 올리는 것이 유지 집합에 증명을 더하기만 하고 사건들의 합집합은 질량을 얻을 수만 있기 때문이며, $10^{-9}$에서의 말단 정확성은 $k = 8 \ge 6$에서 유지 집합이 SLD로 열거된 최소 증명 집합과 같기 때문입니다(provenance.py 383–387행):

    for a, b in zip(ks, ks[1:]):
        assert ladder[b] >= ladder[a] - 1e-12, \
            f"top-k not monotone: P_{a}={ladder[a]} > P_{b}={ladder[b]}"
    assert abs(ladder[ks[-1]] - exact) < TOL_EXACT, \
        f"saturated top-k {ladder[ks[-1]]} != exact {exact}"

이 표를 소리 내어 읽어 보십시오. 이것이 시스템 전체의 설계 논증이기 때문입니다. $k = 1$에서는 거의 아무 비용도 치르지 않고 비터비 답을 얻지만 $0.169$만큼 빗나갑니다. 증명 하나를 더 사면 빠진 질량의 절반이 돌아옵니다. $k = 4$가 되면 오차는 $0.026$ 아래이고, 손잡이는 증명 개수에서 포화됩니다: 그 지점을 지나면 $k$를 더 키워도 말 그대로 아무것도 얻지 못하며, 실행의 $k = 8$ 행이 여섯 개의 증명만 유지하는 이유가 그것입니다. 다이얼의 가치는, 이 곡선 위 어디에 앉을지를 질의마다, 훈련 에폭마다, 논리를 건드리지 않은 채 여러분이 고른다는 데 있습니다; 정확성은 엔진의 속성이기를 멈추고 실행 시간 매개변수가 되었습니다 [1].

하나의 엔진, 세 가지 스티커 산술: 세미링 소켓을 갖춘 2권의 고정점 루프, 정확한 값까지 올라가는 커밋된 상위-k 수렴 사다리, 그리고 같은 루프에서 경사를 실어 나오는 이중수 태그. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

같은 루프 위의 경사 세미링

셋째 세미링은 다이얼을 미분 가능하게 만듭니다. 태그는 이제 이중수(dual number)입니다: 값과 그 경사를 담은 쌍 $(p, \nabla p)$로, 여기서 $\nabla p$는 편도함수 $\partial p / \partial p_i$를 담은 12칸짜리 벡터(동전마다 한 칸)입니다. 덧셈은 두 성분을 모두 더하고, 곱셈은 값끼리 곱하며 경사에는 곱의 법칙(product rule) $\partial (ab) = a\,\partial b + b\,\partial a$를 적용합니다. 이것은 "도함수를 실어 나르는 레이블"을 그저 또 하나의 세미링으로 논리 프로그래밍 안에 들여온 대수적 프롤로그 aProbLog의 경사 세미링입니다(쌍 구성 자체는 더 오래된 것으로, DeepProbLog 장의 참고문헌에 주석된 Eisner의 기댓값 세미링입니다) [4]; DeepProbLog 장이 컴파일된 회로 위에서, 이 쌍 산술이 정확히 전진 모드 미분인 이유까지 포함해 그것을 온전히 유도했으므로, 그 유도를 여기서 반복하지는 않습니다. 정의는 일곱 줄입니다(provenance.py 260–266행):

DUAL = Semiring(
    (0.0, _ZERO_G),
    (1.0, _ZERO_G),
    lambda a, b: (a[0] + b[0], tuple(x + y for x, y in zip(a[1], b[1]))),
    lambda a, b: (a[0] * b[0],
                  tuple(a[0] * db + b[0] * da for da, db in zip(a[1], b[1]))),
    "dual-number gradient")

각 동전은 $(p_i, e_i)$로 EDB에 들어가는데, 여기서 $e_i$는 $i$번째 단위 벡터, 곧 칸 $i$에 $1.0$이 있고 그 밖에는 $0.0$인 튜플로, "이 태그의 값은 $p_i$이고, 동전 $i$에 대한 도함수는 $1$이다"라고 말합니다(provenance.py 284–299행). 그런 다음 바뀌지 않은 고정점 루프가 값과 도함수를 함께 계산합니다. 확률이 두 지도 동전의 순수한 곱 $P = p_{ab} \cdot p_{bc}$인 단일-증명 질의 grandAdvisor(alice, carol)에서 곱의 법칙은 $\partial P / \partial p_{ab} = p_{bc} = 0.9$와 $\partial P / \partial p_{bc} = p_{ab} = 0.9$를 주며, 커밋된 실행은 둘 다를 세미링에 대해 아무것도 모르는 검사, 곧 정확한 세계 열거 위의 중심 유한 차분(central finite difference) $\partial P/\partial p_i \approx [P(p_i + h) - P(p_i - h)]/(2h)$($h = 10^{-5}$)와 대조하여 확인합니다(fd_gradient, provenance.py 332–340행). 정직한 미묘함 하나가 이 검사를 유난히 강하게 만듭니다. 다른 동전들을 고정한 채 한 좌표 $p_i$에 대한 $P$의 1계, 2계, 3계 도함수를 $P'$, $P''$, $P'''$로 씁시다. $p_i$ 주변의 테일러(Taylor) 전개는 $P(p_i \pm h) = P \pm h\,P' + \tfrac{h^2}{2}P'' \pm \tfrac{h^3}{6}P''' + \cdots$를 주는데, 두 전개를 빼면 모든 짝수 차수 항이 소거되고, $2h$로 나누면 $[P(p_i + h) - P(p_i - h)]/(2h) = P' + \tfrac{h^2}{6}P''' + \cdots$가 남으므로, 중심 차분의 오차는 $O(h^2)$($h$의 제곱처럼 줄어든다는 뜻입니다)이고 3계 도함수가 그것을 지배합니다. 그러나 $P$는 동전 벡터에 대해 다중선형(multilinear)이므로(각 세계의 가중치는 각 $p_i$를 많아야 한 번, 일차로만 사용합니다) $P$는 각 단일 좌표에 대해 차수 1이고, $P'''$는 항등적으로 0이며, 차분 몫은 부동소수점 반올림까지 정확하고, 따라서 허용오차 $10^{-6}$에서의 비교는 수치적 요행이 아니라 세미링의 대수를 시험하는 것입니다.

[4] dual-number gradient semiring on the raw fixpoint (+ , x)
    single-proof query grandAdvisor(alice, carol): value 0.810000 == exact (+ is never wrong with one proof)
      coin         dP/dp (dual)   dP/dp (central FD)
      adv(a,b)        0.900000             0.900000
      adv(b,c)        0.900000             0.900000
    shared-coin query citesTransitively(p3, p1): dual value 1.220000 vs true P 0.860000
    -> the disjoint-sum problem: + adds overlapping proofs' mass

자취의 후반부는 모듈이 과대 포장을 거부하는 대목입니다. 이중수 세미링의 $\oplus = +$를 증명들이 동전을 공유하는 질의에 곧바로 돌리면 과대 계수가 됩니다: citesTransitively(p3, p1)은 동전 하나짜리 증명 {cit(p3,p1)}과 동전 두 개짜리 증명 {cit(p3,p2), cit(p2,p1)}을 가지며, 순진한 덧셈은 참값 $0.86$에 맞서 전혀 확률이 아닌 $0.5 + 0.9 \times 0.8 = 1.22$를 돌려줍니다. 이것은 분포 의미론 장이 전시했던 것과 같은 서로소-합 문제가 이번에는 세미링 안에서 다시 나타난 것이며, 값-과-경사 대수가 날 고정점이 아니라 질의의 서로소 표현 위에서 돌아야 하는 이유입니다. 모듈의 책상 규모 해법은 dual_inclusion_exclusion입니다(provenance.py 308–329행): 같은 이중수 산술을 발견된 증명 집합에 대한 포함-배제 공식에 통과시켜, 모든 곱이 DUAL의 $\otimes$를 쓰고 교대합이 항들을 $\pm 1$로 비례시키게 합니다. 결과는 두 성분 모두에서 정확하며, 대표 동전 세 개에 대해 검사됩니다(provenance.py 415–425행):

[5] the fix at desk scale: dual arithmetic through incl-excl
    value 0.934360942 == exact 0.934360942  (1e-9)
      coin         dP/dp (dual)   dP/dp (central FD)
      adv(a,b)        0.298868             0.298868
      cit(p3,p1)      0.051967             0.051967
      au(d,p3)        0.199248             0.199248
    (the real Scallop hands the top-k DNF to WMC; same algebra)

그것이 결정타이며, 평이한 문장 하나를 들일 가치가 있습니다: 미분 가능 데이터로그는 데이터로그 더하기 세미링이며, 그 밖에는 아무것도 바뀌지 않았습니다. 2권에서 불리언 도출 가능성을 계산하던 고정점 루프가 여기서 여섯 개의 증명을 발견했고(상위-$8$ 태그가 SLD 증명 집합과 같음이 단언됩니다), 그 태그 위에 이중수 대수를 돌리자 $\partial P(\text{influences}(\text{alice}, \text{dave})) / \partial p(\text{advises}(\text{alice}, \text{bob})) = 0.298868$이 나왔습니다; 그 두 실행 사이에서 바뀐 코드라고는 인수로 넘겨진 네 연산짜리 대수가 어느 것이냐 뿐입니다. DeepProbLog의 신경 술어가 그러하듯 신경망이 동전 확률을 공급한다면, 이 경사는 역전파가 논리의 입력 경계에서 필요로 하는 바로 그것입니다; 추론 계층은 논리를 고스란히 유지한 채 미분 가능한 모듈이 되었습니다.

실제 Scallop이 더하는 것

이 소형판은 대수에는 충실하지만, 실제 시스템은 하나의 언어입니다. Scallop의 표면 문법은 부정과 집계(파생 관계에 대한 세기, 합산, argmax)를 갖춘 온전한 데이터로그 방언인데, 둘 다 층화(stratification)로 규율됩니다: 프로그램은 어떤 관계도, 간접적으로라도, 자기 자신의 부정이나 집계를 통해 정의되지 않도록 층들로 나뉘고, 각 층은 다음 층이 시작되기 전에 자신의 고정점까지 돌며, 유래 프레임워크는 태그가 부정과 집계의 경계를 어떻게 흘러 지나는지 명시합니다 [2]. 이 장이 세 개의 세미링을 지은 자리에서, 이 언어는 이산적인 것(불리언, 증명 집합), 확률적인 것(min-max-prob, add-mult 계열, 상위-$k$ 증명과 그 미분 가능 형태), 그리고 미분 가능한 것(이 장의 $(\max, \times)$ 대수는 여기에 diff-max-mult-prob으로 실려 있습니다)을 아우르는 18개의 내장 유래 구조 라이브러리를 모두 같은 다이얼 뒤에 실어 배송합니다 [2]. 그리고 우리의 경사 소비자가 유한 차분 검사였던 자리에서, 실제 시스템은 PyTorch 모듈입니다: 예측된 확률의 텐서가 태그 붙은 사실로 흘러 들어가고, 추론기가 돌고, 질의 확률이 경사를 붙인 채 흘러나오므로, Scallop 프로그램은 여느 계층과 똑같이 훈련 루프 안에 자리 잡습니다 [2].

출처가 보고하는 보상은 다이얼이 실제 일을 해내는 모습입니다. MNIST-sum 과제군(손으로 쓴 숫자 이미지 두 장을 분류하되 그 합만으로 지도하는, DeepProbLog 장이 소개한 벤치마크)에서 상위-$k$-증명 구성은 작은 사례에서 정확한 DeepProbLog에 견줄 만한 정확도에 이르면서 두세 자릿수 규모만큼 더 빠르게 훈련하고(두 자리 숫자 합에 대한 언어 논문의 측정: DeepProbLog의 에폭당 21,430초에 맞선 72초), 더 긴 합으로도 계속 규모를 키우는데, 그곳에서는 정확한 시스템의 컴파일 기반 추론이 어떤 합리적 예산 안에서도 더는 실행 가능하지 않습니다 [1][2]. 그 비교는 있는 그대로 인용하십시오: "Scallop이 정확한 추론보다 낫다"가 아니라 "태그에 대한 통제된 과소근사가 측정된 충실도 비용을 치르고 몇 자릿수 규모의 확장을 사 온다"입니다. 이 설계 교훈은 이 시스템 너머로 일반화되며 슬로건으로 적어 둘 가치가 있습니다: 태그를 근사하고, 논리는 정확하게 유지하라. 규칙, 조인, 고정점, 그리고 집합 의미론은 결코 완화되지 않습니다; 완화되는 것은 도출들을 요약하는 대수뿐입니다. Dolphin을 비롯한 이 계보의 후속 시스템들은 정확히 이 분업을 유지하면서 태그 산술 자체를 GPU 위로 벡터화하여, 수천 개의 태그 붙은 질의를 하나의 융합된 유래 계산으로 배칭합니다 [5].

왜 데이터로그가 올바른 기반인가

미분 가능 다이얼이 프롤로그가 아니라 데이터로그 위에 내려앉은 것은 우연이 아니며, 그 이유는 1권과 2권이 이미 가르친 것들입니다. 1권의 SLD 귀결은 탐색 절차입니다: 증명은 절 순서가 지시하는 차례로 한 번에 하나씩 발견되고, 재귀 프로그램은 탐색을 무한 가지 아래로 내려보낼 수 있습니다. 2권의 데이터로그는 고정점 절차입니다: 함수 기호가 없다는 것은 바닥 원자들의 유한한 전체를 뜻하므로 최소 고정점은 증명 가능하게 종료하고, 집합 의미론은 천 가지 방식으로 도출된 사실도 여전히 자기 태그들의 $\oplus$를 실은 하나의 사실이라는 뜻이므로 비용은 증명의 수가 아니라 사실의 수를 따라가며, 층화는 그 보장을 부정과 집계까지 확장합니다. 이것들이 정확히 태그-근사 방식이 그 아래에 필요로 하는 성질들입니다: 종료성은 "고정점까지 돌린 다음 태그를 읽어 내라"를 잘 정의된 것으로 만들고, 각 사실에서의 $\oplus$-병합은 근사 세미링이 자신의 절단을 수행하는 단 하나의 길목입니다. 데이터로그는 근사를 대수 안에 격리하며, 바로 그것이 "$k$가 증명 개수에 이르면 정확하다" 같은 진술을 아예 증명 가능한 것으로 만들어 줍니다.

언어 논문 자신의 지침에서 나온 정직한 경고 하나가 이 절을 닫습니다. 라이브러리의 값싼 유래들, 곧 증명 집합 대신 사실당 클램프된 수 하나를 전파하는 add-mult 류의 구조들은 특히 깊이 재귀적인 프로그램에서 열화됩니다: 긴 도출이 같은 사실들에 라운드마다 다시 들어가고, 합은 위로 표류하며, $[0,1]$로의 클램프가 그 과대 계수를 소리 없이 흡수하므로, 태그와 그 경사는 더 이상 어떤 확률도 추적하지 않게 됩니다. 상위-$k$ 증명은 정확히 그 지점에서 견고한데, 그 태그는 도출이 어느 동전을 썼는지를 기억하고 집합 합집합은 동전을 두 번 세기를 거부하기 때문입니다; 출처의 권고도 그에 따라, 재귀가 깊을 때는 증명을 실어 나르는 태그의 추가 비용을 치르라는 것입니다 [2]. 다시 말해 재귀 깊이는 사용자가 통제하지 못하는 두 번째 다이얼이며, 사용자가 통제하는 다이얼을 반대편에서 밀어붙입니다.

아직 풀리지 않은 부분

수렴 표는 단조롭게 올라 정확한 값에 안착했고, 두 성질 모두 여기서는 정리입니다. 그러나 보장되지 않는 것을 보십시오. 상위-$k$는 과소근사(under-approximation)입니다: 유지된 증명들의 합집합 사건이 온전한 합집합에 포함되므로 항상 $P_k \le P$입니다. 얼마나 밑도는지는 전혀 별개의 문제입니다. 버려진 증명들의 질량은 선험적으로 무계입니다: 어떤 질의는 무거운 증명 하나와, 그것을 압도하는 집단 질량을 가진 백만 개의 가벼운 증명을 가질 수 있고, 작은 $k$는 무언가 빠졌다는 신호도 없이 진실의 아주 작은 조각만을 보고할 것입니다. 우리 표 자체는 온화한 경우, 곧 빠르게 감쇠하는 여섯 개의 증명을 보여 주며, 거기서는 $k = 2$가 이미 확률의 $91$퍼센트를 되찾습니다; 대수의 어떤 것도 그런 모양을 약속하지 않습니다. 일반적인 문제, 곧 정확한 추론의 값을 치르지 않고 절단 오차 $P - P_k$의 경계를 잡거나 추정이라도 하는 문제는 열려 있으며, 이는 학습 중에는 곱절로 중요해집니다. 과소근사의 경사는 손실이 건강해 보이는 동안에도 진실의 경사와 다른 곳을 가리킬 수 있기 때문입니다. 규모에서 이 분야의 응답은 두 갈래 길을 택했습니다. 하나는 근사 태그를 유지한 채 그 비용을 공격합니다: Dolphin은 태그 산술 자체를 벡터화하고 수천 개의 태그 붙은 질의를 GPU 위에서 배칭하여, 같은 근사를 날카롭게 벼리는 대신 그 규모를 키웁니다 [5]. 다른 하나는 질문 자체를 바꿉니다: 증명 집합을 절단하는 대신 정확한 논리식을 회로로 컴파일하고, 신경망이 이미 쓰는 하드웨어 위에서 배칭되고 병렬화되도록 회로 자체를 충분히 빠르게 만드는 것입니다. 근사를 안전하게 만드는 대신 정확성을 값싸게 만들 수 있는가는 GPU 네이티브 뉴로-심볼릭 장의 주제입니다.

왜 중요한가

이 장은 이 권의 제목에 대한 가장 깔끔한 진술입니다: 논리를 미분 가능하게 만드는 데 새 논리는 필요하지 않았고, 옛 논리 위의 새 대수가 필요했습니다. 2권에서 유래 장부 정리를 위해 쓰인 하나의 고정점 루프가 고전적 도출 가능성, 비터비식 최선 증명, 애니타임(anytime) 확률적 추론, 그리고 정확한 경사를 계산했으며, 이것들을 가른 것은 인수로 넘겨진 네 연산짜리 객체뿐이었습니다. 그 모듈성이 이 권이 문을 열며 제기한 두-기둥 긴장에 대한 공학적 답입니다: 기호 기둥은 자기 의미론을 지키고(규칙은 결코 물러지지 않았고, 상위 1개 증명은 1권의 SLD 증명기와 비트 하나까지 일치했습니다), 신경 기둥은 자신이 필요로 하는 것(경계에서의 경사, $10^{-6}$에서 유한 차분과 대조 검증된)을 얻습니다. 정확성 다이얼은 또한 5권의 중심 거래를 미리 보여 줍니다: 지금 얼마나 근사적인지를 보고할 수 있고 계산으로 정확성을 되살 수 있는 시스템은, 한 덩어리 소프트 추론기로서는 불가능한 방식으로 감사 가능합니다. 5권이 무엇이 뉴로-심볼릭 시스템을 규모에서 신뢰할 만하게 만드는가를 물을 때, "논리는 정확하게 남았고 근사는 우리가 돌릴 수 있는 손잡이 안에 살았다"는 정리가 딸린 몇 안 되는 답 가운데 하나입니다.

핵심 용어

• 가환 세미링 $(K, \oplus, \otimes, 0, 1)$ — 태그 집합 $K$ 위의 결합적이고 가환적인 두 연산으로, 항등원 $0$과 $1$, 소멸원 $0$을 가지며 $\otimes$가 $\oplus$ 위로 분배됩니다; 2권의 엔진이 임의의 태그 대수에 요구하는 계약입니다.
• 유래 / 태그 — 사실이 고정점을 거치며 실어 나르는 값입니다: $\otimes$는 규칙 몸체의 태그들을 결합하고, $\oplus$는 같은 머리에 대한 대안적 도출들을 병합합니다.
• 최댓값-확률 세미링 — $([0,1], \max, \times)$; 파생된 사실의 태그는 그 단일 최선 증명의 확률로, 데이터로그의 비터비 읽기이자 트로피컬 세미링의 $[0,1]$ 사촌입니다.
• 상위 $k$개 증명 유래 — 태그는 많아야 $k$개의 증명(동전 집합)으로 이루어진 집합입니다; $\vee_k$는 합집합에서 가장 그럴듯한 $k$개의 증명을, $\wedge_k$는 가장 그럴듯한 $k$개의 충돌 없는 쌍별 합집합을 유지하며, $k$가 증명 개수에 이르면 정확합니다.
• 흡수 — 법칙 $a \vee (a \wedge b) = a$; 구체적으로는 초집합 증명을 떨어뜨리는 일로, 태그 성장을 상한하고 재귀적 고정점이 종료하게 해 줍니다.
• 포함-배제 — 겹치는 증명들의 집합을 정확한 확률로 바꾸는 교대합 공식으로, 각 항은 동전 집합들의 합집합에 대한 곱입니다; 증명 DNF에 대한 가중 모델 계수의 책상 규모 대역입니다.
• 이중수 경사 세미링 — 성분별 $\oplus$와 $\otimes$ 안의 곱의 법칙을 갖는 태그 $(p, \nabla p)$; aProbLog의 경사 세미링이며, 태그 산술로서의 전진 모드 미분입니다.
• 서로소-합 문제 — 증명들은 서로 겹치는 사건들이므로 $\oplus = +$는 과대 계수합니다(참값 $0.86$에 맞선 커밋된 $1.22$); 서로소 표현 위의 포함-배제나 WMC로 해결됩니다.
• 정확성 다이얼 — 매개변수 $k$입니다: 충실도는 다항적으로 유계인 라운드당 비용으로 $k$와 함께 단조 증가하며, 정확한 추론에서 포화됩니다.
• 층화 — 어떤 관계도 자기 자신의 부정이나 집계에 의존하지 않도록 프로그램을 층으로 쌓는 것입니다; 각 층은 다음 층 전에 고정점까지 돌며, 데이터로그의 보장을 언어 전체로 확장합니다.

이 장이 이끄는 곳

Scallop은 논리를 고전적으로 유지하고 유연성을 전부 태그에 넣었습니다: 규칙 안에서 진리는 두 값에 머물렀고, 확률은 그것을 감싼 대수 속에 살았습니다. 다음 장은 정반대의 내기를 겁니다. 논리 텐서 네트워크는 실수를 의미론 자체 안으로 밀어 넣습니다: 상수는 벡터가 되고, 술어는 $[0,1]$로 가는 신경 함수가 되며, 결합자는 t-노름 장의 퍼지 t-노름 연산자가 되어, 일차 논리식이 실수 논리(Real Logic)라 불리는 미분 가능한 진리 정도로 평가됩니다. 이 장의 슬로건이 "태그를 근사하고 논리는 정확하게 유지하라"였다면, 다음 장의 슬로건은 "진리값을 완화하고 논리식은 유지하라"입니다; 이 두 설계가 3부의 모든 미분 가능 프레임워크가 사는 공간을 양쪽에서 감쌉니다.

---

짝이 되는 코드: examples/integration/provenance.py는 이 장 전체를 2권의 들여온 엔진 위에 구현합니다: 세 개의 새 세미링(MAXPROB 221행, topk_semiring 237–249행, DUAL 260–266행), distsem.P_query에 고정핀으로 묶인 정확한 세계-열거 오라클(146–162행), SLD 증명 오라클(180–190행), 스칼라와 이중수 산술 두 벌의 포함-배제(201–212행과 308–329행), 유한 차분 경사 검사(332–340행), 그리고 여기 인용된 모든 주장을 지키는 단언문들(351–425행)입니다. 이 장의 모든 숫자를 바이트 단위까지 재현하려면 python3 examples/integration/provenance.py를 실행하십시오; 실행은 SUMMARY provenance: exact=0.934361 maxprob=0.765000 ladder=0.7650/0.8487/0.9084/0.9344 proofs=6 overcount=1.220 grad_ok=1e-6으로 끝납니다.