arXiv CSopen access

NeSyCat Torch: A Differentiable Tensor Implementation of Categorical Semantics for Neurosymbolic Learning

Preprint 1–13, 2026

NeSyCat Torch: A Differentiable Tensor Implementation of Categorical Semantics for Neurosymbolic Learning Daniel Romero Schellhorn Till Mossakowski Björn Gehrke

[email protected] [email protected] [email protected]

arXiv:2606.19279v1 [cs.AI] 17 Jun 2026

University of Osnabrück, Osnabrück, Germany

Abstract Neurosymbolic semantics is fragmented: classical, fuzzy, probabilistic and neural systems each define truth by their own inductive rules. NeSyCat, extending ULLER, subsumes them under a single inductive definition of truth, parametric in a strong monad and an aggregation structure on truth-values. NeSyCat has so far lacked an account of predicates and functions learned by neural networks. We provide NeSyCat Torch as the missing link and interpret computational symbols via neural networks, implementing the framework in probabilistic programming and tensor-based backends. We use the distribution monad for reference semantics and metric evaluation, and complement it by a monad for numerically stable, differentiable training: the lazy log-tensor monad over the log-semiring. For efficient training in batches, we furthermore employ a batch monad. The axioms are the source code: written once in monad-based do-notation, monadic bind performs marginalisation, lazily pruning unneeded branches. On MNIST addition, our HaskTorch, JAX, and PyTorch implementations outperform LTN and DeepProbLog in speed and accuracy, while achieving nearly the accuracy of DeepStochLog. However, unlike DeepStochLog, we stay in a uniform framework that applies to many first-order NeSy approaches. Namely, the construction is parametric in the monad; instantiating it with, e.g., the Giry monad extends the approach to continuous probability (working out a neural representation here is left for future work).

1. Introduction Neurosymbolic (NeSy) AI combines the perceptual strength of neural networks with the structured, verifiable reasoning of symbolic logic. A recurring obstacle is fragmentation: classical, fuzzy, and probabilistic NeSy systems each come with their own logical language and semantics, so knowledge bases and learning objectives rarely transfer between them. ULLER - the Unified Language for Learning and Reasoning (Van Krieken et al., 2024) - endows First-Order-Logic (FOL) syntax with three pairwise-independent semantics - classical, fuzzy, probabilistic - each carrying its own inductive definition of truth. A recent line of work (Schellhorn and Mossakowski, 2026) reformulates all three semantics as instances of a single categorical framework built on monads, Moggi’s construct for computational effects in functional programming (Moggi, 1991). The key observation is that an ULLER computation formula x := m(T1 , . . . , Tn ) (F ), interpreted as “run model m, then bind its result to x, then evaluate F ”, is exactly monadic do-notation. Fixing a strong monad M (the effect) and an aggregated truth-value space Ω with connectives and quantifiers yields a NeSy framework ; classical, fuzzy, probabilistic, LTN, and possibilistic semantics all reappear as choices of M and Ω, evaluated by one inductive definition of truth. © 2026 D. Romero Schellhorn, T. Mossakowski & B. Gehrke.

Romero Schellhorn Mossakowski Gehrke

Monad

Code

Effect

Description

D

Dist

finite probability

T

Tens

logit weights

Tlog

LogTens

stable arithmetic

B

Batch

batching

Finitely supported probability distributions; the reference semantics and metric readout. Finite-support Tensor monad T m = Rm (leaves are weight tensors) and (>>=) is the linear pushforward. Tens in logarithmic coordinates, over the log-semiring (R, logsumexp, +): numerically stable and differentiable, the monad used in training. Reader monad on the batch index object B (Sec. 5), parallel processing of a mini-batch in training.

Table 1: Monads in NeSyCat Torch, in the format of Kohl and Schwaiger (2021, Table 1).

For efficiency reasons, we use lazy monads. The lifting operation in the distribution monad computes probabilities using marginalization; a lazy monad ensures that marginalization is only done in cases where it is actually needed. Besides usual FOL function and predicate symbols, we consider computational function symbols X → MY and computational predicate symbols X → MΩ. At the deep learning level, we need also to consider two-sided computational function symbols MX → MY and two-sided computational predicate symbols MX → MΩ. We now recall monads and present the monads used in this paper in Table 1:

2. Monads for Computational Effects Definition 1 (Monad (Kohl and Schwaiger, 2021, §3.1)) A monad is given by a triple (m, return, >>=) where m is a type constructor mapping a type a to a type m a of computational effects with values from a, return embeds values into computation and >>= (bind) is used for composition of computations: return :: a -> m a (>>=) :: m a -> (a -> m b) -> m b

