Pith. sign in

REVIEW 4 major objections 5 minor 61 references

Moose: Latent concept learning with reasoning-shortcut awareness in $\mathcal{EL}^{++}$

T0 review · 4 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Moose compiles OWL 2 EL ontologies into an exact differentiable reasoning layer, enabling latent concept learning from partial ABox evidence.

desk verdict Lean-verified EL compilation is the real contribution; the ABox-level exactness claim is narrower than the abstract suggests, and the role-pinning caveat deserves a major revision rather than a desk reject. read the letter →

arxiv 2608.12961 v1 pith:7W2VTOMN submitted 2026-08-13 cs.AI

Olga Mashkova , Asaad Mohammedsaleh , Fernando Zhapa-Camacho , Robert Hoehndorf This is my paper · ORCID
classification cs.AI
keywords OWL2ELdescriptionlogicneuro-symboliclearningknowledgecompilationsententialdecisiondiagramweightedmodelcountinglatentconceptreasoningshortcuts
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Moose tries to establish that OWL 2 EL ontologies, the description-logic profile behind SNOMED CT and the Gene Ontology, can be compiled into an exact and differentiable reasoning layer rather than approximated by embeddings or fuzzy relaxations. The paper compiles a finite EL++ ontology into a sentential decision diagram whose weighted model count equals the distribution-semantics marginal of the ontology, making the circuit a faithful supervision channel for learning latent concept classifiers from partial ABox evidence. On relational and role-chain MNIST regimes, the closure-augmented variant reaches 74.6 and 96.1 percent family-argmax accuracy, against 38.9 and 59.6 for a propositional neuro-symbolic baseline, and it reports the first reasoning-shortcut analysis for OWL EL. A reader should care because production ontologies use EL, and existing neuro-symbolic learners accept only propositional theories or Datalog, not ontology axioms with role chains.

What carries the argument

The central object is a sentential decision diagram (SDD), a tractable Boolean circuit whose smooth, decomposable, and deterministic structure makes weighted model counting linear in circuit size. The construction first saturates the ontology with consequence-based completion rules, then extracts only the ABox-relevant consequences: atomic subsumptions, disjointness clauses, unsatisfiable concepts, and existential role links, adding a reverse clause when the witness concept is unique. Those clauses, together with optional closure clauses over exhaustive families, are compiled into the SDD; neural perception outputs become the per-atom literal weights, and the training objective is the negative log weighted model count of the diagram with observed evidence clamped.

What would settle it

Take the ontology with a single axiom $E \sqsubseteq \exists R.C$ and domain $\Delta=\{a,b\}$, with evidence $E(a)=\mathrm{true}$, $\neg C(a)$, $\neg C(b)$, and no role atom for $R$ asserted. Under EL++ semantics no model exists because the existential witness for $E(a)$ can be neither $a$ nor $b$, so the correct marginal probability is zero. Moose's grounded clause set is satisfied by setting $R(a,b)=\mathrm{false}$, giving a nonzero weighted model count and violating the claimed WMC/entailment correspondence on this instance.

Watch

Extended reading notes

Core claim

At the TBox level, the paper's central mathematical discovery is the compilation identity stated in Theorem 2: for every EL++ ontology $O$, every pair of concepts $C,D$, and every rational weight function $w$, the weighted model count of the compiled sentential decision diagram equals the rational distribution-semantics marginal, $\mathrm{WMC}_{\mathbb{Q}}(\mathrm{cmp}(O,C,D),w)=P_{\mathbb{Q}}(O,C,D,w)$. That identity makes the circuit an exact and differentiable oracle for entailment, so one diagram supports a training loss, a conditional posterior, and a perception-free entailment query. At the ABox level, the pipeline grounds the saturated consequence set as Horn clauses over the finite named domain, adds optional closure clauses on modeller-declared exhaustive families, and learns per-individual classifiers for latent concept atoms by maximizing the weighted model count of the evidence. The paper claims that this pipeline outperforms propositional neuro-symbolic baselines by tens of points on relational and role-chain tasks, and that the gain separates cleanly: the EL-aware grounding propagates evidence across individuals, while closure clauses render the latent signal learnable when no exhaustive family is otherwise constrained.

Load-bearing premise

The load-bearing premise is that every observable role atom within the finite named domain is pinned by evidence, so that encoding an existential axiom $E \sqsubseteq \exists R.C$ as the universal Horn clause $\neg E(a) \lor \neg R(a,b) \lor C(b)$ preserves the ontology's models; when a witnessing role is unobserved, the compiled circuit can admit models the ontology does not have.

Editorial extensions

