This paper presents LEXR, a framework for explaining the decision making of recurrent neural networks (RNNs) using a formal description language called Linear Temporal Logic (LTL). LTL is the de facto standard for the specification of temporal properties in the context of formal verification and features many desirable properties that make the generated explanations easy for humans to interpret: it is a descriptive language, it has a variable-free syntax, and it can easily be translated into plain English. To generate explanations, LEXR follows the principle of counterexample-guided inductive synthesis and combines Valiant's probably approximately correct learning (PAC) with constraint solving. We prove that LEXR's explanations satisfy the PAC guarantee (provided the RNN can be described by LTL) and show empirically that these explanations are more accurate and easier-to-understand than the ones generated by recent algorithms that extract deterministic finite automata from RNNs.

In the real world, linguistic agents are also embodied agents: they perceive and act in the physical world. The notion of Language Grounding questions the interactions between language and embodiment: how do learning agents connect or ground linguistic representations to the physical world ? This question has recently been approached by the Reinforcement Learning community under the framework of instruction-following agents. In these agents, behavioral policies or reward functions are conditioned on the embedding of an instruction expressed in natural language. This paper proposes another approach: using language to condition goal generators. Given any goal-conditioned policy, one could train a language-conditioned goal generator to generate language-agnostic goals for the agent. This method allows to decouple sensorimotor learning from language acquisition and enable agents to demonstrate a diversity of behaviors for any given instruction. We propose a particular instantiation of this approach and demonstrate its benefits.

Data preprocessing is an important component of machine learning pipelines, which requires ample time and resources. An integral part of preprocessing is data transformation into the format required by a given learning algorithm. This paper outlines some of the modern data processing techniques used in relational learning that enable data fusion from different input data types and formats into a single table data representation, focusing on the propositionalization and embedding data transformation approaches. While both approaches aim at transforming data into tabular data format, they use different terminology and task definitions, are perceived to address different goals, and are used in different contexts. This paper contributes a unifying framework that allows for improved understanding of these two data transformation techniques by presenting their unified definitions, and by explaining the similarities and differences between the two approaches as variants of a unified complex data transformation task. In addition to the unifying framework, the novelty of this paper is a unifying methodology combining propositionalization and embeddings, which benefits from the advantages of both in solving complex data transformation and learning tasks. We present two efficient implementations of the unifying methodology: an instance-based PropDRM approach, and a feature-based PropStar approach to data transformation and learning, together with their empirical evaluation on several relational problems. The results show that the new algorithms can outperform existing relational learners and can solve much larger problems.

Descriptor revision by Hansson is a framework for addressing the problem of belief change. In descriptor revision, different kinds of change processes are dealt with in a joint framework. Individual change requirements are qualified by specific success conditions expressed by a belief descriptor, and belief descriptors can be combined by logical connectives. This is in contrast to the currently dominating AGM paradigm shaped by Alchourr\'on, G\"ardenfors, and Makinson, where different kinds of changes, like a revision or a contraction, are dealt with separately. In this article, we investigate the realisation of descriptor revision for a conditional logic while restricting descriptors to the conjunction of literal descriptors. We apply the principle of conditional preservation developed by Kern-Isberner to descriptor revision for conditionals, show how descriptor revision for conditionals under these restrictions can be characterised by a constraint satisfaction problem, and implement it using constraint logic programming. Since our conditional logic subsumes propositional logic, our approach also realises descriptor revision for propositional logic.

Rintanen and Gretton 2013; Abdulaziz, Gretton, and Norrish Many techniques for solving problems defined on transition 2015; Abdulaziz, Gretton, and Norrish 2017; Abdulaziz systems, like SATbased planning (Kautz and Selman 2019). Such compositional methods are currently the only 1992) and bounded model checking (Biere et al. 1999), benefit practically viable method to compute bounds on plan lengths from knowledge of upper bounds on the lengths of solution or the state space diameter. Compositional approaches provide transition sequences, aka completeness thresholds. If N useful approximations of plan bounds using smaller is such a bound, and if a solution exists, then that solution computational effort, since only explicit representations of need not comprise more than N transitions.

Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from achieving a large scale success in this field. In this data description, we present a simple dataset that contains data on over 400k proof method applications along with over 100 extracted features for each in a format that can be processed easily without any knowledge about formal logic. Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL without requiring domain expertise in logic.