Here, c >>= f first executes computation c over type a and passes its value(s) to a function f delivering a computation over type b. A monad needs to satisfy associativity and unit laws. Haskell provides the do notation as syntactic sugar for composing monadic maps: with it monadic code almost looks like imperative code, but under the hood there are only pure maps and monads: do { x <- y; f} is syntactic sugar for y >>= (\x-> do { f }). Three monad layers.

In this work, we will use three different monads:

1. the probability layer : the distribution monad D (Schellhorn and Mossakowski, 2026) is the reference semantics. MX is the space of all finitely supported probability distributions P over X. return x is the distribution assigning all probability mass to x. f >>= ρ = x∈X f (x)(y) · ρ(x). This corresponds to a two-level random process: first x is drawn from ρ, then y is drawn from f (x). This results in a marginal distribution for the joint distribution ρ̂(x, y) := f (x)(y) · ρ(x). Distributions over Booleans can be regarded as single probabilities (namely those for true). 2

NeSyCat Torch

2. the tensor layer : the tensor monad T works with the same equations. It implements the distribution monad in a differentiable way, but uses real numbers (logits) instead of probabilities. It is connected to D by a bridge (see Sect. 4 below). The implementation uses LogTens, i.e. T in logarithmic coordinates (over the log-semiring) for stable differentiation. 3. the batching layer : the batch monad B, defined in Sect. 5 below, allows the parallel processing of training samples, evaluated together in one run. It carries no probability and no geometry, and, dually to the first layer, it never uses the samples’ randomness.

3. Syntax and Semantics Using these monads, we extend the categorical semantics of Johnstone (2002, D1.1.) by adding monad symbols and monadic interpretations. Refining (Schellhorn and Mossakowski, 2026), NeSyCat Torch organises syntax and semantics into four layers, each a pair of a signature (only symbols) and an interpretation (their meaning): categorical, logical, domain, and grammatical. The first three declare and interpret symbols; the fourth generates terms and formulas over them and assigns them their monadic semantics by one induction. 3.1. Categorical, logical and domain layers (i) Categorically, we work in the category of sets and maps, Set; computationally it is the category of (inhabited) Haskell types and maps, on which every Haskell monad of Section 2 is defined. Parameters are drawn from the category Tensor of tensor spaces, which has as objects the Euclidean spaces Rn and as morphisms differentiable maps. Implementation-wise, these are implemented as HaskTorch/PyTorch/JAX tensors, where the neural networks live and backpropagation is performed (Fong et al., 2019). The one choice that genuinely varies is the effect: we keep a single monad symbol ⃝, which allows for the choice of a monad M := I(⃝) from Table 1. This paper uses two readings: probabilistic (M := Dist), and tensorial (M := T ). (ii) Logically, the basic truth values are Booleans, Ω := B = {False, True}. The connective symbols Conn (e.g. ∧, ∨, ¬, →) are the ordinary Boolean operations (Johnstone, 2002, D1.1) given by I(∗) : Bari(∗) → B. In the neural setting, though, a predicate does not return a plain Boolean but a monadic truth value in M Ω, for example a distribution over B, or a vector of logit weights. Hence we lift each connective to act on M Ω: bind its arguments, apply the Boolean operation to the plain truth-values and then return the result (connective clause of Def. 4). The only logical symbols whose interpretation is genuinely monadic are the quantifier symbols Quan: a quantifier Q takes its body (a map into monadic truth) and aggregates it to a monadic truth value, indexed by a finite (infinitary are future work) object D: I(Q)D : (D → M Ω) −→ M Ω, Definition 2 (Domain signature Σ) A domain signature consists of domain symbols Dom, variable symbols Var (each over a domain symbol, x : S), and function symbols Fun and relation symbols Rel, each partitioned into Fun = FunTarski ⊔ FunKleisli ⊔ FunNesy and Rel = RelTarski ⊔ RelKleisli ⊔ RelNesy : 3

Romero Schellhorn Mossakowski Gehrke

Kind

Function symbol

Relation symbol

Implementation

Tarski Kleisli Nesy

f : S 1 , . . . , Sn → T f : S1 , . . . , Sn → ⃝T f : ⃝S1 , . . . , ⃝Sn → ⃝T

R : S1 , . . . , Sn → τ R : S1 , . . . , Sn → ⃝τ R : ⃝S1 , . . . , ⃝Sn → ⃝τ

