We introduce a new operation which can be used to compositionally construct second-order multi-hop templates in a neural model, and evaluate a number of alternative implementations, with different time and memory trade offs. These techniques scale to KBs with millions of entities and tens of millions of triples, and lead to simple models with competitive performance on several learning tasks requiring multi-hop reasoning.

Automated theorem proving in large theories can be learned via reinforcement learning over an indefinitely growing action space. In order to select actions, one performs nearest neighbor lookups in the knowledge base to find premises to be applied. Here we address the exploration for reinforcement learning in this space. Approaches (like epsilon-greedy strategy) that sample actions uniformly do not scale to this scenario as most actions lead to dead ends and unsuccessful proofs which are not useful for training our models. In this paper, we compare approaches that select premises using randomly initialized similarity measures and mixing them with the proposals of the learned model. We evaluate these on the HOList benchmark for tactics based higher order theorem proving. We implement an automated theorem prover named DeepHOL-Zero that does not use any of the human proofs and show that our improved exploration method manages to expand the training set continuously. DeepHOL-Zero outperforms the best theorem prover trained by imitation learning alone.

Artificial Intelligence has come a long way from being the stuff of science fiction movies and books to becoming an integral part of our daily lives. Today, AI is one of the fastest growing global industries. Investments and experiments in AI have been taking place all around the world. Given its unimaginably wide range of uses; AI is a field of expertise that is set to grow in a very huge way over the coming years. AI professionals are among the highest paid in the field of IT. Ans: Artificial Intelligence is a part of computer science that aims to create machine that are intelligent and seek to work and react the way humans do. Q2)What to you understand by an artificial intelligence Neural Network?

Continuous queries over data streams may suffer from blocking operations and/or unbound wait, which may delay answers until some relevant input arrives through the data stream. These delays may turn answers, when they arrive, obsolete to users who sometimes have to make decisions with no help whatsoever. Therefore, it can be useful to provide hypothetical answers - "given the current information, it is possible that X will become true at time t" - instead of no information at all. In this paper we present a semantics for queries and corresponding answers that covers such hypothetical answers, together with an online algorithm for updating the set of facts that are consistent with the currently available information.

This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem provers allow for the formalization of most mathematical theories and have been shown to pose a significant challenge for deep learning. Higher-order logic is highly expressive and, even though it is well-structured with a clearly defined grammar and semantics, there still remains no well-established method to convert formulas into graph-based representations. In this paper, we consider several graphical representations of higher-order logic and evaluate them against the HOList benchmark for higher-order theorem proving.

In this work we describe a new learning-based proof guidance -- ENIGMAWatch -- for saturation-style first-order theorem provers. ENIGMAWatch combines two guiding approaches for the given-clause selection implemented for the E ATP system: ProofWatch and ENIGMA. ProofWatch is motivated by the watchlist (hints) method and based on symbolic matching of multiple related proofs, while ENIGMA is based on statistical machine learning. The two methods are combined by using the evolving information about symbolic proof matching as an additional information that characterizes the saturation-style proof search for the statistical learning methods. The new system is experimentally evaluated on a large set of problems from the Mizar Library. We show that the added proof-matching information is considered important by the statistical machine learners, and that it leads to improvements in E's Performance over ProofWatch and ENIGMA.

Representation of defeasible information is of interest in description logics, as it is related to the need of accommodating exceptional instances in knowledge bases. In this direction, in our previous works we presented a datalog translation for reasoning on (contextualized) OWL RL knowledge bases with a notion of justified exceptions on defeasible axioms. While it covers a relevant fragment of OWL, the resulting reasoning process needs a complex encoding in order to capture reasoning on negative information. In this paper, we consider the case of knowledge bases in $\textit{DL-Lite}_{\cal R}$, i.e. the language underlying OWL QL. We provide a definition for $\textit{DL-Lite}_{\cal R}$ knowledge bases with defeasible axioms and study their properties. The limited form of $\textit{DL-Lite}_{\cal R}$ axioms allows us to formulate a simpler encoding into datalog (under answer set semantics) with direct rules for reasoning on negative information. The resulting materialization method gives rise to a complete reasoning procedure for instance checking in $\textit{DL-Lite}_{\cal R}$ with defeasible axioms.

When proving theorems from large sets of logical assertions, it can be helpful to restrict the search for a proof to those assertions that are relevant, that is, closely related to the theorem in some sense. For example, in the Watson system, a large knowledge base must rapidly be searched for relevant facts. It is possible to define formal concepts of relevance for propositional and first-order logic. Various concepts of relevance have been defined for this, and some have yielded good results on large problems. We consider here in particular a concept based on alternating paths.We present efficient graph-based methods for computing alternating path relevance and give some results indicating its effectiveness. We also propose an alternating path based extension of this relevance method to DPLL with an improved time bound, and give other extensions to alternating path relevance intended to improve its performance.

Humans prove theorems by relying on substantial high-level reasoning and problem-specific insights. Proof assistants offer a formalism that resembles human mathematical reasoning, representing theorems in higher-order logic and proofs as high-level tactics. However, human experts have to construct proofs manually by entering tactics into the proof assistant. In this paper, we study the problem of using machine learning to automate the interaction with proof assistants. We construct CoqGym, a large-scale dataset and learning environment containing 71K human-written proofs from 123 projects developed with the Coq proof assistant. We develop ASTactic, a deep learning-based model that generates tactics as programs in the form of abstract syntax trees (ASTs). Experiments show that ASTactic trained on CoqGym can generate effective tactics and can be used to prove new theorems not previously provable by automated methods. Code is available at https://github.com/princeton-vl/CoqGym.

In AI, FSCs are much sought after for automated planning paradigms such as generalized planning, as in Figure 1, where one attempts to synthesize a controller that works in multiple initial states. Such controllers are usually handwritten by domain experts, which is problematic when expert knowledge is either unavailable or unreliable. To that end, the automated synthesis of FSCs has received considerable attention in recent years, e.g., [16, 7, 26, 24, 11, 27]. Of course, FSCs synthesis is closely related to program synthesis [16], and FSCs are frequently seen as program-like plans [17], and recent synthesis literature involves an exciting exchange of technical insights between the two fields [26]; representative examples include the use of program synthesis to infer high-level action types [25], and the use of partial order planning for imperative program synthesis [13]. Naturally, from an algorithmic perspective, the two most immediate questions are: in which sense are controllers correct, and how do we synthesize controllers that are provably correct?