Neural Theorem Proving: NTP and CTP

📍 Where we are: Part IV · Differentiable Rule Learning — Chapter 13. Neural-LP and DRUM relaxed the choice of a rule: attention weights over a fixed menu of relation matrices, with the prover replaced by matrix algebra. This chapter keeps the prover and relaxes the matching: backward chaining survives intact, and only the symbol-equality gate inside it becomes a learned kernel.

Volume 1 built a backward chainer whose every decision was a string comparison: a goal predicate either equals a rule-head predicate or the branch dies. Volume 3's Soft Unification preview loosened that gate with hand-placed embeddings and showed inference surviving the change, but it trained nothing and it used a deliberately simplified kernel, a substitution it flagged. This chapter supplies both missing pieces. The Neural Theorem Prover (NTP) runs genuine SLD-style (Selective Linear Definite-clause resolution, Volume 1's backward-chaining strategy) proof search, or-branches over facts and and-branches over rule bodies, depth-bounded, with substitutions binding variables exactly as before, except that every predicate comparison (in the full system, every symbol comparison, constants included) returns a similarity in $(0, 1]$ instead of a verdict in $\lbrace$fail, succeed$\rbrace$ [1]. A proof's score is the minimum of its comparisons, a goal's score the maximum over its proofs, and because minimum, maximum, and the kernel are all (sub)differentiable, the whole prover becomes a loss surface. That is what makes this chapter's headline act possible: a rule template with unknown predicate slots, #1(X,Z) ← #2(X,Y) ∧ #2(Y,Z), whose slots are free vectors, is dropped into the knowledge base, and gradient descent through the prover moves those vectors until the template is a rule. The companion module ntp_mini.py runs the entire experiment on the academic world and prints the honest bill at the end: the proof-path count whose exponential growth created GNTP (Greedy NTP) and CTP (the Conditional Theorem Prover), the two scaling successors this chapter closes with.

The simple version

