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-aware methods plug in by replacing pθ (x) in w without modifying α. Moose+BEARS trains a K-encoder ensemble diversified by Kullback–Leibler (KL) divergence against the running ensemble average; Moose+NeSyDM replaces Q i pθ (ci x) with a masked discrete-diffusion qθ, evaluated with both the REINFORCE leave-one-out (RLOO) estimator and an exact-WMC gradient estimator.

Correctness and complexity. The four theorems constitute the formal contribution of Moose: a verified SDD encoding of the ELK-derived saturation, the unconditional rational DISPONTE correspondence, and the SCC-compositional factorizations at the Sat and WMC levels. Each theorem is mechanized in Lean 4; the infrastructure on which they rest (ELK soundness/completeness on EL++ and polynomial-time Sat decidability) is reused unchanged from the ELK literature and remechanized in our Lean library.

Theorem 1 (Verified SDD encoding). For every EL++ ontology O and concepts C, D, there exists an SDD tree t such that: 1. model(t, M) ⇐⇒ Sat(sel(O, M), C, D) for every world M: O → 0, 1; 2. for every weight w, WMC(t, w) = P(O, C, D, w); 3. t = 2O+1 − 1. Theorem 1 is the formal contract of Moose’s compilation step: the SDD’s models are exactly the worlds whose selected sub-ontology ELK-entails C ⊑ D, the SDD’s WMC is the DISPONTE marginal under arbitrary weights, and the worst-case size is the explicit 2O+1 − 1 bound of the Shannon expansion.

Theorem 2 (Rational DISPONTE correspondence). For every EL++ ontology O, every concepts C, D, and every rational weight w, WMCQ cmp(O, C, D), w = PQ (O, C, D, w). The identity holds unconditionally on rational weights: no distributional assumption is required. It is the formal warrant of the standard entailment-as-WMC-zero phrasing of probabilistic DLs (at the uniform prior w ≡ 1 2, WMCQ = 0 iff no world’s sub-ontology entails C ⊑ D), and lifts that phrasing from the propositional encoding to the verified compiled circuit.

Theorem 3 (SCC compositional theorem, Sat level). Let O = O1 ⊎ O2 with disjoint signatures, both components nominal-free and range-chain-safe, O2 consistent (¬ Sat(O2, ⊤, ⊥)), and C, D nominal-free with C, D in the signature of O1. Then Sat(O1 ⊎ O2, C, D) ⇐⇒ Sat(O1, C, D). The result formalizes the intuition that an inferentially irrelevant SCC cannot affect Sat-derivability inside the relevant component, provided the irrelevant component is itself consistent. SCC-wise compilation follows: each SCC can be saturated and compiled in isolation, and the joint posterior recovered by combination.

Theorem 4 (Per-SCC posterior equivalence). Under the hypotheses of Theorem 3, for any uniform per-axiom prior w ≡ c with c > 0, the per-SCC and joint DISPONTE posteriors coincide. In the unnormalized counting case w ≡ 1, PQ (O1 ⊎ O2, C, D, w) = PQ (O1, C, D, w) · 2O2. The multiplicative 2O2 from the irrelevant SCC cancels under posterior normalization, and the same cancellation extends the identity to any c > 0 after factoring out cO1 +O2. This is the WMC-level analogue of Theorem 3: per-SCC compilation is posterior-faithful.

The closure-augmented variant of the SDD (which materializes the per-individual partition constraints on declared exhaustive families) satisfies an analogous correctness theorem (Theorem 7, appendix). Inference is linear in cmp(O, C, D) (Theorem 8, appendix). All proofs and the DeepProbLog equivalence Proposition 1 are in Section D; the implementation index in Section D.10 cross-references every paper claim with its formalized counterpart.

Experiments. We evaluate Moose on two benchmarks: the MNIST-with-ontology benchmark we developed for this work, instantiated under three supervision regimes (atomic property literals, relational ∃R.C evidence, and role-chain evidence); and the Pizzaı̈olo dataset of 4,800 synthetic pizza images generated to conform to the published OWL pizza ontology, which lets us test transfer to a third-party ontology and a different image distribution. Within each benchmark, the experiments share the ontology and differ only in the observable signature, the domain size ∆, and the supplied evidence.

