Search papers, labs, and topics across Lattice.
This paper introduces Baobab, a method that compiles OWL 2 DL ontologies into Sentential Decision Diagrams (SDDs) using a consequence-based calculus, allowing for effective neuro-symbolic learning that retains classical entailment. By leveraging a perception network trained on real images with partial ABox supervision, Baobab demonstrates the ability to recover latent ontology concepts that traditional independent perception methods fail to capture. The results show that Baobab achieves Bayes-optimal performance on a real-image MNIST task, addressing reasoning shortcuts in non-Horn description logics for the first time.
Baobab reveals that a mixture indexed by query justifications can outperform independent perception in reasoning tasks, achieving Bayes-optimal performance where others fail.
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.
