NeSyCat

A monad-based categorical framework that unifies neurosymbolic reasoning.

Classical, fuzzy, probabilistic and neural systems each define truth their own way. NeSyCat recasts them as one categorical framework: fix a monad and a space of truth values, and every one of those logics follows from a single inductive definition of truth. NeSyCat Torch is its differentiable, neural implementation.

Read the paper ↓ GitHub

§ The idea

The axioms are the source code.

Neurosymbolic AI joins neural perception with symbolic reasoning, but the field is fragmented: classical, fuzzy and probabilistic systems each carry their own logic and semantics, so knowledge bases and learning objectives rarely transfer. ULLER unifies the syntax — one first-order language — yet still ships three separate, hand-written definitions of truth.

NeSyCat collapses them into one. It recasts classical, fuzzy and probabilistic semantics as instances of a single categorical framework built on monads, Moggi's construct for computational effects. A semantics is then fixed by just two choices: a strong monad $\mathcal{M}$ — the computational effect — and a space of truth-values $\Omega$ carrying the connectives and quantifiers.

What NeSyCat lacked was neural learning. NeSyCat Torch supplies it: predicates and functions become neural networks, interpreted as computational symbols — a function symbol $f : X \to \mathcal{M}\,Y$ and a predicate symbol $R : X \to \mathcal{M}\,\Omega$ , with two-sided tensor forms $\mathcal{M}X \to \mathcal{M}Y$ at the deep-learning level.

And because the semantics is a single induction over monadic do-notation, the axiom you write is the program that runs: monadic bind performs the marginalisation, and the monads are lazy, so it only marginalises the branches it actually needs.

Fix the effect $\mathcal{M}$ and the truth-values $\Omega$ , and classical, fuzzy, probabilistic, LTN and possibilistic logics all fall out as special cases — evaluated by one inductive definition of truth.

§ Monads for computational effects

Three monad layers.

A monad is a triple (m, return, >>=): return embeds a value into a computation; >>= (bind) composes computations. The one choice that genuinely varies is the effect — the monad $\mathcal{M}$ . NeSyCat is parametric in that choice; NeSyCat Torch instantiates the framework with four monads, in three layers.

\mathcal{D}

Dist

finite probability

Finitely supported probability distributions; the reference semantics and metric readout.

\mathcal{T}

Tens

logit weights

Finite-support tensor monad $\mathcal{T}\,m = \mathbb{R}^m$ (leaves are weight tensors); bind is the linear pushforward.

\mathcal{T}_{\log}

LogTens

stable arithmetic

Tens in logarithmic coordinates, over the log-semiring $(\mathbb{R},\ \mathrm{logsumexp},\ +)$ : numerically stable and differentiable — the monad used in training.

\mathcal{B}

Batch

batching

Reader monad on the batch index $\underline{B}$ ; parallel processing of a mini-batch in training.

Probability layer

\mathcal{D}

the reference semantics.

Tensor layer

\mathcal{T} / \mathcal{T}_{\log}

differentiable; real logits instead of probabilities.

Batching layer

\mathcal{B}

parallel training samples; carries no probability and no geometry.

The training monad is the composite $\mathcal{B} \circ \mathcal{T}$ .

Why log space? Products of probabilities become sums and marginalisation becomes log-sum-exp (numerically stable); weights range over all of $\mathbb{R}$ instead of being squashed into $[0,1]$ ; and because softmax is shift-invariant, normalising is deferred — score now, normalise once at the boundary.

§ Syntax & semantics

Four layers, one induction.

NeSyCat Torch organises syntax and semantics into four layers, each a pair of a signature (the symbols) and an interpretation (their meaning). The first three declare and interpret symbols; the fourth generates the terms and assigns their monadic semantics by one induction.

01Categorical

Work in $\mathbf{Set}$ (computationally: Haskell types and maps). Parameters are drawn from $\mathbf{Tens}$ — Euclidean spaces $\mathbb{R}^n$ with differentiable maps, where the neural networks live and backpropagation happens. The one choice that varies is the effect: a single monad symbol $\bigcirc$ , with $\mathcal{M} := \mathcal{I}(\bigcirc)$ .

02Logical

Basic truth values are Booleans, $\Omega = \mathbb{B}$ . The connectives $\wedge,\ \vee,\ \neg,\ \rightarrow$ are the ordinary Boolean operations, lifted to act on monadic truth values $\mathcal{M}\,\Omega$ . The only genuinely monadic logical symbols are the quantifiers: $\mathcal{I}(Q)_D : (D \to \mathcal{M}\,\Omega) \to \mathcal{M}\,\Omega$ .