deterministic effectful neural

Here, τ is the type of truth values. In order to stay close to FOL, we disallow function and relation symbols taking arguments of type τ or ⃝τ . Definition 3 (Domain interpretation I) A domain interpretation assigns a set I(S) to each domain symbol S, and to each function symbol f a map I(f ) as in Signature

Interpretation

f : S1 , . . . , S n → T

I(f ) : I(S1 , . . . , Sn ) → I(T )

f : S1 , . . . , Sn → ⃝T

I(f ) : I(S1 , . . . , Sn ) → M I(T )

f : ⃝S1 , . . . , ⃝Sn → ⃝T

I(f ) : M I(S1 ) × · · · × M I(Sn ) → M I(T )

where M := I(⃝) and I(S1 , . . . , Sn ) := I(S1 ) × · · · × I(Sn ). Relations similarly, with I(T ) replaced by Ω. A Tarski symbol is a plain map, a Kleisli symbol a map into M I(T ), and a Nesy symbol takes monadic carriers as input and produces monadic carriers as output. 3.2. Grammar We write terms t in the do-notation of Section 2, the same notation the implementation uses. To avoid duplication of do-notation for terms and formulas, we construe formulas ϕ as terms of type τ and connectives as operations on τ .1 Tarski terms are terms of type S or formulas of type τ . Monadic terms are terms of type ⃝S or ⃝τ (the latter are monadic formulas); such terms can be used as terms t1 , . . . , tn , t in the do -notation. In order to stay close to FOL, the term t in return t must have a Tarskian, i.e. ⃝-free type. With x ∈ Var, c, f ∈ Fun ∪ Rel ∪ Conn, Q ∈ Quan, we define terms as follows: t ::= x | c | f (t1 , . . . , tn )

(standard FOL term/formula)

| return t | do { x1 ← t1 ; . . . ; xn ← tn ; t } (monadic term/formula) | Qx(t)

(quantifier, t, Qx(t) : ⃝τ )

Each term t has free variables in(t) and (result) type out(t). Term formation has to be type-correct. Formulas ϕ are terms with out ϕ = τ . Standard FOL terms can have type S (or τ ) or ⃝S (or ⃝τ ), depending on whether f has a monadic result. Monadic terms are always of type ⃝S (or ⃝τ ). do-notation has to be used for the application of connectives to monadic formulas. We can recover the original ULLER and NeSyCat syntax for terms Ti , formula F with variable x, and a neural model m in NeSyCat Torch as follows: [x := m(T1 , . . . , Tn )]F

≡

do { x ← m(T1 , . . . , Tn ); F }

1. This is standard in higher-order logic (Church, 1940; Andrews, 1986), and with suitable restrictions, it can be used also for first-order logic.

4

NeSyCat Torch

We define the semantics pointwise at a valuation ν: for the context [x1 :S1 , . . . , xk :Sk ], ν maps variables to values and can be construed as a tuple in I(S1 ) × · · · × I(Sk ), one component per variable. The following semantics uses the do-notation of Section 2. Subterm values are always monadic and therefore always bound with ←. A Tarski symbol is pure, so its result reenters the monad through return; a Kleisli symbol is already monadic, so it stands as the final do-expression without return; a Nesy symbol takes the monadic values themselves, so no binds occur at all. A quantifier likewise consumes its body as the map a 7→ JϕK(c, a) directly, matching its interpretation type from Section 3.1. Definition 4 (Semantics J·K) Terms and formulas denote maps JtK : I(in(t)) → I(out(t)), defined by induction on the grammar with t := (t1 , . . . , tn ): JxK(ν) = ν(x) JcK(ν) = I(c)

Jf (t)K(ν) = I(f ) Jt1 K(ν), . . . , Jtn K(ν)

Jreturn tK(ν) = return JtK(ν)

Jdo { x1 ← t1 ; . . . ; xn ← tn ; t }K(ν) = do { a1 ← Jt1 K(ν); . . . ; an ← Jtn K(ν); JtK(ν, x1 7→ a1 , . . . xn 7→ an ) }
JQx(t)K(ν) = I(Q)I(S) λa. JtK(ν, x 7→ a) (x : S)

The order of independent binds in these clauses is irrelevant: all monads in this paper are commutative (Kock, 1970) (Dist: the independent joint distribution; T : the outer product), so commutative connectives stay commutative under the monadic reading. Section 4 unfolds these clauses step by step on the running example:

