Search engines can quickly response a hyperlink list according to query keywords. However, when a query is complex, developers need to repeatedly refine the search keywords and open a large number of web pages to find and summarize answers. Many research works of question and answering (Q and A) system attempt to assist search engines by providing simple, accurate and understandable answers. However, without original semantic contexts, these answers lack explainability, making them difficult for users to trust and adopt. In this paper, a brain-inspired search engine assistant named DeveloperBot based on knowledge graph is proposed, which aligns to the cognitive process of human and has the capacity to answer complex queries with explainability. Specifically, DeveloperBot firstly constructs a multi-layer query graph by splitting a complex multi-constraint query into several ordered constraints. Then it models the constraint reasoning process as subgraph search process inspired by the spreading activation model of cognitive science. In the end, novel features of the subgraph will be extracted for decision-making. The corresponding reasoning subgraph and answer confidence will be derived as explanations. The results of the decision-making demonstrate that DeveloperBot can estimate the answers and answer confidences with high accuracy. We implement a prototype and conduct a user study to evaluate whether and how the direct answers and the explanations provided by DeveloperBot can assist developers' information needs.
Developing an AI Assistant for Knowledge Management and Workforce Training in State DOTs
Department of Computer Science, University of Houston（计算机科学系，休斯顿大学）；Department of Civil and Environmental Engineering, University of Houston（土木与环境工程系，休斯顿大学）；Ph.D Department of Civil and Environmental Engineering, University of Houston（土木与环境工程系，休斯顿大学）；Engineering Data Science, University of Houston（工程数据科学，休斯顿大学）
Isabelle/PIDE平台解决了LCF系列的证明助手是否适合作为教育工具的技术基础的问题。像HOL、Coq或Isabelle这样的系统传统上强大的逻辑基础到目前为止已经被TTY（或像著名的Proof General / Emacs接口这样的小变体）的一些不可访问的交互所抵消。因此，数学教育工具与完全正式的背景理论的基本问题，往往是否定的回答，由于现有的证明引擎偶然的弱点。“PIDE”（意为“ProverIDE”）的理念是将现有的证明器（如Isabelle）集成到一个更大的环境中，以方便最终用户和其他工具的访问。我们使用Scala将ML中的证明引擎公开给JVM世界，那里已经存在许多用户界面、编辑器框架和教育工具。这将最终导致组合数学助手，其中逻辑引擎是在后台，而不妨碍形式化方法，形式化数学，特别是数学教育的应用程序的看法。