We address five research questions. RQ1–RQ3 test latent digit recovery on OMNIST as the supervision signal grows from a single individual with unary property literals (RQ1), to a pair of individuals connected by an observed r(a, b) role literal under an ∃R.C axiom (RQ2), to a pair connected by observed role literals only through an ELK-derived role-chain consequence (RQ3). RQ4 tests transfer to the pre-existing third-party OWL pizza ontology, restricted to its EL fragment (Pizzaı̈olo). RQ5 asks which RS-mitigation regime works under which conditions: with encoder, ontology, and compiled SDDs fixed, we vary only the output-distribution treatment: an independent per-atom baseline (no logical structure), Moose on the EL theory alone (the DPL surface, Proposition 1), Moose with closure Φclos, and the BEARS / NeSyDM wrappers, across factorized relational, tied symmetric, and high-arity disjunctive ambiguity. The independent baseline (binary cross-entropy, BCE, on observed atoms) is a lower-bound reference that cannot propagate evidence through subsumption, disjointness, or role axioms and so cannot beat chance on latent atoms.

The MNIST ontology and supervision regimes. A single OWL EL ontology OMNIST (14 concepts, 2 roles, 76 axioms) is used in all three MNIST experiments; the experiments differ only in ∆ and the evidence regime, never in the TBox. ELK saturation derives the chain consequence Di ⊑ ∃plus two. D(i+2) mod 10 from the axiom succ ◦ succ ⊑ plus two at compile time. The compiled SDD has 14m + 2m2 ground atoms. A small convolutional neural network (CNN) fθ (2 conv blocks + 2 fully-connected layers, weight-shared across individuals) maps each image to per-atom probabilities; training minimizes L(θ) = − log WMC(αclos; pθ (x), e) with Adam, batch 32, 5 seeds. Exp. 1 (atomic, RQ1) uses ∆ = a with nobs ∈ 1, 2, 3 unary literals over SigoC = Even, Odd, Prime, Composite. Exp. 2 (relational, RQ2) uses ∆ = a, b with the role atom succ(a, b) asserted (digits satisfy digit(b) = (digit(a)+1) mod 10) plus nobs ∈ 1, 2, 3 primality literals. Exp. 3 (role chain, RQ3) flips the asserted role to plus two(a, c) and widens the unary pool to parity and primality; the only chain from a to c is the NF7-derived consequence above. The digit family is declared exhaustive at every individual; Φclos supplies pairwise disjointness, covering, and reverse-implication clauses. Some property profiles uniquely identify the latent digit (e.g. Even(a) ∧ Prime(a) pins D2), while others leave it ambiguous (e.g. Even(a) alone admits D0, D2, D4, D6, D8); RScons on the ambiguous cases measures confident commitment to a wrong digit.

Experiment 4: Pizzaı̈olo (RQ4). Pizzaı̈olo provides 4,800 synthetic pizza images. The canonical pizza ontology contains non-EL constructs (universal restrictions on hasTopping, complement-based definitions such as VegetarianPizza ≡ Pizza ⊓ ¬∃hasTopping.MeatTopping ⊓ ¬∃hasTopping.FishTopping, and cardinality on NumberedPizza); we use only its EL-expressible fragment, restating the four-pizza recipes and property classes as conjunctive subsumption and disjointness axioms, and treating classes whose canonical definitions fall outside EL (e.g. VegetarianPizza) as atomic concepts whose truth values come from the dataset labels rather than from non-EL closure. The method targets the four-pizza subset Mushroom, Cajun, Capricciosa, FourSeasons over 16 topping concepts, with conjunctive per-pizza axioms (e.g. Capricciosa ⊑ Ham⊓Anchovy⊓Olive⊓Peperonata), pairwise pizza disjointness, and disjointness axioms P ⊓ T ⊑ ⊥ for every topping T outside P ’s recipe. EL forward subsumption plus these disjointness axioms pin the topping vector once pizza identity is observed; no out-of-profile closure is added. Track A reveals pizza identity; toppings are latent. We test distribution shift via an OOD split: the four training pizzas all carry Anchovy and Olive together, so a network can score well on the in-distribution split by coupling the two atoms; we hold out five tie-breaker pizzas (Fiorentina, Giardiniera, LaReine, Soho, Veneziana) whose recipes break this co-occurrence. Track B reveals one of four property-class atoms (NonVegetarianPizza, SpicyPizza, RealFrenchPizza, VegetarianPizza); revealing NonVegetarianPizza leaves Cajun, Capricciosa, FourSeasons indistinguishable (a 3-way RS over pizza identity). Track C (the is spicy task in the codebase) adds four axioms Ti ⊑ SpicyTopping for Ti ∈ Jalapeno, Peperonata, PeperoniSausage, Prawn together with SpicyTopping ≡ SpicyPizza (two GCIs; here SpicyTopping acts as a label-class denoting “pizza with a spicy topping”). Symbolic supervision SpicyPizza(a) forces SpicyTopping(a) but the EL theory leaves the witness ambiguous over 24 =16 topping subsets (the multi-witness regime BEARS/NeSyDM target). We train the perception CNN from scratch with batch size 32, 5 seeds, and 60 epochs on Tracks A and B (Track C uses 15 epochs).