4. The Running Example: MNIST Addition We instantiate the MNIST single-digit addition under distant supervision: only the sum of two handwritten
digits is observed, never the digits. The axiom is ∀(x, y, n):S n = digit(x) + digit(y) . The domain signature Σ has sorts Image, Digit, Nat, one Kleisli symbol digit : Image → M Digit, and two Tarski symbols + : Digit2 → Nat, = : Nat2 → τ . Writing digθ := Iθ (digit), the clauses of Section 3.2 are given as: do



d1 ← digθ (x); d2 ← digθ (y); return n = (d1 + d2 ) .

Each ← performs the law of total probability in D and the log-space convolution in T respectively, so this program is not pseudo-code: it is the semantic value, the monad laws guarantee it equals the literal inductive unfolding, and the identical text compiles as Haskell. What “+” becomes. The Tarski symbol + is ordinary addition sum : n × m → n+m−1 in the base, where k = {0, . . . , k − 1}; the monad enters only by lifting it: the functor sends this map to T (sum) : T (n × m) → T (n+m−1). Over R the carrier is the finitely 5

Romero Schellhorn Mossakowski Gehrke

supported tensor monad T m = Rm (unit ηm (i) = ei ), a lawful Haskell Monad.2 This lift is the pushforward, which on sum marginalises a joint vector onto the sum. The two classifiers return a pair, joined by the outer product a ⊗ b, yielding exactly the discrete convolution: P T (sum)(a ⊗ b)(s) = i+k=s ai bk = (a ∗ b)(s), s ∈ {0, . . . , 18}, i.e. the unnormalized distribution of the sum of two independent digits, exactly what the axiom scores against (the DeepProbLog reading (Manhaeve et al., 2021)). The first two monad layers. The digit symbol is two-sided, digθ : ⃝ Image → ⃝Digit: an observed image enters as a certain one-hot encoded tensor. Why encode a tensor that is already a tensor? Because the input lives in ⃝Image, a distribution over images, and a single observation is just the certain case: the point mass at that image (one-hot in T , a delta distribution in D), exactly how one datum is represented in an empirical data distribution as empirical state. The encoding sends a delta distribution on an element to the one-hot encoding on the same element. The decoding sends logit tensors via a softmax to a T distribution. The probability reading is defined as the composition digD θ = dec ◦ digθ ◦ enc: T (Image)

digT θ (CNN)

enc

D(Image)

T (Digit) dec=softmax

D(Digit)

digD θ

The do-notation derivation above is no paraphrase: it is the actual Haskell, written once and polymorphic over the monad m. The sorts are plain types, + and == are host functions, and digit is the only monad-dependent symbol and the bind supplies the marginalisation. In Python, we use yield instead of <- utilising the generator syntax as syntactic sugar for the same monadic composition as Haskell’s do-notation. class MNistAddition(Example, DistLogTensBridge): def formula(self, m, x: Monad[Image], y: Monad[Image], n: Monad[int]) -> Formula[bool]: d1 = yield self.digit(m, x) d2 = yield self.digit(m, y) s = yield n return s == d1 + d2

Here, apart from the bind s = yield n, which relates only to batching and is explained in Section 5, the formula corresponds to the abstract formula in Section 3.2. The arithmetic is interpreted identically in both monads - plain integer addition - and the only per-monad choice is how digit is read: in LogTens the CNN’s raw logits become a leaf; in Dist that same leaf is decoded to a distribution: class MNistAddition(Example, DistLogTensBridge): @monad_method def digit(self, img: Monad[Image]) -> Monad[int]: ... @digit.instance(LogTens)

2. The finite-dimensional vector-space construction is, strictly, a relative monad on Fin ,→ Set rather than an endofunctor (Altenkirch et al., 2015): its bind sums only over finite index set. The finitely supported version is an ordinary monad.

6

NeSyCat Torch

def digit_logtens(self, img: LogTens[Image]) -> LogTens[int]: model = self.tensor_interpretation.models[type(self).digit] return LogTens.bind(img, lambda x: LogDefer(list(range(10)), x, model)) @digit.instance(Dist) def digit_dist(self, img: Dist[Image]) -> Dist[int]: return self.decode(self.digit(LogTens, self.enc_dist(img)))

The LogTens monad represents the type constructor Tens a = [a -> Real] realized over the logsemiring (R, logsumexp, +) with finite support given by a list [a] of elements of type a: class LogTens[A](Monad[A]): ...

class Pure[A](LogTens[A]): value: A

