Neuro-symbolic learning over OWL 2 DL via consequence-based compilation to differentiable circuits
Baobab compiles SROIQ ontologies into differentiable circuits, enabling robust neuro-symbolic learning with complex logic features.
Key Findings
Methodology
This paper introduces Baobab, which compiles OWL 2 DL ontologies based on SROIQ into Sentential Decision Diagrams (SDDs). Using consequence-based calculus, it saturates a propositional core and instantiates remaining features like nominals, number restrictions, and role axioms over the active domain. The compiled SDD enables evidence-conditioned weighted model counting (WMC) to serve as a differentiable training signal for perception networks, allowing them to learn latent ontology concepts from real images under partial supervision. The approach ensures logical consistency, handles complex features, and mitigates reasoning shortcuts. It integrates formal compilation guarantees, mechanized in Lean 4, and demonstrates superior performance on tasks like MNIST digit recognition and real-world datasets, outperforming traditional methods in accuracy, calibration, and robustness.
Key Results
- On MNIST, CNNs trained with the compiled ontology achieved 99% digit recognition accuracy, vastly outperforming baseline models at 20%.
- In scenarios with multiple ontology-consistent completions, the MixtureEncoder with justifications approximated the Bayesian posterior, reducing NLL to 4.17 and improving calibration.
- The method covered 23% of OWL 2 DL axioms, validating its applicability to complex ontologies, and effectively mitigated reasoning shortcuts in non-Horn DLs.
Significance
This work advances neuro-symbolic AI by enabling full-featured SROIQ reasoning within a differentiable framework, bridging the gap between symbolic logic and deep perception. It addresses longstanding limitations in scalability and logical fidelity, opening pathways for large-scale knowledge graph reasoning, biomedical data integration, and semantic web applications. The ability to learn latent concepts while maintaining logical consistency marks a significant step toward more intelligent, explainable AI systems capable of complex reasoning and perception fusion.
Technical Contribution
The core technical innovation is the complete compilation of SROIQ into SDDs, supporting all features including nominals and role axioms, combined with consequence-based saturation for logical closure. The introduction of evidence-conditioned WMC as a differentiable loss function enables end-to-end training of perception networks. The MixtureEncoder model addresses the challenge of multiple valid completions, providing a Bayesian-calibrated posterior. Formal guarantees, mechanized in Lean 4, ensure the correctness and completeness of the compilation process, setting a new standard for logic-aware neural models.
Novelty
This is the first work to fully compile OWL 2 DL's complex features, including nominals and role axioms, into a differentiable circuit framework. It extends knowledge compilation beyond Horn fragments, introduces consequence-based saturation for non-Horn DLs, and integrates latent concept learning with Bayesian calibration, thus significantly broadening the scope and fidelity of neuro-symbolic reasoning.
Limitations
- The current approach faces scalability issues with very large ontologies, as SDD size and compilation time grow exponentially with complexity. Handling dynamic or infinite knowledge bases remains challenging.
- Dependence on finite ABox limits applicability to static knowledge; real-time updates or streaming data require incremental compilation strategies.
- Training costs are high, requiring extensive hyperparameter tuning and computational resources, which may hinder deployment in resource-constrained environments.
Future Work
Future efforts will focus on scaling the compilation process, optimizing SDD storage and inference, and extending support for dynamic knowledge bases. Incorporating incremental compilation, online learning, and multi-modal data integration will enhance practical deployment. Additionally, exploring approximate inference techniques and hardware acceleration could further improve efficiency, enabling broader adoption in real-world AI systems.
AI Executive Summary
This paper introduces Baobab, a pioneering framework that compiles OWL 2 DL ontologies based on SROIQ into Sentential Decision Diagrams (SDDs), enabling fully differentiable, logic-aware neural perception systems. Traditional neuro-symbolic approaches often restrict themselves to Horn fragments or abandon classical entailment, limiting their reasoning capabilities. Baobab overcomes these limitations by leveraging consequence-based calculus to compile complex features such as nominals, role axioms, and number restrictions into a unified circuit. This compilation guarantees logical soundness and completeness, supported by formal proofs mechanized in Lean 4.
The core innovation lies in using evidence-conditioned weighted model counting (WMC) as a differentiable loss function, allowing perception networks like CNNs and ResNets to learn latent ontology concepts directly from real images under partial supervision. Experiments on MNIST digits demonstrate that CNNs trained with this method reach 99% accuracy, vastly outperforming baseline models. Moreover, in scenarios with multiple ontology-consistent completions, the MixtureEncoder model, which incorporates justifications, approximates the Bayesian posterior, reducing negative log-likelihood to 4.17 and achieving superior calibration.
This approach significantly advances the field of neuro-symbolic AI by enabling the integration of complex description logic features into end-to-end trainable systems. It addresses key challenges such as reasoning shortcuts and logical inconsistency, providing a scalable, formal, and practical solution for large-scale knowledge reasoning and perception tasks. Looking ahead, the authors plan to improve scalability, support dynamic knowledge bases, and incorporate multi-modal data, paving the way for more intelligent, explainable AI systems capable of complex reasoning and perception fusion in real-world applications.
Deep Analysis
Background
描述逻辑（DL）作为知识表达的核心工具，广泛应用于生物医学、语义Web等领域。OWL 2 DL基于SROIQ，提供丰富的表达能力，但传统推理方法在大规模复杂本体中面临计算瓶颈。近年来，神经符号（NeSy）试图结合深度学习与符号推理，解决符号系统的可扩展性和鲁棒性问题。现有方法多采用嵌入技术或知识编译，但多局限于Horn子集或缺乏对nominals、角色公理等复杂特征的支持，导致推理不完备或逻辑不一致。本文在此背景下，提出支持所有SROIQ特征的完整知识编译方案，弥补了现有技术的不足。
Core Problem
核心问题在于如何在保持描述逻辑完整性的同时，实现高效、可微的推理机制。现有NeSy方法多依赖简化的逻辑子集，难以处理nominals、角色公理等复杂特征，导致推理捷径（reasoning shortcuts）问题严重。此外，如何在有限ABox监督下学习潜在概念，确保逻辑一致性与感知性能的平衡，也是亟待解决的难题。
Innovation
本研究的创新点包括：1）将完整的SROIQ本体编译为SDD，支持所有特征，确保推理完备；2）结合后果推理实现实例化，避免Horn限制；3）提出证据条件化WMC机制，将逻辑推理融入深度学习训练中；4）引入MixtureEncoder模型，有效应对多重补全带来的推理捷径问题，达到贝叶斯最优后验。这些创新突破了传统NeSy的局限，显著提升了逻辑推理的表达能力与感知的协同性能。
Methodology
- �� 规范化：将所有概念转为否定范式（NNF）；• 转换：将Axioms转为DL子句，形成结构化的推理基础；• 后果推理：利用基于规则的饱和（saturation）机制，闭合推理集，避免Skolem项的引入；• 归结：在有限域上实例化nominals、数限制、角色公理，生成有限的CNF；• 编译：将CNF转为SDD，支持线性时间的模型计数；• 训练：利用证据条件化WMC作为损失，训练感知网络识别潜在概念。整个流程确保推理的完备性与可微性，结合深度学习实现感知-推理的端到端训练。
Experiments
采用MNIST与Pizzaiolo数据集，训练CNN与ResNet模型，通过本体特征学习潜在概念。评估指标包括识别准确率、逻辑一致性、校准误差（ECE）和模型置信度。对比无本体、Horn子集及不同补全策略，验证方法在多重补全、复杂特征场景下的优越性。实验还包括推理捷径的分析与模型鲁棒性测试，确保在真实场景中的应用潜力。
Results
在MNIST任务中，模型达99%准确率，显著优于无本体模型的20%。在多补全场景中，MixtureEncoder结合justifications实现贝叶斯最优后验，NLL降低至4.17，校准效果优异。支持所有SROIQ特征的完整编译，验证了方法的广泛适用性。推理捷径问题得到缓解，模型在复杂本体中表现出良好的逻辑一致性与感知能力。
Applications
该方法适用于生物医学知识图谱、语义Web、自动推理系统等领域，支持大规模复杂本体的逻辑推理与感知融合。可用于智能问答、自动诊断、知识补全等场景，提升系统的推理准确性与鲁棒性。未来还可结合多模态数据，推动AI系统的通用智能发展。
Limitations & Outlook
目前方法在超大规模本体（如数千角色与限制）上面临存储与计算瓶颈，SDD的规模限制了实际应用。知识编译依赖有限ABox，难以适应动态或无限知识库。模型训练成本较高，调参复杂，实际部署中存在一定的调试成本。未来需优化算法与硬件支持，提升扩展性。
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.