If this is right

  • Any OWL 2 EL ontology with a finite named ABox can supervise latent concept learning without a hand-written propositional translation, preserving role hierarchies and role chains.
  • The weighted-model-count and distribution-semantics identity means training gradients are exact rather than sampled or relaxed, and inference on the SDD is linear in its node count.
  • On the MNIST-style relational and role-chain regimes, the closure-augmented variant beats the propositional baseline by 35.7 and 36.5 points in family-argmax accuracy, but the ablation shows that removing the closure clauses collapses accuracy to near chance.
  • Reasoning-shortcut mitigations transfer from propositional settings to OWL EL: under symbolic ambiguity, ensemble diversification favors accuracy while diffusion-style distributions favor calibration, whereas plain Moose is best when forward subsumption pins the latent vector.
  • The same compiled circuit serves as training loss, posterior estimator, and entailment oracle through one linear-time traversal, so the learned perception and the exact reasoner share a single artifact.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial: the cleanest extension is latent-role learning: if unobserved role atoms are freed from the uniform one-half weight and predicted from perception, the same weighted-model-count layer could supervise role assertions, an open direction the paper itself names.
  • Editorial: the role-pinning caveat draws a sharp boundary for exactness: the method is exact precisely when all observably used witness roles are pinned by evidence, so ontologies with genuinely latent existential witnesses may require explicit witness variables or lifted reasoning.
  • Editorial: because the large MNIST gains depend on closure axioms outside the EL profile, applying the approach to open-world biomedical ontologies requires deciding which families are exhaustive; the reported advantage may track that modelling choice as much as the EL compilation itself.
  • Editorial: scaling to SNOMED-sized knowledge bases is blocked by circuit growth, since the SDD size scales empirically as roughly the square of the domain size with a sharp compile-time jump at four individuals; lifted weighted model counting would be needed.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. Moose compiles an EL++ ontology and a finite ABox domain into a Sentential Decision Diagram (SDD) and uses the SDD's weighted model count as a differentiable supervision signal for learning per-individual classifiers over latent concept atoms. The paper's formal core is a set of four theorems: a verified SDD encoding of the ELK saturation, a rational DISPONTE distribution-semantics correspondence, and SCC-compositional factorizations at the Sat and WMC levels, all claimed to be machine-checked in Lean 4. The empirical part introduces an MNIST-with-ontology benchmark in three supervision regimes (atomic, relational, role-chain) plus a Pizzaiolo transfer track, and reports gains over propositional NeSy, fuzzy, and ontology-embedding baselines, together with a reasoning-shortcut analysis using BEARS and NeSyDM wrappers.

Significance. If the claims hold, the contribution is substantial: a formally verified compilation of an OWL profile into a tractable circuit, a distribution-semantics correspondence for probabilistic ontology reasoning, and the first reasoning-shortcut analysis in an ontology setting. The paper is unusually transparent and careful in several respects: it ships a Lean 4 library with a stated audit-clean axiom footprint, an explicit assumptions table (Table 5), a closure ablation (Section F.10), paired significance tests over 20 seeds (Section F.8), an inductive held-out-edge split (Section F.9), and reproducible code and data. These are genuine strengths. The central caveat, however, is that the four verified theorems concern the TBox-level circuit cmp(O,C,D) over axiom-selection worlds, while the production learning signal is the Stage 6-7 ABox encoding whose soundness rests on an unproven role-pinning assumption that the paper itself labels 'not an ELK theorem.' Because the exactness of the supervision channel is the paper's main claimed advantage over fuzzy and embedding alternatives, this gap is load-bearing.

major comments (4)
  1. [§3.2 (Stage 7), §D.2, Eq. (13)] The four verified theorems certify the TBox-level circuit cmp(O,C,D) over axiom-selection worlds, not the Stage 6-7 ABox encoding used for learning. Stage 6 grounds a saturation link (E,R,C) as the universal Horn clause ¬E(a)∨¬R(a,b)∨C(b), plus an NF4 reverse clause when the witness concept is unique; this is a universal reading of an existential axiom and omits any existence clause. The manuscript itself concedes in Stage 7 and in Limitations (iii) that soundness depends on role atoms over Sig_o_R being pinned by evidence and that this is 'a Moose-specific encoding choice for the finite-named-domain regime, not an ELK theorem.' Section D.2 then asserts without proof that soundness of the four-extractor encoding follows from Theorem 5 under role-pinning. The consequence is load-bearing: the entailment oracle of Eq. (13) can return a false positive because an assignment with E(a)=true and all R(a,b) false is a model of the Horn clauses but not of E⊑∃R.C over a closed domain. Theorem 2, which concerns WMC_Q(cmp(O,C,D),w) for axiom weights, does not cover the ABox-atom weights of Table 1. The paper should either prove a dedicated soundness/completeness theorem for the Stage 6-7 encoding under explicit assumptions (including existence witnesses), or weaken the exactness claims and characterize the approximation error.
  2. [§3.1, Theorem 2, Table 1] Section 3.1 invokes Theorem 2 to assert that the WMC layer's output is a probability under the per-atom product distribution defined by Table 1. But Theorem 2's formal statement is about a different object: cmp(O,C,D) with rational weights on ontology axioms, measuring entailment over axiom-selection worlds. The learning pipeline's weights in Table 1 are per ground ABox atom C(a), R(a,b), and the two WMCs coincide only if a further equivalence is proved. This is not a notation issue: TBox-level worlds index subsets of axioms, while ABox worlds assign truth to ground atoms. The paper should state and prove a transfer lemma for the ABox encoding, or explicitly limit the 'formal contract' claim to the probabilistic-ontology-reasoning use case and describe the learning signal as an approximation.
  3. [§5.1, Experiment 1, Table 1] The role-pinning assumption is not satisfied in one of the reported benchmarks. Experiment 1 uses |∆|=1 with no role evidence, so succ(a,a) and plus_two(a,a) receive weight 1/2 under Table 1. The Stage 6 Links clauses for the ten successor existentials are therefore active in the compiled SDD under the universal reading, and neither Theorem 5 nor Theorem 2 certifies that the resulting WMC equals the distribution-semantics marginal for the Exp-1 training signal. This is not a merely theoretical concern: the paper's own Table 5 concedes that 'unobserved role witnesses are not hypothesized.' The exactness claims should be scoped to regimes in which role-pinning provably holds, with Experiment 1 either excluded from the exactness claim or supplied with a separate argument.
  4. [Abstract, §3.3, §D.5] The abstract and contribution list claim 'polynomial intermediate sizes' as part of the formal contribution, but Section 3.3 states that the polynomial saturation-closure bound of Theorem 6 applies to the EL Horn fragment only and does not transfer to ΓEL∪Φclos, and Section D.5 gives an exponential worst case for SDD compilation under rising treewidth. Since the headline MNIST results use the closure-augmented variant and the closure ablation (Section F.10) shows that most of the empirical gain comes from Φclos, the 'polynomial intermediate sizes' phrasing overstates what is proved for the shipped system. The claims should be qualified so that the reader can see that the polynomial bound applies to the EL fragment and that the closure-augmented pipeline has only an empirical complexity statement.