class Bind[A, B](LogTens[A]): dist: LogTens[B] func: Callable[[B], LogTens[A]]

class LogLeaf[A](LogTens[A]): support: list[A] log_weights: torch.Tensor

LogTens is used for training since log space is computationally convenient: products of prob-

abilities become sums and marginalisation becomes log-sum-exp, the numerically stable evaluation (Blanchard et al., 2021); weights range over all of R instead of being squashed into [0, 1], where differentiable fuzzy operators degenerate gradient-wise (van Krieken et al., 2022); and, since softmax is shift-invariant (softmax(z) = softmax(z + c 1)), normalising early would discard the shift, so it is deferred - score now, normalise once at the boundary.

5. Training with Monads Training minimises the knowledge loss, the mean negative log-truth of axioms over data, b L(θ) = N1

N X

− log φθ (si ),

i=1

where φθ (s) is the truth value the axiom’s semantics assigns to sample s under weights θ (empirical risk minimisation; equivalently, maximum likelihood on the logical evidence). This section answers the computational question: why one batched evaluation of the axiom b and in particular why an observation may be bound in the do-notation. computes L, b runs the do-notation program N times, once per sample. The obvious way to compute L The implementation instead runs it on a whole batch of samples at once, on tensors carrying a batch axis. b lives entirely in the first monad - it exists because the data The finite-sample average L is a finite sample of the world, not because of batching. The per-sample formula is written once, polymorphic over the first two monad layers (in D for evaluation, in T for training). The batching layer is different: it is never a reading of the formula but is applied outermost, the training monad is the composite B ◦ T . Definition 5 (Batch monad) Let B = {1, . . . , B} index the samples evaluated together in one run, a mini-batch of the observations, with B = N for the full sample. The batch monad3 is the B-fold power, i.e. the reader monad on B:
B X = XB ∼ ηB (x) = const x, (m >>= f )(b) = f m(b) (b). = (B → X), 3. The same repeated, conditionally independent structure is called a plate in graphical models (Buntine, 1994); cf. pyro.plate (Bingham et al., 2019) and plated factor graphs (Obermeyer et al., 2019).

7

Romero Schellhorn Mossakowski Gehrke

Its bind is the diagonal: the continuation of index b sees only index b’s value. In order to combine the batch monad with other monads, we need to extend it to a monad transformer. Monad transformers transform a given monad to a new one by adding extra structure; in this case, by adding a batch dimension. Proposition 6 (Batch transformer) For every strong monad M the composite
BM X = B → M X is again a monad (the reader monad transformer at B applied to M), and there are two canonical monad morphisms into it: liftM : M X → BM X, liftM = const

and

liftB : B X → BM X, liftB m = ηM ◦ m.

liftM embeds a batch-constant effect; liftB embeds a batched but certain value. A single run in the resulting composite provably yields all per-sample values of its batch at once (Proposition 7). An observation is a value of the pure batch monad, batched but certain, m : B → X, and enters a formula only through liftB = ηM ◦(−). In the do-notation this is the bind s ← m: the bound s is per-sample data carrying no uncertainty. The training semantics of this paper is the composite B ◦ T : a leaf with log-weight tensor of shape [B, k] is the carrier of B → T X under the rectangularity invariant - all B component measures of the batch share one support of size k. Under this representation liftB is the one-hot embedding: an observed value becomes the [B, k] one-hot log-weight leaf, the log-space image of ηM (the numerical floor at ϵ stands in for log 0 = −∞).

6. Inference and Evaluation b a The inferential level turns the formula into an optimisation problem: the knowledge loss L, data loss Ldata , and their convex combination. MNIST addition is pure distant supervision: b Adam minimises only the knowledge loss L(θ). We run the same specification in two backends, Haskell (HaskTorch) and Python (JAX). In Python JAX the log-space convolution is JIT-compiled and differentiated. All numbers below come from the JAX backend on a single A100 GPU, averaged over 15 seeds. We never use digit labels: the network learns to read the digits (about 97% digit accuracy) from the observed sums alone. Table 3 puts NeSyCat Torch next to LTN (Badreddine et al., 2022), DeepProbLog (Manhaeve et al., 2021), and for two digits, logLTN (Badreddine et al., 2023), NeuPSL and DeepStochLog. For the single-digit case we give each NeSyCat Torch variant the same CNN, batch size and number of epochs as the baseline it is compared to. NeSyCat Torch is ahead in both matchups: 94.6 vs LTN’s 93.5, and 94.2 vs DeepProbLog’s 92.2. The real gap is a little larger, because LTN reports only its 10 best of 15 runs (about one in five gets stuck early on), while we average all 15. Although this issue has been solved by working in log space (Badreddine et al., 2023), we outperform even logLTN in both accuracy and speed. In general, speed is not even an issue: at batch 32 our step times (Table 2) are well under the 5.36/3.44 ms LTN reports on an older V100 GPU. 8

