Neuro-symbolic learning over OWL 2 DL via consequence-based compilation to differentiable circuits

Olga Mashkova; Asaad Mohammedsaleh; Fernando Zhapa-Camacho; Robert Hoehndorf

cs.AIAug 18, 2026

Neuro-symbolic learning over OWL 2 DL via consequence-based compilation to differentiable circuits

Authors: Olga Mashkova, Asaad Mohammedsaleh, Fernando Zhapa-Camacho, Robert Hoehndorf

Organizations: Computer Science Program, Computer, Electrical, and Mathematical Sciences & Engineering Division, King Abdullah University of Science and Technology, Thuwal 23955, Saudi Arabia

Abstract

OWL 2 DL ontologies, grounded in the description logic $\mathcal{SROIQ}$ , express large knowledge bases in biomedicine and the Semantic Web. Neuro-symbolic (NeSy) learners over description logics either embed the ontology in a continuous space, abandoning classical entailment, or restrict to the Horn fragment $\mathcal{EL}^{++}$ , which has a single canonical model. We present Baobab, which compiles a $\mathcal{SROIQ}$ ontology with a finite ABox into a Sentential Decision Diagram (SDD): it saturates a propositional core under a consequence-based calculus and instantiates the remaining $\mathcal{SROIQ}$ features (nominals, number restrictions, and the role axioms) over the active domain. The SDD's evidence-conditioned weighted model count then trains a perception network to recognize real images under partial ABox supervision: on an ontology that exercises every distinctive $\mathcal{SROIQ}$ feature, a CNN learns to read MNIST digits coupled by a successor relation and recovers latent ontology concepts that an independent perception leaves at chance. When the supervision admits several ontology-consistent completions, an independent perception collapses onto one, a reasoning shortcut: we show that a mixture indexed by the query's justifications can represent the calibrated posterior no independent perception can, and that seeding it from the circuit's enumerated completions attains the Bayes-optimal posterior on a real-image MNIST task where single-WMC and learned mixtures (the BEARS-ensemble hypothesis class) do not: to our knowledge the first to characterize and mitigate reasoning shortcuts in a non-Horn description logic. Soundness of the compiler and the representation result are machine-checked in Lean 4. Code is available at https://github.com/bio-ontology-research-group/baobab.

Figures & tables