Imagine a genealogist tracing "grand-advisor" chains through a stack of university records, where different departments wrote "advises," "supervises," or "mentors" for the same relationship. The old clerk (Volume 1's prover) matches words letter for letter, so a chain that switches vocabulary mid-way is simply lost. The new clerk accepts near-matches, but stamps each one with a confidence, and grades a whole chain by its weakest stamp; when several chains reach the same conclusion, the best chain speaks for it. The twist is how the clerk learns which words to trust: she starts with no dictionary at all, only a folder of solved cases. Every time treating "supervises" as "advises" completes a chain that the solved cases confirm, her trust in that pairing grows; every time it endorses a known-wrong conclusion, it shrinks. After enough cases the dictionary has written itself, and one blank index card in her rulebook, "any ___ of a ___ is a grand-advisor," has filled itself in with the right words. The price appears when the archive grows: a clerk who never says "no match" must consider every record at every step of every chain.

What this chapter covers

• Two ancestors, precisely reconnected: Volume 1's backward chainer (goal, head unification, recursive body proving) and Volume 3's untrained preview, and exactly which two pieces were missing: the paper's kernel and learning from proof success.
• The kernel, exactly: $k(a, b) = \exp(-\lVert \theta_a - \theta_b \rVert_2 / (2\mu^2))$ with $\mu = 1/\sqrt{2}$, the Euclidean distance not squared, a detail the source code pins despite the literature's "RBF" (radial basis function) label, contrasted honestly with Volume 3's squared variant.
• The prover as a scored search: or/and recursion quoted from the companion, minimum along a proof path (the Gödel t-norm, Part I returning inside a prover), maximum across proofs, the depth bound, and the design split that keeps substitutions hard while predicates soften.
• Templates as learnable rules: what "learning a rule" now means (placing the slots #1 and #2 near real predicates in embedding space), the negative log-likelihood objective with per-epoch corrupted negatives, and the two pinned tricks: the paper's self-unification masking and the module's unit-norm embeddings (its documented substitute for the paper's Adam + ℓ2).
• Gradients through min and max: subgradient routing (only the weakest link of the winning proof moves), the kernel derivative worked out by the chain rule, and the committed loss trace from 0.4579 down to 0.0333.
• The committed results, read carefully: the template decoded back to the gold chain rule, held-out grandAdvisor proofs at 0.9032 against a corruption ceiling of 0.1354, and a synonym learned from two facts.
• The cost ledger, counted not asserted: the printed proof-path table, the per-depth blowup it demonstrates, and the field's two answers, GNTP's top-k fact filtering and CTP's learned rule selection.

Two ancestors, one missing half

Volume 1's Resolution and SLD chapter built a prover that takes a goal, an atom to be established, such as grandAdvisor(alice, carol). It scans the program for a rule whose head unifies with the goal, meaning the two atoms can be made identical by substituting terms for variables, and the unification computes that substitution. It then recursively proves every atom of the rule's body under that substitution, treating facts as rules with empty bodies, and a goal succeeds exactly when some such recursion bottoms out entirely in facts. The recursion is visible in the committed code: sld.py lines 52–60 loop over rules, call unify(head, g, sub), and on success descend into _solve(body, ...). One line of that loop is this chapter's entire subject: if s is None: continue. Unification either succeeds or fails, and the very first check inside Volume 1's unify is predicate-name equality, so a goal written with supervises can never touch a fact written with advises, no matter how transparently the two words name the same relation.

The second ancestor already attacked that line. Volume 3's Soft Unification preview gave every predicate name an embedding and replaced the equality gate with a similarity score, and its committed run answered supervises(bob, Z), a predicate with no facts at all, through the advises facts, at score 0.9783, while the hard prover returned nothing. But that demonstration was deliberately half of the idea. Its embeddings were hand-placed: seeded random unit vectors, with supervises constructed to sit near advises by the line _sup = EMB["advises"] + 0.25 * _noise (soft_unification.py lines 74–77), standing in for what learning would produce. And its kernel squared the distance, $\exp(-\lVert u_p - u_q \rVert^2 / (2\sigma^2))$ with $\sigma = 1$ (soft_unification.py lines 80–88), a simplification the preview flagged and this chapter now repays. The two missing pieces are exactly the two contributions of NTP [1]: the paper's kernel, stated next, and the training loop that makes embeddings earn their positions from proof success, stated after.

The kernel, exactly

Notation first. Every predicate symbol $a$ owns an embedding $\theta_a \in \mathbb{R}^{16}$, a row of 16 real numbers; 16 is the embedding dimension, called $D$ in the code (ntp_mini.py line 72). The symbol $\lVert v \rVert_2$ is the Euclidean norm of a vector $v$, the square root of the sum of its squared coordinates, so $\lVert \theta_a - \theta_b \rVert_2$ is the ordinary straight-line distance between the two embeddings (the subscript 2 is why this distance is also called the L2 distance). The soft unification score of two predicate symbols is

$$k(a, b) \;=\; \exp\!\left(-\,\frac{\lVert \theta_a - \theta_b \rVert_2}{2\mu^2}\right), \qquad \mu = \frac{1}{\sqrt{2}},$$

where $\mu$ is a fixed bandwidth (how quickly similarity decays with distance) and $\exp$ is the exponential function. The chosen bandwidth makes the denominator vanish from sight: $2\mu^2 = 2 \cdot (1/\sqrt{2})^2 = 2 \cdot \tfrac{1}{2} = 1$, so the kernel is simply $k = e^{-d}$ with $d = \lVert \theta_a - \theta_b \rVert_2$. Two consequences follow immediately. First, identical symbols have $d = 0$, so $k = e^{0} = 1$ exactly: hard unification survives as the special case, and a proof that never leaves exact matches scores a classical 1. Second, the kernel is never zero, since $e^{-d} \gt 0$ for every finite $d$: soft unification never fails, a fact that will dominate the cost analysis. On unit-norm embeddings the failure-to-fail is even quantitative. The triangle inequality bounds the distance between two unit vectors by the sum of their lengths, $\lVert \theta_a - \theta_b \rVert_2 \le \lVert \theta_a \rVert_2 + \lVert \theta_b \rVert_2 = 1 + 1 = 2$, with equality exactly when the vectors are antipodal (opposite points on the sphere). So every kernel value lives in $[e^{-2}, 1]$, and $e^{-2} \approx 0.1353$ is a hard floor: any structurally valid proof scores at least that, no matter how wrong its predicates are. Keep the number 0.135 in mind; it will reappear, to three decimals, in the committed corruption table.

Now the honesty note, front and center. The distance in that exponent is not squared. The literature calls this kernel an RBF (radial basis function) kernel, and the standard Gaussian RBF does square the distance; but the reference implementation's similarity computes the plain L2 distance, which makes the function a Laplacian-family similarity rather than a Gaussian one, and the companion module follows the code (ntp_mini.py lines 5–16 state the verification; the kernel itself is lines 125–138):

def kernel(theta: np.ndarray, a: str, b: str) -> float:
    """Soft unification score of two predicate symbols — the paper's §3.1
    kernel on the UNSQUARED Euclidean distance (μ = 1/√2, so 2μ² = 1):

        k(a, b) = exp( -‖θ_a − θ_b‖₂ / (2μ²) ).

    Identical symbols have distance 0, so k = e⁰ = 1.0 exactly: hard
    unification survives as the special case.  On the unit sphere the
    distance is at most 2 (antipodal), so every kernel is ≥ e⁻² ≈ 0.135 —
    any structurally valid proof scores at least that."""
    # d = ‖θ_a − θ_b‖₂  (plain L2 — NOT squared; the pinned detail)
    d = float(np.linalg.norm(theta[S_ID[a]] - theta[S_ID[b]]))
    # k = exp(-d / (2μ²)) = exp(-d) since 2μ² = 1
    return math.exp(-d / TWO_MU_SQ)

One honest paragraph on the contrast with Volume 3's preview, because both variants are legitimate. The squared form $e^{-d^2/2}$ and the plain form $e^{-d}$ are both valid similarity functions mapping distance into $(0, 1]$, both equal 1 at $d = 0$, and on unit-sphere embeddings both happen to bottom out at $e^{-2}$ (the squared form because $d^2 \le 4$ and $2\sigma^2 = 2$). They differ in shape, and the shape matters to training. Differentiating each with respect to $d$: for the Gaussian, $\frac{\partial}{\partial d} e^{-d^2/2} = -d\, e^{-d^2/2}$, which vanishes as $d \to 0$; for the Laplacian form, $\frac{\partial}{\partial d} e^{-d} = -e^{-d}$, which approaches $-1$ as $d \to 0$. A Gaussian kernel therefore goes flat precisely where two symbols are nearly synonymous, starving the gradient just as the pairing gets interesting, while the unsquared kernel keeps pulling near-synonyms together at full strength. The preview chose the squared form for continuity with Volume 3's Gaussian intuitions; the reimplementation follows the paper because the paper's own code does [1].

	Volume 3 preview (soft_unification.py)	This chapter (ntp_mini.py)
distance in the exponent	$\lVert u_p - u_q \rVert^2$ (squared)	$\lVert \theta_a - \theta_b \rVert_2$ (plain)
bandwidth	$\sigma = 1$, so $2\sigma^2 = 2$	$\mu = 1/\sqrt{2}$, so $2\mu^2 = 1$
kernel family	Gaussian	Laplacian-style
slope at $d \to 0$	$0$ (flat near synonyms)	$-1$ (full strength)
floor on unit vectors	$e^{-4/2} = e^{-2} \approx 0.135$	$e^{-2} \approx 0.135$
embeddings	hand-placed, seeded	learned through the prover

Backward chaining survives; only the equality gate changes: kernels score each match, min grades a proof, max picks the winner, and the right panel prices the search that a never-failing matcher must pay for. Original diagram by the authors, created with AI assistance.

The prover as a scored search

The prover's skeleton is unchanged from Volume 1: an or-module tries every way to establish one goal (each fact, each rule head), and an and-module proves a rule body's atoms left to right, threading the substitution. What changes is that each branch now carries a score, and the two modules compose scores with the two operators Part I certified. Along one proof, the matches are a conjunction, and their scores combine by minimum, the Gödel t-norm of the T-norms chapter: a chain of matches is only as strong as its weakest link. Across proofs of the same goal, the alternatives are a disjunction, and their scores combine by maximum, the Gödel t-conorm. Writing $S_\rho$ for the score of one proof $\rho$ built from unification steps with kernels $k_1, \dots, k_m$ (here $m$ counts the soft matches in that proof),

$$S_\rho = \min(k_1, \dots, k_m), \qquad \mathrm{ntp}(G) = \max_{\rho \,\vdash\, G} S_\rho,$$

where the subscript $\rho \vdash G$ ranges over the proofs of goal $G$ that complete within the depth bound of 2 (the code's DEPTH constant; the letter $d$ stays reserved for the kernel's distance): the template may expand once, and its body must then close on facts. The bound is what keeps the recursion finite, exactly as in Volume 3's preview, and it is a hard ceiling this chapter returns to at the end. Here is the depth-2 half of the search, quoted through the score because the score threading is the entire lesson, with the proof-recording bookkeeping of lines 231–239 elided (ntp_mini.py lines 211–230):

    # -- depth 2: goal ~ template head, body against facts ---------------------
    # unify(goal, #1(X,Z)): predicates compare soft, X/a and Z/b bind free.
    counts[2]["attempts"] += 1
    k_head = kernel(theta, p, "#1")
    for q1, c1, y in KB:                      # first body atom  #2(a, Y)
        counts[2]["attempts"] += 1
        if mask_self and (q1, c1, y) == goal:
            continue
        if c1 != a:
            continue
        k1 = kernel(theta, "#2", q1)          # Y binds to y symbolically
        for q2, c2, d2 in KB:                 # second body atom #2(y, b)
            counts[2]["attempts"] += 1
            if mask_self and (q2, c2, d2) == goal:
                continue
            if (c2, d2) != (y, b):
                continue
            k2 = kernel(theta, "#2", q2)
            # S_ρ = min(k_head, k1, k2): the soft AND along this proof.
            score = min(k_head, k1, k2)

Read the structure. The goal (p, a, b) unifies with the template head #1(X, Z): the predicate comparison is soft (k_head), but the variables X and Z bind to the constants a and b symbolically, for free, exactly as in Volume 1. The outer loop is the or-module for the first body atom #2(a, Y): every knowledge-base fact is a candidate, Y binds to the fact's second argument, and the binding is threaded into the inner loop, the or-module for the second body atom #2(Y, b). Each completed inner iteration is one proof, scored by the min of its three kernels.

This code also displays the design split that makes NTP a hybrid rather than a blur: arguments bind, predicates soften. Variable-to-constant substitution stays exact because binding is bookkeeping, not evidence; there is nothing graded about "Y now refers to carol." Predicate matching softens because that is where meaning lives: supervises versus advises is a semantic judgment, and semantic judgments are what embeddings are for. One simplification of the miniature must be stated in the same breath: the lines if c1 != a: continue make constants unify hard too, so a fact whose arguments clash is pruned outright. Real NTP embeds constants as well as predicates, so among same-arity atoms (atoms with the same number of arguments) every fact soft-unifies with every subgoal at some nonzero kernel and nothing is pruned (an arity mismatch is still FAIL, the one hard gate the paper keeps, and every fact here is binary) [1]; the module's docstring pins this simplification and its consequence, and the committed output prints both path counts side by side, ours and the unpruned one. The aggregation is the paper's too: goal_score (ntp_mini.py lines 242–256) takes the maximum over the returned proofs, with ties broken deterministically by enumeration order.

mechanism	Volume 1's prover	ntp_mini.py	full NTP
predicate match	string equality, else fail	kernel $k(a,b) \in [e^{-2}, 1]$	kernel
constant match	equality, else fail	equality, else fail (pinned simplification)	kernel
variable binding	substitution, exact	substitution, exact	substitution, exact
conjunction (one proof)	all body atoms succeed	min of step kernels	min
disjunction (many proofs)	first success	max over proofs	max
failure	pruned branch	only argument clashes prune	only arity mismatch prunes

Templates: what "learning a rule" now means

The Neural-LP and DRUM chapter learned rules by softly choosing among existing relations. NTP learns rules by parameterizing the rule itself. The module declares one rule template (ntp_mini.py line 154):

TEMPLATE: str = "#1(X,Z) :- #2(X,Y), #2(Y,Z)"

The head slot #1 and the (tied) body slot #2 are not predicate names; they are two additional rows of the embedding matrix $\theta$, initialized as random unit vectors alongside the seven real predicates (ntp_mini.py lines 119–121 build the vocabulary; lines 141–147 initialize all nine rows). The template asserts a shape, "something(X, Z) follows from something(X, Y) and the same something(Y, Z)", with the two somethings left as free parameters. Learning a rule now has a precise geometric meaning: gradient descent moves $\theta_{\#1}$ and $\theta_{\#2}$ through $\mathbb{R}^{16}$, and wherever they come to rest, the template means whatever real predicates they landed near. After training, the rule is decoded by nearest neighbor: report the known predicate with the highest kernel to each slot (ntp_mini.py lines 377–382), with the min of those kernels as the rule's confidence, an upper bound on the score of any proof routed through the decoded reading.

The training signal is proof success on known atoms. The positives are four: the two grandAdvisor pairs derivable by composing advises with advises over Volume 1's facts, computed rather than retyped, with the third pair (bob, erin) held out entirely (ntp_mini.py lines 99–107), plus two facts of a deliberately planted synonym predicate, supervises, which asserts a subset of the advising relation under another name (lines 91–94). The negatives are corrupted atoms: for each positive (p, a, b), one head corruption (p, ã, b) and one tail corruption (p, a, b̃), the replacement person drawn uniformly and redrawn while the corruption is a known-true atom, the same filtered protocol as Volume 3's ranking chapters, resampled fresh every epoch (ntp_mini.py lines 327–343). The loss on one atom with label $y$ (1 for a positive, 0 for a corruption) is the negative log-likelihood (NLL) of the proof score, treating $\mathrm{ntp}(G)$ as if it were a probability of truth [1]: with $s = \mathrm{ntp}(G)$ clipped away from 0 and 1,

$$L = -\,y \ln s \;-\; (1 - y)\,\ln(1 - s).$$

Two pinned tricks make this objective trainable, and both are quoted from the code because both are the kind of detail reimplementations die on (the first trick is the paper's; the second is this module's own). The first is self-unification masking. The two supervises positives are also knowledge-base facts; without intervention, the atom supervises(alice, bob) proves itself at depth 1 by unifying with itself, kernel $k(\text{supervises}, \text{supervises}) = 1$ exactly. That proof always wins the max, the loss on the positive is already zero, and, worse, the winning kernel compares an embedding with itself, so its gradient moves nothing. Omitting the mask therefore makes the supervises positives inert: the direct two-fact synonym signal disappears, and supervises is positioned only at second hand, because grandAdvisor proof bodies can route their #2 atoms through the supervises facts as well as the advises facts, pulling supervises toward #2 while #2 is pulled toward advises (retraining with the mask disabled, an ablation not in the committed output, still lands supervises nearest advises, but at kernel 0.883 against the committed 0.9111); the template itself would still be learned from the grandAdvisor positives, whose goals are derived pairs, not knowledge-base facts, so they never self-unify. The fix is one guard, applied wherever a fact row is tried, quoted here from the depth-1 or-module; the two depth-2 body or-modules repeat the same guard with their own loop variables (lines 217–218 and 224–225). It skips the goal's unification with its own fact row during training [1] (ntp_mini.py lines 200–201):

        if mask_self and (q, c, d_) == goal:
            continue  # self-unification masked to 0 (paper §4.1)

The second trick is the unit-norm constraint, this module's substitute for the paper's Adam optimizer with ℓ2 regularization (a substitution the docstring pins, ntp_mini.py lines 37–38): after every gradient step, each touched embedding row (the code's theta[row], one row per predicate name or template slot) is projected back onto the unit sphere, $\theta_{\text{row}} \leftarrow \theta_{\text{row}} / \lVert \theta_{\text{row}} \rVert_2$ (ntp_mini.py lines 368–369):

                theta[row] -= LR * g
                theta[row] /= float(np.linalg.norm(theta[row]))

The step and the projection are one motion in the training loop: LR is the learning rate $\eta = 0.1$ (the step size scaling each gradient), g is the gradient row computed by nll_and_grads, and the division by the norm is the projection itself. This is what makes the kernel-floor argument of the previous section true throughout this module's training (real NTP, trained with Adam and ℓ2 rather than a projection, keeps no such floor), keeps every distance in $[0, 2]$ so one fixed bandwidth serves all pairs, and denies the optimizer the degenerate escape of shrinking all norms toward zero, which would inflate every kernel toward 1 without learning anything about which predicates belong together.

Gradients through min and max

The loss must now be differentiated through three layers: the NLL, then the max-over-proofs and min-within-a-proof routing (handled together), and finally the kernel. Every step is in nll_and_grads (ntp_mini.py lines 261–324), and every step is derived here.

Layer 1, the NLL. With $s$ the clipped proof score, $L = -y \ln s - (1-y)\ln(1-s)$. Differentiate term by term using $\frac{d}{ds}\ln s = 1/s$ and, by the chain rule on the inner function $1 - s$ (whose derivative is $-1$), $\frac{d}{ds}\ln(1-s) = -1/(1-s)$:

$$\frac{\partial L}{\partial s} = -\frac{y}{s} + \frac{1-y}{1-s}.$$

For a positive ($y = 1$) this is $-1/s \lt 0$: the loss falls as the score rises, so the update raises the score. For a corruption ($y = 0$) it is $+1/(1-s) \gt 0$: the update lowers the score.

Layer 2, max and min. Both operators are piecewise linear, and the argument is the one From Fuzzy to Neural made for the Gödel t-norm. Where the maximizing proof $\rho^\ast$ is unique, small perturbations of the parameters leave it maximizing, so on a whole neighborhood $\mathrm{ntp}(G) = S_{\rho^\ast}$ as an identity of functions; differentiating both sides gives $\partial\, \mathrm{ntp}(G) / \partial S_{\rho^\ast} = 1$ and exactly 0 for every losing proof. The same argument one level down: where the minimizing kernel $k_{\min}$ inside $\rho^\ast$ is unique, $S_{\rho^\ast} = k_{\min}$ identically, so the derivative is 1 through the weakest step and 0 through the others. At a tie neither operator is differentiable, and the code takes the first minimizer, a valid subgradient (any slope a kinked function admits at the kink; the linked chapter derived why the first minimizer qualifies), deterministically (ntp_mini.py lines 307–313). The composed routing is brutal and simple: of all the kernels in all the proofs of a training atom, exactly one receives gradient, the weakest link of the winning proof. Part I measured this sparsity abstractly (98 percent of a fifty-conjunct body starved per step); here it acquires consequences inside search, and we return to them below.

Layer 3, the kernel. Let $\delta = \theta_a - \theta_b$ be the difference vector of the two embeddings in the winning step and $d = \lVert \delta \rVert_2$ its length. Volume 3's EL Embeddings chapter derived the gradient of a norm coordinate by coordinate: writing $d = (\sum_{j=1}^{16} \delta_j^2)^{1/2}$, with $j$ indexing the 16 coordinates, the chain rule on the square root gives, for any single coordinate $\delta_i$ (the index $i$ naming the coordinate being varied), $\partial d / \partial \delta_i = \tfrac{1}{2}(\sum_j \delta_j^2)^{-1/2} \cdot 2\delta_i = \delta_i / d$, so $\partial d / \partial \delta = \delta / d$, the unit vector along the difference. Since $\delta$ depends on $\theta_a$ with coefficient $+1$ and on $\theta_b$ with coefficient $-1$, we get $\partial d / \partial \theta_a = \delta / d$ and $\partial d / \partial \theta_b = -\delta / d$. Now push through the exponential, whose derivative is itself: $k = e^{-d}$, so $\partial k / \partial d = -e^{-d} = -k$, and by the chain rule

$$\frac{\partial k}{\partial \theta_a} = -k \cdot \frac{\theta_a - \theta_b}{d}, \qquad \frac{\partial k}{\partial \theta_b} = +k \cdot \frac{\theta_a - \theta_b}{d},$$

with subgradient 0 chosen at $d = 0$, where the norm has its kink and the kernel is already at its maximum. This is TransE's norm gradient wearing a new coat: a positive pulls the two winning symbols together along their difference direction, a corruption pushes them apart. The full chain multiplies the three layers, $\partial L / \partial \theta_a = \frac{\partial L}{\partial s} \cdot 1 \cdot 1 \cdot \frac{\partial k_{\min}}{\partial \theta_a}$, the two middle factors being the max and min routing. The code is the derivation transcribed (ntp_mini.py lines 315–324):

    diff = theta[ia] - theta[ib]
    d = float(np.linalg.norm(diff))
    if d < 1e-12:
        return loss, {}  # subgradient 0 at d = 0 (kernel already maximal)
    # ∂k/∂θ_a = -k·(θ_a − θ_b)/d   and   ∂k/∂θ_b = +k·(θ_a − θ_b)/d
    dk_da = -min_k * diff / d
    # ∂L/∂θ = ∂L/∂s · ∂s/∂k_min · ∂k_min/∂θ, with ∂s/∂k_min = 1 (max∘min
    # both pass the unique winner through at slope 1).
    grads = {ia: dL_ds * dk_da, ib: -dL_ds * dk_da}
    return loss, grads

Training is projected stochastic gradient descent (SGD): each epoch visits the four positives and two fresh corruptions each, applies $\theta \leftarrow \theta - \eta\, \partial L / \partial \theta$ with learning rate $\eta = 0.1$ row by row, and re-projects each touched row onto the unit sphere (ntp_mini.py lines 357–372). The committed run's loss trace, deterministic under seed 0:

[1] training: NLL on the proof score, 500 epochs of projected SGD (η = 0.1)
    positives: grandAdvisor(alice,carol) grandAdvisor(alice,dave) (derived; grandAdvisor(bob,erin) HELD OUT)
    + supervises facts; 2 corruptions per positive, resampled each epoch;
    self-unification masked: a fact never proves itself
    epoch :  mean NLL
        1 :    0.4579
       10 :    0.0745
       50 :    0.0605
      100 :    0.0581
      250 :    0.0818
      500 :    0.0333

The mean NLL falls by a factor of six within ten epochs and lands at 0.0333. It is not monotone: the epoch-250 snapshot reads 0.0818, higher than epoch 50, because the corruptions are resampled every epoch and some draws land nearer the decision boundary than others. The module asserts the honest version of "training worked", that the final NLL is below 0.10 and started above it (ntp_mini.py lines 431–432), rather than asserting a smoothness the stochastic objective does not have.

Reading the committed run

Training over, the run decodes the template by nearest neighbor:

[2] decoded template (nearest known predicate per learned slot)
    #1 → grandAdvisor k = 0.9769
    #2 → advises      k = 0.9032   (supervises a near-tie at 0.9026 — it
         learned to be advises' synonym, so #2 is close to both
         names of the same relation)
    induced rule (0.9032 confidence, the paper's min-kernel decode):
      grandAdvisor(X,Z) :- advises(X,Y), advises(Y,Z)   — Volume 1's chain rule, relearned from pairs
    synonym check: supervises embeds nearest advises (k = 0.9111)

Read it slowly, because three separate claims are being verified at once. First, the induced rule is the gold rule: #1 decoded to grandAdvisor at kernel 0.9769 and #2 to advises at 0.9032, so the template's learned reading is exactly the chain rule Volume 1 wrote by hand, recovered from nothing but entity pairs and proof feedback. Second, the near-tie is not noise but correctness: #2 sits at 0.9032 from advises and 0.9026 from supervises, which is precisely what a slot should do when the knowledge base contains one relation under two names. Third, the synonym itself was earned, and by the cleanest mechanism in the run. Volume 3's preview constructed supervises next to advises by hand; here the two embeddings started as independent random unit vectors and were pulled to kernel 0.9111 by two facts' worth of proof success. With self-unification masked, each supervises positive has exactly one proof: a depth-1 soft unification with the parallel advises fact. The template body cannot close for these goals, because under hard constant matching no two-hop chain of facts connects alice to bob or bob to carol. So the winning proof's single kernel is $k(\text{supervises}, \text{advises})$, and every gradient step on these positives pulls exactly that pair of rows together.

Next, the held-out pair, never seen in training:

[3] held-out pair grandAdvisor(bob,erin) — never trained on
    proof score = 0.9032   (winning proof below; the proof path IS the explanation)
      grandAdvisor(bob,erin) ~ head #1(X,Z)   k(grandAdvisor,#1)=0.9769
          #2(bob,Y) ~ fact advises(bob,carol)   k(#2,advises)=0.9032   Y:=carol
          #2(carol,erin) ~ fact advises(carol,erin)   k(#2,advises)=0.9032
      score = min of the three kernels = 0.9032

The score clears the module's 0.5 threshold with room to spare, and the winning proof is not a black box: it is a legible derivation, the template head matched at 0.9769, the two body atoms matched against real advises facts at 0.9032 each, the variable Y bound to carol symbolically, and the min taken. One honesty note the module's docstring insists on: because this miniature keeps constants symbolic, the held-out pair is proved by the same three kernels as the training pairs (the run prints all three grandAdvisor scores as identical 0.9032), so the generalization on display is structural, the induced rule transferring to an unseen entity pair, not metric generalization in entity space. The corruption table calibrates the other side:

[4] corruptions of the held-out pair (filtered: true pairs skipped)
    atom                            score
    grandAdvisor(alice,erin)        0.0000  (no proof at depth 2)
    grandAdvisor(bob,alice)         0.0000  (no proof at depth 2)
    grandAdvisor(bob,bob)           0.0000  (no proof at depth 2)
    grandAdvisor(bob,carol)         0.1354  (fact-level k(grandAdvisor,advises): antipodal floor e^-2)
    grandAdvisor(bob,dave)          0.1354  (fact-level k(grandAdvisor,advises): antipodal floor e^-2)
    grandAdvisor(carol,erin)        0.1354  (fact-level k(grandAdvisor,advises): antipodal floor e^-2)
    grandAdvisor(dave,erin)         0.0000  (no proof at depth 2)
    grandAdvisor(erin,erin)         0.0000  (no proof at depth 2)
    max corrupted = 0.1354   →   margin = 0.7678

Every corruption of the held-out pair scores at most 0.1354, so the true pair wins by a margin of $0.9032 - 0.1354 = 0.7678$. And the ceiling value is an old friend: 0.1354 sits about $10^{-4}$ above the antipodal kernel floor $e^{-2} \approx 0.1353$ derived in the kernel section. The three corruptions that reach it are the ones whose entity pair happens to be a real advises edge, giving a depth-1 proof whose single kernel is $k(\text{grandAdvisor}, \text{advises})$; training, fed corruptions exactly like these, pushed those two embeddings nearly to opposite poles of the sphere, driving the score to within about a ten-thousandth of the floor the geometry allows. The floor is a feature here (wrong atoms cannot score lower) and a warning for later: a soft prover's "no" is never 0.

The cost ledger, counted not asserted

Everything above worked because the knowledge base is tiny, and the module refuses to let that go unpriced. Count the search tree for one goal. At depth 1, the or-module attempts a unification with every one of the $K$ facts (here $K = 20$). At depth 2, the goal unifies with the template head, and then each of the two body atoms runs its own or-module over all $K$ facts, with the first atom's binding threaded into the second: the body alone therefore spans $K \times K$ candidate fact pairs. In general, a rule body of $m$ atoms keeps $K^m$ combinations alive per expansion, and each additional level of rule nesting multiplies again: the tree grows as the knowledge-base (KB) size raised to the body length, per depth. The committed run counts it rather than asserting it:

[5] proof paths explored for grandAdvisor(bob,erin) (K = 20 facts)
    depth   this mini (hard constants)      full NTP (soft constants)
        1     20 attempts,  0 proofs           20 live paths (K^1)
        2    121 attempts,  2 proofs          400 live paths (K^2)
    real NTP embeds constants too, so nothing prunes: the 2-atom body alone
    keeps K² = 400 paths alive per goal — the blowup behind the paper's
    batch proving and K_max truncation (and behind GNTP/CTP after it)

The two columns are the honest comparison. Our miniature attempts 121 unifications at depth 2 (one head, plus 20 first-atom candidates, plus 20 more for each of the 5 facts whose first argument survives the hard constant check) and completes only 2 proofs, because symbolic constants prune mercilessly. Full NTP has no such mercy to invoke: with constants embedded too, every one of these all-binary facts soft-unifies with every subgoal at some nonzero kernel, nothing ever fails, and all $K^2 = 400$ paths stay alive for this one goal, per training atom, per epoch, with gradients flowing (the asserts at ntp_mini.py lines 455–456 pin the depth-1 count and the two completed proofs, and bound the depth-2 attempts strictly below the 400-path blowup). Scale the arithmetic once: a knowledge base of $10^5$ facts and a two-atom body gives $10^{10}$ live paths per goal. That number, not any subtlety of the semantics, is why differentiable proving stalled on small benchmarks, and the field's two answers attack the two loops of the search.

GNTP (Greedy NTP) attacks the fact loop [2]. Before unifying, it retrieves only the top-$k$ facts and rules whose embeddings are nearest the current goal, by nearest-neighbor search over the embedding space (this $k$ is a small retrieval budget, a different letter-use from the kernel $k(a,b)$), and lets the rest of the knowledge base contribute nothing: since the proof score is a max of mins, a far-away fact's kernel almost never survives the min anyway, so discarding it changes little while collapsing the branching factor from $K$ to a small constant. The reported effect was to move differentiable proving from the original evaluation's few-thousand-fact benchmarks onto knowledge bases and natural-language corpora orders of magnitude larger, where the unfiltered system could not run [2]. CTP (Conditional Theorem Prover) attacks the rule loop [3]. Instead of iterating over every template with every goal, a learned select module reads the goal and generates the few rules worth trying, conditioned on it; the generation is differentiable, so selection is trained end to end with proving, and the paper instantiates the module three ways, a linear map from the goal predicate's embedding to the rule's predicate embeddings, an attention distribution over the known predicates, and a memory-based lookup [3]. The lineage is worth stating as a lesson. Hard unification, from the resolution principle onward, computes a most general unifier or fails, and failure is free pruning: entire subtrees vanish at a string comparison [4]. The kernel bought synonymy by never failing, and GNTP's retrieval and CTP's selection are that lost discipline re-engineered in soft form, an approximate "no" reinstated where the exact one was traded away.

The unsolved part

The held-out proof scored 0.9032, and this chapter has been careful to say what that number is: the min of three kernels, maximized over proofs. It is honest about what the number is not. It is not a proof: Volume 1's prover returned a derivation whose correctness is a theorem, while a soft proof at 0.9032 is a derivation-shaped object whose three matches are merely close in a learned geometry. It is not a probability either: the training loss treated the score as a likelihood, but nothing in the min/max algebra makes scores calibrated, and Part I already showed the Gödel pair preserves order, not degree. Within one query the ordering is meaningful (0.9032 for the true pair against a 0.1354 ceiling for its corruptions is a real margin); across queries the numbers do not commensurate, a 0.83 on one goal and a 0.79 on another encode nothing about which is likelier, and the kernel floor guarantees that even nonsense scores at least $e^{-2}$. Whether such scores can be calibrated, and what guarantee a soft proof could ever certify, is Volume 5's business, and this chapter deliberately leaves the question standing. The second limit no kernel softens: the depth bound. The template closed grandAdvisor at depth 2 because the rule is a two-hop chain; a three-hop great-grandAdvisor query is unprovable at depth 2 with any embeddings, since no kernel value can conjure a missing level of recursion. That is Volume 3's Expressiveness Ceiling lesson wearing prover's clothes: what the hypothesis space omits, no amount of training recovers.

Why it matters

This chapter is the purest specimen of the volume's title: logic made differentiable by changing one gate. The algorithm is still SLD-style backward chaining, the substitutions are still exact, the proof object is still a legible derivation; only symbol equality was replaced, and everything the volume has built converged on that replacement. Part I's Gödel t-norm stopped being an abstract choice of conjunction and became the operator that grades proof paths, its one-hot gradient now deciding which two symbols in an entire search tree learn anything on a given step. The result also earns two claims Volume 3 could only stage: soft matching whose geometry is learned from proof success rather than hand-placed, and a rule induced from data that decodes back to a human-readable clause. The proof path printed by the committed run is simultaneously the system's computation and its explanation, which is exactly the faithfulness property Volume 5 will demand of trustworthy reasoners, and the cost ledger is the scale problem Volume 5 will inherit: the honest $K^{\text{depth}}$ table is where "make it differentiable" collides with "make it run," and GNTP and CTP are the first two entries in a research program that continues there.

Key terms

• Neural Theorem Prover (NTP) — a backward chainer in which predicate comparisons return kernel similarities instead of fail/succeed, proof scores are mins of kernels, goal scores are maxes over proofs, and everything is trained end to end by gradient descent through the search [1].
• Soft unification kernel — $k(a, b) = \exp(-\lVert \theta_a - \theta_b \rVert_2 / (2\mu^2))$ with $\mu = 1/\sqrt{2}$, hence $k = e^{-d}$ on the plain, unsquared Euclidean distance; identical symbols score exactly 1, and unit-norm embeddings floor every score at $e^{-2} \approx 0.135$.
• Rule template — a rule shape with free predicate slots, here #1(X,Z) ← #2(X,Y) ∧ #2(Y,Z), whose slots are learnable embedding rows; learning a rule means moving the slots near real predicates, and decoding reads each slot as its nearest known predicate.
• Self-unification masking — the training-time guard forbidding a fact from proving itself; without it a positive that is also a fact scores 1 with zero gradient and teaches nothing.
• Subgradient routing — the credit assignment through max and min: only the winning proof, and inside it only the weakest kernel, receives gradient; two embedding rows move per training atom.
• Proof-path blowup — the search tree's growth as (KB size) to the power of the body length per depth; measured here as 400 live paths for 20 facts, and the direct motivation for scaling work.
• GNTP (Greedy NTP) — differentiable proving with top-$k$ nearest-neighbor retrieval of facts and rules before unification, restoring approximate fail-fast pruning [2].
• CTP (Conditional Theorem Prover) — differentiable proving in which a learned select module generates a few goal-conditioned rules instead of iterating over all of them, with linear, attentive, and memory-based variants [3].

Where this leads

NTP welded rule learning to proof search and paid the welded price: every gradient step runs the prover, and the prover's tree grows exponentially. The next chapter, RNNLogic and AnyBURL, unbolts the weld. RNNLogic separates the two roles NTP fused, a generator proposing candidate rules and a predictor scoring them, trained as a latent-variable model so that neither pays the other's search bill; AnyBURL abandons gradients altogether, mining rules by sampling and generalizing ground paths in one-second time slices at a fraction of the compute, and its embarrassing competitiveness is the control experiment this whole part needs: after two chapters of making rule learning differentiable, the honest question is what the differentiability actually bought.

---

Companion code: examples/integration/ntp_mini.py implements this entire chapter: the unsquared kernel (lines 125–138), the scored or/and prover with its depth bound and self-unification mask (lines 169–239), the max aggregation (lines 242–256), the hand-derived NLL subgradients through max, min, and the kernel (lines 261–324), per-epoch corruption sampling (lines 327–343), projected SGD on the unit sphere (lines 346–372), template decoding (lines 377–382), and the competency asserts guarding every claim made here (lines 430–456). Run python3 examples/integration/ntp_mini.py to reproduce every number in this chapter byte for byte; the run ends with SUMMARY ntp_mini: final_nll=0.0333 decode_#1=grandAdvisor:0.9769 decode_#2=advises:0.9032 conf=0.9032 held_out=0.9032 max_corrupt=0.1354 margin=0.7678 paths_d2=121/400.