03Domain

Declares domain symbols, variables, and function/relation symbols — the actual objects of the theory (e.g. Image, Digit, Nat). Each function or relation symbol is one of three kinds: Tarski, Kleisli or Nesy.

04Grammatical

Generates terms in the do-notation the implementation uses; formulas are terms of the truth type $\tau$ . It recovers the ULLER/NeSyCat syntax and fixes the semantics pointwise at a valuation $\nu$ by a single induction.

The grammatical layer's binder desugars directly into monadic do-notation:

[\,x := m(T_1,\dots,T_n)\,]\,F \quad\equiv\quad \mathbf{do}\;\{\; x \leftarrow m(T_1,\dots,T_n);\; F \;\}

§ Symbols

Three kinds of symbol — one is neural.

Function and relation symbols are each partitioned into three kinds. Only the third is neural. (To stay close to first-order logic, symbols may not take truth-typed arguments.)

Tarskideterministic

\begin{aligned} f &: S_1,\dots,S_n \to T \\[3pt] R &: S_1,\dots,S_n \to \tau \end{aligned}

A plain (pure) map; its result re-enters the monad through return.

Kleislieffectful

\begin{aligned} f &: S_1,\dots,S_n \to {\bigcirc} T \\[3pt] R &: S_1,\dots,S_n \to {\bigcirc} \tau \end{aligned}

Already monadic; it stands as the final do-expression, without return.

Nesyneural

\begin{aligned} f &: {\bigcirc} S_1,\dots,{\bigcirc} S_n \to {\bigcirc} T \\[3pt] R &: {\bigcirc} S_1,\dots,{\bigcirc} S_n \to {\bigcirc} \tau \end{aligned}

Takes monadic carriers as input and produces monadic carriers — realised by neural networks; no binds occur.

In the MNIST-addition example, $\mathsf{digit} : \mathsf{Image} \to \mathcal{M}\,\mathsf{Digit}$ is the only monad-dependent symbol; addition and equality are ordinary (Tarski) symbols.

§ NeSyCat Torch · Running example

MNIST addition, by distant supervision.

NeSyCat Torch's running example: single-digit MNIST addition under distant supervision — only the sum of two handwritten digits is observed, never the digits themselves. The axiom is $\forall\,(x,y,n){:}S\;\bigl(n = \mathsf{digit}(x) + \mathsf{digit}(y)\bigr)$ .

The derivation

Monadic do-notation

\mathbf{do}\;\{\; d_1 \leftarrow \mathrm{dig}_\theta(x);\;\; d_2 \leftarrow \mathrm{dig}_\theta(y);\;\; \mathbf{return}\,(n = d_1 + d_2)\;\}

Each $\leftarrow$ performs the law of total probability in $\mathcal{D}$ and the log-space convolution in $\mathcal{T}$ . This is not pseudo-code — it is the semantic value, and the identical text compiles as Haskell.

The formula

Python

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

In Python, yield replaces Haskell's $\leftarrow$ — the same monadic composition.

The two classifiers return a pair, joined by the outer product $a \otimes b$ , giving exactly the discrete convolution

\mathcal{T}(\mathsf{sum})(a \otimes b)(s)\;=\;\sum_{i+k=s} a_i\,b_k\;=\;(a * b)(s)

— the unnormalised distribution of the sum. The network learns to read digits (about 97% digit accuracy) from the observed sums alone, never using digit labels.

§ NeSyCat Torch · Results

Competitive — in one uniform framework.

All numbers come from the JAX backend on a single A100 GPU, averaged over 15 seeds. NeSyCat Torch never uses digit labels; the network learns to read digits (≈97% accuracy) from observed sums alone.

94.6%

single-digit sum accuracy (LTN-style)

vs LTN's 93.5%

94.2%

single-digit sum accuracy (DPL-style)

vs DeepProbLog's 92.2%

≈97%

digit accuracy from sums alone

no digit labels, ever

Test sum accuracy (%), mean ± std, on MNISTAdd by N digits.