minor comments (5)
  1. [Table 2 caption and §F.6] The DeepProbLog rows on Pizza tracks A-C are not separate runs, as Section F.6 explains, yet the Table 2 caption does not say so. A reader comparing rows could mistakenly attribute independent performance to DeepProbLog; the caption should carry the same ‡ note as Table 9.
  2. [§F.2 and Table 4] There is an inconsistency in the use of the label 'NF7.' Table 4 lists BBL normal form NF7 as ⊥⊑A, while Section F.2 calls the role-chain axiom succ◦succ⊑plus_two 'NF7.' This notation collision should be corrected, for example by using 'role-chain axiom' instead of NF7 in the experimental section.
  3. [§D.1, Theorem 5] Theorem 5's completeness is conditional on OWL2ELFragment (branches (a)-(e)), and Section A states that the branches are not jointly compatible. The main text should state this condition alongside the theorem, not only in the appendix, to avoid the impression that full EL++ completeness is verified in all cases.
  4. [Table 9, Pizza Track A] Table 9 notes that RScons and F1macro on Track A are computed on the in-distribution eval block, not on the OOD harness. The main text should state this restriction where Track A is discussed, so the reader does not interpret those columns as OOD metrics.
  5. [§5.3, Table 10] The discussion of family-argmax accuracy on Pizza Track B would be clearer if Table 10 appeared earlier in the main text: the current presentation in Section F.7 argues convincingly that AccF is uninformative there, and that argument belongs next to the definition of the Pizza metrics.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the compilation theorems are self-contained and machine-checked, and the latent-label predictions are not fitted to the evaluation labels.

full rationale

The paper's load-bearing formal claims are Theorems 1-4, which are mechanized in Lean 4 with an audit-clean dependency set ({propext, Classical.choice, Quot.sound}) and no Moose-specific axioms. Theorem 2 (WMC_Q(cmp(O,C,D),w) = P_Q(O,C,D,w)) is proved by Shannon decomposition and does not assume the distribution semantics it derives; it is independent support rather than a self-citation or a definitional restatement. The reused ELK saturation results are re-mechanized in the same Lean library rather than imported as black-box axioms, so the correctness of the compilation pipeline does not reduce to a self-citation chain. The ABox-level role-pinning caveat at Stage 7 is explicitly disclosed as a finite-domain encoding choice and a soundness scope assumption, not as a predicted consequence; it is a correctness risk, not a circularity. The empirical claims are also non-circular: latent digit atoms receive no supervised labels, training uses only partial observable literals plus the ontology, and accuracy is scored against labels never seen in the loss; the closure ablation (Table 13) shows that without Phi_clos the base WMC objective collapses to near chance, demonstrating that the reported gains come from the constraints rather than from leakage of the evaluation labels. The DeepProbLog equivalence (Proposition 1) is proved for the EL Horn theory, and self-citations appear only in background/survey contexts, not as load-bearing justification. Accordingly, no fitted parameter is renamed as a prediction, no theorem is equivalent to its input by construction, and no load-bearing premise depends on an unverified self-citation.

Assumptions & free parameters 4 free parameters · 5 assumptions · 1 invented entities

Everything the central claim rests on beyond the ontology itself: the ELK saturation calculus (re-certified in Lean but restricted to a five-branch fragment), SDD compilation correctness (mechanized), the closed finite domain, role-pinning of observable role atoms, and modeller-declared exhaustiveness justifying Phi_clos. The numeric parameters are per-regime hyperparameters tuned on seed 0 (learning rate, BEARS gamma_1, NeSyDM gamma_c and gamma_h) plus the hand-authored profile-keyed reverse-implication clauses; none is fit to the latent labels. No new particles, mediators, or forces are introduced. The heaviest unpayed-for assumption is role-pinning, acknowledged by the authors as 'a Moose-specific encoding choice... not an ELK theorem'.