NeSyCat Torch

Table 2: Single-digit MNIST addition: NeSyCat Torch’s two variants, 3000 training pairs. The DPL-style sweep is longer only because its harness uses batch 2 (∼10× more steps) - the network is not slower, its per-step cost is even a little lower. Metric

LTN-style (100n. head, ELU)

DPL-style (120n. head, ReLU)

94.6 ± 0.6 % ≈ 100.0 % 0.52 / 0.20 ms ≈ 1.5 min 32 batches, 20 epochs

94.2 ± 0.7 % ≈ 100.0 % 0.44 / 0.20 ms ≈ 5.6 min 2 batches, to convergence.

Sum accuracy (test) Sum accuracy (train) Train / test step (batch 32) Wall-clock, 15-seed sweep Training harness

Table 3: Test sum accuracy (%), mean ± std, on MNISTAdd for N digits. NeSyCat Torch averages 15 seeds; LTN averages its 10 best of 15. 1 from (Badreddine et al., 2023), 2 from (van Krieken et al., 2023), “T/O”: timeout; “-”: not reported N =1 Method

Trainings:

NeSyCat Torch (LTN-style) NeSyCat Torch (DPL-style) LTN logLTN DeepProbLog DeepStochLog A-NeSI Reference (0.992N )

N =2

N =4

3k

1.5k

15k

7.5k

94.6 ± 0.6 94.2 ± 0.7 93.5 ± 0.3 1 92.2 ± 1.6 1 -

89.7 ± 0.7 89.2 ± 0.7 88.4 ± 1.0 1 88.3 ± 0.8 1 87.2 ± 1.9 1 -

95.7 ± 0.5 95.8 ± 0.6 95.4 ± 0.3 1 95.6 ± 0.5 1 95.2 ± 1.7 2 96.4 ± 0.1 2 96.0 ± 0.4 2

92.0 ± 0.6 91.8 ± 0.8 T/O 2 T/O 2 92.7 ± 0.6 2 92.6 ± 0.8 2

98.01 2

96.06 2

96.06 2

92.27 2

Longer numbers. The N =4 column uses two four-digit numbers (sums up to 19,998). How high any method can score here is set by the digit classifier: if it is 99% accurate, getting all 2N digits right caps the sum accuracy at 0.992N (the Reference row). NeSyCat Torch, DeepProbLog and (in the non-recursive and mass-conserving case) also DeepStochLog optimise the same marginal likelihood, so they end up near that cap. NeSyCat Torch still runs at N =4 (92.0%, just below the cap) where DeepProbLog and LTN time out, with DeepStochLog and A-NeSI a little ahead.

7. Related Work ULLER (Van Krieken et al., 2024) leaves the semantics split into duplicated inductive definitions. The categorical framework of Schellhorn and Mossakowski (2026) instead derives one definition parametric in a monad. But they do not implement neural learning, which we do here with NeSyCat Torch. LTN (Badreddine et al., 2022) uses fuzzy semantics and thereby avoid probabilistic semantics and hence do not derive any distributions. Further, logLTN (Badreddine et al., 2023) moves LTN’s operators to log space by composing log with softmax, whereas here log space is the native carrier and the softmax is confined to the decode bridge. 9

Romero Schellhorn Mossakowski Gehrke

DeepProbLog (Manhaeve et al., 2021) trains on the same exact likelihood we do, but compiles the program to a Sentential Decision Diagram and scores it by weighted model counting; van Krieken et al. (2023) show this counting is #P-hard, so it times out at N =4 (Table 3). DeepStochLog (Winters et al., 2022) is the most accurate baseline, marginally ahead of both A-NeSI and NeSyCat Torch. It avoids DeepProbLog’s blow-up by writing the sum as a stochastic grammar (a random walk rather than a random graph) which is cheaper but can lose mass on failing derivations. However, DeepStochLog changes the aggregation structure to grammar-derivation probability, while our approach keeps the distribution marginal known from DeepProbLog, yet achieves scalability via laziness and tensor structure. DeepStochLog’s grammar-based approach corresponds to formulas dynamically adapted to the input (e.g. input length); we can achieve this by using NeSyCat Torch formulas inside Python or Haskell programs (that e.g. adapt the number of do binds to the number of input digits). A-NeSI (van Krieken et al., 2023) scales instead by training a network to approximate the counting, which gives up exactness and requires additional factorization preparations, which are example specific and therefore not generalizable. NeSyCat Torch needs none of this: the same marginalisation is just the monadic bind and by changing the monad the one framework also gives the classical and fuzzy semantics, more aligned with standard firstorder logic. The differentiable reading connects to the logic of differentiable logics (Ślusarz et al., 2023) and to categorical deep learning (Gavranović et al., 2024; Fong et al., 2019), with broader motivation in the survey of Smet et al. (2023).

