Moose: Latent concept learning with reasoning-shortcut awareness in EL++

Moose: Latent concept learning with reasoning-shortcut awareness in EL++

Abstract. 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 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 EL++ profile on declared exhaustive families to overcome the limited expressivity of 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.

Introduction. The OWL 2 EL profile underpins some of the largest and most widely-used ontologies, such as the Gene Ontology with ∼50K classes and ∼8M annotations, SNOMED CT, and most of the OBO Foundry ontologies, because EL trades expressivity for polynomial-time reasoning on subsumption, instance checking, and consistency. Neuro-symbolic (NeSy) learning combines neural perception with symbolic constraints; several families coexist. Fuzzy / t-norm methods replace propositional truth with continuous operators on [0, 1]; embedding methods score entities and relations in a continuous geometry; knowledge-compilation methods compile the constraint to an arithmetic circuit whose weighted model count (WMC) is differentiable in the inputs. The knowledge-compilation family retains an exact WMC of the constraint as its training signal under partial supervision.

The task we address, ABox-supervised latent concept learning, takes the following form. Each training instance supplies one perceptual input per named individual (e.g. an image of a digit) together with a partial set of ABox literals over an observable signature; the truth values of atoms over a separate latent signature are never directly supervised. The objective is to learn per-individual classifiers for the truth values of latent concept atoms. A WMC layer over a circuit compiled from the ontology supplies the training signal: evaluated with the perception’s per-atom outputs and clamped on the observed evidence, the layer scores how compatible the perception’s predictions are with the ontology, and the gradient steers the perception toward configurations that the constraints admit. When several latent configurations satisfy the same evidence, no method can recover the true labels from supervision alone; per-atom-independent predictors fail to recognize this and collapse to high confidence on a single arbitrary configuration rather than spreading mass over the satisfying ones.

Existing knowledge-compilation NeSy frameworks accept propositional formulas, Datalog programs, or finite-domain rules, but not OWL ontologies directly. Two recent works target description logics: a domino-style reduction of ALCI to a probabilistic circuit that treats the circuit as a regulariser under full label supervision, and a fuzzy approximation of EL++ via Goguen-implication semantics that targets knowledge-base completion without exact WMC or compilation soundness; neither performs partial-supervision concept learning over OWL EL. Embedding methods such as ELEmbeddings and OWL2Vec∗ map ontology structure to a continuous geometry, trading exact entailment for differentiability. A separate body of work on reasoning shortcuts (RS) formally proves that conditional independence among predicted concepts is incompatible with RS-awareness, and develops mitigation strategies (BEARS ensembles, neuro-symbolic diffusion); these results are stated entirely in propositional or Datalog NeSy. OWL 2 EL underpins many production ontologies, so the RS phenomena documented in propositional settings translate directly into uncertainty-modeling failures in deployed ontology-driven systems.

Translations of OWL EL into other formalisms are well established: it is Datalog-rewritable, and probabilistic and fuzzy variants have been studied at length. However, a rewriting yields a reasoning procedure rather than a learning signal, and the probabilistic and fuzzy variants relax or re-specify the model-theoretic semantics rather than compiling it.

Here we present Moose, a method that compiles an EL++ ontology and a finite ABox domain into a Sentential Decision Diagram whose models coincide with ABox interpretations satisfying the entailments of the input ontology, paired with a learning framework that uses the differentiable circuit as the sole supervision channel for latent concept atoms and provides the first RS analysis in an OWL EL setting. Our contributions are:

1. End-to-end OWL 2 EL compilation with full proofs. We compile the EL profile, including role chains R1 ◦ R2 ⊑ S and role hierarchies (the constructs that distinguish SNOMED CT and the Gene Ontology from a propositional or ALCI setting), via ELK-style saturation to an SDD supporting WMC. The four formal contributions are a verified SDD encoding (Theorem 1), the rational DISPONTE distribution-semantics correspondence (Theorem 2), and SCC-compositional factorizations at the Sat and WMC levels (Theorems 3 and 4). All four are mechanized in Lean 4 (no Moose-specific axioms; Sections D and D.10), along with the supporting Lean libraries for ELK saturation, soundness/completeness on EL++, and SDD knowledge compilation, which to our knowledge are the first such formalizations (Section D.1). The closure-augmented variant is correct (Theorem 7) and inference is linear in the SDD (Theorem 8).

