We have developed a tool for fact-checking in automated question answering based on four technologies: (i) the Suggested Upper Merged Ontology (SUMO) for knowledge representation, (ii) the Vampire theorem prover [1] for fact verification, (iii) WordNet for lexical semantics and (iv) GPT (Generative Pretrained Transformer) for concept learning and alignment. SUMO provides a structured representation of knowledge in an expressive logic, facilitating semantic understanding and analysis. Vampire serves as an automated reasoning tool to check the validity of facts and claims. WordNet and GPT contribute to concept learning and alignment, enhancing the system's ability to interpret natural language (NL) expressions and align them with the underlying ontological representations. By combining these components, the proposed framework ofers a robust solution for fact-checking, combating misinformation, and promoting informed decision-making.
also provides supporting evidence for its conclusions. By enriching SUMO with a food domain ontology, we provide a running scenario for detecting fake claims regarding diets.
Figure 1 illustrates the deployment diagram of the application, showing how three microservices interact with each other. The server-side includes the following microservices: (i) ontology-rest responsible for interacting with the ontology: ontology alignment, Vampire querying; (2) fakenews-detector-api: implementing the algorithm for text verification; (3) gpt-translator: serving as a REST interface for interacting with the fine-tuned models; (4) users interact with the system through a web page deployed by the fake-news-detector-api.
The content of SUMO [
SUMO also benefits from the Sigma Knowledge Engineering Environment (SigmaKEE) [
The Algorithm 1 evaluates the truth value of an input text, yielding an output of ’True’, ’False’, or ’Unknown’. The algorithm processes the current claim txt which undergoes ontology matching, transforming it into a form suitable for further processing. This matched text is then translated into tSUO-KIF, creating a query. The query is then put through a theorem prover. If a proof is found for this query, it implies that the txt corresponds to a ’True’ statement. If the theorem prover does not find a proof for the query, the algorithm takes the negation of the query and poses it to the theorem prover. This is necessary because not finding a proof for a query doesn’t automatically mean the negation of the query is true. Under the open world assumption, the negation of a statement can be ’Unknown’. Finding a proof for the negated query means that the txt corresponds to a ’False’ statement. In case of no proof found for the negated query, the validity of the claim is assessed as ’Unknown’, as neither the query nor its negation could be proven. Finally, the output True, False, or Unknown is passed to the explanation step, which is an example of Explainable AI (XAI).
The execution of this algorithm corresponds to the flowchart in Figure 2. The main four steps: (1) ontology alignment; (2) translation to SUO-KIF, (3) theorem proving and (4) explanation are detailed in the following paragraphs.
First, for aligning text to ontology, we map and substitute tokens from a corpus of text to
concepts from SUMO. The Natural Language Processing (NLP) pipeline defined in SigmaNLP
[
Second, automatic translation of input text to SUO-KIF was done by fine-tuning the GPT Curie model. We created a dataset containing pairs of diferent types of input text and their corresponding translation into SUO-KIF. It contains training data for the following SUO-KIF patterns and relations: attribute, agent-patient, subclass, contains, part. Table 1 shows the number of examples created for each type. The dataset is divided 80% for training and 20% to testing.
The translation is done in 2 steps (Listing 1 - 4). In the first step, text is translated to a "formal" format and then, the "formal" format is used for conversion to SUO-KIF : { t e x t : " D e s e r t s a r e dry " f o r m a l : " I f ?X i s an i n s t a n c e o f d e s e r t , t h e n ?X has t h e a t t r i b u t e dry " k i f : " (= > ( i n s t a n c e ?X D e s e r t ) ( a t t r i b u t e ?X Dry ) ) " }
Algorithm 1 FactCheck procedure FactCheck(, ) ← AlignWithOntology(, ) ← TranslateToKif( ) ′ ← MergeOntologies(, ) ℎ , ← RunProver(′) if ℎ == true then ← TRUE ← Verbalize( ) else ′ ← Negate() ′′ ← MergeOntologies(′, ) ℎ , ← RunProver(′′) if ℎ == true then ← FALSE ← Verbalize( ) ← FALSE ← Verbalize( ) return , { t e x t : " Apples and bananas a r e f r u i t s " f o r m a l : " Apple and banana a r e s u b c l a s s e s o f f r u i t " , k i f : " ( and ( s u b c l a s s Apple F r u i t ) ( s u b c l a s s Banana F r u i t ) ) " }
Third, for theorem proving we relied on Vampire [
Fourth, for proof verbalisation, Vampire outputs a lot of steps, which it used when searching for proof. For this case, only the axioms was selected and verbalized using the manually created formats in English for each term.
First, we compare GPT-based translations with SigmaNLP translations. Diferent from GPT, Sigmakee applies the agent-patient pattern. On the one hand, this pattern is adequate when the text represents processes. For instance SigmaNLP performs well in the agent-patient context (see Table 2). However, the translation does not explicitly indicate that "Salmon" is the cause of "Increasing"; rather, it suggests a "Increasing" process with two patients: "Salmon" and "Cholesterol". On the othe rhand, the pattern fails when the task includes the translation of predicates ”is”, ”have”, ”part”. For instance, given the claim "Broccoli contains vitamins.", the translation using the predicate part is more suitable than the agent-patient pattern (see Table 3).
The GPT-model was fine-tuned with 418 training examples (recall Table 1). For fine-tuning the Curie model we used 4 epochs, batch size of 1, learning rate multiplier (0.05, 0.1, or 0.2), while the parameter computing classification metrics was set on false. The cost for training is $0.0030 / 1K tokens and the usage costs $0.0120 / 1K tokens. On average, each example has 100 tokens, resulting in $0.13 for training and $0.1 for testing. On the 83 new examples used for testing, the accuracy was 0.84. This accuracy indicates the percentage of correct completions in the translation from natural language text to KIF. The tuned model achieved an accuracy of 0.96 for KIF translation and 0.82 for the formal model. By analysing errors, we observed that most errors were related to the diferences in variable names, which, in fact, do not afect the semantics. When testing with variables substituted with placeholders, the accuracy was 0.92. Out of 83 testing examples, 76 were translated correctly.
For testing fact-checking in the diet and nutrition domain, an domain ontology was built on top of SUMO. It includes the concepts required for the test set described in Table 4 and also concepts for various categories, including organic food, lipids, fibers, fatty acids, and axioms, aimed at confirming or contradicting test samples.
Next, we detail the computations for the claim: Vegetables are healthy. Our Diet ontology built on top of SUMO includes the following axioms: (subclass Vegetable FruitOrVegetable) (instance Healthy BiologicalAttribute) (=> (instance ?F FruitOrVegetable) (attribute ?F Healthy))
First, the text is aligned with ontology. That is, each token of the input sentence is not just mapped to a SUMO concept. Here the system computes the following output: Vegetable Attribute Healthy with the mappings Vegetables = Vegetable, are = Attribute, a = [None], healthy = Healthy. Additionally to mapping, a semantic analysis was done, because the verb are was correctly mapped to Attribute and the article a is not mapped to anything, even though it has only one mapping to AlphabeticCharacter concept.
In the second step, the text is converted in to SUO-KIF format. The translator constructs the following intermediate format: If ?V is an instance of vegetable, then ?V has attribute healthy Based on it, the following SUO-KIF representation is obtained: (=> (instance ?V Vegetable) (attribute ?V Healthy))
In the third step, the checker searches for a proof for the obtained query. For this, Vampire is run in cascade mode and a proof is found, which means the input text is true in relation with ontology.
In the final step, axioms from proof steps are automatically paraphrased in English by Sigma. SigmaKEE has a facility to convert SUO-KIF statements into natural language paraphrases in several diferent languages. This includes use of natural language templates for relations and logical operators and words or phrases for each term. These are built recursively for complex formulas.
1 . f o r a l l a c l a s s , a n o t h e r c l a s s and an e n t i t y i f t h e o t h e r c l a s s i s an i n s t a n c e o f c l a s s and t h e c l a s s i s an i n s t a n c e o f c l a s s , t h e n i f t h e e n t i t y i s an i n s t a n c e o f t h e c l a s s and t h e c l a s s i s a s u b c l a s s o f t h e o t h e r c l a s s , t h e n t h e e n t i t y i s an i n s t a n c e o f t h e o t h e r c l a s s 2 . v e g e t a b l e i s an i n s t a n c e o f c l a s s 3 . v e g e t a b l e i s a s u b c l a s s o f f r u i t o r v e g e t a b l e 4 . f r u i t o r v e g e t a b l e i s an i n s t a n c e o f c l a s s 5 . f o r a l l an o b j e c t i f t h e o b j e c t i s an i n s t a n c e o f f r u i t o r v e g e t a b l e , t h e n h e a l t h y i s an a t t r i b u t e o f t h e o b j e c t
These paraphrases can be rephrased by GPT, with the following result: 1 . I f b o t h a c l a s s ( C l a s s A) and a n o t h e r c l a s s ( C l a s s B ) a r e i n s t a n c e s o f a common c l a s s ( C l a s s C ) , and an e n t i t y ( E n t i t y X ) i s an i n s t a n c e o f C l a s s A , and C l a s s A i s a s u b c l a s s o f C l a s s B , t h e n E n t i t y X i s a l s o an i n s t a n c e o f C l a s s B . 2 . V e g e t a b l e i s an i n s t a n c e o f a c l a s s ( C l a s s A) . 3 . V e g e t a b l e i s a s u b c l a s s o f a c l a s s ( C l a s s B ) t h a t i n c l u d e s b o t h f r u i t s and v e g e t a b l e s . 4 . F r u i t s o r v e g e t a b l e s a r e i n s t a n c e s o f a c l a s s ( C l a s s C ) . 5 . F o r any o b j e c t ( O b j e c t Y ) , i f O b j e c t Y i s an i n s t a n c e o f a f r u i t o r v e g e t a b l e , t h e n t h e o b j e c t has a p r o p e r t y " h e a l t h y . "
Table 4 exemplifies some input text and the corresponding answer computed by the checker and also by GPT. In the first line, "All salt is unhealthy" is detected as false since in the knowledge base there are the following axioms "Some salt is unhealthy" and "Some salt is healthy". "Calcium strengthens bones" is detected as true since this knowledge appears in the ontology in the SUO-KIF format, and the translator has correctly converted the given text into SUO-KIF.
The processing time for fact-checking varies depending on the verdict. On average, "True" texts take 7.16 seconds, needing just one Vampire run. For "False" texts, the average time is 17.11 seconds, involving 2 runs where the first run might either time out or Vampire finishes processing, but the second run yields a proof. As for "Unknown" texts, they take 30-40 seconds on average, with 2 runs either reaching timeout or Vampire completing the processing.
We have shown initial experiments in the use of SUMO, Sigma, Vampire, and GPT Curie language model in an eficient method for verifying text validity. SUMO provides an expressive ontological framework that aids in stating precise meaning. Vampire uses SUMO’s knowledge structure to systematically evaluate statement validity. We use a GPT model in translating the text into the SUO-KIF format, and then passing the result to Vampire. One output of this study is a dataset for training the GPT model. The GPT model facilitated text transformation for Vampire to evaluate, resulting in an advanced text credibility assessment system with fact-checking and misinformation detection.
Ongoing work consists of: assessing the system performance on larger sets of claims. The current running version of the tool, the diet ontology built on top of SUMO and the dataset used for fine-tuned the models are available at https://github.com/ldan22/fake-news-detector.git
A. Groza is supported by the grant CCCDI-UEFISCDI, project number PN-III-P2-2.1-PED-20212709, within PNCDI III of of the Ministry of Research, Innovation and Digitization, Romania