free parameters (4)
  • Perception learning rate (lr) = 1e-3 (mnist2, pizzaA, pizzaB) or 3e-3 (mnist1, mnist3, pizzaC)
    Tuned per regime on a two-point grid at seed 0, then a 5-seed final (F.4); the F.5 sensitivity analysis shows spread 0.10-0.18 with headline rates at or adjacent to the grid optimum. Standard optimizer tuning, not a fitted scientific constant.
  • BEARS diversity weight gamma_1 = 1.0 on MNIST and pizzaA/pizzaC; 2.0 on pizzaB
    Swept over {0.5,1.0,2.0} per regime on seed 0; gamma_2=0.1 and K=5 are BEARS defaults (E.3, F.4). Influences the RS-mitigation comparison, not the compilation.
  • NeSyDM weights (gamma_c, gamma_h) = Per-regime best of {0.1,1.0} x {1.0,2.0}
    Four-cell RLOO sweep per regime (F.4); beta=10 and T=10 are NeSyDM defaults. The sweep selects the wrapper's calibration-versus-accuracy operating point.
  • Phi_profile profile-keyed reverse implications = 6 clauses per individual on MNIST; none on Pizzaolo
    Hand-authored clauses matching each parity-primality profile to its digit set, part of Phi_clos. Without the full closure package, Experiment 1 collapses to 21.7 (F.10). A structural design choice rather than a fitted number, but it is the main crafted component of the empirical signal.
assumptions (5)
  • standard math ELK saturation calculus is sound and complete for EL++ under the OWL2ELFragment witness (Theorem 5)
    Re-proved in Lean (ELKSDD.ELpp.sound owl2el, complete owl2el); the completeness branch has five preconditions that are not jointly compatible, restricting coverage (Section A).
  • standard math SDD compilation is correct, and WMC is exact on smooth, decomposable, deterministic circuits
    Mechanized in ELKSDD.SDD (compile correct, wmc linear); this is the Darwiche and Choi knowledge-compilation background.
  • ad hoc to paper Role atoms over the observable signature are pinned by the evidence, so the universal encoding of existentials is sound on the named-pair domain
    Stated in Section 3.2 Stage 7 and Limitations (iii); if an observable role atom is unpinned or latent, the NF3/NF4 clause encoding does not correspond to EL++ existential semantics.
  • domain assumption The ABox domain Delta is finite and closed; learning and entailment queries range only over named individuals
    Definition 1; disclosed in Limitations (ii). No open-domain inference over anonymous individuals is performed.
  • domain assumption Exhaustive families are declared by the modeler; covering, mutex, and profile-keyed clauses are appended only for those families
    Section 3.3 and Table 5; the MNIST digit family is declared exhaustive and Phi_clos is added, while Pizzaolo tracks use no out-of-profile closure.
invented entities (1)
  • Closure axiom set Phi_clos (mutex, covering, profile-keyed reverse implications) outside the EL profile
    purpose: Makes latent family members identifiable under partial supervision by enforcing exhaustiveness and mutual exclusion that EL++ cannot express
    The clauses encode modeller-declared domain knowledge (the ten digits are exhaustive and mutually exclusive); no external falsifiable handle is provided, and the F.10 ablation shows the method collapses without them. This is an honest disclosure of where the learning signal comes from.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Moose: Latent concept learning with reasoning-shortcut awareness in $\mathcal{EL}^{++}$." pith.science (2026). https://pith.science/paper/7W2VTOMN