2. ABox-supervised latent concept learning under partial axiom observation. We pose a learning task in which a subset of ABox literals over the observable signature is given as evidence (with truth values written true and false, so that they are not confused with the EL++ concepts ⊤ and ⊥), and the goal is to learn per-individual classifiers for the truth values of latent concept atoms (role atoms are observed or marginalized, never classified), to our knowledge the first such formulation over an OWL EL ontology, generalizing DeepProbLog and Semantic Loss to description logic constraints with role chains and role hierarchies.

3. Reasoning-shortcut analysis transposed to OWL EL. We compute family-argmax accuracy, expected calibration error (ECE), and the RS-consistency rate under Moose and two plug-in mitigations (Moose+BEARS and Moose+NeSyDM), and isolate a calibration-vs-accuracy tradeoff: BEARS leads on family-argmax accuracy via ensemble diversification on RS-suspect inputs, NeSyDM leads on calibration (ECE) under symbolic ambiguity.

4. A benchmark suite. A single MNIST-with-ontology benchmark covering three supervision regimes (atomic, relational, and role-chain), together with a fourth experiment on the Pizzaı̈olo synthetic-image dataset that transfers the method to a real expert-authored OWL EL ontology.

Methods. The compilation algorithm compiles an EL++ ontology and a finite ABox domain to an SDD over the ground vocabulary in seven stages; the SDD is built once at startup and reused across every training step. Stage 1 runs the ELK saturation, which derives all entailed subsumptions and role links and records the grounded rule instances that justify each derivation. Stages 2–5 build a propositional encoding of the full saturation closure, including deeply nested existential derivations and cyclic dependency chains, via Clark completion, strongly-connected-component (SCC) detection, time-stamped unrolling, and conjunctive normal form (CNF) conversion. Stages 6–7 ground the saturation onto the finite ABox domain and compile the resulting clauses into the SDD that the differentiable WMC layer evaluates.

The two groups of stages operate at different abstraction levels and serve complementary purposes. Stages 2–5 produce a TBox-level propositional theory whose variables are concept-level atoms such as xC⊑D and x R, including derived complex concepts (e.g. C ⊑ ∃R.∃S.D); the input axiom variables αi in this theory are free, so the theory supports probabilistic ontology reasoning: assigning a weight pi to each αi and computing the WMC gives P (query entailed). Stages 6–7 operate on the ground vocabulary whose variables are ABox atoms C(a) and R(a, b); for NeSy learning all ontology axioms are certain and the WMC literal weights come from a neural network’s per-atom outputs, so the input-axiom tracking of Stages 2–5 is not consumed.

In the NeSy learning use case, Stages 6–7 return to the Stage 1 saturation output and extract the subset relevant for ABox grounding: subsumptions, disjointness, and role links between named concepts. Deeply nested existential derivations that Stages 2–5 process, including those that create cyclic SCCs requiring time-stamped unrolling, have no ABox-level counterpart: the complex concepts produced during saturation (e.g. ∃R.C or ∃R.∃S.D) do not lie in the named signature SigC (O), and the shape-aware extractors of Stage 6 correctly filter them out. Stages 2–5 still serve a diagnostic and validation role: the Clark completion, SCC structure, and CNF size characterize the TBox complexity and verify that the Stage 6 filter captures every ABox-relevant consequence.

Stage 1: ELK saturation. Saturate(O, E) runs the ten ELK completion rules and returns the saturation pair (Σ, Λ), where Σ is the set of derived subsumptions C ⊑ D and Λ the set of derived role links E −→ C, sound and complete with respect to O. We write Sat(O):= Σ ∪ Λ for the saturation closure. For each derived atom the saturation records all grounded rule instances that can derive it (there may be multiple justifications), and these form the input to Stage 2. When the ontology contains existential restrictions or role chains, the saturation may derive non-atomic concepts (e.g. ∃R.C, ∃R.∃S.D); these are internal to the completion and are consumed by Stages 2–5 but filtered out by the shape-aware extractors of Stage 6.