8. Conclusion NeSyCat is a general unifying neurosymbolic framework for reasoning and learning in firstorder logic that is parameterized over a computational monad. Monads in NeSyCat have covered different theoretical frameworks, such as discrete and continuous probabilities and nondeterminism. With NeSyCat Torch, we provide the first neural implementation of this general framework, i.e. using neural networks as realisations of computational function and predicate symbols. We concentrate on finitely supported distributions here. We provide implementation at Haskell: https://anonymous.4open.science/r/nesycattorch-hs/, Python JAX: https://anonymous.4open.science/r/nesycattorch-jax/, and Python PyTorch: https://anonymous.4open.science/r/nesycattorch-py/. It turns out that for these implementations, we need the finitely supported distribution monad plus two other monads: for (log-scale) tensors and for training batches. NeSyCat Torch thus scales the generality of NeSyCat to the neural implementation level, while simultaneously obtaining competitive results, in terms of accuracy and training time, for the classical MNIST digit addition example. Our approach also scales to multi-digit addition. This is achieved by using lazy monads that defer evaluation of marginalized probabilities to cases where really needed. Future work will study how well this generalises to more complex examples. The generalization of our implementation to other monads like continuous probability and to infinite domains is left to future work as well. Note that an efficient neural representation of continuous probability is non-trivial. 10

NeSyCat Torch

References Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. Logical Methods in Computer Science, 11(1):1–40, 2015. doi: 10.2168/LMCS-11(1: 3)2015. Conference version in FoSSaCS 2010, LNCS 6014, pp. 297–311. P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic press, 1986. Samy Badreddine, Artur S. d’Avila Garcez, Luciano Serafini, and Michael Spranger. Logic tensor networks. Artif. Intell., 303:103649, 2022. doi: 10.1016/J.ARTINT.2021.103649. URL https://doi.org/10.1016/j.artint.2021.103649. Samy Badreddine, Luciano Serafini, and Michael Spranger. logLTN: Differentiable Fuzzy Logic in the Logarithm Space. arXiv:2306.14546, June 2023. Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul Szerlip, Paul Horsfall, and Noah D. Goodman. Pyro: Deep universal probabilistic programming. Journal of Machine Learning Research, 20(28):1–6, 2019. Pierre Blanchard, Desmond J. Higham, and Nicholas J. Higham. Accurately computing the log-sum-exp and softmax functions. IMA Journal of Numerical Analysis, 41(4):2311– 2330, 2021. doi: 10.1093/imanum/draa038. Wray L. Buntine. Operations for learning with graphical models. Journal of Artificial Intelligence Research, 2:159–225, 1994. doi: 10.1613/jair.62. Alonzo Church. A formulation of the simple theory of types. The journal of symbolic logic, 5(2):56–68, 1940. Brendan Fong, David I. Spivak, and Rémy Tuyéras. Backprop as functor: A compositional perspective on supervised learning. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13. IEEE, 2019. doi: 10.1109/LICS.2019.8785665. Bruno Gavranović, Paul Lessard, Andrew Dudzik, Tamara von Glehn, João G. M. Araújo, and Petar Veličković. Position: Categorical Deep Learning is an Algebraic Theory of All Architectures. arXiv:2402.15332, June 2024. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium. Oxford University Press, Oxford, September 2002. ISBN 978-0-19-851598-2. doi: 10.1093/oso/ 9780198515982.001.0001. Anders Kock. Monads on symmetric monoidal closed categories. Archiv der Mathematik, 21:1–10, 1970. doi: 10.1007/BF01220868. Christina Kohl and Christina Schwaiger. Monads in computer science, 2021. Seminar report, winter term 2021. 11

Romero Schellhorn Mossakowski Gehrke

