Amirhoshang Hoseinpour Dehkordi
School of Computer Science, Institute for Research in Fundamental Sciences
|Majid Alizadeh||Ali Movaghar|
|School of Mathematics, Statistics and Computer Science College of Science||Department of Computer Engineering, Sharif University of Technology|
Abstract. Current applied intelligent systems have crucial shortcomings either in reasoning the gathered knowl- edge, or representation of comprehensive integrated information. To address these limitations, we develop a formal transition system, which is applied to classifiers (the common artificial intelligence (AI) systems), to reason about the findings. The developed model was created by combining the Public Announcement Logic (PAL) and the Linear Temporal Logic (LTL), which will be done to analyze both single-framed data and the following time-series data. To do this, first, the achieved knowledge by a classifier for an individual single-framed data will be taken, and then, it would be modeled by a PAL. Alongside the PAL, all the time-series knowledge changes will be modeled, using an LTL. This will integrate the information of the recognized input data, rules, and knowledge. As an application, assume that we have a video stream and some questions about the video. By translating the natural language questions into the temporal formulas, this model could resolve a question answering system. Finally, we suggest a mechanism to reduce the investigated paths for the performance improvements, in semi-continues data-streams. Besides, this approach would perform a partial correction for such an object-detection system. The LTPAL model leads to developing a unified representation of knowledge, and the smoothness in the integration of the gathered and external experiences. Therefore, using LTPAL, the model could receive the classifiers’ predefined -or any external- knowledge, to assemble them in a unified manner. Herein, we will develop a reasoning model on the top of a preexisted intelligent system, to reason about the knowledge, in the following steps:
- First of all, we are going to collect all the intelligent system’s possible answers. Therefore, because of the statistical nature of most classifiers, and the fact that the accuracy is based on the architecture and training set, this kind of classifier could not guarantee full accuracy. To overcome this problem, Huang et al.  presented an approach to verify predefined properties for each input (point-wise verification) in such models. If the input point is verified, the single and verified output would be demonstrated. Otherwise, and in the case that the property could not be verified, Dehkordi et al.  developed a multi-agent epistemic logic model to find all possibleA PREPRINT - J ANUARY 10, 2021 outcomes concerning that property. By applying this step, the outcome of such classifiers would be a set of all possible outputs (i.e., possible worlds).
- Generally, the set of knowledge is directly driven by classifiers, from the possible worlds. This set of knowledge for input and a system of intelligent agents contains all possible output classes, yet from a real-world perspective, each class of objects would contain more information (i.e., ontology rules). To reflect this, an intelligent agent should understand the category of the object together with sub-categories which are fed in as input rules. In this step of the model, for each possible class of object, predefined inferences would be extracted in a unified and formal manner.
- The previously developed model was exclusively designed for single-framed data, therefor the time-series data could not be considered until this step. To bring them into consideration, we developed a combination of temporal logic transition systems Gerth et al.  with the developed epistemic logic model. Let each frame of time-series data, as an input. After execution of the above steps on all frames, we have a set of extracted knowledge (in form of possible worlds) for each single-framed data of the input time-series data. By placing the possible worlds in hierarchical order, a transition system could be created. This leads us to extract all possible sequences (named execution path) of knowledge represented in time-series data.
- Here, we will develop an approach to use our model for a question-answering application. Accordingly, to get an outcome from the developed model, it should provide answers to questions. To do this, first, using preexisted approaches, natural language statements will be translated into temporal formulas. Then, all possible answers (in the shape of a formula) would be extracted due to the asked question (which is translated to a formula). Finally, each formula of every possible answer would be investigated in the developed temporal model and the satisfying formula reflects the answers to the question.
- The verification in this transition system is also defined by modifying the verification definition in Huang et al.  and Dehkordi et al. . Accordingly, the situation of the answer would be determined, in other words, it is checked whether it is a verified answer, possible answer, or it by adding some missing information it would be a possible/verified answer.
- The space state explosion, and following that, numerous execution paths could make the proposed method very time and space consuming in large models. To overcome that difficulty, an approach is also developed, to find the most probable path and investigate the satisfaction on that path. This method for finding the most probable path could be lead us to a data-stream correction (if there are misclassifications in small fractions of such data), in semi-continuous data-streams.
 Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, pages 3–29, 2017.
 Amirhoshang Hoseinpour Dehkordi, Majid Alizadeh, Ebrahim Ardeshir-Larijani, and Ali Movaghar. Masks: A multi-classifier’s verification approach, 2020.
 Rob Gerth, Doron Peled, Moshe Y Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In International Conference on Protocol Specification, Testing and Verification, pages 3–18. Springer, 1995.