Stages 2–5: TBox-level encoding. The saturation of Stage 1 can be viewed as a monotone Datalog program. Stages 2–5 turn it into a propositional TBox theory: Clark completion replaces each derived atom’s justifications with a biconditional, Tarjan’s algorithm isolates cyclic strongly-connected components, these are broken by SCC-local time-stamped unrolling, and the Tseitin transformation yields an equisatisfiable CNF. With all input-axiom variables true this theory has Sat(O) as its unique model; when the axioms carry weights it supports probabilistic ontology reasoning. For NeSy learning these stages are diagnostic: the deeply nested and cyclic derivations they handle lie outside the named signature and are filtered by the Stage 6 extractors, so the ABox grounding of Stages 6–7 consumes only the Stage-1 saturation.

Stage 6: shape-aware extractors and ABox grounding. Stage 6 extractors return to the Stage 1 saturation output (Σ, Λ) and select the subset that maps to ground ABox atoms over the ground vocabulary. AtomSub emits ¬A(a) ∨ B(a) for every subsumption A ⊑ B in Σ where both A and B are named concepts in SigC (O); Disj emits W i ¬Ai (a) for n-ary atomic disjointness A1 ⊓ · · · ⊓ An ⊑ ⊥ (flattened from any parenthesization); Unsat emits ¬A(a) for atomic A ⊑ ⊥; Links emits the NF3-forward clause ¬E(a) ∨ ¬R(a, b) ∨ C(b) per saturation-derived atomic link (E, R, C) ∈ Λ (i.e. E ⊑ ∃R.C with E, C ∈ SigC (O)), plus an NF4-reverse clause ¬R(a, b) ∨ ¬C(b) ∨ E(a) when L(E, R):= C: (E, R, C) ∈ Λ is a singleton (so the NF4 direction is deterministic). The union of the clauses produced by these extractors is the propositional Horn program Γ over the ground vocabulary; the saturation closure is polynomial by Theorem 6 and grounding multiplies it by at most ∆2.

Stage 7: SDD compilation. Γ is compiled bottom-up into an SDD α that is smooth, decomposable, and deterministic. The role-pinning caveat applies to the Links clause: ELK derives E ⊑ ∃R.C (existential, “some witness”); Moose encodes the propositional clause E(a) ∧ R(a, b) → C(b), which is universal on the named pair. Soundness depends on ∆ being closed and on role atoms over SigoR being pinned by evidence (a Moose-specific encoding choice for the finite-named-domain regime, not an ELK theorem). The differentiable WMC layer traverses α and evaluates WMC(α; w) by the standard smooth/decomposable/deterministic recursion, with literal weights w read from Table 1. Decomposability factors the product at each decision node; determinism makes the prime/sub pairs mutually exclusive, so the sum is plain rather than an inclusion–exclusion. Conditioning on e clamps the literal weight of every observed atom to 0 or 1.

Closure axioms outside the EL profile. OWL EL is open-world and lacks both right-hand-side disjunction and cardinality constructors, so the covering axiom ⊤ ⊑ D0 ⊔ · · · ⊔ DK−1 on an exhaustive family is unstatable in EL. Under partial supervision the WMC gradient on unobserved members of such a family vanishes at every all-False extension (e.g. on MNIST, observing Even(a) without closure leaves the digit posterior uninformative). We therefore optionally append a finite set of closure axioms Φclos to ΓEL on each modeller-declared exhaustive family F: pairwise disjointness, the covering clause W i Di (a), and (when each Di carries a distinguishing property profile πi) profile-keyed reverse implications. We write these three jointly manipulated components as Φclos = Φmutex ∪ Φcover ∪ Φprofile. Two of the three are outside the EL profile but are standard OWL-DL machinery; Moose’s contribution is the ELK-via-SDD infrastructure that absorbs Φclos at the propositional level, so the same compilation yields αEL or αclos with no method change. This absorption is free at the CNF level (Φclos adds at most K 2 m + (K+1)m clauses per declared family: K 2 m mutex, m covering, and up to Km profile-keyed reverse implications), but the polynomial saturation-closure bound of Theorem 6 applies to the EL Horn fragment only and does not transfer to ΓEL ∪ Φclos: covering disjunctions can raise the primal-graph treewidth, and SDD compilation is worst-case exponential in Γ with a O(Γ · 2w) bound under treewidth w; inference remains O(α) in the SDD node count regardless (Theorem 8). Whether closure is needed is ontology- and regime-dependent: a forward-only EL hierarchy under factorized perception leaves the all-false latent assignment consistent with any property evidence, so the WMC gradient is uninformative and closure restores a non-trivial gradient (an architectural softmax head encoding mutex+covering, as DeepProbLog uses via nn(·), achieves the same effect by other means); when forward subsumption alone pins the latent vector, no closure is added. The choice is orthogonal to RS-awareness, which targets the cross-atom factorization at the perception output and is implemented by the BEARS / NeSyDM wrappers.