Robin Manhaeve, Sebastijan Dumancic, Angelika Kimmig, Thomas Demeester, and Luc De Raedt. Neural probabilistic logic programming in DeepProbLog. Artif. Intell., 298: 103504, 2021. doi: 10.1016/J.ARTINT.2021.103504. URL https://doi.org/10.1016/ j.artint.2021.103504. Eugenio Moggi. Notions of computation and monads. Information and Computation, 93 (1):55–92, July 1991. doi: 10.1016/0890-5401(91)90052-4. Fritz Obermeyer, Eli Bingham, Martin Jankowiak, Justin Chiu, Neeraj Pradhan, Alexander M. Rush, and Noah D. Goodman. Tensor variable elimination for plated factor graphs. In Proceedings of the 36th International Conference on Machine Learning (ICML), volume 97 of Proceedings of Machine Learning Research, pages 4871–4880, 2019. Daniel Romero Schellhorn and Till Mossakowski. NeSyCat: A monad-based categorical semantics of the neurosymbolic ULLER framework. arXiv:2604.24612, 2026. URL https: //arxiv.org/abs/2604.24612. Natalia Ślusarz, Ekaterina Komendantskaya, Matthew L. Daggitt, Robert Stewart, and Kathrin Stark. Logic of Differentiable Logics: Towards a Uniform Semantics of DL. arXiv:2303.10650, October 2023. Lennert De Smet, Pedro Zuidberg Dos Martires, Robin Manhaeve, Giuseppe Marra, Angelika Kimmig, and Luc De Raedt. Neural Probabilistic Logic Programming in DiscreteContinuous Domains. arXiv:2303.04660, March 2023. Emile van Krieken, Erman Acar, and Frank van Harmelen. Analyzing Differentiable Fuzzy Logic Operators. Artificial Intelligence, 302:103602, January 2022. doi: 10.1016/j.artint. 2021.103602. Emile van Krieken, Thiviyan Thanapalasingam, Jakub M. Tomczak, Frank van Harmelen, and Annette ten Teije. A-NeSI: A scalable approximate method for probabilistic neurosymbolic inference. In Advances in Neural Information Processing Systems (NeurIPS), 2023. Emile Van Krieken, Samy Badreddine, Robin Manhaeve, and Eleonora Giunchiglia. ULLER: A Unified Language for Learning and Reasoning. In Tarek R. Besold, Artur d’Avila Garcez, Ernesto Jimenez-Ruiz, Roberto Confalonieri, Pranava Madhyastha, and Benedikt Wagner, editors, Neural-Symbolic Learning and Reasoning, volume 14979, pages 219–239. Springer Nature Switzerland, Cham, 2024. doi: 10.1007/978-3-031-71167-1 12. Thomas Winters, Giuseppe Marra, Robin Manhaeve, and Luc De Raedt. DeepStochLog: Neural stochastic logic programming. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2022.

12

NeSyCat Torch

Appendix A. Categorical Background Monads. Categorically, a monad on a category C is a functor T : C → C with natural transformations η : idC ⇒ T (unit) and µ : T T ⇒ T (multiplication) satisfying µ ◦ ηT = id = µ ◦ T η and µ ◦ T µ = µ ◦ µT . The programming definition above corresponds one-to-one to the equivalent presentation as a Kleisli triple (T, η, (·)M ), where f M : T A → T B for M = id M ◦ η M = f , and g M ◦ f M = (g M ◦ f )M : return is f : A → T B satisfies ηA T A, f A M η, (>>=) is the Kleisli lift (·) (applied flipped), and the do-notation of Section 2. is its syntactic sugar. States. We work over a concrete Cartesian category C: objects are sets equipped with structure (for example measurable spaces, tensor spaces or also plain sets), morphisms are structure-preserving maps, finite products exist, and the terminal object 1 is the one-element set. Effectful maps are always written explicitly as maps f : S → M T of the chosen strong monad M. Because C is concrete and Cartesian, a state on S, formally a Kleisli point 1 → M S, is the same thing as an element of M S; we use this identification throughout and simply write D ∈ M S. Proposition 7 (Pointwise evaluation) For each i ∈ B, evaluation evi : BM X → M X, m 7→ m(i), is a monad morphism, and therefore commutes with the interpretation of donotation programs: for a batch s : B → S, JφKBM (s)(i) = JφKM (si )

(i ∈ B).

One batched run thus yields all per-sample truth values; over the full sample these are the b averages, a mini-batch gives an unbiased estimate of L. b N numbers L

13