Neuro Symbolic Categories

A monad-based categorical framework for neurosymbolic AI.

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.

Hover or click a corner of the diamond — or the dot at its center — to explore each area.

Read the work.

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

@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},
}

@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},
}

One definition of truth.

A semantics is a strong monad $\mathcal{M}$ on a copy-discard category with a truth object $\Omega$. The categorical layer builds $\mathcal{M}$ as the weight monad of a semiring: finitely supported weight functions, with bind as matrix multiplication. Boolean, mass, log and t-norm rows are all instances, and the monad is commutative exactly when the semiring is. Probability itself is not a semiring, so distributions enter as the mass-one submonad.

The logical layer takes $\Omega$ to be $\mathcal{M}$ applied to the Booleans, deriving connectives by lifting Boolean operations through it. What lifts is not a semiring but a bounded lattice carrying two monoids, in linear logic's vocabulary — and the copying axioms hold only where the carrier is idempotent. The domain layer adds function and relation symbols whose argument slots are tagged plain or monadic; the grammatical layer gives terms and formulas a Kleisli interpretation, with substitution as a grammar rule rather than a meta-operation.

The statistical layer meets implementation: batching is a reader transformer, proved semantically transparent, and softmax bridges the log-weight and probability readings exactly when every bound continuation preserves mass. All of it is a blueprint-driven Lean 4 library over mathlib — categorical, logical, domain, grammatical, statistical — where an item is marked proved only when its Lean declaration actually is.

The categorical layer in Lean: $\mathcal{M}$ over a semiring, with return, bind, and the left unit law.

variable {S : Type*} [Semiring S] {X Y Z : Type*}

/-- Semiring monad: finitely supported S-weighted combinations. -/
abbrev MS (S : Type*) [Semiring S] (X : Type*) := X →₀ S

/-- Unit: the Dirac delta at `x`. -/
noncomputable def ret (x : X) : MS S X := Finsupp.single x 1

/-- Bind: matrix multiplication over `S`; addition marginalises. -/
noncomputable def bind (f : MS S X) (k : X → MS S Y) : MS S Y :=
  f.sum fun x w => w • k x

/-- Left unit law — one of the proved monad laws. -/
theorem ret_bind (x : X) (k : X → MS S Y) : bind (ret x) k = k x := by
  unfold bind ret
  rw [Finsupp.sum_single_index (zero_smul S (k x))]
  exact one_smul S (k x)

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.

The axiom, compiled.

NeSyCat.Informatics is the JAX port: the same axiom, written once as a Python generator. Each yield is the monadic bind — s = yield n binds the observation, and return s == d1 + d2 is the predicate. The monad stays an explicit argument, LogTens for differentiable training and Dist for the probability readout, and digit and big_wedge are Method instances, so nothing matches on the monad. Ordinary Python composes: mnist_multidigit puts yield inside nested for-loops.

interpret (a_categorical/do_notation.py) builds the free-monad AST by prefix-replay: Python generators are one-shot, so each Bind's continuation re-creates the generator and re-sends the recorded prefix. collect_leaves flattens that AST into ordered log-weight tensors plus a host-side reconstructor, and log_num_den probes the reconstructor rather than the source: additive predicates fold through log_convolve — variable elimination in the log semiring — otherwise tve_contract schedules an opt_einsum contraction, otherwise the full-joint marginalize runs as fallback and oracle.

Replay, probing and contraction planning are host work at trace time; the only jax.jit on the training path is the step inside train_batched, value_and_grad plus optax Adam. A batch compiles into a log-space tensor contraction that JAX runs on CPU or GPU alike, with an sbatch script targeting an A100 or H100 node on the HPC3 cluster, and g_benchmark/timing.py reports train- and test-step times in milliseconds over 1000 steps behind jax.block_until_ready. Three MNIST examples run via python -m nesycat <ExampleName> [n].

The whole grammatical layer of the MNIST-addition example — the formula as a generator, and the sentence that quantifies it.

from nesycat.b_logical.signature.a2_mon_blat import big_wedge

from .c_domain import digit


def formula(m, theta, x, y, n):
    """n = digit(x) + digit(y)."""
    d1 = yield digit(m, theta, x)
    d2 = yield digit(m, theta, y)
    s = yield n
    return s == d1 + d2


def sentence(m, theta, guard):
    """bigWedge (x, y, n) in guard.  formula."""
    return big_wedge(m, guard, lambda element: formula(m, theta, *element))

From sentence to symbol.

Natural language is the third leg of NeSyCat: a pipeline that parses a sentence into a syntax tree, translates the tree into a many-sorted first-order formula, and hands that formula to NeSyCat as a runnable program and a string diagram.

One shared knowledge base of natural-language / formal-logic pairs will benchmark the translation.

This layer is in active development alongside the NeSyCat NLP paper.

The axiom is the program.

NeSyCat.TypeTheory is the Haskell implementation, built on HaskTorch's libtorch bindings. A shared Library keeps the layer names — A_Categorical (the monads), B_Logical (connectives and quantifiers), C_Domain (sorts and neural Kleisli symbols), D_Grammatical (the axiom), E_Data, F_Inferential (training), G_Statistical (metrics) — and each example is a C–G stack plus a Definition.hs manifest.

A monad is a return and a bind, and here bind is exactly the marginalising composition of the semantics. Dist and LogTens are free monads, so a do-block computes nothing: it builds the formula's tree, and every arrow is a summation sign the interpreter discharges. The law of total probability is literally the interpreter's bind case. The axiom in do-notation is the evaluator.

Choosing $\mathcal{M}$ chooses the logic. At Dist that nested sum gives probabilities; at LogTens the leaves carry batched log-weight tensors and the bind becomes a log-space convolution — variable elimination, so the full joint need not form — and training minimises the axiom's own negative log satisfaction.

Types enforce the discipline. The formula names no monad: it is quantified over $\mathcal{M}$ under one signature class, and the data a quantifier ranges over is a type family, so the same universal is a list fold under Dist and one vectorised op under LogTens. An ill-sorted or unbound term does not compile.

The MNIST-addition axiom in full: one do-block, polymorphic in the monad, with its quantifier.

-- | The per-pair FORMULA  n = digit(x) + digit(y), monad-polymorphic over m.
mnistFormula ::
  forall m.
  (MnistKlFun m) =>
  Weights ->
  (m Image, m Image, m Natural) ->
  m Omega
mnistFormula theta (x, y, n) =
    do d1 <- digit theta x   -- x, y, n all arrive encoded (eta) from the data
       d2 <- digit theta y
       s <- n
       return (s == (d1 + d2))

-- | The SENTENCE  forall (x,y,n) in data. n = digit(x) + digit(y)
mnistSentence ::
  forall m.
  (MnistKlFun m, TwoMonBLat Omega, A2MonBLat m Omega, Monad m) =>
  ParamsLogic Omega ->
  Guard m (m Image, m Image, m Natural) ->
  Weights ->
  m Omega
mnistSentence lp guard theta = bigWedge lp guard (mnistFormula @m theta)