PaperlayerView exact revision on arXiv

Source-linked AI summary

Differentiable Horn Programs: A Constructive Expressivity Theorem for Latent Rule Operators

Aymen Mejri

arXiv:2609.06235v1cs.LOcs.ITmath.IT

TL;DR

Differentiable systems have lacked a closed-form construction that exactly represents Horn closure for arbitrary programs. LatentGamma is a differentiable operator with a constructive parameter assignment, and the paper reports numerical validation of its theoretical properties alongside explicit robustness bounds. Its expressivity result is bounded in time, and the paper does not establish that gradient descent finds the oracle parameters.

  • Problem

    No existing differentiable system exactly represents Horn closure for arbitrary programs through a closed-form parameter assignment.

    Source: §1 · p. 1

  • Method

    LatentGamma is a differentiable parameterized operator with a closed-form assignment for each definite Horn program.

    Source: §1 · p. 2

  • Results

    Numerical validation on programs up to M = 504 atoms and R = 648 rules confirms the paper’s theoretical results.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The construction exactly recovers Horn closure within an explicit time window beginning at derivation depth D(P, F0).

    Source: §1 · p. 2

    The expressivity theorem does not establish that gradient descent finds the oracle parameters, and the results do not cover normal or first-order programs with variable unification.

    Source: §9 · p. 7

Abstract

from arXiv · show

We introduce \textsc{LatentGamma}, a differentiable operator on the unit cube $[0,1]^M$ designed as a smooth surrogate of Tarski's immediate consequence operator $\TP$ associated with a definite Horn program $P$ on $M$ atoms. The operator is built as a five-stage composition combining sigmoidal gating, softmax routing, and a residual update that enforces monotonicity by construction. We establish four theoretical results. First, the iterated sequence is coordinate-wise non-decreasing and bounded by $\ind$, hence converges to a fixed point of \textsc{LatentGamma}; the operator itself is lattice-monotone on $[0,1]^M$. Second, our \emph{constructive expressivity theorem} shows that for every definite Horn program $P$ there exists a closed-form parameter assignment $\theta^*(P)$ and an explicit time bound $T_{\max}(P)$ such that the iterated sequence \emph{exactly} reproduces $\TPinf(F_0)$ for every initial fact set $F_0$ throughout the window $[D(P, F_0), T_{\max}(P)]$, where $D(P, F_0) \leq M$ is the derivation depth. The window $T_{\max}$ is large in practice ($\geq 10^5$ for sparse programs) and reflects the finite-time nature of computation by smooth sigmoidal gates. Third, the oracle is robust to Gaussian noise on its body and head logits, with explicit non-asymptotic bounds. Fourth, we prove a matching information-theoretic lower bound on the parameter count. We provide a complete numerical validation on programs ranging from $M = 33$ to $M = 504$ atoms: oracle accuracy reaches $1.0000$ on $2000$ test cases with zero false-positive and false-negative rates, and the empirical noise tolerance $\sigma_{\max}$ scales precisely as the union bound $RM \cdot \Phi(-10/\sigma_\eta)$ predicts.

1 INTRODUCTION

The paper asks whether a differentiable operator can exactly reproduce Horn-program closure for arbitrary definite programs, addressing the tension between neural learning and symbolic multi-step reasoning. It introduces LatentGamma and proves constructive expressivity alongside structural, robustness, and parameter-count results.

1 INTRODUCTION

  • The motivating challenge is reconciling neural networks’ pattern recognition with contested compositional reasoning and symbolic systems’ exact deduction with brittleness.The paper frames this as a need for operators that are both expressive and differentiable.Source: §1 · p. 1
  • No existing differentiable system exactly represents Horn closure for arbitrary programs through a closed-form parameter assignment.Earlier approaches answer the expressivity question only approximately or for restricted program classes.Source: §1 · p. 1
  • LatentGamma is constructed so that, for every definite Horn program, an explicit parameter assignment exactly recovers its closure throughout a bounded time window.The window begins at derivation depth D(P, F0) and has an explicit upper bound Tmax(P).Source: §1 · p. 2
  • The iterated sequence is coordinate-wise non-decreasing and bounded by 1, while the operator is lattice-monotone.These properties imply convergence of the sequence to a fixed point.Source: §1 · p. 2
  • The oracle tolerates additive Gaussian noise on its logits with explicit non-asymptotic bounds matching RM · Φ(−10/ση).The bound is stated for noise on body and head logits.Source: §1 · p. 2
  • A Horn program with R rules and body size at most k requires Ω(Rk log M) bits, and LatentGamma achieves this up to logarithmic factors.The paper also reports numerical validation on programs up to M = 504 atoms and R = 648 rules.Source: §1 · p. 2

