Logic & Formal Reasoning
SMT-based Constraint Answer Set Solver EZSMT+
Constraint answer set programming integrates answer set programming with constraint processing. System EZSMT+ is a constraint answer set programming tool that utilizes satisfiability modulo theory solvers for search. Its theoretical foundation lies on generalizations of Niemela's characterization of answer sets of a logic program via so called level rankings.
Siamese recurrent networks learn first-order logic reasoning and exhibit zero-shot compositional generalization
Can neural nets learn logic? We approach this classic question with current methods, and demonstrate that recurrent neural networks can learn to recognize first order logical entailment relations between expressions. We define an artificial language in first-order predicate logic, generate a large dataset of sample 'sentences', and use an automatic theorem prover to infer the relation between random pairs of such sentences. We describe a Siamese neural architecture trained to predict the logical relation, and experiment with recurrent and recursive networks. Siamese Recurrent Networks are surprisingly successful at the entailment recognition task, reaching near perfect performance on novel sentences (consisting of known words), and even outperforming recursive networks. We report a series of experiments to test the ability of the models to perform compositional generalization. In particular, we study how they deal with sentences of unseen length, and sentences containing unseen words. We show that set-ups using LSTMs and GRUs obtain high scores on these tests, demonstrating a form of compositionality.
Synthesizing Datalog Programs using Numerical Relaxation
Si, Xujie, Raghothaman, Mukund, Heo, Kihong, Naik, Mayur
The problem of learning logical rules from examples arises in diverse fields, including program synthesis, logic programming, and machine learning. Existing approaches either involve solving computationally difficult combinatorial problems, or performing parameter estimation in complex statistical models. In this paper, we present Difflog, a technique to extend the logic programming language Datalog to the continuous setting. By attaching real-valued weights to individual rules of a Datalog program, we naturally associate numerical values with individual conclusions of the program. Analogous to the strategy of numerical relaxation in optimization problems, we can now first determine the rule weights which cause the best agreement between the training labels and the induced values of output tuples, and subsequently recover the classical discrete-valued target program from the continuous optimum. We evaluate Difflog on a suite of 34 benchmark problems from recent literature in knowledge discovery, formal verification, and database query-by-example, and demonstrate significant improvements in learning complex programs with recursive rules, invented predicates, and relations of arbitrary arity.
Out of Sight But Not Out of Mind: An Answer Set Programming Based Online Abduction Framework for Visual Sensemaking in Autonomous Driving
Suchan, Jakob, Bhatt, Mehul, Varadarajan, Srikrishna
We demonstrate the need and potential of systematically integrated vision and semantics} solutions for visual sensemaking (in the backdrop of autonomous driving). A general method for online visual sensemaking using answer set programming is systematically formalised and fully implemented. The method integrates state of the art in (deep learning based) visual computing, and is developed as a modular framework usable within hybrid architectures for perception & control. We evaluate and demo with community established benchmarks KITTIMOD and MOT. As use-case, we focus on the significance of human-centred visual sensemaking ---e.g., semantic representation and explainability, question-answering, commonsense interpolation--- in safety-critical autonomous driving situations.
Definitively Identifying an Inherent Limitation to Actual Cognition
A century ago, discoveries of a serious kind of logical error made separately by several leading mathematicians led to acceptance of a sharply enhanced standard for rigor within what ultimately became the foundation for Computer Science. By 1931, Godel had obtained a definitive and remarkable result: an inherent limitation to that foundation. The resulting limitation is not applicable to actual human cognition, to even the smallest extent, unless both of these extremely brittle assumptions hold: humans are infallible reasoners and reason solely via formal inference rules. Both assumptions are contradicted by empirical data from well-known Cognitive Science experiments. This article investigates how a novel multi-part methodology recasts computability theory within Computer Science to obtain a definitive limitation whose application to human cognition avoids assumptions contradicting empirical data. The limitation applies to individual humans, to finite sets of humans, and more generally to any real-world entity.
Towards Finding Longer Proofs
Zombori, Zsolt, Csiszárik, Adrián, Michalewski, Henryk, Kaliszyk, Cezary, Urban, Josef
We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). FLoP focuses on generalizing from short proofs to longer ones of similar structure. To achieve that, FLoP uses state-of-the-art RL approaches that were previously not applied in theorem proving. In particular, we show that curriculum learning significantly outperforms previous learning-based proof guidance on a synthetic dataset of increasingly difficult arithmetic problems.
A Boxology of Design Patterns for Hybrid Learning and Reasoning Systems
van Harmelen, Frank, Teije, Annette ten
We propose a set of compositional design patterns to describe a large variety of systems that combine statistical techniques from machine learning with symbolic techniques from knowledge representation. As in other areas of computer science (knowledge engineering, software engineering, ontology engineering, process mining and others), such design patterns help to systematize the literature, clarify which combinations of techniques serve which purposes, and encourage re-use of software components. We have validated our set of compositional design patterns against a large body of recent literature.
Induction of Non-Monotonic Rules From Statistical Learning Models Using High-Utility Itemset Mining
Shakerin, Farhad, Gupta, Gopal
We present a fast and scalable algorithm to induce non-monotonic logic programs from statistical learning models. We reduce the problem of search for best clauses to instances of the High-Utility Itemset Mining (HUIM) problem. In the HUIM problem, feature values and their importance are treated as transactions and utilities respectively. We make use of TreeExplainer, a fast and scalable implementation of the Explainable AI tool SHAP, to extract locally important features and their weights from ensemble tree models. Our experiments with UCI standard benchmarks suggest a significant improvement in terms of classification evaluation metrics and running time of the training algorithm compared to ALEPH, a state-of-the-art Inductive Logic Programming (ILP) system.
Blocksworld Revisited: Learning and Reasoning to Generate Event-Sequences from Image Pairs
Gokhale, Tejas, Sampat, Shailaja, Fang, Zhiyuan, Yang, Yezhou, Baral, Chitta
The process of identifying changes or transformations in a scene along with the ability of reasoning about their causes and effects, is a key aspect of intelligence. In this work we go beyond recent advances in computational perception, and introduce a more challenging task, Image-based Event-Sequencing (IES). In IES, the task is to predict a sequence of actions required to rearrange objects from the configuration in an input source image to the one in the target image. IES also requires systems to possess inductive generalizability. Motivated from evidence in cognitive development, we compile the first IES dataset, the Blocksworld Image Reasoning Dataset (BIRD) which contains images of wooden blocks in different configurations, and the sequence of moves to rearrange one configuration to the other. We first explore the use of existing deep learning architectures and show that these end-to-end methods under-perform in inferring temporal event-sequences and fail at inductive generalization. We then propose a modular two-step approach: Visual Perception followed by Event-Sequencing, and demonstrate improved performance by combining learning and reasoning. Finally, by showing an extension of our approach on natural images, we seek to pave the way for future research on event sequencing for real world scenes.
Dynamic Epistemic Logic with ASP Updates: Application to Conditional Planning
Cabalar, Pedro, Fandinno, Jorge, del Cerro, Luis Fariñas
Dynamic Epistemic Logic (DEL) is a family of multimodal logics that has proved to be very successful for epistemic reasoning in planning tasks. In this logic, the agent's knowledge is captured by modal epistemic operators whereas the system evolution is described in terms of (some subset of) dynamic logic modalities in which actions are usually represented as semantic objects called event models. In this paper, we study a variant of DEL, that wecall DEL[ASP], where actions are syntactically described by using an Answer Set Programming (ASP) representation instead of event models. This representation directly inherits high level expressive features like indirect effects, qualifications, state constraints, defaults, or recursive fluents that are common in ASP descriptions of action domains. Besides, we illustrate how this approach can be applied for obtaining conditional plans in single-agent, partially observable domains where knowledge acquisition may be represented as indirect effects of actions.