Soft Unification: Matching Symbols in Vector Space

📍 Where we are: Part V · Attention and Transformers — Chapter 17. Vector Symbolic Architectures gave a single vector an algebra of binding and superposition; this chapter softens the last hard operation left in the stack, the symbol-equality test on which every proof in Volume 1 turned.

Every proof this series has run, from Volume 1's backward chainer to Volume 2's completion engine, ultimately rests on one primitive act: deciding whether two symbols are the same. That decision has always been binary. advises unifies with advises; it does not, cannot, and will never unify with supervises, no matter that any human reader treats the two words as interchangeable. This chapter replaces the binary decision with a graded one. Each predicate name becomes a vector, two names match with a kernel score between 0 and 1, identical names still score exactly 1, and a proof carries the minimum of its match scores instead of a truth value. The result is a prover that keeps the entire recursive shape of symbolic proof (goals, rules, substitutions, proof trees) while surviving the near-miss that kills its hard ancestor. The committed demo measures both the gain and the price with real numbers, and the price is the honest center of the chapter: a soft proof is a score, and a score is only as trustworthy as the numeric margin defending it.

The simple version

Imagine a form-processing office. The old clerk rejects any form whose field label is not an exact match for the rulebook: write "supervisor" where the rulebook says "adviser" and your application dies on the spot, however obvious the intent. The new clerk accepts near-matches but writes a confidence next to each one: "adviser"/"adviser" gets a 1.0, "adviser"/"supervisor" a 0.98, "adviser"/"citation" a 0.36. When your application passes through a chain of such clerks, the final stamp carries the lowest confidence any clerk wrote, because a chain of judgments is only as trustworthy as its shakiest link. The office then sets a bar: applications stamped 0.80 or higher go through. Everything in this chapter is that office, made precise: the confidence is a kernel on vectors, the lowest-stamp rule is a t-norm, and the bar is a threshold whose exact placement, it turns out, is where all the danger lives.

What this chapter covers

• The hinge, recalled: Volume 1's unification in three sentences (substitutions, the equality gate, hard failure) and the brittleness exhibit, one unknown predicate name killing an entire proof.
• The kernel: predicate names as unit vectors in $\mathbb{R}^{16}$, the RBF match $\exp(-\lVert \mathbf{u}-\mathbf{v}\rVert^2/2\sigma^2)$, a proof that identical symbols score exactly 1, the tolerance dial $\sigma$, and a variance argument for where random symbols land.
• Composition by t-norm: a proof's score is the MIN of its match scores, the Gödel t-norm of Volume 2's annotated logic; MAX pools alternative proofs; product is the stated alternative.
• The design split: the original NTP soft-matches every non-variable symbol, constants included; this module softens predicates only, arguments still bind hard, and the chapter argues why the narrower split is the right one here.
• The chainer, line by line: Volume 1's depth-bounded goal reduction with a score threaded through every recursive call.
• Three committed demos: the exact chain reproduced at 1.0000; an unseen predicate proved at 0.9783 where the hard prover returns nothing; and a control whose best proof stays at 0.4621, with the leak thresholds printed as the knobs they are.
• Where this became a field: end-to-end differentiable proving, the gradient of the kernel derived, the proof-explosion cost, and the line to attention.

The hinge, recalled: match exactly or fail

Volume 1's Resolution and SLD (SLD abbreviates Selective Linear resolution for Definite clauses) built proof on unification: given a goal atom and a rule head (or fact), find a substitution, a dictionary binding variables to terms, that makes the two atoms identical, or report failure [1]. The procedure is all-or-nothing by construction: predicate names must be equal as strings, constants must be equal as strings, and in full first-order logic an occurs check additionally refuses to bind a variable to a term containing itself (Volume 1's function-free fragment never needed to fire it, since its terms cannot nest). When unification succeeds it returns the substitution and the proof continues; when it fails, that branch of the proof dies with no notion of "almost".

Here is the wound that motivates everything below. Ask Volume 1's prover the query supervises(bob, Z). The knowledge base in examples/logic/kb.py holds four advises facts, among them advises(bob, carol) and advises(bob, dave), and any reader of English knows those facts answer the question. The prover does not read English. It scans for a fact or rule head whose predicate is the string supervises, finds none, and returns the empty answer set. One unfamiliar word, and a knowledge base that plainly contains the answer is worth nothing. The failure is not a bug; it is the exact contract that made Volume 1's proofs auditable. The question of this chapter is whether the contract can be relaxed by a controlled amount rather than abandoned.

Symbols as vectors: a kernel grades the match