2 RELATED WORK

Prior differentiable reasoning systems use varied representations and reasoning procedures, but the cited approaches lack LatentGamma’s constructive guarantee of exact Horn closure. The paper positions its contribution as combining constructive expressivity, lattice monotonicity, and an end-to-end differentiable symbolic core.

Differentiable theorem proving

  • Neural theorem provers use embeddings and fuzzy unification for backward chaining, while Neural Logic Machines lack a closed-form Horn-semantics expressivity guarantee.The cited systems do not provide a forward-closure object aggregating all derivable atoms.Source: §2 · p. 2

Differentiable rule induction

  • ∂ILP’s fixed rule templates constrain expressivity, while Logical Neural Networks’ guarantees concern fragments of weighted first-order logic rather than exact Horn closure.Outside its template class, ∂ILP cannot represent TP exactly.Source: §2 · p. 2

Probabilistic logic programs

  • ProbLog, DeepProbLog, and NeurASP retain a non-differentiable symbolic reasoning engine, unlike LatentGamma’s differentiable symbolic pipeline.Their exactness comes from a symbolic engine rather than a differentiable operator.Source: §2 · p. 2

Closed-form Horn surrogates and matrix-based differentiable Datalog

  • Differentiable fixed-point surrogates and TensorLog lack a constructive guarantee of exact Horn closure for arbitrary programs; fuzzy logics instead target satisfaction degrees.The cited surrogate operators are engineered for empirical performance, not a constructive expressivity theorem.Source: §2 · p. 2

Summary

  • LatentGamma is presented as the first system to combine constructive exact expressivity, lattice monotonicity, and an end-to-end differentiable symbolic core.The related-work summary distinguishes this combination from the approaches discussed in the section.Source: §2 · p. 2

3 PRELIMINARIES

The preliminaries define definite Horn programs and their forward-closure semantics, then extend coordinate-wise ordering to the unit cube. They identify the discontinuous Boolean body test as the obstacle to a direct smooth transfer.

Definite Horn programs

  • A definite Horn program is a finite multiset of rules whose bodies are conjunctions of atoms and whose heads are single atoms.The program is defined over a finite set A of atomic propositions.Source: §3 · p. 2

Immediate consequence operator

  • TP maps a fact set to its one-step closure, and its least fixed point containing F0 is reached in at most M iterations.The least fixed point is denoted T∞P(F0).Source: §3 · p. 3

Lattice and smoothness

  • Extending coordinate-wise order to [0,1]M makes it a complete lattice, but TP’s Boolean body indicator is discontinuous in the cube’s relative interior.A smooth surrogate must trade discontinuity for approximation error controlled by sharpness τ.Source: §3 · p. 3

4 THE LATENTGAMMA OPERATOR

LatentGamma parameterizes a five-stage differentiable operator using rule-body and head logits, thresholds, sharpness, and rule confidences. Its gates and residual update are designed to preserve monotonicity while approximating rule firing and head routing.

Parameters

  • The parameterization includes body and head logits, AND thresholds, sharpness parameters, rule confidences, aggregation thresholds, and a global amplitude fixed to 5.The rule-confidence vector has entries in (0, 1).Source: §4 · p. 3

Body firing

  • An additive perceptron followed by a sigmoid provides monotone body firing while avoiding the gradient attenuation of a multiplicative surrogate on long bodies.The threshold kj − 1/2 separates a satisfied body from one that is partially satisfied.Source: §4 · p. 3

Head routing

  • Softmax head routing can concentrate a rule’s weight on its designated head; with Ψ = 20 and M ≤ 10^6, that head receives weight greater than 1 − 2 × 10−3.The stated bound follows when the designated head logit is +Ψ and other logits are 0.Source: §4 · p. 3

Aggregation and gating

  • Rule contributions are weighted at each state, then aggregated and passed through a gate that sharpens discrimination between fired and non-fired states.The gate uses β = 5.Source: §4 · p. 3

Monotone residual update

  • The residual update keeps the trajectory in [0,1]M and makes it non-decreasing.The factor (1 − si) bounds the update, while giΓi preserves coordinate-wise monotonicity.Source: §4 · p. 3