Markov decision processes are of major interest in the planning community as well as in the model checking community. But in spite of the similarity in the considered formal models, the development of new techniques and methods happened largely independently in both communities. This work is intended as a beginning to unite the two research branches. We consider goal-reachability analysis as a common basis between both communities. The core of this paper is the translation from Jani, an overarching input language for quantitative model checkers, into the probabilistic planning domain definition language (PPDDL), and vice versa from PPDDL into Jani. These translations allow the creation of an overarching benchmark collection, including existing case studies from the model checking community, as well as benchmarks from the international probabilistic planning competitions (IPPC). We use this benchmark set as a basis for an extensive empirical comparison of various approaches from the model checking community, variants of value iteration, and MDP heuristic search algorithms developed by the AI planning community. On a per benchmark domain basis, techniques from one community can achieve state-ofthe-art performance in benchmarks of the other community. Across all benchmark domains of one community, the performance comparison is however in favor of the solvers and algorithms of that particular community. Reasons are the design of the benchmarks, as well as tool-related limitations. Our translation methods and benchmark collection foster crossfertilization between both communities, pointing out specific opportunities for widening the scope of solvers to different kinds of models, as well as for exchanging and adopting algorithms across communities.

AlphaZero learns to play go, chess and shogi at a superhuman level through self play given only the rules of the game. This raises the question of whether a similar thing could be done for mathematics -- a MathZero. MathZero would require a formal foundation and an objective. We propose the foundation of set-theoretic dependent type theory and an objective defined in terms of the classification problem -- the problem of classifying concept instances up to isomorphism. The natural numbers arise as the solution to the classification problem for finite sets. Here we generalize classical Bourbaki set-theoretic isomorphism to set-theoretic dependent type theory. To our knowledge we give the first isomorphism inference rules for set-theoretic dependent type theory with propositional set-theoretic equality. The presentation is intended to be accessible to mathematicians with no prior exposure to type theory.

Reasoning over streams of input data is an essential part of human intelligence. During the last decade {\em stream reasoning} has emerged as a research area within the AI-community with many potential applications. In fact, the increased availability of streaming data via services like Google and Facebook has raised the need for reasoning engines coping with data that changes at high rate. Recently, the rule-based formalism {\em LARS} for non-monotonic stream reasoning under the answer set semantics has been introduced. Syntactically, LARS programs are logic programs with negation incorporating operators for temporal reasoning, most notably {\em window operators} for selecting relevant time points. Unfortunately, by preselecting {\em fixed} intervals for the semantic evaluation of programs, the rigid semantics of LARS programs is not flexible enough to {\em constructively} cope with rapidly changing data dependencies. Moreover, we show that defining the answer set semantics of LARS in terms of FLP reducts leads to undesirable circular justifications similar to other ASP extensions. This paper fixes all of the aforementioned shortcomings of LARS. More precisely, we contribute to the foundations of stream reasoning by providing an operational fixed point semantics for a fully flexible variant of LARS and we show that our semantics is sound and constructive in the sense that answer sets are derivable bottom-up and free of circular justifications.

Recent work in proof theory has shed some light on the possibility of modeling reasoning while avoiding undesirable formal paradoxes. Based on category theory and inspired by the seminal work of J. Lambek, monoidal logics were introduced as a foundational framework that allows to treat a wide range of formal systems, including substructural logics (e.g., the syntactic calculus, linear logic, relevant logic, etc.), algebras (e.g., Kleene algebra) as well as intuitionistic, intermediate, and classical logic. This framework has been extended to modal logics and has been used to model normative reasoning, actions and knowledge, and it has been shown that non-classical logics better deal with the formal problems that are usually related to these notions. As such, non-classical systems of modal logics were proposed to model reasoning, actions and knowledge, but unresolved problems remained as to how to deal with conflicting obligations when facing normative inconsistencies. In this paper, we expose this problem and sketch an avenue for future research that might overcome this limitation.