Method	N=1 (3k)	N=2 (1.5k)	N=2 (15k)	N=4 (7.5k)
NeSyCat Torch (LTN-style)	94.6 ± 0.6	89.7 ± 0.7	95.7 ± 0.5	92.0 ± 0.6
NeSyCat Torch (DPL-style)	94.2 ± 0.7	89.2 ± 0.7	95.8 ± 0.6	91.8 ± 0.8
LTN	93.5 ± 0.3	88.4 ± 1.0	95.4 ± 0.3	T/O
logLTN	–	88.3 ± 0.8	95.6 ± 0.5	–
DeepProbLog	92.2 ± 1.6	87.2 ± 1.9	95.2 ± 1.7	T/O
DeepStochLog	–	–	96.4 ± 0.1	92.7 ± 0.6
A-NeSI	–	–	96.0 ± 0.4	92.6 ± 0.8

NeSyCat Torch averages all 15 seeds; LTN averages its 10 best of 15. 'T/O' = timeout. '–' = not reported.

At batch 32, step times (train/test) are 0.52/0.20 ms (LTN-style) and 0.44/0.20 ms (DPL-style); a 15-seed sweep runs in ≈1.5 min. Where DeepProbLog and LTN time out at N=4 (two four-digit numbers, sums up to 19,998), NeSyCat Torch still runs at 92.0%.

§ Papers

Read the work.

NeSyCat Torch is the neural implementation; the categorical theory paper is the foundation it builds on.

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

Daniel Romero Schellhorn · Till Mossakowski · Björn Gehrke · 2026-06-17 · cs.AI / cs.LG / cs.LO / math.CT / math.LO / math.PR

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

@misc{schellhorn2026nesycat,
  title         = {NeSyCat Torch: A Differentiable Tensor Implementation of Categorical Semantics for Neurosymbolic Learning},
  author        = {Schellhorn, Daniel Romero and Mossakowski, Till and Gehrke, Björn},
  year          = {2026},
  eprint        = {2606.19279},
  archivePrefix = {arXiv},
  primaryClass  = {cs.AI},
  url           = {https://arxiv.org/abs/2606.19279},
}

Read on arXiv ↗PDF ↗ Code ↗

NeSyCat: A Monad-Based Categorical Semantics of the Neurosymbolic ULLER Framework

Daniel Romero Schellhorn · Till Mossakowski · 2026-04-27 · cs.AI / cs.LO / math.CT / math.LO

ULLER (Unified Language for LEarning and Reasoning) offers a unified first-order logic (FOL) syntax, enabling its knowledge bases to be used directly across a wide range of neurosymbolic systems. The original specification endows this syntax with three pairwise independent semantics: classical, fuzzy, and probabilistic, each accompanied by dedicated semantic rules. We show that these seemingly disparate semantics are all instances of one categorical framework based on monads, the very construct that models side effects in functional programming. This enables the modular addition of new semantics and systematic translations between them. As example, we outline the addition of generalised quantification in Logic Tensor Networks (LTN) to arbitrary (also infinite) domains by extending the Giry monad to probability spaces. In particular, our approach allows a modular implementation of ULLER in Python and Haskell, of which we have published initial versions on GitHub.

@misc{schellhorn2026nesycat,
  title         = {NeSyCat: A Monad-Based Categorical Semantics of the Neurosymbolic ULLER Framework},
  author        = {Schellhorn, Daniel Romero and Mossakowski, Till},
  year          = {2026},
  eprint        = {2604.24612},
  archivePrefix = {arXiv},
  primaryClass  = {cs.AI},
  url           = {https://arxiv.org/abs/2604.24612},
}

Read on arXiv ↗PDF ↗

§ Semiotics

Sketch it, don't just read it.

Semiotics is NeSyCat's web editor for category-theoretic string diagrams — compose shapes, wire their points, and round-trip the whole diagram as JSON. Sign in with GitHub to save your own.

GitHub sign-in can't complete inside the embed above — open the editor in its own tab to sign in and save.

Open editor↗

§ NeSyCat Torch · Implementations

One spec, three backends.

NeSyCat Torch runs the same monad-polymorphic specification in Haskell and Python — all under the NeSyCat organisation on GitHub.

HaskTorchHaskell

The reference backend. The monad-polymorphic do-notation is literal Haskell — written once, the axioms compile and run as the semantic value.

JAXPython

The benchmark backend. The log-space convolution is JIT-compiled and differentiated; all reported numbers come from JAX on a single A100.

PyTorchPython

The third backend. In Python, yield takes the role of Haskell’s monadic bind — the same do-notation composition.

github.com/NeSyCat ↗