@misc{pith2026260812961,
  author       = {Pith},
  title        = {Pith review of: Moose: Latent concept learning with reasoning-shortcut awareness in $\mathcalEL^++$},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7W2VTOMN}},
  note         = {Machine review of arXiv:2608.12961}
}
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 $\mathcal{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 $\mathcal{EL}^{++}$ profile on declared exhaustive families to overcome the limited expressivity of $\mathcal{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.

Figures

Figures reproduced from arXiv: 2608.12961 by the authors.

Figure 1
Figure 1. End-to-end Moose workflow on OMNIST at ∆={a, b}. The TBox is compiled once via ELK saturation → shape-aware extractors → ΓEL (+Φclos when supplied) → SDD α. The differentiable WMC layer evaluates WMC(α; pθ(x), e) for the training loss, the conditional posterior, and the entailment query [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

61 extracted references · 41 canonical work pages

  1. [1]

    In: Advances in Neural Information Processing Systems 35 (NeurIPS)

    Ahmed, K., Teso, S., Chang, K.W., Van den Broeck, G., Vergari, A.: Semantic probabilistic layers for neuro-symbolic learning. In: Advances in Neural Information Processing Systems 35 (NeurIPS). pp. 29944–29959 (2022). https://doi.org/10. 52202/068431-2171

    work page 2022

  2. [2]

    The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version)

    Alrabbaa, C., Borgwardt, S., Herrmann, S., Kr¨ otzsch, M.: The shape of EL proofs: A tale of three calculi. In: Proceedings of the 38th International Workshop on Description Logics (DL 2025) (2025),https://arxiv.org/abs/2507.21851

    work page Pith review arXiv 2025

  3. [3]

    Nature Genetics25(1), 25–29 (2000).https://doi.org/10.1038/75556

    Ashburner, M., Ball, C.A., Blake, J.A., Botstein, D., Butler, H., Cherry, J.M., Davis, A.P., Dolinski, K., Dwight, S.S., Eppig, J.T., Harris, M.A., Hill, D.P., Issel-Tarver, L., Kasarskis, A., Lewis, S., Matese, J.C., Richardson, J.E., Ringwald, M., Rubin, G.M., Sherlock, G.: Gene ontology: tool for the unification of biology. Nature Genetics25(1), 25–29 ...

    doi:10.1038/75556 2000

  4. [4]

    In: Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning (KR)

    Aspis, Y., Broda, K., Lobo, J., Russo, A.: Embed2Sym: Scalable neuro-symbolic reasoning via clustered embeddings. In: Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning (KR). pp. 421–431 (2022).https://doi.org/10.24963/kr.2022/44

    work page doi:10.24963/kr.2022/44 2022

  5. [5]

    In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI)

    Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI). pp. 364–369 (2005).https://doi.org/10.25368/2022.144

    work page doi:10.25368/2022.144 2005

  6. [6]

    In: Proceedings of the OWLED 2008 DC Workshop on OWL: Experiences and Directions (2008)

    Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope further. In: Proceedings of the OWLED 2008 DC Workshop on OWL: Experiences and Directions (2008)

    work page 2008

  7. [7]

    Artificial Intelligence303, 103649 (2022)

    Badreddine, S., Garcez, A.d., Serafini, L., Spranger, M.: Logic tensor networks. Artificial Intelligence303, 103649 (2022). https://doi.org/10.1016/j.artint. 2021.103649

    arXiv 2022

  8. [8]

    International Journal of Approximate Reasoning52(7), 1073–1094 (2011)

    Bobillo, F., Straccia, U.: Fuzzy ontology representation using OWL 2. International Journal of Approximate Reasoning52(7), 1073–1094 (2011). https://doi.org/10. 1016/j.ijar.2011.05.003

    work page 2011

