Scallop: Differentiable Datalog with Provenance

📍 Where we are: Part III · Differentiable Frameworks — Chapter 9. Semantic Loss and Constraint Layers compiled a fixed propositional constraint into a differentiable penalty; this chapter makes an entire recursive rule engine differentiable, and it does so without writing a new engine at all.

Volume 2 ended its symbolic story with a quiet generalization: run Datalog's fixpoint not over bare facts but over facts carrying tags from an algebra, and the same loop that answered "is this derivable?" starts answering "from which sources?", "via which alternative derivations?", "with what confidence?". That chapter treated the tags as bookkeeping. Scallop's insight is that the bookkeeping is the neuro-symbolic integration: choose a semiring whose tags are probabilities and the loop performs probabilistic inference; choose one whose tags are sets of at most $k$ proofs and the loop performs approximate probabilistic inference with a tunable exactness dial; choose one whose tags carry gradients and the loop is differentiable end to end [1]. What began as a system published at NeurIPS (the Conference on Neural Information Processing Systems) grew into a full neurosymbolic programming language with a library of interchangeable provenance structures and a PyTorch interface [2]. The companion module provenance.py rebuilds this in miniature on the academic world: Volume 2's engine, imported and unchanged, plus exactly three new semirings, with every claim guarded by an assert and every number committed.

The simple version

Imagine a parcel-sorting warehouse. Conveyor belts merge and split according to fixed routing rules, and every parcel carries a sticker. If the sticker is a checkmark, the warehouse computes which destinations are reachable. If the sticker is a list of the suppliers a parcel passed through, the warehouse computes provenance. If the sticker is a price, and merging belts keeps the cheapest sticker while joining belts adds prices, the warehouse computes best routes. Nobody rebuilds a single belt between these three jobs: the machinery is identical, and only the sticker arithmetic changes. Scallop's warehouse is Datalog, the stickers are semiring tags, and the discovery is that one particular sticker arithmetic (sets of the $k$ best proofs, with gradients riding along) turns the whole warehouse into a trainable layer of a neural network.

What this chapter covers

• The inherited engine: Volume 2's Semiring class and provenance_lfp fixpoint, quoted at their real line numbers and imported rather than reimplemented, and the Scallop framing that reads them as neuro-symbolic infrastructure.
• Max-prob, the gentlest new semiring: tags in $[0,1]$ with $\oplus = \max$ and $\otimes = \times$, a derivation that the fixpoint computes each fact's best proof's probability, and the committed check that its answer coincides with Volume 1's SLD prover.
• Top-k proofs, the flagship: tags are sets of at most $k$ proofs, $\vee_k$ keeps the $k$ most probable proofs of a union, $\wedge_k$ the $k$ most probable pairwise unions, and setting $k$ at or above the true proof count recovers exact inference.
• The convergence table: the committed ladder $k = 1, 2, 4, 8$ rising monotonically from $0.765$ to the exact distribution-semantics value $0.934360942$, with the $k = 2$ entry re-derived by hand through inclusion-exclusion.
• The gradient semiring on the same loop: dual-number tags $(p, \nabla p)$, the product rule inside $\otimes$, and the committed spot-check of representative derivatives (both coins of the single-proof query, three coins of the six-proof query) against central finite differences at $10^{-6}$.
• What the real Scallop adds: negation and aggregation under stratification, 18 built-in provenance structures, the PyTorch module boundary, and the honestly quoted speed-versus-exactness story against DeepProbLog.
• Why Datalog: termination, set semantics, and stratification make Datalog the right substrate for approximate tags, and one honest paragraph on where deep recursion and cheap clamped semirings interact badly.

The engine is inherited; only the semirings are new

