Reason-able embeddings are recently proposed embeddings for knowledge bases (KBs) in the description logic ℒ capable of casting multiple KBs into a single latent space using a transferable neural reasoner. While they exhibit remarkable performance on real-world KBs, it is so far unknown what are their exact limits. In this paper, we systematically investigate their performance using a set of synthetic KBs in the description logic ℰℒ, a subset of ℒ. We use the proof length as a measure of reasoning complexity and present a random KB generator taking the proof length into account. We train the reason-able embeddings with and without transfer learning and investigate whether the complexity of the training set and the test set is related to the reasoning performance of the embeddings and their neural reasoner.
The past 10 years brought numerous solutions for embedding concepts from knowledge bases
(KBs) into high-dimensional latent spaces, from a relatively simple TransE to complex
architectures such as recurrent transformers [
Recently proposed reason-able embeddings are a combination of these two trends, ofering
learnable embeddings for KBs with complex semantics and a transferable, neural reasoner [
To facilitate reproducibility we publish the experimental code in Python in a GitHub repository at https://github.com/jpotoniec/reasonable-embeddings/tree/main/src/elpp.
The contributions of the paper are as follows:
• A way to measure reasoning complexity by means of the proof length, described in
subsection 2.2. It exploits a preexisting reasoning algorithm by Baader et al. [
• Experimental evaluation and analysis presented in section 3.
Neither the description logic ℰ ℒ (presented in subsection 2.1) nor the reason-able embeddings (described in subsection 2.3) are contributions of this work, and they are presented here only to make the paper self-contained.
The rest of the paper is organized as follows: subsection 2.1 introduces the DL ℰ ℒ, subsection 2.2 explains how we measure the complexity, the reason-able embeddings are introduced in subsection 2.3, we describe the KB generator in subsection 2.4, and the details of the employed dataset in subsection 2.5. In subsections of section 3, we report the answers to the posed research questions. We discuss the results and conclude in section 4.
2.1. The description logic ℰ ℒ
Description logics (DLs) are a family of logics developed for their desirable computational
properties, to be used in computer systems requiring formal semantics and reasoning capabilities.
In this paper, we concentrate on the DL ℰ ℒ, one of the simplest of practical use [
Concepts in ℰ ℒ are constructed inductively from a set of constructors, a set of atomic concepts , and a set of atomic roles . Their semantics is defined in terms of an interpretation ℐ = (Δℐ , · ℐ ), where Δℐ is a non-empty domain, and · ℐ is the interpretation function, mapping every atomic concept to ℐ ⊆ Δℐ , and every atomic role to ℐ ⊆ Δℐ × Δℐ . Since ℰ ℒ has formal semantics, it is possible to extend · ℐ to arbitrary concepts, summarized in Table 1.
A ℰ ℒ KB consists of a set of subsumption axioms ⊑ , and we say that ℐ is a model of the KB if for every such axiom ℐ ⊆ ℐ . In the DLs, one of the core problems is the subsumption problem, i.e., given two concepts , , and a KB , deciding whether a subsumption ⊑ holds in every model of the KB, denoted |= ⊑ . One of the interesting properties of ℰ ℒ is that there exists a polynomial algorithm for solving the subsumption problem. Syntax and semantics of ℰℒ. , denote arbitrary concepts and an arbitrary role. { ∈ Δℐ : ∃ ∈ Δℐ (, ) ∈ ℐ ∧ ∈ ℐ} to a KB in normal form in polynomial time.
In this paper, we call a subsumption ⊑ an atomic subsumption if , ∈ ∪ {⊥, ⊤}. If |= ⊑ , we say the subsumption follows from the KB.
Throughout this work, we are interested in KBs in the normal form, where the axioms
must be of one of the following forms: ⊑ , ⊓ ⊑ , ⊑ ∃., ∃. ⊑ , where
, ∈ ∪ {⊤} and ∈ ∪ {⊤, ⊥}. It was shown that any ℰ ℒ KB can be transformed
Since we consider only KBs in the normal form, to solve the subsumption problem, we can apply
classification
a rule-based algorithm presented in [
We extend the algorithm to keep track, for every atomic subsumption, of the shortest proof, i.e, a set of rules and their parameters that must be executed in order to generate this particular conclusion. The algorithm starts by creating a set () = {(, ∅), (⊤, ∅)} for every ∈ ∪ {⊤, ⊥}, and a set () = ∅ for every ∈ . Then, rules presented in Table 2 are executed to update the sets () and () until a fixpoint is not reached, i.e., there are changes to () or to (). After the algorithm terminates, () represents the subsumption hierarchy: if (, ) ∈ (), it means that |= ⊑ and at least | | rule executions are necessary to prove it. We call | | the proof length of ⊑ and use it as a complexity measure of atomic subsumptions throughout the paper. It must be noted that this measure is defined only for subsumptions that follow from a KB and that it measures the length of the shortest proof, not any proof. However, since it is supposed to measure reasoning complexity, we believe the shortest proof is the right choice, as it denotes the minimal number of reasoning steps one must make in order to prove a given subsumption, and all the rules seem to be of comparable complexity.
As an example, consider the following KB: = { ⊑ , ⊑ , ⊓ ⊑ , ⊑ ∃., ∃. ⊑ ,
⊑ ⊥}. Unconventionally, we use Greek letters to clearly distinguish concept names present in the KB from the variable names used in the rules. We will consider a few steps of the algorithm, and we chose one possible order of execution for ease of explanation. First, {(, ∅), (⊤, ∅)}, ( ) = {(, ∅), (⊤, ∅)}, () = ∅. Next, the rules are executed: sets (· ) and (· ) are initialized: ( ) = {(, ∅), (⊤, ∅)}, ( ) = {(, ∅), (⊤, ∅)}, ( ) = 1The term usually denotes a much broader set. However, we concentrate only on atomic subsumptions in the paper and thus can hack the term without introducing ambiguity.
CR1 If (′, ′ ) ∈ (), ′ ⊑ ∈ , (, · ) ̸∈ () or (, ) ∈ () and | | < ||, then () ←
()∖{(, )} ∪ {(, )}, where = ′ ∪ {(CR1, , ′, )} If ′ is known to be a superclass of , it is asserted in the KB that ′ ⊑ , and either is not known to be a superclass of or it is known, but the proof is longer than can be achieved by using this rule, then add/replace the existing proof with the new proof .
CR2 If (1, 1 ), (2, 2 ) ∈ (), 1 ⊓ 2 ⊑ ∈ , (, · ) ̸∈ () or (, ) ∈ () ()∖{(, )} ∪ {(, )}, where = 1 ∪ 2 ∪ ′ ∪ {(CR4, , , , ′, )} () and | | < | |, then () ←
()∖{(, )} ∪ {(, )}, where = ∪ from the KB. Each rule is first presented using formal symbols, and then a corresponding textual description is given. (, · ) ̸∈ is an abbreviation for ∀ (, ) ̸∈ .
{(, ∅), (⊤, ∅), (, {(CR1, , , 2. CR1 for = ′
= , isfied: (, ∅ ) ∈ ( ), ) ) } } ⊑
proof can thus be computed as {(, ∅), (⊤, ∅), (, {(CR1, , , 3. CR2 for = , 1 = , 2
= , {(CR1, , , ( ), ⊓ ) . }
The conditions are satisfied: ⊑ ∈ , (, · )
̸∈ If is known to be a subclass of ∃., ′ is known to be a superclass of , it is asserted in the KB that ∃.′ ⊑ , and either is not known to be a superclass of or it is known, but the proof is longer than can be achieved by using this rule, then add/replace the existing proof with the new proof .
CR5 If ((, ), ) ∈ (), (⊥, ) ∈ (), (⊥, · ) ̸∈ () or (⊥, ) ∈ () and | | < | |, then () ← ()∖{(⊥, )} ∪ {
(⊥, )}, where = ∪ ∪ {(CR5, , , )} If is known to be a subclass of ∃., is known to be an unsatisfiable concept, and either is not known to be an unsatisfiable concept or it is known, but the proof is longer than can be achieved by using this rule, then add/replace the existing proof with the new proof . 1. CR1 for = ′ = , = and ′ = . The conditions are satisfied: (, ∅
) ∈ ( ), computed as = ⊑ ∅ ∪ {(CR1, , , ∈ and (, ·
) ̸∈ ( ). The new proof can thus be )} and included in the set ( ): ( ) = {(CR2, , 1, 2, )} and | | < ||, then () ← {(3, , ′, , )} | | < ||, then () ← If it is known that 1 and 2 are superclasses of , it is asserted in the KB that 1 ⊓ 2 ⊑ , and either is not known to be a superclass of or it is known, but the proof is longer than can be achieved by using this rule, then add/replace the existing proof with the new proof . CR3 If (′, ′ ) ∈ (), ′ ⊑ ∃. ∈ , ((, ), · ) ̸∈ () or ((, ), ) ∈ () and ()∖{((, ), )} ∪ {((, ), )}, where = ′ ∪ by using this rule, then add/replace the existing proof with the new proof .
If ′ is known to be a superclass of , it is asserted in the KB that ′ ⊑ ∃., and either is not known to be a subclass of ∃. or it is known, but the proof is longer than can be achieved CR4 If ((, ), ) ∈ (), (′, ′ ) ∈ (), ∃.′ ⊑ ∈ , (, · ) ̸∈ () or (, ) ∈ )}), (, {(CR1, , , ) ) } } = and ′ ∅ .
The conditions are sat∈ =
and (, · ) ∅ ∪ {(CR1, , , ̸∈ ( ).
The new ) } and thus: ( ) = ∅ = = , 1 = {(CR1, , ,
)}, 2 (, 1 ) ∈
( )), (, 2 ) ().
The new proof can thus = ∈ be computed as = 1 ∪ 2 ∪ {(CR2, , , , )}, and we arrive at: ( ) = {(, ∅), (⊤, ∅), (, {(CR1, , , )}), (, {(CR1, , , )}), (, {(CR1, , , ), (CR1, , , ), (CR2, , , , )})} 4. CR3 for = ′ = , = , ′ = ∅. The conditions are satisfied: (, ∅) ∈ ( ), ⊑ ∃. ∈ , ((, ), · ) ̸∈ (). The new proof can thus be computed as = {(3, , , , )} and () can be updated: () = {((, ), {(3, , , , )})}. 5. CR4 for = , = , ′ = , = , = {(3, , , , )}, ′ = ∅, = {(CR1, , , ), (CR1, , , ), (CR2, , , , )}. The conditions are satisfied: ((, ), ) ∈ (), (, ∅) ∈ ( ), ∃. ⊑ ∈ , and (, ) ∈ ( ). This application of a rule is diferent from previous ones: there already is a proof ( ), and it must be determined whether it can be replaced. The new proof is thus computed as = {(3, , , , )}∪∅∪{(4, , , , , )}, and we conclude it is shorter than the preexisting proof, since | | = 3 > | | = 2. We thus proceed with updating ( ), which now becomes: ( ) = {(, ∅), (⊤, ∅), (, {(CR1, , , )}), (, {(CR1, , , )}), (, {(3, , , , ), (4, , , , , )})} 6. CR1 for = ′ = , = ⊥, ′ = ∅. The conditions are satisfied: (, ∅) ∈ ( ), ⊑ ⊥ ∈ and (⊥, · ) ̸∈ ( ). The new proof can thus be computed as = ∅ ∪ {(CR1, , , ⊥)} and included in the set ( ): ( ) = {(, ∅), (⊤, ∅), (⊥, {(CR1, , , ⊥)})}. 7. CR5 for = , = , = {(3, , , , )}, = {(CR1, , , ⊥)}. The conditions are satisfied: ((, ), ) ∈ () and (⊥, ) ∈ ( ). The new proof can thus be computed as = {(3, , , , )} ∪ {(CR1, , , ⊥)} ∪ {(5, , , )} and ( ) can be extended with (⊥, ).
The presented example covers all the proposed rules and the crucial part, namely, replacing longer proofs with shorter ones. While it does not present the entirety of the execution for the given KB, nor the termination condition by reaching a fixpoint, we can still read proof lengths (albeit - since the algorithm did not terminate - not necessarily the shortest), as seen in item 5.
A similar idea is present in the research on DLs under the term justifications , which
concentrates on computing a minimal subset of KB for a subsumption to follow from it [
Exploiting the properties of rule-based reasoning for lightweight DLs was also used in
the context of finding unexplainable triples in RDF graphs [
Reason-able embeddings are a recently proposed framework to compute embedding vectors
for concepts in the ℒ DL [
The neural reasoner consists of two parts: a reasoner head, which is a binary classifier that, given two concept embeddings from the same KB, answers whether one of the concepts is a subclass of the other; and a set of neural operators, which correspond to the logical operators of ℒ and can, e.g., compute the embedding of an intersection of two concepts given the embeddings of those concepts.
In [
Both training and testing a neural reasoner require subsumptions along with a binary label denoting whether a subsumption follows from the corresponding KB or not. We call such a pair an example. Since the label is contextual w.r.t. a KB, it is necessary to keep track of which example is related to which KB. However, this information is not a part of an example and is not presented to the neural reasoner during training. The subsumptions themselves may be synthetic, as long as the label associated with them is correct.
A two-step procedure requires two-level separation into training and test set: first, there is a training set of KBs used to jointly train the reasoner and the embeddings, and there is a test set of KBs used to assess the quality of the trained, frozen reasoner. However, embeddings for the KBs in the test must somehow be trained. Thus, for each KB, be it from the training set or from the test set, a training set and a test set of examples must be constructed. The training set is used to train embeddings for the KB, while the test set is used to evaluate them.
There are numerous hyperparameters that could be tuned in the framework. In this paper,
we follow the setup from [
To generate a random KB, we start by defining an approach to generate a random axiom in the context of a KB . First, we select with uniform probability one of the following forms for the axiom: ⊑ , ⊓ ⊑ , ⊑ ∃., ∃. ⊑ . Then, we populate the form with concrete values by selecting uniformly at random: , , from , from , , from ∪ {⊥, ⊤}.
To construct dificult KBs, i.e., KBs such that some of the atomic subsumptions following from them have long proofs, we have devised the following algorithm. First, an empty KB is initialized with concepts and roles. Then, we repeat at most times: an axiom not yet present in the KB is randomly generated and added to the KB, then the logical consequences with the proof length of at least are counted, and if there are at least , we terminate and return the KB. If we exceed without reaching , the process is restarted from an empty KB.
In the paper we fixed = 100, = 4, = 300, = 4 and = 200. The choice
of and was guided by the original work on reason-able embeddings [
For each KB, we generate several training – test splits using the following procedure. Let ≤ be the set of all atomic subsumptions following from a KB such that their proofs are no longer than . Conversely, let > be the set of all atomic subsumptions following from the KB with the proof length greater than . Let ˜ be the set of all atomic subsumptions ⊑ that uses the vocabulary of the KB, do not follow from the KB nor the atomic subsumption ⊑ follow from the KB:
˜ = { ⊑ : , ∈ ∪ {⊥, ⊤} ∧ ̸|= ⊑ ∧ ̸|= ⊑ } This final requirement on ˜ is introduced to ensure that knowledge from ˜ cannot be trivially exploited for information about > . Since both and ˜ consist of atomic subsumptions, they cannot be separated syntactically and some semantic information from the labels must be exploited by the neural reasoner.
The -th training set for consists of the whole set ≤ , labeled with the positive label, and a random subset of ˜ counting ⃒⃒ ≤ ⃒⃒ to achieve a balanced training set and labeled with the negative label. The -th test set for is equal to > labeled with the positive label. There are no negative examples in the test set, as we have no complexity measure for subsumptions that do not follow from a KB, and thus the answers of a neural reasoner would ofer no insight into the RQs. We thus use recall, i.e., the number of examples labeled as positive by the neural reasoner to the number of positive examples in the test set, as the measure to assess the performance.
Since we have two levels of training-test splits, there is a tremendous possibility for confusion. We thus introduce the following symbols and names: ≤ (resp. ≤ ) denotes the -th training set for the KB (resp. ), and > (resp. > ) denotes the -th test set for the =1 ≤ , and the -th embeddings KB (resp. ). The -th joint training set is ≤ = ⋃︀40 training set is ≤ = ⋃︀2=0 1 ≤ . We use the name joint to underline that both embeddings and the neural reasoner are trained jointly using these training sets; conversely, the embeddings training sets are used to train embeddings while the neural reasoner is already trained and frozen. The -th internal test set is > = ⋃︀4=0 1 > , and the -th external test set > = ⋃︀2=0 1 > . Here, internal underlines that the neural reasoner was trained with these KBs, whereas external denotes KBs that did not participate in the training of the neural reasoner.
To answer RQ1, we employed the joint training sets ≤ and their respective internal test sets > for ∈ {2, 3, . . . , 20}. For each ≤ , we trained a neural reasoner using the training procedure described earlier, and tested it using > , arriving at the average recall 0.701 ± 0.044 [0.587, 0.764]. We then computed the Pearson correlation coeficient between and the recall, arriving at = 0.931 and the -value < 10− 5 (0 : = 0, using the exact probability distribution as computed by SciPy2).
To ensure this is not due to using diferent test sets for each neural reasoner (since > ⊇ >+1), we also tested all the neural reasoners on the common test set >20, arriving at = 0.920 and the -value < 10− 5.
We have decided not to use more complicated approaches for measuring the influence since the Pearson correlation coeficients are high enough (and the p-values low enough) to give us reasonable confidence that the answer to RQ1 is positive and the complexity of the training set is an indicator of the performance on the test set even when transfer learning is not used.
To answer RQ2, we used the neural reasoner trained with ≤ 20, i.e., presumably the best one. We froze it and used it to train embeddings using the embeddings test sets ≤ for ∈ {2, 3, . . . , 20}. Then, we tested the neural reasoner and the newly trained embeddings on the respective external test sets >. Averaging the recall, we arrived at 0.610 ± 0.094 [0.387, 0.699]. The Pearson correlation coeficient between and recall is = 0.913, with the -value < 10− 5 (the same test as for RQ1). Similarly to the previous experiment, we also tested all the embeddings on the common subset >20, arriving at = 0.982 with the -value < 10− 5. 2https://docs.scipy.org/doc/scipy/reference/generated/scipy.stats.pearsonr.html embeddings training set is a good indicator of the reasoning performance on the test set when transfer learning is employed.
After seeing RQ1 and RQ2, a natural question about the interplay of the complexity of the joint training set and the complexity of the embeddings training set arises. To answer RQ3, we have computed recall for all combinations of ∈ {2, 3, . . . , 20} and ∈ {2, 3, . . . , 20}, by ifrst training the neural reasoner using ≤ , then training embeddings on ≤ , and finally testing them using >. We report the results in Figure 1 and observe that they are somewhat counterintuitive. It turns out that for fixed , the higher the worse the recall. Conversely, for ifxed , the higher the better the recall.
We hypothesize that, while using only atomic subsumptions, the reasoning capabilities of the neural reasoner are not necessary and the most important part is the interplay of diferent dimensions in the latent space of embeddings. Thus, on the one hand, higher values of cause the embeddings to be more attuned to the properties of the latent space, whereas the lower values of cause the reasoner to shape the latent space less strictly.
We note in passing that, following [18], we have conducted the Friedman test assuming every KB is a separate dataset, and every pair (, ) constitutes a separate classifier. The test indicated there are diferences between classifiers (the -value < 10− 5). However, deciding which pair-wise diferences are significant would require making and thus it would be extremely hard to achieve reliable results. ︀( 192)︀ = 64, 980 comparisons 2
In the paper, we have presented an approach to generate non-trivial KBs in the ℰ ℒ DL and to measure the complexity of their logical conclusions. We then used these results to evaluate the influence of the complexity on the performance of reason-able embeddings, a recently proposed framework ofering a transferable neural reasoner for deciding the subsumption problem in the ℒ DL.
We have shown that within the assumed framework the complexity of the training set is a good performance indicator in scenarios both employing and not employing transfer learning. Moreover, the experimental results indicate that the complexity of the embeddings training set is much more important than the complexity of the joint training set, and the latter can even influence the performance negatively, possibly because it constrains the latent space too tightly.
The study has numerous limitations: we have concentrated on a very simple DL ℰ ℒ, we considered only atomic subsumptions in the training and test sets, and measured the complexity of only subsumptions following from the KBs. The first assumption limits the generalizability of this study, but since ℰ ℒ is a proper subset of ℒ, one can suspect that the results on ℒ KBs will be no better than on ℰ ℒ KBs. Concentrating on atomic subsumptions only efectively means we have ignored neural operators, one of the most interesting parts of the reason-able embeddings. The third assumption means we were only able to assess the incompleteness of the neural reasoner, i.e., its tendency to reject subsumptions that in fact follow from the KB. Due to these assumptions, this is only the first step to properly evaluating the scope of usefulness and applicability of the reason-able embeddings.
This research was partially supported by 0311/SBAD/0726 and by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA No 952215. [17] M. Ebrahimi, A. Eberhart, F. Bianchi, P. Hitzler, Towards bridging the neuro-symbolic gap: deep deductive reasoners, Appl. Intell. 51 (2021) 6326–6348. URL: https://doi.org/10.1007/ s10489-020-02165-6. doi:10.1007/s10489-020-02165-6. [18] J. Demsar, Statistical comparisons of classifiers over multiple data sets, J. Mach. Learn.
Res. 7 (2006) 1–30. URL: http://jmlr.org/papers/v7/demsar06a.html.