Inference and RS-aware variants. The differentiable WMC layer supports three inference operations on the same SDD (training loss, conditional posterior, and entailment query), varying only literal weights and evidence. The training loss is L(θ; x, e) = − log WMC(α; pθ (x), e), which coincides with the DeepProbLog marginal loss on this Horn theory by Proposition 1. The conditional posterior Pθ (C(a) x, e) is the ratio of two WMCs with C(a) clamped vs. left free; the perception-free entailment query O ∪e = C(a) holds iff WMC(α; w1/2, e ∪ C(a):=false) = 0 (the 1 2-weighted SDD acts as a satisfiability oracle). All three run in O(α) (Theorem 8). The compilation algorithm is independent of the perception’s output distribution, so RS-a…

Based on this paper, here are the specific improvements I can make to AI systems and what the improved systems can do:

Improvement: Integrate the Moose compilation pipeline (EL++ TBox + finite ABox → SDD with differentiable WMC) as a trainable layer in neural architectures. Replace fuzzy-logic or embedding-based ontology constraints with the exact, Lean-verified SDD encoding.

Capability: The AI system can now learn from partial supervision (e.g., a few observed ABox literals) while enforcing complex OWL EL constraints—including role chains (R1 ◦ R2 ⊑ S) and role hierarchies—with provably sound and complete reasoning. Unlike propositional NeSy methods (DeepProbLog, Semantic Loss), it propagates evidence across multiple individuals and relational structures, achieving 74.6–96.1% accuracy on relational/role-chain tasks versus 38.9–59.6% for baselines.

Improvement: Adopt the RS-consistency analysis and mitigation wrappers (BEARS ensemble diversification, NeSyDM masked discrete diffusion) as plug-in modules for any ontology-constrained perception system.

Improvement: Implement the optional closure axioms (Φclos = mutex + cover + profile-keyed reverse implications) for declared exhaustive families, which the paper shows are necessary to avoid vanishing gradients in partial-supervision settings.

Improvement: Use the Lean 4-mechanized theorems (Theorems 1–4, 7–8) as formal guarantees for the compilation pipeline, ensuring soundness, completeness, and polynomial intermediate sizes.

Improvement: Apply the method's ability to compile any EL++ ontology (not just hand-crafted toy problems) to third-party expert ontologies, as demonstrated with Pizzaı̈olo.

Improvement: Leverage the WMC layer's ability to compute exact conditional posteriors P(C(a) x, e) as ratios of WMCs, rather than committing to a single most-likely configuration.

Improvement: Use the O(α) inference time in the SDD node count (Theorem 8) and the SCC-compositional factorization (Theorems 3–4) to decompose large ontologies into independently compilable components.

Improvement: Extend the weight map to predict unobserved role atoms R(a,b) from perception, rather than fixing them at 1/2.

Summary of what the improved AI system can do: It can learn from partial, noisy observations while enforcing complex, real-world ontology constraints with formal guarantees; it can detect and mitigate reasoning shortcuts that cause overconfident errors; it can handle open-world semantics with closure axioms; it can transfer to third-party expert ontologies without modification; and it can represent multi-witness ambiguity explicitly—all with provable correctness and polynomial-time inference.

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 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 EL++ profile on declared exhaustive families to overcome the limited expressivity of 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"iolo. Moose improves over propositional-NeSy, fuzzy-logic, and ontology embedding baselines, and presents the first reasoning-shortcut analysis in an OWL EL setting.