Recall the algebra. A commutative semiring is a set $K$ of possible tags equipped with two binary operations and two distinguished elements, written $(K, \oplus, \otimes, 0, 1)$: the "plus" $\oplus$ is associative and commutative with identity $0$, the "times" $\otimes$ is associative and commutative with identity $1$, the element $0$ annihilates ($a \otimes 0 = 0$), and $\otimes$ distributes over $\oplus$, meaning $a \otimes (b \oplus c) = (a \otimes b) \oplus (a \otimes c)$. Distributivity is the load-bearing law: it is what lets an engine combine tags incrementally, factoring shared sub-derivations instead of enumerating whole proofs, and it is the axiom every semiring in this chapter will have to earn. The reading, fixed once in Volume 2 and never changed since, is the provenance-semiring reading: every fact carries a tag, a rule body is a conjunction so its matched facts' tags combine with $\otimes$, and alternative derivations of the same head are a disjunction so their tags combine with $\oplus$ [3].

Volume 2 implemented that reading in two small pieces, and this chapter reuses both verbatim. The first is the algebra as a data structure, annotated.py lines 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

The second is the engine: provenance_lfp (annotated.py lines 79–96) computes the least fixpoint of the semiring-annotated immediate-consequence operator. Each round recomputes every derivable fact's tag as the $\oplus$-sum, over all one-step derivations, of the $\otimes$-product of the body tags, starting from the tagged base facts (the EDB, the extensional database of given facts; the derived facts recomputed each round form the IDB, the intensional database), stopping when a full round changes nothing, and raising rather than returning if max_iter rounds pass without stabilizing:

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?)")

Volume 2 instantiated this loop with five semirings: the Boolean semiring (plain derivability), which-provenance (the set of base facts a result touches at all), why-provenance (which alternative witness sets), the polynomial semiring $\mathbb{N}[X]$ (the full provenance polynomial), and a confidence semiring (annotated.py lines 100–132). The companion module provenance.py imports the class and the loop directly (provenance.py lines 69–73) and adds nothing to the engine. Everything new in this chapter lives in the tags. That is the Scallop framing stated precisely: a probabilistic-Datalog fact is a tagged fact, inference is provenance_lfp, and the choice of semiring decides what inference means and what it costs [1]. One honest simplification up front: the real Scallop's provenance framework also handles negation (a tag operation for "this fact is absent") and imposes saturation conditions so recursion under approximate tags provably terminates [2]; our program is definite (no negation anywhere), so neither mechanism is exercised here, and we say so rather than pretend the simplification is the system.

The program: twelve coins, seven rules, six proofs

The probabilistic program is the running example at full strength. The twelve independent coins are distsem.extended_prob_facts() (distsem.py lines 95–100): the eleven probabilistic edges of the distribution-semantics chapter plus the shaky direct citation $0.5 :: \text{cites}(\text{p3}, \text{p1})$, read "cites(p3, p1) holds with probability $0.5$". Under the distribution semantics, each subset $F$ of the coin set $\mathcal{F}$ (the symbol $\subseteq$ reads "is a subset of") is a possible world with probability $P(F) = \prod_{f \in F} p_f \cdot \prod_{f \notin F} (1 - p_f)$: the product symbol $\prod$ multiplies one factor per coin, the first product runs over the coins $f \in F$ ($\in$ reads "is a member of"), the coins that came up true, each contributing its probability $p_f$, and the second over the coins $f \notin F$ ("is not a member of"), the coins left out, each contributing $1 - p_f$. A query's success probability is the total mass of the worlds that derive it, $P(q) = \sum_{F \subseteq \mathcal{F}\,:\, F \cup C \cup R \,\vdash\, q} P(F)$, with $C$ the certain facts, $R$ the rules, $F \cup C \cup R$ (the symbol $\cup$ reads "union") the true coins taken together with the certain facts and the rules, and $\vdash$ ("derives") Volume 1's forward chainer. The rules (provenance.py lines 100–110) keep Volume 1's grandAdvisor and citesTransitively verbatim and add one new relation: an influence edge iedge(X, Y) holds when $X$ advises $Y$, or when a paper of $X$ is cited by a paper of $Y$; influences is the transitive closure of iedge. The running query is influences(alice, dave), and it was chosen because it is the first query in this volume with real combinatorial texture: exhaustive SLD (Selective Linear Definite-clause resolution, Volume 1's backward-chaining strategy) enumeration finds exactly six minimal proofs, reaching dave through advising chains, through direct citation, and through two-hop citation paths that share coins with each other.

