This paper describes ongoing interdisciplinary work on integrating logical reasoning and natural language generation, in order to support a drone operator in the task of supervising autonomous drones, e.g. for package delivery. In previous work, justifications were computed to explain description logic (DL) reasoning, and these justifications were then used as the basis for generating a verbal situation description. Here, we consider full proofs instead of justifications, as well as temporal and concrete domains, in order to generate more informative natural language explanations. Following a method for extracting DL proofs, we (i) implemented inference tracing for the DatalogMTL reasoner MeTeoR, and (ii) used the Evee library (a tool collection for explaining DL entailments) to extract small proofs for entailed facts. We provide an empirical evaluation of the tracing and proof extraction phases, which reveals only a minor increase in the computational costs compared to the original MeTeoR reasoner. Finally, we discuss our preliminary findings on using these proofs as input to a natural language generation module that explains the reasons behind entailed facts to a user.
Drone technology and drone control have recently advanced rapidly, to the point that consumer
drones with advanced sensors and improved control algorithms are commonplace [
A tree is in path within 0.3 meter and the battery is low. Please resume human control.
and system stability in various environments and rare critical situations. Second, temporal
ontologies can recognize complex drone states by taking into account also events in the past,
such as water contact, collisions, or battery states from several minutes ago. Third, many logical
reasoners, e.g. Elk [
also proposes a tool to answer temporal queries over time-stamped data records with background
knowledge, but does not consider explanation services, temporal or concrete domain axioms. In
this paper, we focus on reasoning over a temporal ontology, in particular using DatalogMTL [
occur during drone flight. It uses temporal operators as well as concrete domain predicates.
Example 1. Consider the following DatalogMTL rules with concrete domain predicates. ⊞(︀ 0,∞)drone(X) ∶– drone(X)
risk(X) ∶– riskofinternaldamage (X) ⊞(︀ 0,∞)riskofinternaldamage (Y) ∶– hightemperature(Y), drone(Y) hightemperature(X) ∶– temperature(X, S), >(S, 25) (1) (2) (3) (4) 1https://pypi.org/project/meteor-reasoner/ 2https://github.com/de-tu-dresden-inf-lat/meteor-proofs Asserted
⊞[0, ∞)drone(X) :- drone(X) hightemperature(X) :- temperature(X, S), >(S, 25)
reverse_boxplus ⊞[0, ∞)riskofinternaldamage(Y) :- hightemperature(Y), drone(Y)
reverse_boxplus risk(X) :- riskofinternaldamage(X)
inclusion
They express the following statements: (1) once an object is a drone, it keeps being a drone forever; (2) a risk of internal damage is a risk; (3) if a drone experiences a high temperature, then it has a permanent risk of internal damage; and (4) the temperature of an object is high if it is above 25○ .
Then the dataset = {drone(d)@0, temperature(d, 30)@10} containing the two timestamped facts that object d is a drone at time point 0, and at time point 10 the temperature of is 30○C, together with the rules above implies that the drone has experienced overheating and thereafter it has a permanent risk of having internal damage. Figure 2 shows a proof for drone d still being Semantics of ground literals [8, Table 1], where I, ⊧ ⊺ holds for all and I, ⊧ for none.
I, ⊧ x I, ⊧ | I, ⊧ ⊟ I, ⊧ ⊞ I, ⊧ I, ⊧ 1 2 1 2
I, ′ ⊧ I, ′ ⊧ I, ′ ⊧ I, ′ ⊧ if I, ′ ⊧ if I, ′ ⊧ for some ′ with − ′ ∈ for some ′ with ′ − ∈
for all ′ with − ′ ∈ for all ′ with ′ − ∈
2 for some ′ with − ′ ∈ and I, ′′ ⊧ 2 for some ′ with ′ − ∈ and I, ′′ ⊧ 1 for all ′′ ∈ ( ′, ) 1 for all ′′ ∈ (, ′′) at risk at time point 11, i.e. that entails the fact = risk( )@11.
hightemperature and riskofinternaldamage can be used to create a warning message in natural language.
data streams [19, 20]. It extends conventional Datalog rules with metric temporal operators to represent events occurring in the real world at diferent points in time.
Syntax. In DatalogMTL, an atom has the form ( ) with a predicate and an -ary tuple consisting of constants and variables. A literal (a.k.a. metric atom) A takes one of the following forms, where is a non-empty positive interval in Q: ∶= ⊺ ⋃︀ ⋃︀ ( ) ⋃︀ x ⋃︀ | ⋃︀ ⊟ ⋃︀ ⊞ ⋃︀ ⋃︀ A DatalogMTL rule ∶– 1, . . . , consists of body literals 1, . . . , , ≥ 1, and a head literal must also occur in the body. If an atom, literal or rule contains no variable, it is ground. A fact that does not contain the operators x , | , and ; moreover, all variables in the head is of the form @ , where is a ground atom and a rational interval. Moreover, a finite set of facts is a dataset, and a finite set of rules a program. If 3 = 1 ∪ 2 is an interval, then the constants from Π and to variables in Π. a program Π with respect to a dataset is the set of all ground rules obtained by assigning and is also a model of .
Semantics. An interpretation I indicates which ground atoms hold at which time points t ∈ Q, written as I, ⊧ . Additionally, if I, ⊧ for all t ∈ , we say that I satisfies @ . The satisfaction relation for other ground literal is shown in Table 1. An interpretation the fact
I also satisfies the head of at ; it satisfies a (non-ground) rule if it satisfies each ground instance of . Finally, I is a model of a program Π if it satisfies each rule in of a dataset
if it satisfies each fact in . A program Π and a dataset have a common model, and they entail a fact , denoted as Π, ⊧ Π, and it is a model are consistent if they , if each model of both Π Canonical Interpretation. The immediate consequence operator Π for a program Π maps an interpretation I to the least interpretation containing I and satisfying the following property for each ground instance of a rule in Π: whenever I satisfies each body atom of at time point , then Π(I ) satisfies the head of at . For a dataset , let I be the unique least model of .
defines a transfinite sequence of interpretations for ordinals as follows: The successive application of Π to I Π (I ) 2. Π (I ) ∶= Π( Π−1(I )) for a successor ordinal, and
3. Π (I ) ∶= ⋃ < Π(I ) for a limit ordinal. model of Π and .
The canonical interpretation CΠ, uncountable ordinal. If Π and of Π and is the interpretation Π1 I
( ), with 1 the first have a model, the canonical interpretation CΠ, is the least
implemented in Python that supports fact entailment via materialization and automata-based reasoning. Materialization (a.k.a. forward chaining) is a classical technique used in conventional Datalog programs. It successively computes consequences of a program Π by applying its rules to a dataset , similarly to Π. Although materialization of regular Datalog programs always terminates, temporal operators can introduce non-terminating behavior, as they may require infinitely many rounds of rule application. To deal with this, a more costly automata-based technique is used in addition to materialization [20]. However, in this paper we consider only facts that are entailed after finitely many materialization rounds, i.e. those that are satisfied by materialization can be used as the basis for a decision procedure for fact entailment [21]. Π(I ) for a finite . For bounded DatalogMTL programs, in which all intervals are bounded,
MeTeoR implements the materialization using the Python function naive_join3 that determines all facts that can be derived by applying a given rule to the current dataset . To do this, it determines all groundings of the body of that are satisfied in I , computes the intersections of the temporal intervals associated to the ground body literals, and adds the resulting head facts to . To deal with metric body literals, e.g. x , the apply function recursively translates
into corresponding metric facts x @ ′′ by shifting ′ according to . Similarly, the reverse_apply function uses the reverse calculations to translate a derived and ensures the correctness of naive_join.
are merged by coalescing, which reduces
that is to be explained, where Π is a
DatalogMTL program,
the space required to store
materialization round, facts in the extended dataset
Proofs and Evee. We consider a consequence Π,
⊧
a dataset and
a fact. Following [
} ⊧ ℓ( ); the leafs of a proof must be labeled by elements of facts ℓ( ) and hyperedges are of the form (, ), with a tuple of vertices and a vertex such and the root by . In addition, an edge labeling function (see the blue boxes in Figure 2) indicates how the conclusion ℓ( ) was derived from the premises, e.g. by applying a DatalogMTL rule or a temporal operator. In general, there can be several proofs for the same entailment. Here, we focus on finding a proof which is minimal according to its size, i.e. the number of vertices. This slightly difers from the proofs for temporal DL query answering in [ 23], where the root query may contain temporal operators, and ontology axioms are also treated as vertices in the proof.
The Java library Evee4 (EVincing Expressive Entailments) [17] implements various proof generation methods for diferent DLs. In particular,
visualize them like in Figure 2. proofs using a Dijkstra-like algorithm (e.g. from the output of the ℒℰ + reasoner Elk) and
Given a program Π and a dataset , our extended version of MeTeoR traces all derived facts and other relevant information throughout the materialization process. Afterward, we use Evee to extract a proof for a target fact .
Fact Encoding and Tracing. We represent each inference as a simple Python dictionary called connection. Each connection contains three keys, which we denote as preds, succ, and rule. 3We have not yet implemented tracing for the seminaive materialization strategy of MeTeoR [22]. 4https://github.com/de-tu-dresden-inf-lat/evee { } "preds": { "alpha": "drone(d)",
"interval": "[0,0]" }, "rule": "Boxplus[0,inf)drone(X) :- drone(X)", Intuitively, preds specifies the list of facts from which succ is derived, while rule represents the inference label. Using native Python dictionaries is simple and fast, whereas initializing custom data structures is often costly. Figure 3 shows the complete encoding of the inference of ⊞(︀ 0,∞) produced during the various stages of materialization. In addition to the DatalogMTL rules collects each connection themselves, we also trace the application of temporal operators in the apply and reverse_apply functions.
Reverse Apply. For the reverse_apply function in particular, we had to do more extensive modifications. In its original form, the source code was not suitable to connect a metric fact to an underlying non-metric fact, in particular for multiple nested operators, e.g. as in ⊟ | ′ , since the metric operators were processed in a diferent order. Thus, we adjusted the existing reverse_apply function to enable step-wise recording of complex facts in an outside-inside fashion. First, the metric fact is passed to reverse_apply along with an auxiliary list ℒ recording relevant information. Second, its outermost temporal operator is recursively popped for and the interval corresponding to the inner literal is recorded in ℒ . Last, we stop the tracing each traced fact into a connection as described above. process when the innermost atom and its interval are reached, and merge ℒ with by converting Pre-processing, Coalescing and Post-processing. Since the initial dataset is required to construct a full proof with Evee, each fact from is already added to (see Figure 2) while loading the dataset. Furthermore, as mentioned in Section 2, time intervals with label “Asserted” of ground facts are coalesced to represent the final dataset in a more human-readable way and to ensure the correctness of the reasoner. Therefore, we extend MeTeoR accordingly to trace the coalescing step whenever it occurs in the reasoning process and record the information in .
reads the JSON file and outputs a size-minimal proof for the goal fact . in into a JSON format compatible with Evee. Finally, a small Java program using Evee
Machine Configuration.
LUBM Benchmark. We used the LUBM benchmark generator [24] and scripts from [
50 60 Amount of data (k) 70 80 with tracing without tracing polynomial proof time 10 20 30 80 generate proofs.
total CPU time of our implementation for computing the hypergraph to the runtime of the unmodified reasoner, and report the results in Figure 4. As the size of the dataset grows, a more significant performance gap is seen between the baseline and our implementation. However, on average, there is only a 37% increase of runtime, and the tracing does not destroy the nice linear scaling behavior of MeTeoR, which confirms our hypothesis.
Proof Extraction. We also measure the runtime of the Evee library for finding a minimal proof in
, with the results shown in Figure 5. Compared to the tracing, Evee takes considerably longer
to produce minimal-size proofs (e.g. 884 s vs. 140 s on the largest dataset). The reason behind
this blow-up is the polynomial time complexity of finding minimal proofs [
enable the drone operator to take control. Such critical information may be given as an auditory message, as the operator will already be dealing with lots of other visual input. The generated temporal proofs are represented as a Python dictionary or in JSON (see Figure 3) and contain a long step-by-step logical proof. This makes it hard to present relevant information from proofs comprehensibly to drone pilots.
Recently emerging large language models (LLMs) such as GPT-4 [25], LLaMA-2 [26], Gemini [27] can be prompted to perform a wide variety of generative tasks, including code completion and documentation generation. This is ideal for our setup, because prompting strategies such as few-shot prompting only need a few input examples, and do not require a large in-domain dataset for training. We use Gemini-Pro [27] LLM for our experiments, as it performs better than GPT-3.5-Turbo on particularly long and complex reasoning tasks [28]. We deploy Gemini in a zero-shot manner to generate an actionable explanation using temporal proofs.
steps that provide reasoning for the critical situation and verbalize these steps in a coherent manner. We first attempt a select-then-summarize prompting approach, where we prompt the
relevant proof steps, it could not generate a coherent explanation only from the selected steps.
Input Prompt:
Temporal Proof
{"finalConclusion" : "risk(d)@[
"inferences" : [
{"conclusion" : "risk(d)@[
"ruleName" : "inclusion", "premises" : [ "risk(d)@[10,+inf)"]}
, {"conclusion" : "risk(d)@[10,+inf)", "ruleName" : "risk(X):-riskofinternaldamage(X)", "premises" : [ "riskofinternaldamage(d)@[10,+inf)" ]}
, ...
Instructions
The JSON above contains a proof … Symbols used in the JSON and their meanings: …
Only respond with a JSON containing: …
Summary Generation Instructions: Only respond with a JSON response containing "Verbalization" and "Summary".
LLM Output: "Verbalization": ["We can generate a warning for the human drone pilot because at time 10, there is a risk of internal damage to the drone (d).", "The risk of internal damage is because the drone (d) is experiencing a high temperature of 30 degrees Celsius at time 10.", "The high temperature is likely because the drone (d) is flying.", "We know the drone (d) is flying because it was asserted to be true."], "Summary": "At time 10, there is a risk of internal damage to your drone (d) because it has a high temperature of 30 degrees Celsius. This is likely because the drone is flying." proofs. VeSum first instructs the LLM to produce a verbalization of the entire proof, and then use the generated verbalization to generate an explanation summary. VeSum is inspired by well-known prompting approaches – Chain-of-Thought (CoT) [29] and ReAct [30] prompting.
• LLMs are very sensitive to input instructions [31], and input templates [32]. Hence, finding the optimal instructions for long text generation is challenging. • For our task, the predicate names are mostly descriptive and verbose (e.g. hightemperature(X) ∶– temperature(X, S), >(S, 25)). In our preliminary experiments, when we shortened the names (e.g. hightemperature(X) to HT(X)), we found that models failed to understand the meaning of the rules. This suggests that the predicate names have a noticeable impact on the generated explanations, hence they should be chosen carefully. Alternatively, one could provide additional descriptions of each predicate via string annotations and incorporate them into the prompt. • LLMs can write fluently and grammatically; their advantage over traditional templatebased methods lies in their generalizability to new sensor input and better naturalness and variability of expression. However, the generated text is not always grounded in the given information. For instance, if we take a closer look at the generated summary in Figure 6, we can see that LLM generates the reason for the warning as “because it has a high temperature of 30 degrees Celsius. This is likely because the drone is flying.” While the proof mentions the high temperature, it does not specify any further reason for this measurement (see Figure 2).
timestamps and numerical measurements. To achieve this, we implemented inference tracing for
operations in a streaming setting, in which new facts continuously come in and old facts are removed, (ii) improve the quality of the generated verbal messages, and (iii) reduce cognitive load for the drone operator in situations with multiple warnings.
For (i), assuming that sensor measurements arrive incrementally every second, we should avoid re-generating the same proof over and over again if it still holds. Using the streaming version of MeTeoR for forward-propagating rules [33], our system could also be adapted to the forgetting mechanism using sliding windows. This dramatically reduces the data size and makes real-time processing feasible. Nevertheless, we can still improve the tracing and proof extraction themselves, e.g. by goal-directed tracing of the inferences that lead to a target fact, or by using optimized data structures for proof extraction.
For (ii), we will first investigate better prompting techniques that leverage proofs to generate more strongly grounded explanations. We will also experiment with more diverse proof formats based on first-order logic or description logic to test the models’ abilities. We also aim to develop a systematic understanding of how diferent phrasing choices impact explanation quality, which will inform guidelines for designing new ontologies and improving prompting methods for existing ones. Additionally, we will explore the latest open-source LLMs, evaluating their potential for ifne-tuning on the annotated data to improve task performance.
2021. URL: https://ceur-ws.org/Vol-2954/abstract-11.pdf. [12] E. Chang, A. Kovtunova, S. Borgwardt, V. Demberg, K. Chapman, H. Yeh, Logic-guided message generation from raw real-time sensor data, in: N. Calzolari, F. Béchet, P. Blache,
6899–6908. URL: https://aclanthology.org/2022.lrec-1.745. [13] F. Baader, P. Hanschke, A scheme for integrating concrete domains into concept languages, in: J. Mylopoulos, R. Reiter (Eds.), Proc. IJCAI Conference, Morgan Kaufmann, 1991, pp. 452–457. URL: http://ijcai.org/Proceedings/91-1/Papers/070.pdf. [14] C. Lutz, Description logics with concrete domains—a survey, in: Advances in Modal Logics
[15] C. Alrabbaa, F. Baader, S. Borgwardt, P. Koopmann, A. Kovtunova, Combining proofs for description logic and concrete domain reasoning, in: A. Fensel, A. Ozaki, D. Roman,
2023, Proceedings, volume 14244 of Lecture Notes in Computer Science, Springer, 2023, pp. 54–69. doi:10.1007/978-3-031-45072-3_4. [16] L. Westhofen, C. Neurohr, J. C. Jung, D. Neider, Answering temporal conjunctive queries over description logic ontologies for situation recognition in complex operational domains, in:
of Systems - 30th International Conference, TACAS, volume 14570 of Lecture Notes in Computer Science, Springer, 2024, pp. 167–187. doi:10.1007/978-3-031-57246-3_10. [17] C. Alrabbaa, S. Borgwardt, T. Friese, P. Koopmann, J. Méndez, A. Popovič, On the eve of true explainability for OWL ontologies: Description logic proofs with Evee and Evonne, in:
CEUR-WS.org, 2022. URL: https://ceur-ws.org/Vol-3263/paper-2.pdf. [18] A. Kovtunova, S. Borgwardt, Drone program for critical situation detection over sensor data streams, 2024. doi:10.5281/zenodo.10822865. [19] S. Brandt, E. G. Kalayci, V. Ryzhikov, G. Xiao, M. Zakharyaschev, Querying log data with metric temporal logic, J. Artif. Intell. Res. 62 (2018) 829–877. doi:10.1613/jair.1.11229. [20] P. A. Walega, B. C. Grau, M. Kaminski, E. V. Kostylev, DatalogMTL: Computational complexity and expressive power, in: S. Kraus (Ed.), Proceedings of the Twenty-Eighth
1892. doi:10.24963/ijcai.2019/261. [21] P. A. Walega, M. Zawidzki, D. Wang, B. C. Grau, Materialisation-based reasoning in
6574. doi:10.1609/AAAI.V37I5.25807. [22] D. Wang, P. A. Walega, B. C. Grau, Seminaïve materialisation in DatalogMTL, in:
on Rules and Reasoning, RuleML+RR, volume 13752 of Lecture Notes in Computer Science, Springer, 2022, pp. 183–197. doi:10.1007/978-3-031-21541-4_12. [23] C. Alrabbaa, S. Borgwardt, P. Koopmann, A. Kovtunova, Finding good proofs for answers to conjunctive queries mediated by lightweight ontologies, in: O. Arieli, M. Homola, J. C.
Semant. 3 (2005) 158–182. doi:10.1016/j.websem.2005.06.005. [25] J. Achiam, S. Adler, S. Agarwal, L. Ahmad, I. Akkaya, F. L. Aleman, D. Almeida,
arXiv:2303.08774 (2023). doi:10.48550/arXiv.2303.08774. [26] H. Touvron, L. Martin, K. Stone, P. Albert, A. Almahairi, Y. Babaei, N. Bashlykov, S. Batra,
arXiv preprint arXiv:2307.09288 (2023). doi:10.48550/arXiv.2307.09288. [27] G. Team, R. Anil, S. Borgeaud, Y. Wu, J.-B. Alayrac, J. Yu, R. Soricut, J. Schalkwyk,
preprint arXiv:2312.11805 (2023). doi:10.48550/arXiv.2312.11805. [28] S. N. Akter, Z. Yu, A. Muhamed, T. Ou, A. Bäuerle, Á. A. Cabrera, K. Dholakia, C. Xiong,
(2023). doi:10.48550/arXiv.2312.11444. [29] J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V. Le, D. Zhou, et al.,
information processing systems 35 (2022) 24824–24837. URL: https://openreview.net/ forum?id=_VjQlMeSB_J. [30] S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. R. Narasimhan, Y. Cao, ReAct: Synergizing reasoning and acting in language models, in: The Eleventh International Conference on Learning Representations, 2023. URL: https://openreview.net/forum?id=WE_vluYUL-X. [31] M. Loya, D. Sinha, R. Futrell, Exploring the sensitivity of LLMs’ decision-making capabilities: Insights from prompt variations and hyperparameters, in: H. Bouamor, J. Pino, K. Bali (Eds.), Findings of the Association for Computational Linguistics: EMNLP 2023, Association for Computational Linguistics, Singapore, 2023, pp. 3711–3716. doi:10.18653/v1/2023. findings-emnlp.241. [32] M. Sclar, Y. Choi, Y. Tsvetkov, A. Suhr, Quantifying language models’ sensitivity to spurious features in prompt design or: How I learned to start worrying about prompt formatting, arXiv preprint arXiv:2310.11324 (2023). doi:10.48550/arXiv.2310.11324. [33] P. A. Walega, M. Kaminski, D. Wang, B. C. Grau, Stream reasoning with DatalogMTL, J.
Web Semant. 76 (2023) 100776. doi:10.1016/j.websem.2023.100776.