Mastering common-sense reasoning is often regarded as a major obstacle towards natural language understanding (NLU). The growing availability of large-scale knowledge bases and automated theorem provers has motivated studies to determine to which extent common sense knowledge as required in NLU is already provided by existing knowledge bases. However, large-scale knowledge bases may comprise too many axioms to be handled by an automated theorem prover. In 2024, Claudia Schon presented a paper at the FCR workshop demonstrating that similarity of language as captured by the embedding space of a large language model (LLM) can provide an efective heuristic for selecting relevant axioms. The work presented in this paper is motivated by her findings. We first show in a reproduction study that the results not only apply to theorem prover E, but also to prover Vampire. An analysis of the results reveals a complementary heuristic that identifies generally important axioms automatically, improving the performance of reasoning significantly.
Natural language is inherently ambiguous, requiring listeners and readers to fill in missing pieces of
information from context, their understanding of the world, and by logical inference. The importance
of common-sense reasoning to interpret natural language has thus often been stressed in the literature,
prominently in the works by Gary Marcus and Ernest Davis [1, for example]. We characterize reasoning
in natural language understanding as the task of constructing a model in the sense of logic that is
consistent with given natural language input as well as context and background knowledge. Setting
aside the questions of which logic may be most suitable to represent semantics of language and how
knowledge about language can be acquired, we are interested in computational principles that allow a
logic model of a given natural language phrase to be constructed. As has already been shown by Schon
[
Throughout the last decades of AI, several attempts have been made to compile common-sense
knowledge bases on various levels of abstraction. Well-known examples on the side of fine-grained
knowledge bases include the Cyc project [
Applying automated theorem provers to large-scale knowledge bases quickly reveals a major challenge: The sheer size of a knowledge base – in conjunction with high computational costs of automated theorem proving – limits applicability. Clearly, not all elements of a knowledge base are relevant for proving consistency of a candidate model. Selecting the subset of relevant axioms ofers means to improve applicability of theorem proving. But why should it be possible to design a clause selection method that is more efective than the advanced techniques already implemented in automated theorem provers? A potential answer to this question lies in the kind of proofs the theorem prover is requested to perform. Consider the task of proving that leaving your bike unlocked increases the likelihood of the bike being stolen. A potential reasoning chain would likely connect concepts such as “lock” as a means for fixing otherwise movable objects, “thieves“ re-locating objects while overcoming security measures. In a large corpus of text we expect to find such reasoning chains to be spelled out or at least hinted at, hence the co-occurrence of “unlocked bike”, “theft”, and “stolen bike” is likely to occur.
Such co-occurrence is exactly what semantic similarity as determined by LLMs represents. By
inspecting the embedding of a given sentence, i.e., its mapping to a neural activation of the LLM, it
might thus be possible to retrieve related words or phrases. Schon [
In this paper we re-visit the approach by Schon [
Hypothesis 2 A manually designed knowledge base contains relevant axioms that cannot be discovered from semantic similarity alone, but which are essential in the construction of a valid model.
The contribution of this paper is to describe an experimental analysis using the Adimen-SUMO
ontology and theorem provers E [
Traditionally, the domains for automated reasoning, planning, and understanding have been narrow and
application specific. There have been monumental eforts in the common-sense reasoning community
to estimate and capture the knowledge that is relevant to make reasoning about the everyday world
possible. The largest and longest-standing project (in all of artificial intelligence) is Cyc, an ontology
that encodes everyday concepts in a logic-like language. Unfortunately, Cyc is closed source and not
integrated with standard theorem provers. In this study we focus on the Adimen-SUMO ontology [
Atomic truths in Adimen-SUMO are represented as axioms, which can be used to prove theorems. Adimen-SUMO contains around 8000 axioms. Similar to theorem proving in other domains, the amount of axioms provided increases the potential search space for a theorem prover, making it dificult to find proofs in a reasonable time frame. For common-sense reasoning in the context of natural language understanding, this is especially problematic, as often implications are omitted from the natural language sentences, which makes it dificult to identify the relevant axioms for a given proof task. Theorem proving has thus to rely on axiom selection, a technique to select which axioms will be considered in a proof attempt.
Every theorem will require a diferent set of axioms to be proven, which encourages the use of selection strategies to favor dynamic selection over selecting axioms based on fixed rules. These techniques are also referred to as clause selection since the conjunction of all axioms constitutes the background knowledge for a proof. While clause selection appears to be a more natural term when considering the task from a theorem prover’s point of view, axiom selection better captures the outside view of filtering which axioms from a common sense ontology are passed to the theorem prover.
A prominent example of such a strategy is the SUMO Inference Engine (SInE) selection strategy
[
The widespread use of LLMs enables axiom selection based on so-called semantic similarity. Trained on vast text corpora, LLMs capture co-occurrence relationships between words and phrases which are referred to as semantic relationships. Assuming common-sense knowledge bases to reflect concepts from natural language as part of the LLM training data, LLMs can be applied to select axioms based on a semantic similarity of the concepts involved. Computationally, concepts are mapped by the LLM to an (internal) embedding space. Embedding spaces are real-valued vector spaces that are commonly equipped with a cosine similarity · || ||− 1 · || ||− 1 for , ∈ R. In vector-based selection, axioms are selected from an averaged embedding of individual symbols. The SeVEn (Sentence-based Vector Encoding) extends this approach by embedding entire axioms as natural language sentences. Each axiom from a knowledge base KB is first translated into a natural language sentence = (), which is then encoded into a vector () = () using a sentence embedding model. The resulting sentence-based representation of the knowledge base, (KB), maintains the structure of vector-based selection while enabling deeper semantics, which is why we refer to it as semantic axiom selection.
Building on both approaches, [
Formally, let SInE(KB, {1, . . . , }) denote the set of axioms selected by SInE given a set of conjectures, and SeVEn(KB, ) denote the axioms selected by SeVEn for a conjecture . The combined selection strategy is defined as a union of both methods.
Like [
standard full ontology baseline without any pre-selection, i.e., only using the prover’s built-in method;
syntactic axiom selection using the SInE algorithm;
semantic axiom selection using SeVEn based on semantic similarity, computed via sentence
embeddings;
union combined semantic and syntactic selection approach following [
Our experiments validate the findings of [
The combined use of syntactic and semantic selection methods fails to cover a wide enough range of proofs. We observe that conjectures without successful proofs often show higher cosine similarity to their 160 nearest axioms, suggesting that overly specific selections can exclude essential axioms. Since theorem provers rely on axioms to guide simplification steps, missing such axioms hinders proof discovery. To address this, Prover E was run in auto mode on all 8, 010 White-box Truth tests, allowing it to optimize SInE parameters per conjecture. The 25 axioms most frequently used in successful proofs were then identified as core axioms (see Figure 2 for an example).
As such we obtain an axiom selection strategy featuring the core axioms discovered in the previous
step, which we refer to as enhanced. To improve core axiom selection without greatly increasing their
number, a SInE strategy was applied to the 25 core axioms (benevolence 1, depth 1), an overview is
1https://huggingface.co/sentence-transformers/all-MiniLM-L6-v2
2Parameters and models are based on the results of [
0 union shown in Figure 1. The resulting axioms were combined with those from the union-based method, balancing frequency and structural relevance. On the same 1,000 White-box Truth tests, this enhanced approach yielded 286 proofs (see Figure 3).
To explore how internal heuristics interact with external axiom selection we evaluate diferent automatic
theorem provers using their automatic mode also used during CASC competitions. In addition to Prover
E which was used in the original study we selected Vampire 4.9 [
From the results evaluating Prover E in its competition mode, we obtained three subsets of the White-box Truth tests , identified by the axiom selection methods auto, union and enhanced. We can report that the obtained subsets are in fact subsets of their cardinally superior set, such that auto ⊂ union ⊂ enhanced ⊂ .
Furthermore, the versions featuring the additional selection strategies of union and enhanced result in comparably faster proof times on average. Overall, restricting the search space through a combined syntactic and semantic selection process, supplemented by core axioms, consistently improves the prover’s performance. In automatic mode, the average time to find a proof was 5.48 seconds; with the selection strategies in place, it was reduced to less than a second (see Table 1). A slight increase was measured from extending the union strategy with the core axioms, which can be explained by simply having slightly more axioms to choose from for the set union. Finally, presumably the largest of the subset enhanced showed a reduced average time to proof with core axioms in place compared to the automatic mode.
While we have demonstrated the existence of these core axioms for proving conjectures in commonsense ontologies, there are some clear limitations.
First of all, the White-box Truth tests used to evaluate the selection strategies are designed to validate theorem provers on formal ontologies like Adimen-SUMO. As of now, similar truth tests that reflect natural language expressions directly are not available in the same quantity or quality. This makes it unclear to which extent the efects we observe, especially the impact of core axioms, will carry over to an actual NLU setting, or if they are specific to this kind of synthetic evaluation.
Second, we can only extract core axioms from successful proof attempts. This introduces a bias toward axioms that appear in easy or already solvable proofs. Axioms that are essential but only show up in harder proofs, or in cases that currently fail, are missed entirely by this method.
That said, our results suggest that there is an efect, i.e., some axioms appear to act as bridges, iflling in gaps that neither syntactic nor semantic selection strategies can easily cover. In other words, demonstrating the existence of such core axioms shows that several axioms cannot be identified using LLMs. These axioms are not just frequent, they appear to carry structural or semantic importance that helps reasoning succeed. Being able to identify likely core axioms in advance could help improve reasoning performance in settings where no prior proof data is available, and could enable logic-based NLU.
In this study we set out to reproduce a study by Schon [
We could identify a set of axioms from Adimen-SUMO which often is used in successful proofs. Explicitly activating this set of axioms for every proof significantly increased the proof success rate. This suggests that Hypothesis 2 holds too, i.e., there exists a set of axioms specific to the underlying knowledge-base that is not identified by word-level similarity as it represents general concepts.
Taking both observations together and setting them into context with previous findings by Schon [