5 STRUCTURAL PROPERTIES

LatentGamma’s iterates rise monotonically to a fixed point, and the operator is lattice-monotone. Because sigmoid gates leak positive mass even onto unsupported atoms, exact Horn support is a finite-window property rather than generally a fixed-point identity.

5 STRUCTURAL PROPERTIES

  • For every initial state, the iterates are coordinate-wise non-decreasing, bounded by 1, and converge to a fixed point.Source: §5 · p. 3
  • Stage 5 preserves monotonicity because its residual update is jointly monotone in the current state and aggregate rule evidence.Stages 1–4 are also monotone in the state, so their composition with the residual update preserves order.Source: §5 · p. 3
  • From the indicator of F0, the limit is the least fixed point above that initial fact set.Source: §5 · p. 3
  • Strictly positive sigmoid gates leak onto non-derivable atoms, so exact Horn support is guaranteed within a finite time window, not as a fixed-point identity.The supported window is [D(P, F0), Tmax(P)].Source: §5 · pp. 3–4

6 MAIN RESULT: EXPRESSIVITY THEOREM

For each definite Horn program, the theorem gives an explicit parameter assignment whose iterates reproduce Horn closure throughout a specified time window. The construction uses sigmoid and routing thresholds to separate satisfied rules, while the proof controls false positives and preserves support through the window.

6.1 Statement

  • For every definite Horn program, an explicit parameter assignment reproduces Horn-closure support for every initial fact set from derivation depth D(P, F0) through Tmax(P).The derivation depth is at most M.Source: §6.1 · p. 4
  • With default constants, the lower bound is Tmax ≥ 99 when ρmax ≤ 100, and Tmax ≥ 3.6 × 10^5 when ρmax ≤ 10; the latter is typical for sparse programs.The four experimental programs have ρmax values from 2 to 16.Source: §6.1 · p. 4
  • The finite Tmax follows from strictly positive sigmoid gates; bump functions can make gates exactly zero but have vanishing boundary derivatives that obstruct gradient flow.The paper retains sigmoid gates partly to preserve gradients for a future learnability extension.Source: §6.1 · p. 4

6.2 Oracle construction

  • The oracle fixes ηon=ηoff=10, Ψ=20, τs=10, ρ0=0.95, τnor=5, and β=5, with aggregation thresholds set according to each atom’s rule count.The canonical contributions are γ+ ≈4.687 and γ− ≈0.0316.Source: §6.2 · p. 4

6.3 Key lemmas

  • Satisfied rule bodies score above 0.993 and unsatisfied bodies below 0.007; head aggregation separates firing from non-firing rules when γ+ > Riγ−.Source: §6.3 · p. 5
  • For sink atoms, the per-iteration drift is at most 3.4 × 10^-25, keeping a sink starting at zero below 1/2 for T ≤10^20.Source: §6.3 · p. 5

6.4 Proof of Theorem 6.1

  • The induction handles fractional states by combining AND separation with rapid post-derivation saturation, which raises derived coordinates above 0.95 within four iterations.Source: §6.4 · p. 5
  • Since derivation depth is at most M and support remains non-decreasing after derivation, M iterations fit within the stated window under the given bounds.The stated fit covers M ≤100 when ρmax≤100 and M≤10^5 when ρmax≤10.Source: §6.4 · p. 6

7 ROBUSTNESS AND NUMERICAL VALIDATION

Numerical tests validate exact oracle behavior and structural properties across four Horn programs, while noise experiments closely track the predicted robustness bound.

7.1 Robustness to parametric noise

  • At η = 10, Ψ = 20, and unit noise scales, the reported head-routing flip bound is far smaller than the body-flip bound.The body-flip bound is RM · 7.6 × 10^-24; the head-routing bound is R(M − 1) · Φ(−14.1) ≈ 0.Source: §7.1 · p. 6

7.2 Numerical setup

  • Four programs range from 33 to 504 atoms; each used 500 random initial fact sets, totaling 2,000 validation cases.Initial sets had sizes from 2 to 8, and the reference closure was computed symbolically.Source: §7.2 · p. 6, §7.3 · p. 6

7.3 Validation of Theorem 6.1

  • Zero false positives and zero false negatives occurred across all 2,000 Theorem 6.1 test cases.On G4, convergence took 32 iterations, far fewer than its 504 atoms; the result is consistent with convergence requiring the derivation depth rather than M.Source: §7.3 · p. 6, Table 1 · p. 6

