arXiv:2608.17741cs.AI2026-08中稿 · NeSy 2026

将复杂知识库编译为可微电路,让神经网络在部分监督下准确识别图像并还原隐含概念。

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

  • 基于推理规则将SROIQ知识库转化为可微的命题决策图
  • 在部分标注下训练CNN识别手写数字,准确率显著优于独立感知模型
  • 首次揭示并缓解非霍恩逻辑中的推理捷径问题,适合知识推理与医学应用

OWL 2 DL本体基于描述逻辑$SROIQ$,广泛用于生物医学与语义网的大规模知识库表达。现有神经符号学习方法要么将本体嵌入连续空间(放弃经典蕴含),要么局限于仅具单一标准模型的霍恩片段$EL^{++}$。本文提出Baobab,将具有有限实例的$SROIQ$本体编译为命题决策图(SDD):在结论驱动的演算下饱和命题核心,并在活跃域上实例化剩余$SROIQ$特性(名义、数量限制、关系公理)。通过证据条件加权模型计数训练感知网络,在部分本体监督下识别真实图像。在一个涵盖所有$SROIQ$特性的本体上,CNN学习识别由后继关系连接的手写数字,并恢复独立感知无法捕捉的潜在本体概念。当监督允许多个一致补全时,独立感知会坍缩至单一解,形成推理捷径;我们证明,以查询的合理性为索引的混合模型可表示独立感知无法达到的校准后验分布,且从电路枚举的补全中初始化该混合模型,可在真实图像的MNIST任务中实现贝叶斯最优后验——据我们所知,首个在非霍恩描述逻辑中刻画并缓解推理捷径的研究。编译器的正确性与表示结果已在Lean 4中机器验证。代码已公开于https://github.com/bio-ontology-research-group/baobab。

原文摘要 · Abstract (English)

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.

神经符号知识推理可微逻辑本体学习

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。