Exactness has an anchor before any approximation appears. The module's exact_P (provenance.py lines 146–162) materializes all $2^{12} = 4096$ worlds with Volume 1's least_fixpoint and sums the succeeding worlds' masses with math.fsum; it is pinned to distsem.P_query (distsem.py lines 160–169) on a shared query, and the run asserts the two enumerators agree to $10^{-12}$. The committed header of the trace:

[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

Hold on to $P = 0.934360942$: it is the number every approximation in this chapter will be measured against.

Max-prob: the best proof's probability

The gentlest new semiring changes one operation. Keep $\otimes = \times$ on $[0,1]$ (independent coins along one proof multiply) but replace disjunction's sum with a maximum:

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

one line of code (provenance.py line 221): MAXPROB = Semiring(0.0, 1.0, max, lambda a, b: a * b, "max-prob"). First, this really is a semiring, and the check is worth doing because distributivity is exactly what the fixpoint relies on. For any $a, b, c \in [0,1]$, multiplication by the non-negative number $c$ preserves order: if $a \le b$ then $ac \le bc$. Applying this to whichever of $a, b$ is larger gives

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

which is distributivity of $\times$ over $\max$. The remaining axioms are one-line checks on $[0,1]$: $\max(a, 0) = a$ because every tag satisfies $a \ge 0$, so $0$ is $\oplus$'s identity; $a \times 1 = a$, so $1$ is $\otimes$'s identity; and $a \times 0 = 0$ is annihilation.

Now the semantics. Define a proof of a fact as the set of coins some derivation consumes (certain facts contribute the factor $1$ and are dropped), and a proof's probability as $\prod_{f} p_f$ over its coins. Unfolding the fixpoint shows what the tag computes: a base coin's tag is $p_f$, one rule application $\otimes$-multiplies the body tags, so by induction a single derivation contributes exactly its proof's product; alternative derivations of the same head meet at $\oplus = \max$, so, distributivity having let the engine factor shared prefixes without changing the result, the tag that survives is

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

the probability of the best single proof. This is the Viterbi reading of Datalog: in log space, where products become sums and $\max$ stays $\max$, it is the tropical shortest-path semiring's $[0,1]$ cousin, and the fixpoint loop is doing dynamic programming over derivations.

The committed run checks this claim against machinery from two volumes back. sld_proofs (provenance.py lines 180–190) drives Volume 1's SLD prover to enumerate every proof of the query, deduplicates coin sets, and drops supersets; the run then asserts that the max-prob tag equals the best enumerated proof's product to $10^{-12}$, and that the top-1 proof (from the semiring introduced next) is that same proof (provenance.py lines 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

The best proof is the pure advising chain, alice advises bob and bob advises dave, with probability $0.90 \times 0.85 = 0.765$. Three volumes' machinery agree on one object: Volume 1's backward-chaining proof search, Volume 2's annotated fixpoint, and this volume's probabilistic reading all name the same two coins. But notice how far $0.765$ sits from the exact $0.934$: the best proof is not the whole story, because five other proofs carry mass of their own. Closing that gap without paying the full exponential price is exactly what the flagship semiring is for.

Top-k proofs: the exactness dial

Scallop's flagship provenance keeps not one best proof but the $k$ best, where $k$ is a small positive integer the user chooses [1]. A tag is now a set of at most $k$ proofs, each proof a set of coin identifiers. Write $\mathrm{top}_k(A)$ for the operation that takes a set of proofs $A$, discards any proof that is a superset of another (more on that in a moment), and keeps the $k$ remaining proofs with the highest probability $\prod_{f \in \pi} p_f$. The two semiring operations are then

$$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).$$

Read them in the provenance voice. Disjunction pools the two sides' proofs and keeps the $k$ most probable: an alternative derivation adds candidate proofs, never modifies existing ones. Conjunction pairs every proof of the left conjunct with every proof of the right and unions their coin sets, because a proof of "$A$ and $B$" needs both sides' coins, and a coin shared by both sides appears once, which is precisely what the set union does. In the real system, which has negation, $\wedge_k$ additionally drops any pair whose union contains a literal and its complement (a conflict); our program is definite, so that filter exists in the language paper's definition but never fires here [2]. The zero tag is the empty set (no proof) and the one tag is the set containing the empty proof (true for free, probability $1$). The implementation is topk_semiring with its normalizer _norm_topk (provenance.py lines 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")

The superset-dropping step is absorption, the law $a \vee (a \wedge b) = a$: a proof that uses a strict superset of another proof's coins describes an event contained in the smaller proof's event, so it can never add probability mass and may be discarded. Absorption is also what makes the fixpoint safe to run on recursive rules: in an absorptive semiring the tags cannot grow forever, because looping a derivation through a recursive rule only ever adds coins to a proof, producing supersets that absorption (or the top-$k$ cutoff itself, in the real system's argument) throws away, so the annotation map stabilizes and provenance_lfp's termination test new == ann eventually succeeds; the requirement that a fixpoint provenance be absorptive is exactly the language paper's saturation condition [2].

The dial is now visible in the algebra. If $k = 1$, the tag is the single best proof and the semiring collapses to max-prob's information content. If $k$ is at least the query's true number of minimal proofs, nothing is ever discarded, and the tag is the complete minimal-proof set: exact inference, recovered from below. In between, $k$ trades fidelity for cost, because tags never hold more than $k$ proofs and $\wedge_k$ never examines more than $k^2$ pairs, so the per-round work is bounded no matter how combinatorial the query is.

One more step turns a proof set into a probability. The events "proof $\pi_i$'s coins are all true" overlap, so summing proof products overcounts (the disjoint-sum problem of the distribution-semantics chapter). At this scale the module resolves the union exactly by inclusion-exclusion (provenance.py lines 201–212): for the $m$ proofs' events $A_1, \ldots, A_m$ (writing $m$ for the number of proofs, $A_i$ for the event that proof $\pi_i$'s coins are all true, and $\lvert S \rvert$ for the number of elements of the index set $S$), the sum below has one term for every nonempty subset $S$ of the index set $\lbrace 1, \ldots, m \rbrace$ (the symbol $\emptyset$ denotes the empty set, so $\emptyset \neq S$ excludes it), with the sign alternating by the subset's size:

$$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,$$

where each term's product runs over the union of the chosen proofs' coins, counting a shared coin once. Honesty note: this alternating sum has $2^m - 1$ terms, fine for $m \le 8$ proofs at desk scale; the real Scallop instead hands the top-$k$ proof set, read as a formula in disjunctive normal form (DNF), to weighted model counting (WMC), the same machinery as the circuits chapter [1].

The convergence table

Everything is in place for the chapter's centerpiece. For the running query, the module computes the top-$k$ tag at each rung of K_LADDER = (1, 2, 4, 8) (provenance.py line 117), converts each tag to a probability $P_k$ by inclusion-exclusion, and compares against the exact $0.934360942$. The committed table:

[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$	proofs kept	$P_k$	gap to exact	reading
1	1	$0.765000000$	$0.169360942$	max-prob's answer: the single best proof
2	2	$0.848652750$	$0.085708192$	half the gap closed by one more proof
4	4	$0.908377371$	$0.025983571$	the heavy proofs are in; the tail remains
8	6	$0.934360942$	$0.000000000$	$k \ge 6$ proofs: exact inference recovered

The $k = 2$ row is worth recomputing by hand, because it exercises every definition at once. The two most probable proofs are the advising chain $\pi_1 =$ {adv(a,b), adv(b,d)} with $p(\pi_1) = 0.90 \times 0.85 = 0.765$ and the advise-then-cite path $\pi_2 =$ {adv(a,b), adv(b,c), au(c,p2), cit(p3,p2), au(d,p3)} with $p(\pi_2) = 0.90 \times 0.90 \times 0.90 \times 0.90 \times 0.85 = 0.557685$. They share the coin adv(a,b), so the union $\pi_1 \cup \pi_2$ has six coins, not seven, and its product is $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$. Two-event inclusion-exclusion then gives

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

the table's second row to the last digit. The run asserts the two structural claims the table displays: monotonicity, because raising $k$ only ever adds proofs to the kept set and a union of events can only gain mass, and terminal exactness at $10^{-9}$, because at $k = 8 \ge 6$ the kept set equals the SLD-enumerated minimal proof set (provenance.py lines 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}"

Read the table aloud, because it is the design argument for the entire system. At $k = 1$ you pay almost nothing and get the Viterbi answer, off by $0.169$. One extra proof buys back half the missing mass. By $k = 4$ the error is under $0.026$, and the knob saturates at the proof count: past that point more $k$ buys literally nothing, which is why the run's $k = 8$ row keeps only six proofs. The dial's value is that you choose where on this curve to sit, per query, per training epoch, without touching the logic; exactness stopped being a property of the engine and became a runtime parameter [1].

One engine, three sticker arithmetics: Volume 2's fixpoint loop with a semiring socket, the committed top-k convergence ladder rising to the exact value, and a dual-number tag carrying the gradient out of the same loop. Original diagram by the authors, created with AI assistance.

The gradient semiring, on the same loop

The third semiring makes the dial differentiable. A tag is now a dual number: a pair $(p, \nabla p)$ holding a value and its gradient, where $\nabla p$ is a 12-slot vector (one slot per coin) of partial derivatives $\partial p / \partial p_i$. Addition adds both components; multiplication multiplies the values and applies the product rule to the gradients, $\partial (ab) = a\,\partial b + b\,\partial a$. This is the gradient semiring of aProbLog, the algebraic Prolog that brought "labels that carry derivatives" into logic programming as just another semiring (the pair construction itself is older: it is Eisner's expectation semiring, annotated in the DeepProbLog chapter's references) [4]; the DeepProbLog chapter derived it in full on a compiled circuit, including why the pair arithmetic is exactly forward-mode differentiation, and we do not repeat that derivation here. The definition is seven lines (provenance.py lines 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")

Each coin enters the EDB as $(p_i, e_i)$, where $e_i$ is the $i$-th unit vector, the tuple with $1.0$ in slot $i$ and $0.0$ elsewhere, saying "this tag's value is $p_i$, and its derivative with respect to coin $i$ is $1$" (provenance.py lines 284–299). Then the unchanged fixpoint loop computes values and derivatives together. On the single-proof query grandAdvisor(alice, carol), whose probability is the plain product $P = p_{ab} \cdot p_{bc}$ of the two advising coins, the product rule gives $\partial P / \partial p_{ab} = p_{bc} = 0.9$ and $\partial P / \partial p_{bc} = p_{ab} = 0.9$, and the committed run confirms both against a check that knows nothing about semirings: a central finite difference on the exact world enumeration, $\partial P/\partial p_i \approx [P(p_i + h) - P(p_i - h)]/(2h)$ with $h = 10^{-5}$ (fd_gradient, provenance.py lines 332–340). One honest subtlety makes this check unusually strong. Write $P'$, $P''$, $P'''$ for the first, second, and third derivatives of $P$ with respect to the one coordinate $p_i$, holding the other coins fixed. Taylor's expansion around $p_i$ gives $P(p_i \pm h) = P \pm h\,P' + \tfrac{h^2}{2}P'' \pm \tfrac{h^3}{6}P''' + \cdots$; subtracting the two expansions cancels every even-order term, and dividing by $2h$ leaves $[P(p_i + h) - P(p_i - h)]/(2h) = P' + \tfrac{h^2}{6}P''' + \cdots$, so the central difference's error is $O(h^2)$ (it shrinks like $h$ squared) and is controlled by the third derivative. But $P$ is multilinear in the coin vector (each world's weight uses every $p_i$ at most once, to the first power), so $P$ is degree one in each single coordinate, $P'''$ is identically zero, the difference quotient is exact up to floating-point rounding, and the comparison at tolerance $10^{-6}$ is testing the semiring's algebra, not numerical luck.

[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

The trace's second half is the module refusing to oversell. Run the dual semiring's $\oplus = +$ directly on a query whose proofs share coins, and it overcounts: citesTransitively(p3, p1) has the one-coin proof {cit(p3,p1)} and the two-coin proof {cit(p3,p2), cit(p2,p1)}, and naive addition returns $0.5 + 0.9 \times 0.8 = 1.22$, not a probability at all, against the true $0.86$. This is the same disjoint-sum problem the distribution-semantics chapter exhibited, now reappearing inside a semiring, and it is why the value-and-gradient algebra must run over a disjoint representation of the query rather than over the raw fixpoint. The module's desk-scale fix is dual_inclusion_exclusion (provenance.py lines 308–329): run the same dual arithmetic through the inclusion-exclusion formula over the discovered proof set, so every product uses DUAL's $\otimes$ and the alternating sum scales terms by $\pm 1$. The result is exact in both components, checked for three representative coins (provenance.py lines 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)

That is the punchline, and it deserves one plain sentence: differentiable Datalog is Datalog plus a semiring, and nothing else changed. The fixpoint loop that computed Boolean derivability in Volume 2 discovered the six proofs here (the top-$8$ tag equals the SLD proof set, asserted), and running the dual algebra over that tag yielded $\partial P(\text{influences}(\text{alice}, \text{dave})) / \partial p(\text{advises}(\text{alice}, \text{bob})) = 0.298868$; between those two runs, the only code that changed is which four-operation algebra was passed in as an argument. If a neural network supplies the coin probabilities, as DeepProbLog's neural predicates do, this gradient is exactly what backpropagation needs at the logic's input boundary; the reasoning layer has become a differentiable module with the logic intact.

What the real Scallop adds

The miniature is faithful to the algebra; the real system is a language. Scallop's surface syntax is a full Datalog dialect with negation and aggregation (counting, summing, argmax over derived relations), both disciplined by stratification: the program is split into layers so that no relation is defined, even indirectly, through the negation or aggregation of itself, each stratum runs to its fixpoint before the next begins, and the provenance framework specifies how tags flow through the negation and aggregation boundaries [2]. Where this chapter built three semirings, the language ships a library of 18 built-in provenance structures spanning the discrete (Boolean, proof sets), the probabilistic (min-max-prob, add-mult variants, top-$k$ proofs and its differentiable form), and the differentiable (where this chapter's $(\max, \times)$ algebra ships as diff-max-mult-prob), all behind the same dial [2]. And where our gradient consumer was a finite-difference check, the real system is a PyTorch module: tensors of predicted probabilities flow in as tagged facts, the reasoner runs, and query probabilities flow out with gradients attached, so a Scallop program sits inside a training loop exactly like any other layer [2].

The payoff the source reports is the dial doing real work. On the MNIST-sum family of tasks (classify two handwritten digit images and supervise only their sum, the benchmark the DeepProbLog chapter introduced), the top-$k$-proofs configuration reaches accuracy comparable to exact DeepProbLog on the small instance while training two to three orders of magnitude faster (the language paper's measurement on the two-digit sum: 72 seconds per epoch against DeepProbLog's 21,430), and it keeps scaling to longer sums, where the exact system's compilation-based inference stops being feasible within any reasonable budget [1][2]. Quote that comparison for what it is: not "Scallop is better than exact inference" but "a controlled under-approximation of the tags buys orders of magnitude of scale at a measured cost in fidelity." The design lesson generalizes beyond this system and is worth stating as a slogan: approximate the tags, keep the logic exact. The rules, the joins, the fixpoint, and the set semantics are never relaxed; only the algebra that summarizes derivations is. The successor systems in this line, Dolphin among them, keep exactly this division of labor while vectorizing the tag arithmetic itself onto the GPU, batching thousands of tagged queries through one fused provenance computation [5].

Why Datalog is the right substrate

It is not an accident that the differentiable dial landed on Datalog rather than Prolog, and the reasons are the ones Volumes 1 and 2 already taught. Volume 1's SLD resolution is a search procedure: proofs are found one at a time, in an order the clause ordering dictates, and a recursive program can send the search down an infinite branch. Volume 2's Datalog is a fixpoint procedure: no function symbols means a finite universe of ground atoms, so the least fixpoint provably terminates; set semantics means a fact derived a thousand ways is still one fact, carrying the $\oplus$ of its tags, so cost tracks the number of facts, not the number of proofs; and stratification extends the guarantee through negation and aggregation. These are exactly the properties a tag-approximation scheme needs underneath it: termination makes "run to the fixpoint, then read off tags" well defined, and the $\oplus$-merge at each fact is the single choke point where an approximate semiring does its truncating. Datalog isolates the approximation in the algebra, which is what makes statements like "exact when $k$ reaches the proof count" provable at all.

One honest caveat from the language paper's own guidance closes the section. The cheap provenances in the library, the add-mult style structures that propagate a single clamped number per fact instead of a proof set, degrade specifically on deeply recursive programs: a long derivation re-enters the same facts round after round, the sums drift upward, and the clamp to $[0,1]$ silently absorbs the overcount, so the tags and their gradients stop tracking any probability. Top-$k$ proofs is robust exactly there, because its tags remember which coins a derivation used and the set union refuses to count a coin twice; the source's recommendation is accordingly to spend the extra cost of proof-carrying tags when recursion is deep [2]. Recursion depth, in other words, is a second dial the user does not control, and it pushes against the one the user does.

The unsolved part

The convergence table rose monotonically and landed exactly, and both properties are theorems here. But look at what is not guaranteed. Top-$k$ is an under-approximation: $P_k \le P$ always, since the kept proofs' union event is contained in the full union. How far under is another matter entirely. The discarded proofs' mass is unbounded a priori: a query can have one heavy proof and a million light ones whose collective mass dwarfs it, and a small $k$ would report a tiny fraction of the truth with no signal that anything is missing. Our own table shows the benign case, six proofs with fast decay, where $k = 2$ already recovers $91$ percent of the probability; nothing in the algebra promises that shape. The general problem, bounding or even estimating the truncation error $P - P_k$ without paying for exact inference, is open, and it matters doubly during learning, where the gradient of an under-approximation can point away from the gradient of the truth while the loss looks healthy. The field's responses at scale have taken two roads. One keeps the approximate tags and attacks their cost: Dolphin vectorizes the tag arithmetic itself and batches thousands of tagged queries on the GPU, scaling the same approximation rather than sharpening it [5]. The other changes the question: rather than truncate the proof set, compile the exact formula into a circuit and make the circuit itself fast enough, batched and parallelized on the hardware neural networks already use. Whether exactness can be made cheap, instead of approximation being made safe, is the subject of the GPU-native neuro-symbolic chapter.

Why it matters

This chapter is the volume's cleanest statement of its title: making logic differentiable did not require new logic, it required a new algebra over an old logic. One fixpoint loop, written in Volume 2 for provenance bookkeeping, computed classical derivability, Viterbi-style best proofs, anytime probabilistic inference, and exact gradients, distinguished only by the four-operation object passed as an argument. That modularity is the engineering answer to the two-pillars tension this volume opened with: the symbolic pillar keeps its semantics (the rules were never softened, and the top-1 proof matched Volume 1's SLD prover bit for bit), while the neural pillar gets what it needs (a gradient at the boundary, checked against finite differences at $10^{-6}$). The exactness dial also previews Volume 5's central trade: a system that can report how approximate it currently is, and can buy exactness back for compute, is auditable in a way a monolithic soft reasoner is not. When Volume 5 asks what makes a neuro-symbolic system trustworthy at scale, "the logic stayed exact and the approximation lived in a knob we can turn" is one of the few answers with a theorem attached.

Key terms

• Commutative semiring $(K, \oplus, \otimes, 0, 1)$ — two associative, commutative operations on a tag set $K$, with identities $0$ and $1$, annihilating $0$, and $\otimes$ distributing over $\oplus$; the contract Volume 2's engine requires of any tag algebra.
• Provenance / tag — the value a fact carries through the fixpoint: $\otimes$ combines a rule body's tags, $\oplus$ merges alternative derivations of the same head.
• Max-prob semiring — $([0,1], \max, \times)$; a derived fact's tag is its best single proof's probability, the Viterbi reading of Datalog and the tropical semiring's $[0,1]$ cousin.
• Top-$k$-proofs provenance — tags are sets of at most $k$ proofs (coin sets); $\vee_k$ keeps the $k$ most probable proofs of the union, $\wedge_k$ the $k$ most probable pairwise conflict-free unions; exact when $k$ reaches the proof count.
• Absorption — the law $a \vee (a \wedge b) = a$; concretely, dropping superset proofs, which caps tag growth and lets the recursive fixpoint terminate.
• Inclusion-exclusion — the alternating-sum formula converting a set of overlapping proofs into an exact probability, each term a product over a union of coin sets; the desk-scale stand-in for weighted model counting on the proof DNF.
• Dual-number gradient semiring — tags $(p, \nabla p)$ with componentwise $\oplus$ and the product rule in $\otimes$; aProbLog's gradient semiring, forward-mode differentiation as tag arithmetic.
• Disjoint-sum problem — proofs are overlapping events, so $\oplus = +$ overcounts (the committed $1.22$ against the true $0.86$); solved by inclusion-exclusion or WMC over a disjoint representation.
• Exactness dial — the parameter $k$: fidelity rises monotonically with $k$ at polynomially bounded per-round cost, saturating at exact inference.
• Stratification — layering a program so no relation depends on the negation or aggregation of itself; each stratum runs to fixpoint before the next, extending Datalog's guarantees to the full language.

Where this leads

Scallop kept the logic classical and put all the flexibility into the tags: truth stayed two-valued inside the rules, and probability lived in the algebra wrapped around them. The next chapter makes the opposite bet. Logic Tensor Networks push the real numbers into the semantics itself: constants become vectors, predicates become neural functions into $[0,1]$, and the connectives become the fuzzy t-norm operators of the t-norms chapter, so that a first-order formula evaluates to a differentiable degree of truth called Real Logic. Where this chapter's slogan was "approximate the tags, keep the logic exact," the next chapter's is "relax the truth values, keep the formulas"; the two designs bracket the space every differentiable framework in Part III lives in.

---

Companion code: examples/integration/provenance.py implements this entire chapter on Volume 2's imported engine: the three new semirings (MAXPROB line 221, topk_semiring lines 237–249, DUAL lines 260–266), the exact world-enumeration oracle pinned to distsem.P_query (lines 146–162), the SLD proof oracle (lines 180–190), inclusion-exclusion in scalar and dual arithmetic (lines 201–212 and 308–329), the finite-difference gradient check (lines 332–340), and the asserts guarding every claim quoted here (lines 351–425). Run python3 examples/integration/provenance.py to reproduce every number in this chapter byte for byte; the run ends with 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.