7.4 Validation of structural properties

  • All tested structural properties held across 500 random states per program.Tests checked parameter-independent properties and non-decrease along iterated trajectories.Source: §7.4 · p. 6, Table 2 · p. 7

7.5 Edge cases

  • All 33 critical edge cases passed with Jaccard = 1.Cases included empty initial facts, a single root, a full root set, and leaves.Source: §7.5 · p. 7

7.6 Empirical validation of the robustness bound

  • Empirical σmax fell from 3.0 on G1 to 2.0 on G4 as RM grew by two orders of magnitude, closely matching the union-bound estimates.Accuracy collapsed where the theoretical bound became vacuous, supporting the reported σmax scaling as tight rather than merely sufficient.Source: §7.6 · p. 7, Table 3 · p. 7

8 PARAMETER COMPLEXITY

The section establishes an information-theoretic lower bound on parameters needed to represent Horn-program closures, then compares it with LatentGamma’s parameter count and differentiability trade-off.

Parameter count

  • LatentGamma uses Θ(RM) scalar parameters, matching the lower bound up to a factor of M/(k log M).For k = Θ(log M), the gap is Θ(M / log^2 M); the section attributes this excess capacity to preserving differentiability.Source: §8 · p. 7

Theorem 8.1

  • Any operator representing every equivalence class of programs requires at least Ω(Rk log M / b) bits when each parameter has b-bit precision.Distinct equivalence classes induce distinct closure functions and therefore require distinct parameter vectors.Source: §8 · p. 7

Proof sketch

  • The proof counts semantically distinct closure functions after quotienting programs by logical equivalence.The stated counting argument gives log2 |HM,R,k/∼| ≥ R(log2 M + k log2 M − k log2 k) − O(R).Source: §8 · p. 7

9 LIMITATIONS AND CONCLUSION

LatentGamma combines constructive expressivity, structural properties, robustness, and a parameter lower bound, with numerical validation through 504 atoms. The paper distinguishes this oracle guarantee from what gradient descent is known to learn.

9 LIMITATIONS AND CONCLUSION

  • The expressivity theorem supplies oracle parameters but does not show that gradient descent finds them or a useful neighborhood.The paper explicitly treats expressivity as necessary but not sufficient for learnability.Source: §9 · p. 7
  • On synthetic Horn programs, gradient descent can reach parameters far from the oracle while still attaining substantial OOD accuracy.Body-alignment metrics remain at most 2 even where the oracle has alignment k.Source: §9 · p. 8
  • The proposed homotopy strategy gradually increases τs and Ψ, but whether it reaches the oracle basin remains empirically open.The implicit distributed representation suggested by gradient descent is also an open theoretical question.Source: §9 · p. 8
  • The sink-leak analysis requires Ψ ≥ log R + c; the scalable construction instead sets Ψ = log M + 10.The conclusion describes the sink-leak threshold as a practical sensitivity concern.Source: §9 · p. 8
  • Zero-error oracle accuracy and a tight match between theoretical and empirical robustness thresholds are reported for programs up to 504 atoms.The conclusion also reports convergence in at most 32 iterations, far below the time bound.Source: §9 · p. 8

Supplementary Material: Differentiable Horn Programs

The supplementary proofs establish structural properties of LatentGamma by showing its updates are non-decreasing, bounded, convergent, and lattice-monotone. They also show the limit is the least fixed point above the initial state.

A.1 Proof of Lemma 5.1 (Pointwise non-decrease)

  • Each coordinate update is non-decreasing because its increment is a product of nonnegative factors.The proof uses (1 − si) gi(s) Γi(s) ≥ 0.Source: §A.1 · p. 9

A.2 Proof of Proposition 5.2 (Bounded iterated sequence)

  • The iterated sequence remains coordinate-wise non-decreasing and bounded above by 1.The upper bound follows from giΓi ≤ 1 in the residual update.Source: §A.2 · p. 9

A.3 Proof of Theorem 5.3 (Convergence)

  • The sequence converges coordinate-wise because it is non-decreasing and bounded, and continuity lets the limit pass through TΓ.The operator is continuous as a composition of sigmoid, softmax, addition, and multiplication operations.Source: §A.3 · p. 9

A.4 Proof of Proposition 5.4 (Lattice monotonicity)

  • Lattice monotonicity is proved by showing each stage of TΓ is monotone in the input state before composing the stages.The proof uses increasing sigmoids and nonnegative routing weights.Source: §A.4 · p. 9