The relaxation, introduced by Neural Theorem Provers (NTPs), is surgical [2]: keep the whole proof machinery (goals, rules, substitutions, recursion) and replace the string-equality test on symbols with a similarity score on embeddings of those symbols. In the original NTP the softness is total: every non-variable symbol, predicate name and constant alike, gets a vector and may soft-match any other symbol in the same position. The companion module adopts the mechanism but deliberately narrows it to predicate names only, a design restriction defended in its own section below. soft_unification.py sets up the geometry in its constants block (lines 56–58): every predicate name $p$ gets a vector $\mathbf{u}_p \in \mathbb{R}^{D}$ (the symbol $\in$ reads "is an element of", and $\mathbb{R}^{D}$ is the set of all lists of $D$ real numbers), where $D = 16$ is the embedding dimension (the number of coordinates in each symbol's vector), $\sigma = 1$ (sigma) is a width parameter we will decode in a moment, and $\tau = 0.8$ (tau) is the acceptance threshold an answer's score must reach. Each vector is drawn from a seeded random generator and normalized to unit length, so $\lVert \mathbf{u}_p \rVert = 1$ for every predicate (lines 63–68); the double bars $\lVert\cdot\rVert$ denote the Euclidean norm, the square root of the sum of squared coordinates. Two names then match with the radial basis function (RBF) kernel, quoted here from the file (soft_unification.py lines 80–88):

def kernel(p: str, q: str) -> float:
    """NTP's soft-match score for two predicate names: the RBF kernel

        k(p, q) = exp(-‖u_p − u_q‖² / (2σ²)),   σ = 1.

    Identical symbols have distance 0, so k = e⁰ = 1.0 *exactly*: hard
    unification is the special case the kernel recovers."""
    diff = EMB[p] - EMB[q]
    return float(np.exp(-float(np.dot(diff, diff)) / (2.0 * SIGMA * SIGMA)))

One fidelity note before the formula is decoded: the docstring credits the mechanism to NTP, and the mechanism (a similarity kernel in place of the equality test) is indeed NTP's, but the exact formula is this module's choice. NTP's published kernel is $\exp\!\big(-\lVert \mathbf{u}_p - \mathbf{u}_q \rVert_2 / (2\mu^2)\big)$, an exponential of the plain, un-squared Euclidean distance (the subscript 2 marks the same norm decoded above), with its width $\mu$ (mu) fixed at $1/\sqrt{2} \approx 0.707$ [2]. The module uses the standard squared-exponential RBF with $\sigma = 1$ instead; both versions decrease with distance and score identical symbols at exactly 1, and every number in this chapter comes from the squared form quoted above.

Decode the formula before trusting it. Write $\boldsymbol{\delta} = \mathbf{u}_p - \mathbf{u}_q$ for the difference vector between the two symbol embeddings. The kernel is

$$k(p, q) \;=\; \exp\!\left(-\,\frac{\lVert \mathbf{u}_p - \mathbf{u}_q \rVert^2}{2\sigma^2}\right),$$

where $\exp(x) = e^x$ is the exponential function. Three properties carry the whole chapter, and each is a short derivation rather than an assertion.

Identical symbols score exactly 1. If $p = q$ then $\boldsymbol{\delta} = \mathbf{0}$, so $\lVert\boldsymbol{\delta}\rVert^2 = 0$ and $k = e^0 = 1$ exactly, not approximately. Conversely, $\lVert\boldsymbol{\delta}\rVert^2 \ge 0$ always, and the exponential of a non-positive number is at most 1, so $k \le 1$ with equality only when the embeddings coincide. Hard unification therefore survives inside the soft prover as a special case: wherever the old prover would have succeeded, the new one succeeds with score 1.

On unit vectors, the kernel is a function of the angle. Expand the squared distance with the dot product, using $\mathbf{a}\cdot\mathbf{b} = \sum_i a_i b_i$ (the capital sigma $\sum_i$ means: add up the products of matching entries $a_i b_i$, one for each coordinate position $i$ from 1 to $D$) and $\lVert\mathbf{a}\rVert^2 = \mathbf{a}\cdot\mathbf{a}$:

$$\lVert \mathbf{u}_p - \mathbf{u}_q \rVert^2 = (\mathbf{u}_p - \mathbf{u}_q)\cdot(\mathbf{u}_p - \mathbf{u}_q) = \mathbf{u}_p\cdot\mathbf{u}_p - 2\,\mathbf{u}_p\cdot\mathbf{u}_q + \mathbf{u}_q\cdot\mathbf{u}_q = 2 - 2\,\mathbf{u}_p\cdot\mathbf{u}_q,$$

since both vectors have unit norm. Substituting into the kernel with $\sigma = 1$:

$$k(p,q) \;=\; \exp\!\left(-\,\frac{2 - 2\,\mathbf{u}_p\cdot\mathbf{u}_q}{2}\right) \;=\; e^{\,\mathbf{u}_p\cdot\mathbf{u}_q\, -\, 1}.$$

The dot product of two unit vectors is the cosine of the angle between them, so the score depends only on that angle, ranging from $e^{-2} \approx 0.135$ (opposite directions) up to $e^0 = 1$ (same direction). Every kernel number printed by the demo is this expression evaluated on two committed vectors.

The width $\sigma$ is a tolerance dial. In the general form $k = \exp(-(1 - \cos\theta)/\sigma^2)$ on unit vectors, take the two limits. As $\sigma \to 0$ the exponent diverges to $-\infty$ for any angle $\theta \neq 0$, so $k \to 0$ for every non-identical pair while identical pairs stay at 1: the kernel degenerates into the indicator of equality, and hard unification is recovered as a limit, not just a special case. As $\sigma \to \infty$ the exponent goes to 0 for every pair, so $k \to 1$ everywhere and all symbols become interchangeable. Between the two extremes, $\sigma$ sets how much angular disagreement costs; the demo fixes $\sigma = 1$ and does all of its tuning through the threshold $\tau$ instead.

The seeded geometry, measured

Where do unrelated symbols land? The module embeds the eight predicates that occur in the knowledge base or the rule head as independent random unit directions (a ninth, supervises, is constructed deliberately and is Demo B's business). For independent random unit vectors in dimension $D$, the expected dot product is 0 by symmetry, and its variance has an exact value worth deriving. Write $\mathbb{E}[\cdot]$ for the expected value, the average of a random quantity over its random draw. Let $\mathbf{v}$ be a random unit vector and $\mathbf{u}$ any fixed unit vector. The coordinates of $\mathbf{v}$ are exchangeable (any reordering of the coordinates has the same distribution), so all $D$ coordinates share one expected square; since $\sum_{i=1}^{D} \mathbb{E}[v_i^2] = \mathbb{E}[\lVert\mathbf{v}\rVert^2] = 1$, that common value is $\mathbb{E}[v_i^2] = 1/D$. Distinct coordinates satisfy $\mathbb{E}[v_i v_j] = 0$ by sign symmetry (flipping the sign of one coordinate leaves the distribution unchanged but negates the product). Then

$$\operatorname{Var}(\mathbf{u}\cdot\mathbf{v}) = \mathbb{E}\!\left[\Big(\sum_{i=1}^{D} u_i v_i\Big)^{2}\right] = \sum_{i=1}^{D}\sum_{j=1}^{D} u_i u_j\, \mathbb{E}[v_i v_j] = \sum_{i=1}^{D} u_i^2 \cdot \frac{1}{D} = \frac{1}{D}.$$

With $D = 16$ the typical dot product is $\pm 1/\sqrt{16} = \pm 0.25$, so unrelated symbols should score near $e^{0 \pm 0.25 - 1}$, that is, roughly between $e^{-1.25} \approx 0.287$ and $e^{-0.75} \approx 0.472$, centered on $e^{-1} \approx 0.368$. The run confirms it. Here is the committed output of python3 soft_unification.py, the kernel row of advises against every other predicate:

kernel row of advises (its soft match against every other predicate):
  supervises   0.9783   student      0.5292   about        0.4692   professor    0.4189
  cites        0.3621   authored     0.3555   grandAdvisor 0.2939   affiliated   0.2455
  (supervises is constructed: normalize(e_advises + 0.25·noise), a
   stand-in for what training on text would learn; the rest are
   independent random directions, so they land near exp(−1) ≈ 0.37)

Read the row against the derivation. Inverting $k = e^{\cos\theta - 1}$ gives $\cos\theta = 1 + \ln k$, where $\ln$ is the natural logarithm, so student at 0.5292 sits at $\cos\theta = 0.364$ (about $1.5$ standard deviations above 0) and affiliated at 0.2455 sits at $\cos\theta = -0.405$ (about $1.6$ below); all seven random symbols in the row fall within two standard deviations of the predicted center, exactly the concentration the $1/D$ variance promises (advises does not appear in its own row, and the eighth entry, supervises, is the engineered exception). That lone engineered entry scores 0.9783. As a worked trace of the kernel itself: the committed embeddings give $\mathbf{u}_{\text{supervises}}\cdot\mathbf{u}_{\text{advises}} = 0.97802$, so $\lVert\boldsymbol{\delta}\rVert^2 = 2 - 2(0.97802) = 0.04396$ and $k = e^{-0.04396/2} = e^{-0.02198} = 0.9783$, matching the printed value; carry five decimals through the intermediates, because rounding the dot product to 0.9780 first lands on 0.9782 and misses the last digit. For cites, $\cos\theta = -0.0157$ gives $k = e^{-1.0157} = 0.3621$. One number means "near-synonym", the other means "noise floor", and the whole chapter is about the gap between them.

The proof algebra: MIN along the path, MAX across proofs

A single soft match produces a score; a proof chains several matches; a query may have many proofs. Both compositions need an algebra, and the demo takes both from Volume 2. A t-norm is a binary operation on the interval $[0,1]$ that is commutative, associative, monotone in each argument, and has 1 as its neutral element: the standard way to generalize logical AND to graded truth. The module composes a proof's matches with the Gödel t-norm, the minimum:

$$\text{score}(\text{proof}) \;=\; \min\big(k_1, k_2, \ldots, k_m\big),$$

where $k_1, \ldots, k_m$ are the kernel scores of the proof's $m$ predicate matches (one per fact or rule-head match along the path). A chain of matches is exactly as strong as its weakest link. Alternative proofs of the same answer pool with MAX, the Gödel t-conorm: an answer is as good as its best proof. This is precisely the ⟨min, max⟩ confidence algebra that Annotated Logic used in Volume 2 to propagate confidences through derivations, now reappearing uninvited inside a neural prover, and it is the composition the original NTP uses to score proofs [2].

Min is not the only candidate. The product t-norm $k_1 k_2 \cdots k_m$ is the other standard choice, used by some differentiable-proving variants, and it has the probabilist's virtue of compounding independent uncertainties. For this demo, min has three properties that make the printed numbers legible. First, it is idempotent: $\min(a, a) = a$, so a proof does not decay merely for being long. Under product, three matches at 0.9783 would compound to $0.9783^3 = 0.9363$, a penalty for depth with no semantic content here. Second, every proof score is attributable: the printed number is one identifiable kernel value on one identifiable match, not a blend of several. Third, exact sub-proofs are free: any number of 1.0 matches leaves the min untouched, which is what lets the soft prover reproduce hard results exactly. You can watch the min at work in the committed Demo A table below: the answer logic scores 0.3555 through the compact path grandAdvisor~grandAdvisor 1.0000 · advises~authored 0.3555 · advises~about 0.4692, and indeed $\min(1.0000,\, 0.3555,\, 0.4692) = 0.3555$, the middle match, the weakest link.

Hard arguments, soft predicates

One design decision does more for safety than any threshold, and it belongs to this module, not to NTP. The original NTP embeds every non-variable symbol and soft-matches any pair of them, constants as well as predicate names [2]. The companion module narrows the relaxation: only the predicate test goes soft, while arguments, the constants and variables inside an atom, still unify hard with Volume 1's substitution machinery unchanged. The split is visible in two small functions. The predicate gate (soft_unification.py lines 119–127):

def _pred_match(p: str, q: str, soft: bool) -> float | None:
    """Score of matching goal predicate ``p`` against KB predicate ``q``.
    Hard mode is Volume 1's gate: 1.0 iff the names are equal, else fail.
    Soft mode is NTP's: always succeed, with the kernel as the score."""
    if not soft:
        return 1.0 if p == q else None
    if p not in EMB or q not in EMB:
        return None
    return kernel(p, q)

And the argument unifier _unify_args (soft_unification.py lines 98–116), which is Volume 1's unify minus the predicate-equality gate; its final branch still ends in the hard clause return None # two different constants — arguments never go soft. The rationale for the restriction is semantic, not sentimental. A predicate name is a lexical label, and synonymy lives at the lexical level: supervises and advises plausibly denote the same relation. A constant is a pointer to an individual: carol and dave are different people, and no similarity between their embeddings would justify answering a question about one with a fact about the other. Blurring predicates changes how confident an answer is; blurring arguments would change who the answer is about. Keeping arguments hard also keeps the answer set discrete (each answer is a real binding, found by real substitution), which is what makes the demo's tables possible at all. The price is honest too: the module gives up NTP's ability to generalize over entities, and it takes that trade for auditability.

Hard unification's equality gate beside the RBF kernel that replaces it, and below, the MIN-composition of a proof path with the acceptance axis on which the demos land: exact at 1.0000, paraphrase at 0.9783, worst random collision at 0.6806, control at 0.4621, threshold τ = 0.80 inside the operative margin. Original diagram by the authors, created with AI assistance.

The chainer: a score threaded through Volume 1's machinery

The prover is Volume 1's depth-bounded backward chainer with one new passenger: every recursive call now yields a score alongside its substitution. The knowledge base is imported, not retyped: facts come straight from examples/logic/kb.py, and the single rule is Volume 1's chain rule, re-declared with a depth bound of 2 (soft_unification.py lines 49–52):

RULES: list[tuple] = [
    (("grandAdvisor", "X", "Z"), [("advises", "X", "Y"), ("advises", "Y", "Z")]),
]
MAX_DEPTH: int = 2

The core generator _prove yields every proof of a goal as a triple: the extended substitution, the proof's score, and the list of match steps. Facts are tried first (soft_unification.py lines 150–160):

    # 1. Facts.  Predicate match is soft; argument unification is hard.
    for fact in FACTS:
        if len(fact) != len(g):
            continue
        kv = _pred_match(g[0], fact[0], soft)
        if kv is None:
            continue
        s2 = _unify_args(g, fact, sub)
        if s2 is None:
            continue
        yield s2, kv, [Step(indent, g, f"fact {_atom(fact)}", g[0], fact[0], kv)]

Walk the lines. The arity check (len(fact) != len(g)) rejects structural mismatches outright; arity never goes soft. _pred_match returns the kernel score kv, or None in hard mode when the names differ, and that single call site is the entire difference between Volume 1's prover and this one. _unify_args then binds the arguments hard, exactly as Volume 1 did; a constant clash still kills the branch. A successful fact match is a one-step proof whose score is just kv, since the min of a single element is itself. Rules come next (lines 162–179): the goal's predicate soft-matches the rule head's predicate at score kv, the head's arguments bind hard, and the body is proved one level deeper, with the depth bound (if depth == 0: return) keeping recursion finite. The scores meet at the yield:

        for s3, body_score, body_steps in _prove_all(
                body, s2, depth - 1, indent + 1, soft, counter):
            # score = min(head match, body score): the Gödel t-norm again.
            yield s3, min(kv, body_score), [head_step] + body_steps

Conjunctions compose the same way (soft_unification.py lines 182–192): _prove_all proves the first conjunct, threads its substitution into the rest, and yields min(sc1, sc2); the empty conjunction yields 1.0, the neutral element of min, so that a rule with an exhausted body costs nothing. Finally answers (lines 195–212) runs the generator to completion, keeps the best proof per distinct binding (the MAX pooling), and renders each best proof as printable step lines. An answer is accepted when its pooled score reaches the threshold: $\text{score} \ge \tau = 0.8$.

Demo A: the exact chain, reproduced at 1.0000

The first demo asks the soft prover a question the hard prover can already answer, grandAdvisor(alice, Z), to check that softness costs nothing when symbols are exact. The committed output, the full table this time:

Demo A — exact: grandAdvisor(alice, Z) via the chain rule
  Z         score  ≥τ   best proof (pred~pred kernel, MIN-composed)
  carol    1.0000  yes  grandAdvisor~grandAdvisor 1.0000 · advises~advises 1.0000 · advises~advises 1.0000
  dave     1.0000  yes  grandAdvisor~grandAdvisor 1.0000 · advises~advises 1.0000 · advises~advises 1.0000
  mit      0.6806  -    grandAdvisor~affiliated 0.6806
  p1       0.4208  -    grandAdvisor~authored 0.4208
  logic    0.3555  -    grandAdvisor~grandAdvisor 1.0000 · advises~authored 0.3555 · advises~about 0.4692
  bob      0.2939  -    grandAdvisor~advises 0.2939
  erin     0.2939  -    grandAdvisor~grandAdvisor 1.0000 · advises~advises 1.0000 · advises~grandAdvisor 0.2939 · +2 more
  … 5 more bindings, all ≤ 0.2939

The accepted set is exactly the pair {carol, dave}, each at $\min(1, 1, 1) = 1.0000$: the goal matched the rule head exactly, and both body atoms matched advises facts exactly, tracing alice → bob → carol and alice → bob → dave. Everything from p1 down is the noise floor doing what the variance analysis predicted, random collisions in the 0.25–0.42 band. The printed proof paths make the reproduction auditable:

  proof of Z = carol (score 1.0000):
    grandAdvisor(alice,carol) ~ rule grandAdvisor(X,Z) ← advises(X,Y), advises(Y,Z)   k(grandAdvisor,grandAdvisor)=1.0000
      advises(alice,bob) ~ fact advises(alice,bob)   k(advises,advises)=1.0000
      advises(bob,carol) ~ fact advises(bob,carol)   k(advises,advises)=1.0000

The hard prover, run on the same goal, returns the same two bindings; the module asserts the agreement (soft_unification.py lines 279–280). One row deserves a second look. The runner-up mit at 0.6806 is not a near-synonym effect; it is the goal predicate grandAdvisor soft-matching the fact affiliated(alice, mit) through a pure random collision of two seeded directions, $\cos\theta = 0.615$, about $2.5$ standard deviations above the mean for $D = 16$. Among the 28 random pairs in this vocabulary, this one is the maximum: 0.6806 is the vocabulary-wide worst collision, the single number any safe threshold must clear, and it is the reason the demo's $\tau = 0.8$ sits so high above the noise floor near 0.37. Hold on to it; Demo C's honesty audit turns on this row.

Demo B: proving with a predicate that has no facts

The centerpiece asks the question that motivated the chapter: supervises(bob, Z), a predicate that appears in no fact and no rule. First, how supervises got a vector at all, quoted with its honesty note intact (soft_unification.py lines 70–77):

# The UNSEEN query predicate ``supervises``: no fact and no rule mentions it.
# Its vector is placed *near* ``advises`` — normalize(e_advises + 0.25·noise),
# with unit noise — standing in for what training on text would learn, because
# "X supervises Y" is used in the same contexts as "X advises Y".
_noise = _rng.standard_normal(D)
_noise /= float(np.linalg.norm(_noise))
_sup = EMB["advises"] + 0.25 * _noise
EMB["supervises"] = _sup / float(np.linalg.norm(_sup))

No training happens in this module; the placement is seeded geometry standing in for distributional learning. In a trained system, the vector for supervises would end up near advises because the two words occur in the same contexts; here the demo constructs that outcome directly and says so. With the vector placed, the committed output puts the hard and soft provers side by side:

Demo B — soft: supervises(bob, Z), an UNSEEN predicate (no facts)
  hard prover (Volume 1's equality gate): answers = []  — symbolic unification fails outright
  soft prover: k(supervises, advises) = 0.9783, so advises facts carry the query
  Z         score  ≥τ   best proof (pred~pred kernel, MIN-composed)
  carol    0.9783  yes  supervises~advises 0.9783
  dave     0.9783  yes  supervises~advises 0.9783
  p1       0.3638  -    supervises~authored 0.3638
  erin     0.3285  -    supervises~grandAdvisor 0.3285 · advises~advises 1.0000 · advises~advises 1.0000
  logic    0.3285  -    supervises~grandAdvisor 0.3285 · advises~authored 0.3555 · advises~about 0.4692
  p2       0.3285  -    supervises~grandAdvisor 0.3285 · advises~advises 1.0000 · advises~authored 0.3555
  p3       0.3285  -    supervises~grandAdvisor 0.3285 · advises~advises 1.0000 · advises~authored 0.3555
  … 4 more bindings, all ≤ 0.2939

The empty list on the first line is Volume 1's whole verdict: no fact is named supervises, so there is nothing to prove. The soft prover accepts {carol, dave} at 0.9783, each through a one-step proof, goal supervises(bob,carol) against fact advises(bob,carol), score $\min(0.9783) = 0.9783$, above $\tau = 0.8$. The fourth row shows the rule participating too: erin scores 0.3285 through supervises~grandAdvisor 0.3285 · advises~advises 1.0000 · advises~advises 1.0000, the goal soft-matching the rule head while the body proves exactly; the min correctly reports the chain's one weak link, and 0.3285 rightly fails the bar. This is the entire promise of soft unification in one table: the recursive proof machinery intact, the knowledge base untouched, and a query in unseen vocabulary answered at a quantified, attributable confidence.

Demo C: the control, and the threshold read honestly

A method that can prove supervises through advises facts must be checked for what else it will prove. The control query is cites(bob, Z): cites is a real predicate (papers cite papers), but its vector is an independent random direction, unrelated to advises, and bob cites nothing. The hard prover would return nothing here as well, since no fact has the form cites(bob, ...). The committed soft results, again in full:

Demo C — control: cites(bob, Z), a predicate that embeds far away
  Z         score  ≥τ   best proof (pred~pred kernel, MIN-composed)
  mit      0.4621  -    cites~affiliated 0.4621
  carol    0.3621  -    cites~advises 0.3621
  dave     0.3621  -    cites~advises 0.3621
  p1       0.2818  -    cites~authored 0.2818
  erin     0.2627  -    cites~grandAdvisor 0.2627 · advises~advises 1.0000 · advises~advises 1.0000
  logic    0.2627  -    cites~grandAdvisor 0.2627 · advises~authored 0.3555 · advises~about 0.4692
  ml       0.2627  -    cites~grandAdvisor 0.2627 · advises~advises 1.0000 · advises~grandAdvisor 0.2939 · +2 more
  … 4 more bindings, all ≤ 0.2627

Nothing reaches $\tau = 0.8$; nothing is accepted; soft matching did not hallucinate. But the module refuses to leave it at "did not", because the geometry shows exactly when it would have. The printed failure-mode note:

  best soft proof: Z = mit at 0.4621 — under τ = 0.80, so NOTHING is
  accepted: soft matching does not hallucinate an unrelated predicate.
  failure-mode note: acceptance would leak as τ falls.  τ below
  0.4621 (= k(cites,affiliated)) admits mit; τ below k(cites,advises)
  = 0.3621 admits carol/dave through the advises facts.  The guard
  is the kernel margin: paraphrase 0.9783 vs unrelated-symbol noise ≤ 0.4621.

Read the printed bound with its scope. The line "unrelated-symbol noise ≤ 0.4621" is a statement about this query: 0.4621 is the best score any proof can reach starting from cites, whose strongest random neighbor happens to be affiliated. It is not the vocabulary's worst collision; Demo A already exhibited that one, $k(\text{grandAdvisor}, \text{affiliated}) = 0.6806$, the maximum over all 28 random pairs. Because proofs compose by min, any proof that leans on even a single random-pair match can score at most 0.6806, while every intended answer in the three demos scores 0.9783 or 1.0000. The margin that actually defends $\tau = 0.8$ is therefore the gap from 0.6806 to 0.9783: any $\tau$ above the former and not above the latter accepts every intended answer while rejecting every random collision in this vocabulary, and 0.8 sits inside that interval, closer to the collision than the round number suggests. A threshold tuned only against this control would deceive: $\tau = 0.6$ keeps Demo C spotless yet admits the spurious mit at 0.6806 on Demo A's query. Lay the control's own regimes out as the knob they describe:

threshold setting	accepted set for cites(bob, Z)	reading
$\tau \gt 0.4621$	nothing	the demo's regime: the control stays clean
$0.3621 \lt \tau \le 0.4621$	mit	the collision cites~affiliated (0.4621) leaks through
$0.2818 \lt \tau \le 0.3621$	mit, carol, dave	the noise floor itself (cites~advises at 0.3621) starts proving things; at 0.2818 and below, p1 (via cites~authored) and the rest of the tail follow

Say it plainly: the safety of soft unification in this demo is a numeric margin, not a guarantee. The paraphrase scores 0.9783 and the worst random collision scores 0.6806; $\tau = 0.8$ separates them here, with less room to spare than the clean control table implies. And the margin is a property of this seeded geometry with this vocabulary of nine predicates. Grow the vocabulary and the maximum of many random dot products grows with it; let training move the vectors and the margin moves too, in directions no theorem controls. The module's competency asserts (soft_unification.py lines 275–287) pin all three demos: A accepts exactly {carol, dave} at 1.0, B accepts exactly {carol, dave} at 0.8 or better while the hard prover returns nothing, C's best proof stays at or under 0.5. The one-line summary the run ends with collects the demos' headline numbers:

SUMMARY soft_unification: A_answers=2 A_score=1.0000 B_answers=2 B_score=0.9783 k_supervises_advises=0.9783 C_best=0.4621 k_cites_advises=0.3621 hard_B=0 tau=0.80

And the three demos in one view:

demo	query	hard prover	soft prover, accepted at $\tau = 0.8$	best score	verdict
A (exact)	grandAdvisor(alice, Z)	carol, dave	carol, dave	1.0000	soft reproduces hard exactly
B (paraphrase)	supervises(bob, Z)	nothing	carol, dave	0.9783	soft proves where hard cannot
C (control)	cites(bob, Z)	nothing (no such fact)	nothing	0.4621	no leak, by a measured margin

From demo to field: learning the embeddings from proof success

Everything above used fixed embeddings. The step that made soft unification a research field is that the kernel is differentiable, so the embeddings can be learned from proof success [2]: treat the score of a known-true query's best proof as something to push toward 1, a known-false one's toward 0, and run the gradient descent of Volume 1 on the symbol vectors themselves. The gradient is worth deriving, because its form explains the training dynamics. Fix $\mathbf{u}_q$ and differentiate $k$ with respect to the $i$-th coordinate of $\mathbf{u}_p$. With $\boldsymbol{\delta} = \mathbf{u}_p - \mathbf{u}_q$ and $s = \lVert\boldsymbol{\delta}\rVert^2 = \sum_j \delta_j^2$, first

$$\frac{\partial s}{\partial u_{p,i}} \;=\; \frac{\partial}{\partial u_{p,i}} \sum_j \big(u_{p,j} - u_{q,j}\big)^2 \;=\; 2\big(u_{p,i} - u_{q,i}\big) \;=\; 2\,\delta_i,$$

since only the $j = i$ term of the sum depends on $u_{p,i}$ and its inner derivative is 1. Then, by the chain rule on $k = \exp(-s/2\sigma^2)$:

$$\frac{\partial k}{\partial u_{p,i}} \;=\; \exp\!\left(-\frac{s}{2\sigma^2}\right)\cdot\left(-\frac{1}{2\sigma^2}\right)\cdot 2\,\delta_i \;=\; -\,\frac{k}{\sigma^2}\,\delta_i, \qquad\text{so}\qquad \nabla_{\mathbf{u}_p}\, k \;=\; \frac{k}{\sigma^2}\,\big(\mathbf{u}_q - \mathbf{u}_p\big).$$

Here $\nabla_{\mathbf{u}_p} k$ (read "nabla", the gradient of $k$ with respect to $\mathbf{u}_p$) is the vector that collects all $D$ partial derivatives $\partial k / \partial u_{p,i}$ into one direction; since $\delta_i = u_{p,i} - u_{q,i}$, the $D$ entries $-(k/\sigma^2)\,\delta_i$ assemble into $(k/\sigma^2)(\mathbf{u}_q - \mathbf{u}_p)$. Gradient ascent on $k$ pulls $\mathbf{u}_p$ straight toward $\mathbf{u}_q$, with a strength proportional to $k$ times the remaining distance: near-misses feel a strong pull, while far-apart symbols ($k \approx 0$) feel almost none, so training refines plausible near-synonyms rather than collapsing the whole vocabulary onto one point. Composition routes the gradient just as selectively. The subgradient of $\min(a, b)$, the generalization of the derivative at the kink where the two arguments tie (away from a tie it is the ordinary derivative), is 1 with respect to the smaller argument and 0 with respect to the larger; symmetrically, MAX passes gradient only to its largest argument. So one backward pass through an answer's score touches exactly one kernel, the weakest match of the best proof. Supervision lands precisely on the link that limited the conclusion.

The cost that came with this elegance is enumeration. The chainer above tries every fact and every rule at every goal, because in soft mode _pred_match never returns None for embedded symbols; the OR-branching that hard unification pruned to a handful of name-matched candidates becomes the full knowledge base at every step, and the proof tree grows exponentially with depth. On the academic world's couple dozen facts this is invisible; on a real knowledge base it is fatal, and the original NTP could not scale past small benchmarks [2]. The follow-on line attacked exactly this bottleneck: Greedy NTPs (GNTPs) restrict each goal's fact matches to its nearest neighbors in embedding space, recovering orders of magnitude and reaching large knowledge bases and natural-language corpora [3], and Conditional Theorem Provers (CTPs) learn a rule-selection module that produces only the handful of rules worth trying for a given goal, replacing blind enumeration with a learned reasoning strategy [4].

The Attention chapter's closing promise can now be kept. Scaled dot-product attention is one-step soft retrieval: a query vector scores every key, softmax grades the matches, and a weighted value comes back; one round of matching with no variables, no substitutions, and no recursion. Soft unification is the structured version of the same act: the match scores are kernels rather than softmax weights, the retrieved content binds variables that thread through further goals, and the recursion composes scores by a t-norm into an auditable proof path. Attention is soft lookup; soft unification is soft lookup with a logic wrapped around it, and that wrapper is exactly what Volume 4's differentiable-reasoning chapters will generalize.

The unsolved part

A hard proof is a certificate: Volume 1's soundness theorem says that if the prover derives an answer, that answer is true in every model of the knowledge base, and Volume 2 rebuilt an entire reasoning stack on that guarantee. A soft proof is a score, and no theorem of this chapter connects the score to truth. When the kernel blurs supervises into advises, the proof of supervises(bob, carol) "goes through" at 0.9783, but there is no model-theoretic sense in which the conclusion follows from the premises; the knowledge base says nothing about supervises at all, and the number 0.9783 measures the geometry of two constructed vectors, not entailment. Demo C sharpened the point: the difference between "does not hallucinate" and "hallucinates" was not a semantic property of the method but the accident that 0.6806, the vocabulary's worst random collision, sits below a hand-set 0.8 while 0.9783 sits above it. Whether kernel margins can be engineered, by training objectives, calibration, or vocabulary structure, into something with the reliability of a guarantee, and how a system should report a conclusion whose provenance is a 0.83 rather than a proof, are open questions this volume cannot close. What it can do is total up the ledger honestly, and that is exactly the next chapter's job.

Why it matters

Soft unification is the first construction in this series where the procedure of symbolic reasoning, not just its conclusions, survives translation into vector space: goals reduce against rules, substitutions bind, proof trees print, and yet the whole pipeline is built from differentiable pieces that training can shape. That makes it the load-bearing precedent for Volume 4, whose integrations (semantic loss, differentiable query answering, neural theorem proving at scale) all need reasoning steps that pass gradients. It also fixes the vocabulary this series will use to audit such systems: the exact-match case must come back at score 1 (Demo A), the generalization case must be attributable to an identifiable relaxation (Demo B's one kernel), and every acceptance threshold must be reported together with the margin defending it (the 0.9783-versus-0.6806 gap, not just the control's clean table). A neural prover evaluated any less concretely than this toy is being graded on plausibility rather than evidence.

Key terms

• Unification: Volume 1's matching operation: find a substitution making two atoms identical, or fail; the equality gate this chapter softens.
• Soft unification: replacing the symbol-equality test with a kernel score on symbol embeddings, so near-synonyms match to a degree while identical symbols still score exactly 1.
• RBF kernel: $k(p,q) = \exp(-\lVert\mathbf{u}_p-\mathbf{u}_q\rVert^2/2\sigma^2)$; on unit vectors with $\sigma = 1$, equal to $e^{\cos\theta - 1}$.
• Width $\sigma$: the tolerance dial: $\sigma \to 0$ recovers hard equality as a limit, $\sigma \to \infty$ matches everything.
• Gödel t-norm / t-conorm: min and max; a proof scores the MIN of its matches (weakest link), an answer the MAX over its proofs; Volume 2's ⟨min, max⟩ confidence algebra inside a prover.
• Hard arguments, soft predicates: this module's design split, narrower than NTP's fully soft matching: lexical labels may blur, pointers to individuals may not.
• Acceptance threshold $\tau$: the score an answer must reach (0.8 here); its safety is the numeric margin between paraphrase scores and the worst random-collision score.
• Neural Theorem Prover (NTP): the architecture that made proof success differentiable, embedding every non-variable symbol (constants included) and learning the embeddings by backpropagating through kernel-scored proofs.
• Kernel margin: the gap between the intended match (0.9783) and the vocabulary's worst random collision (0.6806, grandAdvisor~affiliated); the control query's own noise tops out lower, at 0.4621. This margin is the demo's only defense against hallucinated proofs.

Where this leads

Part V is complete: attention gave vectors a differentiable where to look, vector symbolic architectures a what goes with what, and this chapter a how to prove, each with its powers and costs measured on the same tiny world. What remains is the accounting. The next chapter, The Honest Verdict, totals the volume's ledger: what the geometry of embeddings genuinely holds (similarity, hierarchy, composition, retrieval, even proof-shaped inference at a score), what only symbols guarantee (soundness, completeness, certificates that survive scrutiny), and where on that boundary the neuro-symbolic integrations of Volume 4 must build.

---

Companion code: examples/neural/soft_unification.py implements the kernel, the score-threading backward chainer, and all three demos from one seeded generator, importing Volume 1's facts and substitution machinery unchanged from examples/logic/. Run python3 soft_unification.py from examples/neural/ to reproduce every number in this chapter; the acceptance harness examples/neural/validate.py re-executes its competency asserts (exact chain at 1.0, soft recovery at 0.8 or better with the hard prover empty, control at or under 0.5) as part of the volume's verdict.