Show all 61 references
  1. [9]

    In: Advances in Neural Information Processing Systems 38 (NeurIPS), Datasets and Benchmarks Track (2024)

    Bortolotti, S., Marconato, E., Carraro, T., Morettin, P., van Krieken, E., Vergari, A., Teso, S., Passerini, A.: A neuro-symbolic benchmark suite for concept quality and reasoning shortcuts. In: Advances in Neural Information Processing Systems 38 (NeurIPS), Datasets and Bench...

    2024

  2. [10]

    https://hal.science/hal-04401953 (2024), dataset DOI:https://doi.org/10.5281/zenodo.10165941

    Bourguin, G., Lewandowski, A.: Pizza¨ ıolo dataset: Des images synth´ etiques on- tologiquement explicables. https://hal.science/hal-04401953 (2024), dataset DOI:https://doi.org/10.5281/zenodo.10165941

    2024 doi

  3. [11]

    Proceedings of the AAAI Conference on Artificial Intelligence33(01), 2736–2743 (2019)

    Carral, D., Gonz´ alez, L., Koopmann, P.: From Horn-SRIQ to Datalog: A data- independent transformation that preserves assertion entailment. Proceedings of the AAAI Conference on Artificial Intelligence33(01), 2736–2743 (2019). https: //doi.org/10.1609/aaai.v33i01.33012736

    2019 doi

  4. [12]

    In: Proceedings of the 27th International Workshop on Description Logics (DL)

    Ceylan, ˙I.˙I., Pe˜ naloza, R.: Bayesian description logics. In: Proceedings of the 27th International Workshop on Description Logics (DL). CEUR Workshop Proceedings, vol. 1193, pp. 447–458 (2014)

    2014

  5. [13]

    Journal of Automated Reasoning58(1), 67–95 (2017)

    Ceylan, ˙I.˙I., Pe˜ naloza, R.: The bayesian ontology language BEL. Journal of Automated Reasoning58(1), 67–95 (2017). https://doi.org/10.1007/ s10817-016-9386-0

    2017

  6. [14]

    Artificial Intelligence172(6-7), 772–799 (2008) 18 Mashkova et al

    Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artificial Intelligence172(6-7), 772–799 (2008) 18 Mashkova et al

    2008

  7. [15]

    Machine Learning110(7), 1813–1845 (2021).https://doi.org/10.1007/s10994-021-05997-6

    Chen, J., Hu, P., Jimenez-Ruiz, E., Holter, O.M., Antonyrajah, D., Horrocks, I.: OWL2Vec*: embedding of OWL ontologies. Machine Learning110(7), 1813–1845 (2021).https://doi.org/10.1007/s10994-021-05997-6

    2021 doi

  8. [16]

    IEEE Transactions on Knowledge and Data Engineering37(7), 4193–4212 (2025)

    Chen, J., Mashkova, O., Zhapa-Camacho, F., Hoehndorf, R., He, Y., Horrocks, I.: Ontology embedding: A survey of methods, applications and resources. IEEE Transactions on Knowledge and Data Engineering37(7), 4193–4212 (2025). https: //doi.org/10.1109/TKDE.2025.3559023

    2025

  9. [17]

    In: Proceedings of the 27th AAAI Conference on Artificial Intelligence (2013)

    Choi, A., Darwiche, A.: Dynamic minimization of sentential decision diagrams. In: Proceedings of the 27th AAAI Conference on Artificial Intelligence (2013). https://doi.org/10.1609/aaai.v27i1.8690

    2013 doi

  10. [18]

    In: Gallaire, H., Minker, J

    Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293–322. Plenum Press (1978). https://doi.org/10.1007/ 978-1-4684-3384-5_11

    1978

  11. [19]

    Machine Learning112(9), 3293–3331 (2023).https://doi.org/10.1007/s10994-023-06310-3

    Daniele, A., van Krieken, E., Serafini, L., van Harmelen, F.: Refining neural network predictions using background knowledge. Machine Learning112(9), 3293–3331 (2023).https://doi.org/10.1007/s10994-023-06310-3

    2023 doi

  12. [20]

    In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI)

    Darwiche, A.: SDD: A new canonical representation of propositional knowledge bases. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI). pp. 819–826 (2011). https://doi.org/10.5591/978-1-57735-516-8/ IJCAI11-143

    2011 doi

  13. [21]

    Journal of Artificial Intelligence Research17, 229–264 (2002).https://doi.org/10.1613/jair.989

    Darwiche, A., Marquis, P.: A knowledge compilation map. Journal of Artificial Intelligence Research17, 229–264 (2002).https://doi.org/10.1613/jair.989

    2002 doi

  14. [22]

    Studies in Health Technology and Informatics121, 279–290 (2006)

    Donnelly, K.: SNOMED-CT: The advanced terminology and coding system for eHealth. Studies in Health Technology and Informatics121, 279–290 (2006)

    2006

  15. [23]

    In: Proceedings of the 34th International Conference on Machine Learning (ICML)

    Guo, C., Pleiss, G., Sun, Y., Weinberger, K.Q.: On calibration of modern neural networks. In: Proceedings of the 34th International Conference on Machine Learning (ICML). pp. 1321–1330 (2017)

    2017

  16. [24]

    In: Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence (AAAI)

    Guti´ errez-Basulto, V., Jung, J.C., Lutz, C., Schr¨ oder, L.: A closer look at the probabilistic description logic Prob-EL. In: Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence (AAAI). pp. 197–202 (2011). https://doi. org/10.1609/aaai.v25i1.7856

    2011 doi

  17. [25]

    Database2021, baab069 (2021)

    Jackson, R.C., Matentzoglu, N., Overton, J.A., Vita, R., Balhoff, J.P., Buttigieg, P.L., Carbon, S., Courtot, M., Diehl, A.D., Dooley, D.M., Duncan, W.D., Harris, N.L., Haendel, M.A., Lewis, S.E., Natale, D.A., Osumi-Sutherland, D., Ruttenberg, A., Schriml, L.M., Smith, B., St...

    2021 doi

  18. [26]

    Journal of Automated Reasoning 53(1), 1–61 (2014).https://doi.org/10.1007/s10817-013-9296-3

    Kazakov, Y., Kr¨ otzsch, M., Simˇ c´ ık, F.: The incredible ELK: From polynomial pro- cedures to efficient reasoning with EL ontologies. Journal of Automated Reasoning 53(1), 1–61 (2014).https://doi.org/10.1007/s10817-013-9296-3

    2014 doi

  19. [27]

    In: Proceedings of the 3rd International Conference on Learning Representations (ICLR) (2015)

    Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization. In: Proceedings of the 3rd International Conference on Learning Representations (ICLR) (2015)

    2015

  20. [28]

    Kool, W., van Hoof, H., Welling, M.: Buy 4 REINFORCE samples, get a baseline for free! In: Workshop on Deep Reinforcement Learning Meets Structured Prediction (ICLR Workshop) (2019)

    2019

  21. [29]

    In: Proceedings of the 41st International Conference on Machine Learning (ICML)

    van Krieken, E., Minervini, P., Ponti, E.M., Vergari, A.: On the independence assumption in neurosymbolic learning. In: Proceedings of the 41st International Conference on Machine Learning (ICML). PMLR, vol. 235 (2024) Moose 19

    2024

  22. [30]

    In: Advances in Neural Information Processing Systems 39 (NeurIPS) (2025)

    van Krieken, E., Minervini, P., Ponti, E.M., Vergari, A.: Neurosymbolic diffusion models. In: Advances in Neural Information Processing Systems 39 (NeurIPS) (2025)

    2025

  23. [31]

    In: Proceedings of the 19th Confer- ence on Neurosymbolic Learning and Reasoning (NeSy)

    van Krieken, E., Minervini, P., Ponti, E.M., Vergari, A.: Neurosymbolic reasoning shortcuts under the independence assumption. In: Proceedings of the 19th Confer- ence on Neurosymbolic Learning and Reasoning (NeSy). Proceedings of Machine Learning Research, vol. 284, pp. 1–18 (2025)

    2025

  24. [32]

    In: Advances in Neural Information Processing Systems 36 (NeurIPS) (2023).https://doi.org/10.52202/075280-1069

    van Krieken, E., Thanapalasingam, T., Tomczak, J.M., van Harmelen, F., ten Teije, A.: A-NeSI: A scalable approximate method for probabilistic neurosymbolic inference. In: Advances in Neural Information Processing Systems 36 (NeurIPS) (2023).https://doi.org/10.52202/075280-1069

    2023 doi

  25. [33]

    Kr¨ otzsch, M.: Efficient Inferencing for OWL EL, pp. 234–246. Springer Berlin Heidelberg (2010).https://doi.org/10.1007/978-3-642-15675-5_21

    2010 doi

  26. [34]

    Nature Machine Intelligence6, 220–228 (2024)

    Kulmanov, M., Guzm´ an-Vega, F.J., Duek Roggli, P., Lane, L., Arold, S.T., Hoehndorf, R.: Protein function prediction as approximate semantic entail- ment. Nature Machine Intelligence6, 220–228 (2024). https://doi.org/10.1038/ s42256-024-00795-w

    2024

  27. [35]

    Bioinformatics 38(Supplement 1), i238–i245 (2022)

    Kulmanov, M., Hoehndorf, R.: DeepGOZero: improving protein function prediction from sequence and zero-shot learning based on ontology axioms. Bioinformatics 38(Supplement 1), i238–i245 (2022). https://doi.org/10.1093/bioinformatics/ btac256

    2022 doi

  28. [36]

    In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI)

    Kulmanov, M., Liu-Wei, W., Yan, Y., Hoehndorf, R.: EL embeddings: Geometric construction of models for the description logic EL ++. In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI). pp. 6103–6109 (2019).https://doi.org/10.2...

    2019 doi

  29. [37]

    CoRR abs/2601.14894(2026).https://doi.org/10.48550/arXiv.2601.14894

    Lazzari, N., Presutti, V., Vergari, A.: To neuro-symbolic classification and be- yond by compiling description logic ontologies to probabilistic circuits. CoRR abs/2601.14894(2026).https://doi.org/10.48550/arXiv.2601.14894

    2026 doi

  30. [38]

    In: Proceedings of the ACM on Programming Languages (PLDI) (2023)

    Li, Z., Huang, J., Naik, M.: Scallop: A language for neurosymbolic programming. In: Proceedings of the ACM on Programming Languages (PLDI) (2023). https: //doi.org/10.1145/3591280

    2023 doi

  31. [39]

    In: Advances in Neural Informa- tion Processing Systems 31 (NeurIPS)

    Manhaeve, R., Dumanˇ ci´ c, S., Kimmig, A., Demeester, T., De Raedt, L.: Deep- ProbLog: Neural probabilistic logic programming. In: Advances in Neural Informa- tion Processing Systems 31 (NeurIPS). pp. 3753–3763 (2018)

    2018

  32. [40]

    CoRR abs/2402.12240(2024).https://doi.org/10.48550/arXiv.2402.12240

    Marconato, E., Bortolotti, S., van Krieken, E., Passerini, A., Teso, S., Vergari, A.: BEARS make neuro-symbolic models aware of their reasoning shortcuts. CoRR abs/2402.12240(2024).https://doi.org/10.48550/arXiv.2402.12240

    2024 doi arXiv

  33. [41]

    In: Advances in Neural Information Processing Systems 36 (NeurIPS)

    Marconato, E., Passerini, A., Teso, S., Vergari, A.: Not all neuro-symbolic concepts are created equal: Analysis and mitigation of reasoning shortcuts. In: Advances in Neural Information Processing Systems 36 (NeurIPS). pp. 72507–72539 (2023). https://doi.org/10.52202/075280-3170

    2023 doi

  34. [42]

    arXiv preprintabs/2412.08739(2024),https://arxiv.org/abs/2412.08739

    Mishra, A., Tahar, S.: VEL: A formally verified reasoner for OWL2 EL profile. arXiv preprintabs/2412.08739(2024),https://arxiv.org/abs/2412.08739

    2024 arXiv

  35. [43]

    In: Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI)

    Pryor, C., Dickens, C., Augustine, E., Albalak, A., Wang, W.Y., Getoor, L.: NeuPSL: Neural probabilistic soft logic. In: Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI). pp. 4145–4153 (2023). https://doi. org/10.24963/ijcai.2023/461

    2023 doi

  36. [44]

    Semantic Web6(5), 477–501 (2015)

    Riguzzi, F., Bellodi, E., Lamma, E., Zese, R.: Probabilistic description logics under the distribution semantics. Semantic Web6(5), 477–501 (2015). https: //doi.org/10.3233/SW-140154 20 Mashkova et al

    2015 doi

  37. [45]

    Nature Biotechnology25(11), 1251–1255 (2007)

    Smith, B., Ashburner, M., Rosse, C., Bard, J., Bug, W., Ceusters, W., Goldberg, L.J., Eilbeck, K., Ireland, A., Mungall, C.J., Leontis, N., Rocca-Serra, P., Ruttenberg, A., Sansone, S.A., Scheuermann, R.H., Shah, N., Whetzel, P.L., Lewis, S.: The OBO Foundry: coordinated evolu...

    2007 doi

  38. [46]

    https://github.com/ owlcs/pizza-ontology, manchester University tutorial OWL ontology

    Stevens, R., Drummond, N., Rector, A.: The pizza ontology. https://github.com/ owlcs/pizza-ontology, manchester University tutorial OWL ontology

  39. [47]

    SIAM Journal on Computing1(2), 146–160 (1972).https://doi.org/10.1137/0201010

    Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing1(2), 146–160 (1972).https://doi.org/10.1137/0201010

    1972 doi

  40. [48]

    In: Description Logic, Theory Combination, and All That, Lecture Notes in Computer Science, vol

    Tena Cucala, D., Cuenca Grau, B., Horrocks, I.: 15 years of consequence-based reasoning. In: Description Logic, Theory Combination, and All That, Lecture Notes in Computer Science, vol. 11560, pp. 573–587. Springer (2019). https: //doi.org/10.1007/978-3-030-22102-7_27

    2019 doi

  41. [49]

    Genetics 224(1), iyad031 (2023).https://doi.org/10.1093/genetics/iyad031

    The Gene Ontology Consortium: The gene ontology knowledgebase in 2023. Genetics 224(1), iyad031 (2023).https://doi.org/10.1093/genetics/iyad031

    2023 doi

  42. [50]

    In: Siekmann, J.H., Wrightson, G

    Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning: Classical Pa- pers on Computational Logic 1967–1970, pp. 466–483. Springer (1983). https: //doi.org/10.1007/978-3-642-81955-1_28

    1983 doi

  43. [51]

    In: Proceedings of the 35th International Conference on Machine Learning (ICML)

    Xu, J., Zhang, Z., Friedman, T., Liang, Y., Van den Broeck, G.: A semantic loss function for deep learning with symbolic knowledge. In: Proceedings of the 35th International Conference on Machine Learning (ICML). PMLR, vol. 80, pp. 5498–5507 (2018)

    2018

  44. [52]

    In: Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI) (2020)

    Yang, Z., Ishay, A., Lee, J.: NeurASP: Embracing neural networks into answer set programming. In: Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI) (2020). https://doi.org/10.24963/ijcai.2020/ 243

    2020 doi

  45. [53]

    In: Proceedings of the 34th ACM International Conference on Information and Knowledge Management (CIKM) (2025)

    Zhao, Y.: Fast and faithful: Scalable neuro-symbolic learning and reasoning with differentiable fuzzy EL ++. In: Proceedings of the 34th ACM International Conference on Information and Knowledge Management (CIKM) (2025). https: //doi.org/10.1145/3770854.3780220

    2025

  46. [54]

    entailment-as-WMC-zero

    Zhapa-Camacho, F., Kulmanov, M., Hoehndorf, R.: mOWL: Python library for machine learning with biomedical ontologies. Bioinformatics39(1), btac811 (2023). https://doi.org/10.1093/bioinformatics/btac811 Moose 21 AEL ++ syntax, semantics, and ELK calculus This appendix collects ...

    2023 doi

  47. [55]

    Each ground atomA(a)∈V ∆ O becomes aprobabilistic factp θ(A(a)) ::A(a)

  48. [56]

    Each definite Horn clause ¬B1∨···∨¬B k∨H∈Γ EL (AtomSub,Unsat, and Linksshapes) becomes a DatalogruleH:-B 1,...,B k

  49. [57]

    Loss objects

    Each non-Horn atomic-disjointness clause ¬A1∨···∨¬A n (Disjshape) becomes a ProbLogintegrity constraint:-A 1,...,A n. Loss objects. LMoose/EL(θ;x, e) := −logWMC (αEL;pθ(x), e) is the Semantic- loss WMC objective of§3.4 on the EL theory alone (no closure axioms); LDPL(θ;x, e) :...

    2018

  50. [58]

    Perception forward.The neural extractor fθ :X|∆|→ [0, 1]|V∆ O| maps the input tuple to a per-atom probability vectorpθ(xi), factorized asQ ℓpθ(ℓ| xi) (the marginal-independence factorization targeted by the RS literature,§2.2)

  51. [59]

    Evidencee i clamps observed literals

    Literal-weight assignment.The atom-weight map of Table 1 routes pθ(ℓ| xi) to literalℓand 1−p θ(ℓ|x i) to¬ℓ. Evidencee i clamps observed literals

  52. [60]

    Smoothness, decomposability, and determinism (Section D) make each sum disjoint and each product over disjoint scopes, so the result is exact

    SDD WMC traversal.The post-order traversal visits each node once (memo- ized by node id) and accumulates the WMC value (Equation (8)) in O(|α|) time. Smoothness, decomposability, and determinism (Section D) make each sum disjoint and each product over disjoint scopes, so the r...

  53. [61]

    diff” is the mean per-seed difference (Moose − baseline); “Holm p

    Backward pass.PyTorch autograd composes the backward pass through the same WMC traversal at O(|α|) additional cost, plus the perception back- bone’s own backward pass. Every intermediate WMC value is the prod- uct/sum of literal weights, hence differentiable in θ via the chain...

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.