A.5 Proof of Corollary 5.5 (Least fixed point)

  • The converged fixed point is below every fixed point that contains the initial state.The proof inducts using lattice monotonicity and then takes the limit.Source: §A.5 · p. 9

B COMPLETE PROOF OF LEMMA 6.3 (AND SEPARATION)

The AND-separation proof bounds the rule activation score for satisfied versus unsatisfied bodies under the oracle parameters. Its stated assumptions include a size-dependent constraint on M and k.

B COMPLETE PROOF OF LEMMA 6.3 (AND SEPARATION)

  • For a satisfied body, the activation score exceeds 0.993; for an unsatisfied body, it is below 0.007.These separation bounds are stated for every rule under the oracle parameters and the lemma's assumption.Source: B COMPLETE PROOF OF LEMMA 6.3 (AND… · p. 10
  • The lower bound for satisfied bodies follows from a margin of at least 1/4 under the stated condition on k and ε0.The proof gives the sharper margin 1/2 − 1/(4k), including a stronger bound for k = 1.Source: B COMPLETE PROOF OF LEMMA 6.3 (AND… · p. 10
  • The revised size condition is 4kMe^-10 ≤ 1, which the passage says covers all experimental graphs, including M = 504 and k = 2.The passage identifies this as the corrected assumption needed for the case-2 upper bound.Source: B COMPLETE PROOF OF LEMMA 6.3 (AND… · p. 10

C COMPLETE PROOF OF LEMMA 6.4 (AGGREGATION SEPARATION)

The supplementary proofs establish aggregation separation and a strong sink bound, derive robustness and parameter-count results, and report edge-case and multi-head validation. Together they extend and substantiate the paper's main construction.

C COMPLETE PROOF OF LEMMA 6.4 (AGGREGATION SEPARATION)

  • A firing rule makes the head logit positive despite contributions from other rules, while the no-firing case keeps it negative.The proof bounds aggregate contributions from other heads by 5 · 10^-9 and gives respective logit bounds of at least 0.732 and at most −0.74.Source: C COMPLETE PROOF OF LEMMA 6.4… · pp. 10–11

D LEMMA 6.5 (SINKS) WITH STRONG BOUND

  • For sink atoms, the oracle update product is at most 3.4 × 10^-25; over 10^20 iterations, the accumulated increment stays below 10^-4.This is the strong sink bound used to control sink accumulation.Source: D LEMMA 6.5 (SINKS) WITH STRONG BOUND · p. 11

E.1 Body-logit perturbations

  • Under the body-logit perturbation conditions, the AND-separation argument and Theorem 6.1's conclusion continue to hold.The proof uses a union-bound event controlling sign flips and bounds the perturbed body-gate error.Source: §E.1 · p. 11

E.2 Head-logit perturbations

  • With head-logit perturbations, the true head remains the softmax argmax outside the stated misrouting event, preserving a contribution of at least γ+/2 under the separation condition.The passage states this for the specified perturbation assumptions.Source: §E.2 · p. 12

E.3 Numerical scaling for the head bound

  • At σψ = 2, the head-routing tail probability is about 7.7 × 10^-13; at σψ = 4, it is about 2.0 × 10^-4.The passage characterizes head routing as more resilient than body matching, consistent with Ψ = 20 versus η = 10.Source: §E.3 · p. 12

F COMPLETE PROOF OF THEOREM 8.1 (LOWER BOUND)

  • The parameter-count lower bound is Ω(Rk log M) bits, and the passage states that LatentGamma achieves it up to logarithmic factors.The counting proof bounds the number of closure-equivalence classes of Horn programs.Source: F COMPLETE PROOF OF THEOREM 8.1 (LOWER… · p. 12

G EDGE CASES (PHASE E)

  • Across G1–G4, all 33 edge cases achieve Jaccard = 1, including tests of extremal initial sets.The caption says E2 and E3 validate Theorem 6.1 on those extremal sets.Source: Table 4 · p. 12

H DISJUNCTIVE EXTENSION

  • The construction extends to conjunctively interpreted multi-head rules, and the supplement reports a 100% all-heads-active rate on about 30 tested rules.The per-head softmax mass is 1/m, with the aggregation condition unchanged.Source: H DISJUNCTIVE EXTENSION · p. 13
Loading 2609.06235v1…