Baselines, metrics, and results. We compare Moose against seven baselines. Independent (BCE on observed atoms) is the NeSy-free lower bound. Semantic Loss shares the − log WMC objective but compiles only the directly-stated NF1/NF2 atomic axioms, dropping NF3/NF4/NF7 and ELK saturation, isolating the EL-aware method of §3.2. DeepProbLog hand-codes each MNIST regime as a ProbLog program with one nn(·) digit directive; by Proposition 1 DPL and Moose compute the same loss on the same Horn theory, though that directive is an annotated disjunction, so DPL is not closure-free. Moose+BEARS keeps the factorized perception and αclos but replaces the single encoder with K=5 diversified encoders. Moose+NeSyDM replaces the factorized extractor with a masked-diffusion concept distribution; we evaluate both RLOO and exact-WMC gradient estimators. LTN substitutes a fuzzy product T-norm; ELEmbeddings embeds the EL ontology into ball geometries with a classifier head.

Metrics. The headline tables report the regime’s principal accuracy and ECE, the expected calibration error binned by predicted confidence. The two ontologies do not admit the same accuracy metric. On MNIST the digit family is declared exhaustive and we report AccF, family-argmax accuracy: per individual, the argmax of the WMC posterior over that family. On Pizzaı̈olo we report AccC, per-atom accuracy on the latent slice, since Track C declares no exhaustive family and the decode degenerates on the other two.

Findings on Experiments 1–3 (RQ1–3, RQ5). At ∆=1 (Exp. 1) Moose leads DeepProbLog on AccF (48.1 vs. 42.1). Independent stays near random (AccF = 13.2). BEARS cuts ECE from 10.6 to 3.9 at no cost to accuracy; at ∆=1 there is little diversifiable structure left for the ensemble to exploit. NeSyDM matches Moose on AccF (46.6 and 49.4 for the RLOO and exact estimators vs. 48.1). On the relational and role-chain regimes (Exps. 2–3) Moose dominates DeepProbLog by tens of points on AccF (74.6 vs. 38.9 on Exp. 2; 96.1 vs. 59.6 on Exp. 3): the EL-aware Links extractor propagates evidence across the ∆=2 ground individuals, but the closure clauses Φclos are what make this signal learnable. The ablation in Section F.10 shows the base WMC objective falling to 17.4 and 9.4 (near chance) once Φclos is removed, so the EL compilation supplies the structure and Φclos the identifying constraint, with reasoning-shortcut mitigations partially substituting for the latter. BEARS reduces RScons but gives up a few points of accuracy on Exp. 3 (89.2 vs. 96.1); NeSyDM lags even at tuned (γc, γh). LTN and ELEmbeddings under-perform on AccF (14.5 and 34.8 on Exp. 2): LTN’s ECE saturates near the uniform prior (10.0, information-vacuous), while ELEmbeddings’ lower ECE on Exps. 2–3 (7.2, 6.3) does not translate into accuracy. An inductive held-out-edge split, in which query individuals appear only in relational configurations never supervised, leaves Moose’s accuracy essentially unchanged while NeSyDM collapses to near-chance.