regime	method	digit	latent	viol $\downarrow$	ECE $\downarrow$
grounded ( $\#\mathrm{RS}{=}1$ )	Independent	$0.25$ $\pm.09$	$0.49$ $\pm.14$	$0.80$ $\pm.12$	$0.33$ $\pm.14$
grounded ( $\#\mathrm{RS}{=}1$ )	WMC	$\mathbf{0.99}$ $\pm.00$	$\mathbf{1.00}$ $\pm.00$	$\mathbf{0.02}$ $\pm.01$	$\mathbf{0.00}$ $\pm.00$
under-det. ( $\#\mathrm{RS}{=}5$ )	Independent	$0.20$ $\pm.03$	$0.46$ $\pm.10$	$0.93$ $\pm.10$	$0.08$ $\pm.08$
under-det. ( $\#\mathrm{RS}{=}5$ )	WMC	$0.18$ $\pm.07$	$0.67$ $\pm.03$	$0.78$ $\pm.05$	$0.15$ $\pm.02$

Table 1: MNIST-

\mathcal{SROIQ}

, mean

\pm

std over ten seeds (metrics in § 4 ; digit identities never supervised). Grounding the concept evidence collapses

\#\mathrm{RS}

from

5

1

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

feature	emitted ground clauses	count
nominal $\mathsf{Nom}_{a}$	$\mathsf{Nom}_{a}(a)$ ; $\neg\mathsf{Nom}_{a}(b)$ , $b\neq a$	$d$
${\geq}\,n\,R.C$ at $x$	$Q(a)\leftrightarrow\bigvee_{\|S\|=n}\bigwedge_{y\in S}R(a,y)\wedge C(y)$	$d\,(\binom{d}{n}{+}1)$
${\leq}\,n\,R.C$ at $x$	$Q(a)\leftrightarrow\bigwedge_{\|T\|=n+1}\big(\bigwedge_{y\in T}R(a,y)\wedge C(y)\to\bigvee_{i<j}y_{i}\approx y_{j}\big)$	$O(d^{\,n+1})$
inverse $R\equiv S^{-}$	$R(a,b)\leftrightarrow S(b,a)$	$2d^{2}$
$\mathsf{Trans}(R)$	$R(a,b)\wedge R(b,c)\to R(a,c)$	$d^{3}{-}d$
chain $R_{1}{\circ}\dots{\circ}R_{k}\sqsubseteq S$	$R_{1}(a_{0},a_{1})\wedge\dots\wedge R_{k}(a_{k-1},a_{k})\to S(a_{0},a_{k})$	$d^{\,k+1}$

Appendix

Table 2: Grounding schemata over the active domain

\Delta

d=|\Delta|

a,b,c

range over

\Delta

;

\binom{d}{n}

is the

n

-subset count.

refinement	method	topping	property	viol $\downarrow$
closed	Independent	$0.95$ $\pm.01$	$0.45$ $\pm.15$	$0.89$ $\pm.18$
closed	WMC	$0.93$ $\pm.01$	$\mathbf{0.92}$ $\pm.02$	$0.06$ $\pm.02$
open	Independent	$0.95$ $\pm.01$	$0.45$ $\pm.16$	$0.86$ $\pm.28$
open	WMC	$0.95$ $\pm.01$	$0.78$ $\pm.01$	$0.00$ $\pm.00$

Appendix

Table 3: Closed-world ablation on the Pizzaiolo fragment (mean

\pm

std over ten seeds, five epochs; same fragment and metrics as Table 7 ). Closed materializes the exact biconditional

X(a)\Leftrightarrow\bigsqcup_{t}\mathsf{hasTopping}(a,t)\sqcap C(t)

; open keeps the forward direction

X(a)\!\to\!\exists\mathsf{hasTopping}.C

only, dropping the closure clause

\exists\mathsf{hasTopping}.C\!\to\!X(a)

. Removing the closure clause leaves supervised toppings untouched but lowers latent property recovery from

0.92

0.78

; the reported violation falls to

0.00

because the removed clause is the constraint whose violation was counted (§ 4.1 ).

	clauses	fixed vtree	minimized
ontology	unsat $\to$ sat	unsat $=$ sat	unsat	sat
horn-chain	$3\to 6$	$10$	$8$	$8$
disjunction	$7\to 12$	$23$	$17$	$\mathbf{12}$
two-disjunctions	$11\to 29$	$38$	$22$	$\mathbf{18}$
exists+disjunction	$8\to 73$	$73$	$41$	$\mathbf{36}$
bird-penguin	$11\to 44$	$1011$	$139$	$143$

Appendix

Table 4: Effect of saturation on SDD node count, measured with the accompanying library. Saturation adds entailed clauses (column clauses ) without changing the atom set. Over a fixed vtree the size is identical with and without saturation (Theorem 0.F.1 ); under dynamic vtree minimization it usually shrinks but is not guaranteed to ( bird-penguin ).

toppings ( $\|\Delta\|$ )	atoms	clauses	ground (s)	SDD nodes	peak mem
$1$ ( $\|\Delta\|{=}2$ )	$201$	$638$	$0.04$	$3{,}182$	$0.7$ GB
$2$ ( $\|\Delta\|{=}3$ )	$302$	$957$	$0.19$	$12{,}064$	$5.7$ GB
$3$ ( $\|\Delta\|{=}4$ )	$403$	$1{,}276$	$0.01$	—	$>22$ GB †

Appendix

Table 5: Compiling the full Pizzaïolo

\mathcal{SROIQ}

ontology (

66

named classes,

90

existential and

44

universal restrictions, right-hand-side disjunctions on

\mathsf{Pizza}

and

\mathsf{SpicyPizza}

) over a growing active domain, with a fixed vtree throughout. Grounding stays sub-second at every size; the compiled SDD grows super-linearly and exceeds a

22

GB /

600

s budget at three toppings. The

59

-atom two-topping fragment of § 4.1 is a separately extracted role-based sub-signature, not a row here.

experiment	feat. dim	hidden	epochs	$\lambda$	$\kappa$	$K$
MNIST (CNN)	$28^{2}$	CNN	12	0.5	–	–
Pizzaiolo frag. (ResNet-18)	$224^{2}$	linear head	5	0.5	–	–
Pizza (synthetic)	12	64	10	0.3	–	–
MNIST-Disj. (CNN)	$28^{2}$	CNN	20	0.5	2.0	4

Appendix

Table 6: Hyperparameters (Adam; learning rates and batch sizes in the text).

\lambda

: semantic-loss weight;

\kappa

: diversity weight;

K

: mixture / ensemble size.

method	topping	property	viol $\downarrow$
Independent	$0.95$ $\pm.01$	$0.45$ $\pm.15$	$0.89$ $\pm.18$
WMC	$0.93$ $\pm.01$	$\mathbf{0.92}$ $\pm.02$	$\mathbf{0.06}$ $\pm.02$

Appendix

Table 7: Pizzaiolo two-topping role-based fragment (mean

\pm

std over ten seeds; metrics in § 4 ). topping is supervised; property are the latent Vegetarian/NonVegetarian/Spicy classes recovered through

\mathsf{hasTopping}

Method	digit	NLL $\downarrow$	ECE $\downarrow$	mode-cov. TV $\downarrow$
Independent (UCI)	$0.99$ $\pm.00$	$6.93$ $\pm.00$	$0.00$ $\pm.00$	$1.00$ $\pm.00$
Single-WMC (SL / DPL)	$0.99$ $\pm.00$	$6.13$ $\pm.00$	$0.00$ $\pm.00$	$0.99$ $\pm.00$
JustWMC (learned mix)	$0.99$ $\pm.00$	$6.69$ $\pm.43$	$0.11$ $\pm.03$	$0.99$ $\pm.01$
BEARS	$-$	$6.36$ $\pm 2.36$	$0.41$ $\pm.12$	$0.44$ $\pm.11$
JustWMC (anchored)	$0.99$ $\pm.00$	$\mathbf{4.17}$ $\pm.00$	$\mathbf{0.00}$ $\pm.00$	$\mathbf{0.02}$ $\pm.00$

Appendix

Table 8: MNIST-Disjunction (

\#\mathrm{RS}=4

; mean

\pm

std over ten seeds; metrics in § 4 ). NLL is over the gender atoms (Bayes-optimal

4.16

); ECE and mode-coverage TV are the reasoning-shortcut diagnostics. BEARS is a

K{=}4

deep-ensemble mitigation [ 24 ] trained on the same circuit; its per-digit accuracy is not separately evaluated (

-

method	topping	pizza	latent	violation
	(observed)	(4 latent)	(11 latent)	rate
Independent	$0.99$ $\pm.00$	$0.44$ $\pm.12$	$0.43$ $\pm.08$	$1.00$
WMC	$0.76$ $\pm.01$	$\mathbf{0.75}$ $\pm.00$	$\mathbf{0.58}$ $\pm.05$	$\mathbf{0.00}$

Appendix

Table 9: Pizza-

\mathcal{SROIQ}

, 64 held-out examples, mean

\pm

std over ten seeds (higher is better except for violation). The pizza (4 latent) and latent (11 atoms) columns are the headline: WMC infers them from topping evidence though those atoms receive no direct supervision.

OWL kind	axioms	ours	DPL (Horn)	DPL (manual)	DPL clauses
SubClassOf	23	46	15	8	30
DisjointClasses	14	28	14	0	14
EquivalentClasses	3	12	0	3	11
RoleInclusion	2	4	2	0	2
AsymmetricRole	2	4	2	0	2
IrreflexiveRole	2	4	2	0	2

Appendix

Table 10: Per-OWL-axiom-kind encoding cost for the MNIST-

\mathcal{SROIQ}

ontology. ours : normalized DL-clauses produced by the structural transformation. DPL Horn / DPL manual : DPL admits / requires user-written disjunctive / cardinality / negation encoding.

Neurosymbolic Learning

Neurosymbolic learning combines neural models with symbolic rules, knowledge, and reasoning to support structured, interpretable AI.

See all 60 papers

Aug 13, 2026

Moose: Latent concept learning with reasoning-shortcut awareness in $\mathcal{EL}^{++}$

The OWL 2 EL profile is used in some of the largest production ontologies, including the Gene Ontology and SNOMED CT. Existing neuro-symbolic (NeSy) learning methods accept propositional theories or Datalog, and reasoning-shortcut (RS) awareness has not been investigated in ontology settings. We present Moose, a method that compiles an

\mathcal{EL}^{++}

TBox and finite ABox to a Sentential Decision Diagram (SDD). The SDD acts as a differentiable weighted-model-counting layer, and we add closure clauses outside the

\mathcal{EL}^{++}

profile on declared exhaustive families to overcome the limited expressivity of

\mathcal{EL}^{++}

under partial supervision. We show termination, soundness, completeness, and polynomial intermediate sizes, and validate the proofs in Lean. We then define the first formal partial-supervision latent-concept-learning task over an OWL EL ontology, i.e., learning per-individual classifiers for latent concepts from observed ABox literals, and evaluate Moose on MNIST-with-ontology and Pizzaïolo. Moose improves over propositional-NeSy, fuzzy-logic, and ontology embedding baselines, and presents the first reasoning-shortcut analysis in an OWL EL setting.

Olga Mashkova, Asaad Mohammedsaleh, Fernando Zhapa-Camacho +1

Computer Science Program, Computer, Electrical, and Mathematical Sciences & Engineering Division, King Abdullah University of Science and Technology, Thuwal 23955, Saudi Arabia

Neurosymbolic Learning Description Logic

Ask PDF

Jul 17, 2026

NeurOWL: An LLM-Based Neural-symbolic Framework for Incomplete OWL Ontology Reasoning

OWL ontologies provide a formal knowledge representation framework that enables semantic reasoning, and have been widely adopted across domains such as healthcare and bioinformatics. In practice, however, real-world ontologies are often incomplete, which pose challenges for reasoning. In this work, we focus on a fundamental subsumption reasoning problem: given an incomplete ontology and a candidate (non-entailed) subsumption, determine whether the subsumption is semantically plausible and, if so, providing a logically sound explanation containing potential missing axioms. This task unifies subsumption verification with ontology abduction, and generalizes the latter by removing the need for a predefined candidate set of missing axioms. To address this subsumption reasoning problem, we propose NeurOWL, an end-to-end neuro-symbolic framework that jointly performs verification and abduction, leveraging both formally defined semantics and textual semantics through Large Language Models and ontology embeddings. We evaluate NeurOWL on real-world ontologies across multiple domains, demonstrating strong and robust performance across different domains.

Hui Yang, Jiaoyan Chen, Yiping Song +2

The University of Manchester · Zhejiang University

Logical Reasoning Abductive Reasoning Symbolic Reasoning Neuro-Symbolic Reasoning

Ask PDF

Oct 5, 2026

DPNL: A DPLL-based Algorithm for Probabilistic Neurosymbolic Learning

Probabilistic Neurosymbolic Learning (PNL) combines neural predictions with symbolic reasoning, enabling end-to-end learning from final-output supervision without labels for intermediate concepts. A central challenge is probabilistic inference: state-of-the-art approaches often rely on materializing the logical provenance of a query, which can itself become a major computational bottleneck. We introduce Dynamic Probabilistic Neurosymbolic Learning (DPNL), an oracle-guided framework that avoids requiring complete provenance materialization before inference. DPNL lazily explores the space of intermediate assignments, while oracles resolve entire regions that can already be certified to produce or exclude the target output. We establish conditions ensuring soundness and termination. ApproxDPNL extends the same search with early termination while maintaining certified bounds on the exact output probability, providing controlled approximation guarantees. The oracle interface decouples inference from the representation of the symbolic component, enabling problem-specific reasoning within the same framework. Experiments on several neurosymbolic tasks show that DPNL and ApproxDPNL substantially extend the range of problem instances tractable by probabilistic neurosymbolic inference.

Thomas Jean-Michel Valentin, Pierre Genev{è}s, Luisa Sophie Werner +3

ENS Paris Saclay,TYREX · LIG,TYREX · TYREX +1

Probabilistic Logic Neurosymbolic Learning

Ask PDF

Abstract

Neurosymbolic Learning

Explore similar work

Moose: Latent concept learning with reasoning-shortcut awareness in EL++\mathcal{EL}^{++}EL++

NeurOWL: An LLM-Based Neural-symbolic Framework for Incomplete OWL Ontology Reasoning

DPNL: A DPLL-based Algorithm for Probabilistic Neurosymbolic Learning

Moose: Latent concept learning with reasoning-shortcut awareness in $\mathcal{EL}^{++}$