Findings on Experiment 4 (RQ4–5). Track A is an OOD generalization test on five held-out tie-breaker pizzas whose recipes break the Anchovy, Olive co-occurrence admissible on the four training pizzas; on the in-distribution split most methods reach near-perfect topping accuracy, but on the OOD split the Moose family clusters around 67–72% on AccC. Track B is the canonical RS test (3-way symbolic ambiguity: a property-class observation leaves three pizzas indistinguishable). Plain Moose-WMC commits to a single constraint-consistent latent (“Mechanism A” of [41]); BEARS lifts AccC from 84.5 to 87.9 via ensemble diversification on RS-suspect pizzas, and NeSyDM (RLOO) trades a few points of accuracy (78.5) for the lowest ECE of any row (2.6). Track C (is spicy disjunction) is the multi-witness regime NeSyDM was designed for: among the Moose variants BEARS leads on AccC (84.2 vs. 81.0 for plain Moose-WMC) and NeSyDM (exact) leads on ECE (6.9, the column best); LTN matches BEARS on accuracy (84.8, the highest value in the column but not significantly so) at higher ECE (14.1). On both Track B and Track C the Moose-family results separate along an argmax-vs-calibration axis (BEARS leads accuracy, NeSyDM leads ECE). These mitigation effects are sizeable rather than marginal: paired over 20 seeds, BEARS significantly exceeds plain Moose-WMC on both Track B and Track C, and NeSyDM significantly exceeds it on the Track A OOD split. In the symbolically ambiguous regimes it is therefore the RS-mitigation wrapper, not the exact base layer, that is the stronger configuration; the mitigation is doing substantive work, not fine-tuning. This reverses the relational regime (Exps. 2–3), where forward subsumption already pins the latent vector, no residual reasoning shortcut remains to remove, and plain Moose is best; mitigation helps precisely where symbolic ambiguity leaves an RS to exploit. Whether this generalizes beyond the regimes tested here is left to future work.

Conclusion and outlook. Moose compiles OWL 2 EL into a Lean 4-verified weighted-model-counting layer with native role chains and role hierarchies, and supplies the first end-to-end formally verified circuit for an OWL profile together with the first reasoning-shortcut analysis in OWL EL. Empirically, the closure-augmented variant dominates propositional NeSy baselines by tens of points on relational and role-chain regimes, where the EL-aware grounding propagates evidence that propositional encodings cannot and the closure clauses render the resulting signal learnable; under symbolic ambiguity BEARS and NeSyDM separate along an argmax-vs-calibration axis.

Limitations. Three assumptions bound the present results. (i) Scale. Our experiments use ∆ = 2; the compiled SDD grows empirically as ≈ ∆2.9 with a 40× compile-time jump at ∆ = 4. Saturation and grounding are polynomial and the compilation is exact, but we do not demonstrate ontology-scale ABoxes such as SNOMED CT or the Gene Ontology; that regime requires lifted WMC and is the principal open problem. (ii) Finite named domain. Moose learns over a given finite ABox of named individuals; this defines the ABox-supervised task rather than weakening it, but it does not by itself perform open-domain inference over unnamed individuals. (iii) Role-pinning. Soundness of the Links encoding treats an existential as universal on the named pair, assuming role atoms over SigoR are pinned by evidence, a Moose-specific choice for the finite-named-domain regime, not an ELK theorem. The theoretical contribution, a Lean-verified exact compilation and the RS analysis, stands independently of the scaling outcome: it is the learned-perception pipeline at ontology scale, not the correctness result, that the scalability question concerns.

Open directions include lifted WMC for larger ABox domains, ALC rewriting that would extend the same encoding to existential-on-the-left axioms, and evaluation on biomedical ontologies such as SNOMED CT and the Gene Ontology, and link prediction over latent role assertions: the role atoms R(a, b) that the weight map currently fixes at 1 2 when unobserved would instead be predicted from perception, extending the same WMC layer from latent-concept learning to latent-role learning.

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.