This report explores the evolution and current state of neuro- symbolic artificial intelligence, an approach that integrates neural network capabilities with symbolic reasoning. We trace the historical context from early AI aspirations to modern implementations and successes, highlighting key paradigms, and other logical and semantical considerations. We argue against the “scaling is all you need” hypothesis, and point to persistent challenges in reliable symbolic reasoning with deep and large models. We conclude by suggesting that despite numerous implementation choices and the ”broad church” nature of neuro-symbolic AI, these approaches offer the most promising path towards AI systems that combine pattern recognition with robust reasoning, particularly for applications requiring structured knowledge, explainability, and trustworthiness.

Learning defaults is a longstanding goal in the field of knowledge representation and reasoning. We provide a novel method for learning defaults by way of introducing a new predicate: the abnormal predicate, which explicitly covers all the exceptions to a rule, thus forming a default theory. Our proposed method for learning defaults is sound and complete for all rule-exceptions, and can be extended for use on other frameworks.

Issues of safety, explainability, and efficiency are of increasing concern in learning systems deployed with hard and soft constraints. Loss-function based techniques have shown promising results in this area, by embedding logical constraints during neural network training. Through an integration of logic and information geometry, we provide a construction and theoretical framework for these tasks that generalize many approaches. We propose a loss-based method that embeds knowledge—enforces logical constraints—into a machine learning model that outputs probability distributions. This is done by constructing a distribution from the logical formula, and constructing a loss function as a linear combination of the original loss function with the Fisher-Rao distance or Kullback-Leibler divergence to the constraint distribution. This construction is primarily for logical constraints in the form of propositional formulas (Boolean variables), but can be extended to formulas of a first-order language with finite variables over a model with compact domain (categorical and continuous variables), and others statistical models that is to be trained with semantic information. We evaluate our method on a variety of learning tasks, including classification tasks with logic constraints, transferring knowledge from logic formulas, and knowledge distillation.

Cosmological simulations aim to understand the matter distribution in the universe by employing either semi-analytic methods or hydrodynamical models of matter distribution. These simulations describe the evolution of baryonic structures within dark matter potential wells, where dark matter is modeled as a self-gravitating, collisionless system. Despite advances in reducing computational costs, these simulations still require millions of CPU hours to achieve stable solutions. This raises the question: can generative models predict galaxy properties from a partial history of their dynamical evolution? Tractable probabilistic models, such as sum-product networks, enable efficient computation of conditional probabilities, allowing conditional marginals to be computed in time linear to the model size. In this work, we investigate the application of sum-product networks to compactly represent and learn distributions for predictions in concordance cosmology. Using the Eagle suite of cosmological hydrodynamical simulations, we demonstrate that these graphical models can effectively reproduce mock galaxy catalogs, capturing the relationship between baryonic and dark matter with promising accuracy.

A computational ethics framework is essential for AI and autonomous systems operating in complex, real-world environments. Existing approaches often lack the adaptability needed to integrate ethical principles into dynamic and ambiguous contexts, limiting their effectiveness across diverse scenarios. To address these challenges, we outline the necessary ingredients for building a holistic, meta-level framework that combines intermediate representations, probabilistic reasoning, and knowledge representation. The specifications therein emphasize scalability, supporting ethical reasoning at both individual decision-making levels and within the collective dynamics of multi-agent systems. By integrating theoretical principles with contextual factors, it facilitates structured and context-aware decision-making, ensuring alignment with overarching ethical standards. We further explore proposed theorems outlining how ethical reasoners should operate, offering a foundation for practical implementation. These constructs aim to support the development of robust and ethically reliable AI systems capable of navigating the complexities of real-world moral decision-making scenarios.

The deployment of autonomous agents that interact with humans in safety-critical situations raises new research problems as we move towards fully autonomous systems in domains such as autonomous vehicles or search and rescue. If autonomous agents are placed in a dilemma, how would they act? The literature in computational ethics has explored the actions and learning methods that emerge in ethical dilemmas. However, our position paper examines how ethical dilemmas are not isolated in a social vacuum. Our central claim in our position paper is that to enable trust among all human users, a neuralsymbolic verification of moral preference alignment is required. We propose that the formal robustness properties be applied to social choice modelling. We outline how robustness properties can help validate the formation of stable social preference clusters in deep neural network classifiers. Our initial results highlight the vulnerabilities of models in moral-critical scenarios to perturbations, suggesting a verification-training loop for improved robustness. We position this work as an inquiry into the viability of verifying moral preference alignment, based on our initial results. Ultimately, we aim to contribute to the broader interdisciplinary effort that integrates formal methods, social choice theory, and empirical moral psychology for interpretable computational ethics.

Integrating fairness into machine learning models has been an important consideration for the last decade. Here, neurosymbolic models offer a valuable opportunity, as they allow the specification of symbolic, logical constraints that are often guaranteed to be satisfied. However, research on neurosymbolic applications to algorithmic fairness is still in an early stage. With our work, we bridge this gap by integrating counterfactual fairness into the neurosymbolic framework of Logic Tensor Networks (LTN). We use LTN to express accuracy and counterfactual fairness constraints in first-order logic and employ them to achieve desirable levels of both performance and fairness at training time. Our approach is agnostic to the underlying causal model and data generation technique; as such, it may be easily integrated into existing pipelines that generate and extract counterfactual examples. We show, through concrete examples on three real-world datasets, that logical reasoning about counterfactual fairness has some important advantages, among which its intrinsic interpretability, and its flexibility in handling subgroup fairness. Compared to three recent methodologies in counterfactual fairness, our experiments show that a neurosymbolic, LTN-based approach attains better levels of counterfactual fairness.

There is a fundamental trade-off between the expressiveness of the language and the tractability of the reasoning task in knowledge representation. On the one hand it is widely acknowledged that relations and more generally, the expressiveness of first-order logic is extremely useful for capturing concepts required for common-sense reasoning. But at the same time the entailment problem is only semi-decidable. There have been a wide range of approaches to deal with this trade-off, from restricting the language to propositional logic to limit the expressiveness of the language in terms of the arity of the predicates (as in description logics) or the use of negation (as in Horn logic) to limit reasoning by weakening the entailment relation using non-standard semantics. In this work, we address a gap in this literature. We show that there is an intuitive fragment of first-order disjunctive knowledge, for which reasoning is decidable and can be reduced to propositional satisfiability. Knowledge bases in this fragment correspond to universally quantified first-order clauses, but without arity restrictions and without restrictions on the appearance of negation. Queries, however, are expected to be ground formulas. We achieve this result by showing how the entailment over infinitely many infinite-sized structures can be reduced to a search over finitely many finite-size structures. The crux of the argument lies in showing that constants not mentioned in the knowledge base and/or query behave identically (in a suitable formal sense). We then go on to also show that there is also an extension to this result for function symbols.

Abstract Deep neural networks, despite their capabilities, are constrained by the need for large-scale training data, and often fall short in generalisation and interpretability. Inductive logic programming (ILP) presents an intriguing solution with its data-efficient learning of first-order logic rules. However, ILP grapples with challenges, notably the handling of non-linearity in continuous domains. With the ascent of neuro-symbolic ILP, there’s a drive to mitigate these challenges, synergising deep learning with relational ILP models to enhance interpretability and create logical decision boundaries. In this research, we introduce a neuro-symbolic ILP framework, grounded on differentiable Neural Logic networks, tailored for non-linear rule extraction in mixed discrete-continuous spaces. Our methodology consists of a neuro-symbolic approach, emphasising the extraction of non-linear functions from mixed domain data. Our preliminary findings showcase our architecture’s capability to identify non-linear functions from continuous data, offering a new perspective in neural-symbolic research and underlining the adaptability of ILP-based frameworks for regression challenges in continuous scenarios.

Abstract Machine learning (ML) applications have automated numerous real-life tasks, improving both private and public life. However, the black-box nature of many state-of-the-art models poses the challenge of model verification; how can one be sure that the algorithm bases its decisions on the proper criteria, or that it does not discriminate against certain minority groups? In this paper we propose a way to generate diverse counterfactual explanations from multilinear models, a broad class which includes Random Forests, as well as Bayesian Networks.

Belief-based programming is a probabilistic extension of the Golog programming language family, where every action and sensing could be noisy and every test refers to the subjective beliefs of the agent. Such characteristics make it rather suitable for robot control in a partial-observable uncertain environment. Recently, efforts have been made in providing formal semantics for belief programs and investigating the hardness of verifying belief programs. Nevertheless, a general algorithm that actually conducts the verification is missing. In this paper, we propose an algorithm based on symbolic dynamic programming to verify belief programs, an approach that generalizes the dynamic programming technique for solving (partially observable) Markov decision processes, i.e. (PO)MDP, by exploiting the symbolic structure in the solution of first-order (PO)MDPs induced by belief program execution.

Sum-product networks guarantee that conditionals and marginals can be computed efficiently, for a wide range of models, bypassing the hardness of inference. However, this advantage comes at the expense of transparency, since it is unclear how variables interact in sum-product networks. Due to this, a series of decompilation algorithms transform sum-product networks back to Bayesian networks. In this work, we first study the transparency and causal utility of the resulting Bayesian networks. We then propose a novel decompilation algorithm to address the identified limitations.

Reinforcement learning has made significant strides in recent years, including in the development of Atari and Go-playing agents. It is now widely acknowledged that logical syntax adds considerable flexibility in both the modelling of domains as well as the interpretability of domains. In this survey paper, we cover the fundamentals of how logic, reinforcement learning, and deep learning can be unified, with some ideas for future work.

Artificial intelligence (AI) and especially machine learning (ML) has been increasingly incorporated into a wide range of critical applications, such as healthcare, justice, credit risk assessment, and loan approval. In this paper, we survey the motivations for caring about model transparency, especially as AI systems are becoming increasingly complex leviathans with many moving parts. We then briefly outline the challenges in providing computational solutions to transparency.

The unification of logic and probability has been seen as a long-standing concern in philosophy and mathematical logic. In this paper, we propose a new general probabilistic modal logic of belief and only-believing in the situation calculus. Our logic can express both continuous and discrete degrees of belief. More importantly, expressing degrees of belief for arbitrary first-order formulas in a dynamic setting is possible for the first time, going well beyond previous proposals where fluents are assumed to be nullary or discrete. We show that our notion of belief retains many of the properties known from the previous related work.

First-order model counting (FOMC) is a computational problem that asks to count the models of a sentence in finite-domain first-order logic. In this paper, we argue that the capabilities of FOMC algorithms to date are limited by their inability to express many types of recursive computations. To enable such computations, we relax the restrictions that typically accompany domain recursion and generalise the circuits used to express a solution to an FOMC problem to directed graphs that may contain cycles. To this end, we adapt the most well-established (weighted) FOMC algorithm ForcLift to work with such graphs and introduce new compilation rules that can create cycle-inducing edges that encode recursive function calls. These improvements allow the algorithm to find efficient solutions to counting problems that were previously beyond its reach, including those that cannot be solved efficiently by any other exact FOMC algorithm. We end with a few conjectures on what classes of instances could be domain-liftable as a result.

Abstract Fairness in machine learning is of considerable interest in recent years owing to the propensity of algorithms trained on historical data to amplify and perpetuate historical biases. In this paper, we argue for a formal reconstruction of fairness definitions, not so much to replace existing definitions but to ground their application in an epistemic setting and allow for rich environmental modeling. Consequently we look into three notions: fairness through unawareness, demographic parity and counterfactual fairness, and formalize these in the epistemic situation calculus.

Abstract The tension between deduction and induction is perhaps the most fundamental issue in areas such as philosophy, cognition, and artificial intelligence. In an influential paper,Valiantrecognized that the challenge of learning should be integrated with deduction. In particular, he proposed a semantics to capture the quality possessed by the output ofprobably approximately correct(PAC) learning algorithms when formulated in a logic. Although weaker than classical entailment, it allows for a powerful model-theoretic framework for answering queries. In this paper, we provide a new technical foundation to demonstrate PAC learning with multi-agent epistemic logics. To circumvent the negative results in the literature on the difficulty of robust learning with the PAC semantics, we consider so-called implicit learning where we are able to incorporate observations to the background theory in service of deciding the entailment of an epistemic query. We prove correctness of the learning procedure and discuss results on the sample complexity, that is how many observations we will need to provably assert that the query is entailed given a user-specified error bound. Finally, we investigate under what circumstances this algorithm can be made efficient. On the last point, given that reasoning in epistemic logics especially in multi-agent epistemic logics is PSPACE-complete, it might seem like there is no hope for this problem. We leverage some recent results on the so-calledRepresentation Theoremexplored for single-agent and multi-agent epistemic logics with theonly knowingoperator to reduce modal reasoning to propositional reasoning.

We propose a novel way to incorporate expert knowledge into the training of deep neural networks. Many approaches encode domain constraints directly into the network architecture, requiring non-trivial or domain-specific engineering. In contrast, our approach, called MultiplexNet, represents domain knowledge as a quantifier-free logical formula in disjunctive normal form (DNF) which is easy to encode and to elicit from human experts. It introduces a latent Categorical variable that learns to choose which constraint term optimizes the error function of the network and it compiles the constraints directly into the output of existing learning algorithms. We demonstrate the efficacy of this approach empirically on several classical deep learning tasks, such as density estimation and classification in both supervised and unsupervised settings where prior knowledge about the domains was expressed as logical constraints. Our results show that the MultiplexNet approach learned to approximate unknown distributions well, often requiring fewer data samples than the alternative approaches. In some cases, MultiplexNet finds better solutions than the baselines; or solutions that could not be achieved with the alternative approaches. Our contribution is in encoding domain knowledge in a way that facilitates inference. We specifically focus on quantifier-free logical formulae that are specified over the output domain of a network. We show that this approach is both efficient and general; and critically, our approach guarantees 100% constraint satisfaction in a network's output.

In automated planning, there has been a recent interest in solving a class of problems, where a single solution applies for multiple, possibly infinitely many, instances. This necessitates a generalized notion of plans, such as plans with loops. However, the correctness of such plans is non-trivial to define, making it difficult to provide a clear specification of what we should be looking for. In an influential paper, Levesque proposed a formal specification for analyzing the correctness of such plans. He motivated a logical characterization within the situation calculus that included binary sensing actions. This characterization argued that from each state considered possible initially, the plan should terminate while satisfying the goal. Increasingly, classical plan structures are being applied to stochastic environments such as robotics applications. This raises the question as to what the specification for correctness should look like, since Levesque's account makes the assumption that actions are deterministic. In this work, we aim to generalize Levesque's account to handle actions with nondeterministic outcomes, which may also be accorded probabilities. By appealing to an extension of the situation calculus to handle probabilistic nondeterminism, we will show that Levesque's definition, as well as a notion of goal achievability proposed by Lin and Levesque, have limited appeal under stochastic nondeterminism. In essence, they correspond to one correct execution, which is unlikely to be adequate. Rather, we propose to delineate between goal satisfaction and termination leading to a range of correctness criteria. To better study these criteria, and to position the results in a broader context while still allowing for the generality of the situation calculus, we consider an abstract framework to study the correctness of plans with loops, in domains that are possibly unbounded, and/or stochastic, and/or continuous. Within that framework, we then prove numerous relationships between the criteria, including some impossibility results for categorically satisfying goals. Finally, we show that these notions provide a more granular view than those discussed in the literature, such as strong planning and strong cyclic planning.

Convolutional Neural Networks have achieved state-of-the-art performance in image classification. Their lack of ability to recognise the spatial relationship between features, however, leads to misclassification of the variants of the same image. Capsule Networks were introduced to address this issue by incorporating the spatial information of image features into neural networks. In this paper, we are interested in showcasing the digit recognition task on CAPTCHA images, widely considered a challenge for computers in relation to human capabilities. Our intention is to provide a rigorous empirical regime in which we can compare the competitive performance of Capsule Networks against the Convolutional Neural Networks. Indeed since CAPTCHA distorts images, by adjusting the spatial positioning of features, we aim to demonstrate the advantages and limitations of Capsule Networks architecture. We train the Capsule Networks with Dynamic Routing version and the convolutional-neural-network-based deep-CAPTCHA baseline model to predict the digit sequences on numerical CAPTCHAs, investigate the performance results and propose two improvements to the Capsule Networks model.

Robust learning in expressive languages with real-world data continues to be a challenging task. Numerous conventional methods appeal to heuristics without any assurances of robustness. While probably approximately correct (PAC) Semantics offers strong guarantees, learning explicit representations is not tractable, even in propositional logic. However, recent work on so-called “implicit" learning has shown tremendous promise in terms of obtaining polynomial-time results for fragments of first-order logic. In this work, we extend implicit learning in PAC-Semantics to handle noisy data in the form of intervals and threshold uncertainty in the language of linear arithmetic. We prove that our extended framework keeps the existing polynomial-time complexity guarantees. Furthermore, we provide the first empirical investigation of this hitherto purely theoretical framework. Using benchmark problems, we show that our implicit approach to learning optimal linear programming objective constraints significantly outperforms an explicit approach in practice.

Weighted model counting (WMC) has emerged as the unifying inference mechanism across many (probabilistic) domains. Encoding an inference problem as an instance of WMC typically necessitates adding extra literals and clauses. This is partly so because the predominant definition of WMC assigns weights to models based on weights on literals, and this severely restricts what probability distributions can be represented. We develop a measure-theoretic perspective on WMC and propose a way to encode conditional weights on literals analogously to conditional probabilities. This representation can be as succinct as standard WMC with weights on literals but can also expand as needed to represent probability distributions with less structure. To demonstrate the performance benefits of conditional weights over the addition of extra literals, we develop a new WMC encoding for Bayesian networks and adapt a state-of-the-art WMC algorithm ADDMC to the new format. Our experiments show that the new encoding significantly improves the performance of the algorithm on most benchmark instances.

Exact inference in probabilistic graphical models is particularly challenging in the presence of relational and other deterministic constraints. For discrete domains, weighted model counting has emerged as an effective and general approach in a variety of formalisms. Weighted first-order model counting, which allows relational atoms and function-free first order logic has pushed the envelope further, by exploiting symmetry properties over indistinguishable groups of objects, and by extension avoids the need to perform inference on the exponential ground theory. Given the limitation to discrete domains, the formulation of weighted model integration was proposed as an extension to weighted model counting for mixed discrete-continuous domains over both symbolic and numeric weight functions. While that formulation has enjoyed considerable attention in recent years, there is very little understanding on whether the task can be solved at a lifted level, that is, whether we can reason with relational models by avoiding grounding. In this paper, we consider this question. We show how to generalize algorithmic ideas known in the circuit compilation for function-free lifted inference to functions with a continuous range.

Abstract Moral responsibility is a major concern in autonomous systems, with applications ranging from self-driving cars to kidney exchanges. Although there have been recent attempts to formalise responsibility and blame, among similar notions, the problem of learning within these formalisms has been unaddressed. From the viewpoint of such systems, the urgent questions are: (a) How can models of moral scenarios and blameworthiness be extracted and learnt automatically from data? (b) How can judgements be computed effectively and efficiently, given the split-second decision points faced by some systems? By building on constrained tractable probabilistic learning, we propose and implement a hybrid (between data-driven and rule-based methods) learning framework for inducing models of such scenarios automatically from data and reasoning tractably from them. We report on experiments that compare our system with human judgement in three illustrative domains: lung cancer staging, teamwork management, and trolley problems.

Programming or scripting languages used in real-world systems are seldom designed with a formal semantics in mind from the outset. Therefore, developing well-founded analysis tools for these systems requires reverse-engineering a formal semantics as a first step. This can take months or years of effort. Can we (at least partially) automate this process? Though desirable, automatically reverse-engineering semantics rules from an implementation is very challenging, as found by Krishnamurthi, Lerner and Elberty. In this paper, we highlight that scaling methods with the size of the language is very difficult due to state space explosion, so we propose to learn semantics incrementally. We give a formalisation of Krishnamurthi et al.'s desugaring learning framework in order to clarify the assumptions necessary for an incremental learning algorithm to be feasible. We show that this reformulation allows us to extend the search space and express rules that Krishnamurthi et al. described as challenging, while still retaining feasibility. We evaluate enumerative synthesis as a baseline algorithm, and demonstrate that, with our reformulation of the problem, it is possible to learn correct desugaring rules for the example source and core languages proposed by Krishnamurthi et al., in most cases identical to the intended rules. In addition, with user guidance, our system was able to synthesize rules for desugaring list comprehensions and try/catch/finally constructs.

The unification of low-level perception and high-level reasoning is a long-standing problem in artificial intelligence, which has the potential to not only bring the areas of logic and learning closer together but also demonstrate how abstract concepts might emerge from sensory data. Precisely because deep learning methods dominate perception-based learning, including vision, speech, and linguistic grammar, there is fast-growing literature on how to integrate symbolic reasoning and deep learning. Broadly, efforts seem to fall into three camps: those focused on defining a logic whose formulas capture deep learning, ones that integrate symbolic constraints in deep learning, and others that allow neural computations and symbolic reasoning to co-exist separately, to enjoy the strengths of both worlds. In this paper, we identify another dimension to this inquiry: what do the hidden layers really capture, and how can we reason about that logically? In particular, we consider variational autoencoders that are widely used for dimensionality reduction and inject a symbolic generative framework onto the feature layer. This allows us, among other things, to generate example images for a class to get a sense of what was learned. Moreover, the modular structure of the proposed model makes it possible to learn relations over multiple images at a time, as well as handle noisy labels. Our empirical evaluations show the promise of this inquiry.

To deploy knowledge-based systems in the real world, the challenge of knowledge acquisition must be addressed. Knowledge engineering by hand is a daunting task, so machine learning has been widely proposed as an alternative. However, machine learning has difficulty acquiring rules that feature the kind of exceptions that are prevalent in real-world knowledge. Moreover, it is conjectured to be impossible to reliably learn representations featuring a desirable level of expressiveness. Works by Khardon and Roth and by Juba proposed solutions to such problems by learning to reason directly, bypassing the intractable step of producing an explicit representation of the learned knowledge. These works focused on Boolean, propositional logics. In this work, we consider such implicit learning to reason for arithmetic theories, including logics considered with satisfiability modulo theory (SMT) solvers. We show that for standard fragments of linear arithmetic, we can learn to reason efficiently. These results are consequences of a more general finding: we show that there is an efficient reduction from the learning to reason problem for a logic to any sound and complete solver for that logic.

Weighted model integration (WMI) extends weighted model counting (WMC) in providing a computational abstraction for probabilistic inference in mixed discrete-continuous domains. WMC has emerged as an assembly language for state-of-the-art reasoning in Bayesian networks, factor graphs, probabilistic programs and probabilistic databases. In this regard, WMI shows immense promise to be much more widely applicable, especially as many real-world applications involve attribute and feature spaces that are continuous and mixed. Nonetheless, state-of-the-art tools for WMI are limited and less mature than their propositional counterparts. In this work, we propose a new implementation regime that leverages propositional knowledge compilation for scaling up inference. In particular, we use sentential decision diagrams, a tractable representation of Boolean functions, as the underlying model counting and model enumeration scheme. Our regime performs competitively to state-of-the-art WMI systems but is also shown to handle a specific class of non-linear constraints over non-linear potentials.

We consider the problem of answering queries about formulas of first-order logic based on background knowledge partially represented explicitly as other formulas, and partially represented as examples independently drawn from a fixed probability distribution. PAC semantics, introduced by Valiant, is one rigorous, general proposal for learning to reason in formal languages: although weaker than classical entailment, it allows for a powerful model theoretic framework for answering queries while requiring minimal assumptions about the form of the distribution in question. To date, however, the most significant limitation of that approach, and more generally most machine learning approaches with robustness guarantees, is that the logical language is ultimately essentially propositional, with finitely many atoms. Indeed, the theoretical findings on the learning of relational theories in such generality have been resoundingly negative. This is despite the fact that first-order logic is widely argued to be most appropriate for representing human knowledge. In this work, we present a new theoretical approach to robustly learning to reason in first-order logic, and consider universally quantified clauses over a countably infinite domain. Our results exploit symmetries exhibited by constants in the language, and generalize the notion of implicit learnability to show how queries can be computed against (implicitly) learned first-order background knowledge.

Weighted model integration (WMI) extends weighted model counting (WMC) to the integration of functions over mixed discrete-continuous probability spaces. It has shown tremendous promise for solving inference problems in graphical models and probabilistic programs. Yet, state-of-the-art tools for WMI are generally limited either by the range of amenable theories, or in terms of performance. To address both limitations, we propose the use of extended algebraic decision diagrams (XADDs) as a compilation language for WMI. Aside from tackling typical WMI problems, XADDs also enable partial WMI yielding parametrized solutions. To overcome the main roadblock of XADDs -- the computational cost of integration -- we formulate a novel and powerful exact symbolic dynamic programming (SDP) algorithm that seamlessly handles Boolean, integer-valued and real variables, and is able to effectively cache partial computations, unlike its predecessor. Our empirical results demonstrate that these contributions can lead to a significant computational reduction over existing probabilistic inference algorithms.

Weighted model counting (WMC) has recently emerged as an effective and general approach to probabilistic inference, offering a computational framework for encoding a variety of formalisms, such as factor graphs and Bayesian networks.The advent of large-scale probabilistic knowledge bases has generated further interest in relational probabilistic representations, obtained by according weights to first-order formulas, whose semantics is given in terms of the ground theory, and solved by WMC. A fundamental limitation is that the domain of quantification, by construction and design, is assumed to be finite, which is at odds with areas such as vision and language understanding, where the existence of objects must be inferred from raw data. Dropping the finite-domain assumption has been known to improve the expressiveness of a first-order language for open-universe purposes, but these languages, so far, have eluded WMC approaches. In this paper, we revisit relational probabilistic models over an infinite domain, and establish a number of results that permit effective algorithms. We demonstrate this language on a number of examples, including a parameterized version of Pearl's Burglary-Earthquake-Alarm Bayesian network.

Numerical optimization is arguably the most prominent computational framework in machine learning and AI. It can be seen as an assembly language for hard combinatorial problems ranging from classification and regression in learning, to computing optimal policies and equilibria in decision theory, to entropy minimization in information sciences. Unfortunately, specifying such problems in complex domains involving relations, objects and other logical dependencies is cumbersome at best, requiring considerable expert knowledge, and solvers require models to be painstakingly reduced to standard forms. To overcome this, we introduce a rich modeling framework for optimization problems that allows convenient codification of symbolic structure. Rather than reducing this symbolic structure to a sparse or dense matrix, we represent and exploit it directly using algebraic decision diagrams (ADDs). Combining efficient ADD-based matrix-vector algebra with a matrix-free interior-point method, we develop an engine that can fully leverage the structure of symbolic representations to solve convex linear and quadratic optimization problems. We demonstrate the flexibility of the resulting symbolic-numeric optimizer on decision making and compressed sensing tasks with millions of non-zero entries.

Logical AI is concerned with formal languages to represent and reason with qualitative specifications; statistical AI is concerned with learning quantitative specifications from data. To combine the strengths of these two camps, there has been exciting recent progress on unifying logic and probability. We review the many guises for this union, while emphasizing the need for a formal language to represent a system's knowledge. Formal languages allow their internal properties to be robustly scrutinized, can be augmented by adding new knowledge, and are amenable to abstractions, all of which are vital to the design of intelligent systems that are explainable and interpretable.

When it comes to robotic agents operating in an uncertain world, a major concern in knowledge representation is to better relate high-level logical accounts of belief and action to the low-level probabilistic sensorimotor data. Perhaps the most general formalism for dealing with degrees of belief and, in particular, how such beliefs should evolve in the presence of noisy sensing and acting is the account by Bacchus, Halpern, and Levesque. In this paper, we reconsider that model of belief, and propose a new logical variant that has much of the expressive power of the original, but goes beyond it in novel ways. In particular, by moving to a semantical account of a modal variant of the situation calculus based on possible worlds with unbounded domains and probabilistic distributions over them, we are able to capture the beliefs of a fully introspective knowledge base with uncertainty by way of an only-believing operator. The paper introduces the new logic and discusses key properties as well as examples that demonstrate how the beliefs of a knowledge base change as a result of noisy actions.

The ability to solve probability word problems such as those found in introductory discrete mathematics textbooks, is an important cognitive and intellectual skill. In this paper, we develop a two-step end-to-end fully automated approach for solving such questions that is able to automatically provide answers to exercises about probability formulated in natural language.In the first step, a question formulated in natural language is analysed and transformed into a high-level model specified in a declarative language. In the second step, a solution to the high-level model is computed using a probabilistic programming system. On a dataset of 2160 probability problems, our solver is able to correctly answer 97.5% of the questions given a correct model. On the end-to-end evaluation, we are able to answer 12.5% of the questions (or 31.1% if we exclude examples not supported by design).

Counting the models of a propositional formula is an important problem: for example, it serves as the backbone of probabilistic inference by weighted model counting. A key algorithmic insight is component caching (CC), in which disjoint components of a formula, generated dynamically during a DPLL search, are cached so that they only have to be solved once. In the recent years, driven by SMT technology and probabilistic inference in hybrid domains, there is an increasing interest in counting the models of linear arithmetic sentences. To date, however, solvers for these are block-clause implementations, which are nonviable on large problem instances. In this paper, as a first step in extending CC to hybrid domains, we show how propositional CC systems can be leveraged when limited to piecewise polynomial densities. Our experiments demonstrate a large gap in performance when compared to existing approaches based on a variety of block-clause strategies.

Only knowing captures the intuitive notion that the beliefs of an agent are precisely those that follow from its knowledge base. It has previously been shown to be useful in characterizing knowledge-based reasoners, especially in a quantified setting. While this allows us to reason about incomplete knowledge in the sense of not knowing whether a formula is true or not, there are many applications where one would like to reason about the degree of belief in a formula. In this work, we propose a new general first-order account of probability and only knowing that admits knowledge bases with incomplete and probabilistic specifications. Beliefs and non-beliefs are then shown to emerge as a direct logical consequence of the sentences of the knowledge base at a corresponding level of specificity.

Many AI applications involve the interaction of multiple autonomous agents, requiring those agents to reason about their own beliefs, as well as those of other agents. However, planning involving nested beliefs is known to be computationally challenging. In this work, we address the task of synthesizing plans that necessitate reasoning about the beliefs of other agents. We plan from the perspective of a single agent with the potential for goals and actions that involve nested beliefs, non-homogeneous agents, co-present observations, and the ability for one agent to reason as if it were another. We formally characterize our notion of planning with nested belief, and subsequently demonstrate how to automatically convert such problems into problems that appeal to classical planning technology. Our approach represents an important first step towards applying the well-established field of automated planning to the challenging task of planning involving nested beliefs of multiple agents.

The area of cognitive robotics is often subject to the criticism that the proposals investigated in the literature are too far removed from the kind of continuous uncertainty and noise seen in actual real-world robotics. This paper proposes a new language and an implemented system, called PREGO, based on the situation calculus, that is able to reason effectively about degrees of belief against noisy sensors and effectors in continuous domains. It embodies the representational richness of conventional logic-based action languages, such as context-sensitive successor state axioms, but is still shown to be efficient using a number of empirical evaluations. We believe that PREGO is a powerful framework for exploring real-time reactivity and an interesting bridge between logic and probability for cognitive robotics applications.

Planning with sensing actions under partial observability is a computationally challenging problem that is fundamental to the realization of AI tasks in areas as diverse as robotics, game playing, and diagnostic problem solving. Recent work on generating plans for partially observable domains has advocated for online planning, claiming that offline plans are often too large to generate. Here we push the envelope on this challenging problem, proposing a technique for generating conditional (aka contingent) plans offline. The key to our planner's success is the reliance on state-of-the-art techniques for fully observable non-deterministic (FOND) planning. In particular, we use an existing compilation for converting a planning problem under partial observability and sensing to a FOND planning problem. With a modified FOND planner in hand, we are able to scale beyond previous techniques for generating conditional plans with solutions that are orders of magnitude smaller than previously possible in some domains.

The idea of "only knowing" a collection of sentences, as proposed by Levesque, has been previously shown to be very useful in characterizing knowledge-based agents: in terms of a specification, a precise and perspicuous account of the beliefs and non-beliefs is obtained in a monotonic setting. Levesque's logic is based on a first-order modal language with quantifying-in, thus allowing for de re versus de dicto distinctions, among other things. However, the logic and its recent dynamic extension only deal with the case of a single agent. In this work, we propose a first-order multiagent framework with knowledge, actions, sensing and only knowing, that is shown to inherit all the features of the single agent version. Most significantly, we prove reduction theorems by means of which reasoning about knowledge and actions in the framework simplifies to non-epistemic, non-dynamic reasoning about the initial situation.

Building on a general theory of action by Reiter and his colleagues, Bacchus et al. give an account for formalizing degrees of belief and noisy actions in the situation calculus. Unfortunately, there is no clear solution to the projection problem for the formalism. And, while the model has epistemic features, it is not obvious what the agent's knowledge base should look like. Also, reasoning about uncertainty essentially resorts to second-order logic. In recent work, Gabaldon and Lakemeyer remedy these shortcomings somewhat, but here too the utility seems to be restricted to queries (with action operators) about the initial theory. In this paper, we propose a fresh amalgamation of a modal fragment of the situation calculus and uncertainty, where the idea will be to update the initial knowledge base, containing both ordinary and (certain kinds of) probabilistic beliefs, when noisy actions are performed. We show that the new semantics has the right properties, and study a special case where updating probabilistic beliefs is computable. Our ideas are closely related to the Lin and Reiter notion of progression.

In a seminal paper, Lin and Reiter introduced the notion of progression of basic action theories. Unfortunately, progression is second-order in general. Recently, Liu and Lakemeyer improve on earlier results and show that for the local-effect and normal actions case, progression is computable but may lead to an exponential blow-up. Nevertheless, they show that for certain kinds of expres-sive first-order knowledge bases with disjunctive infor-mation, called proper+, it is efficient. However, answer-ing queries about the resulting state is still undecidable. In this paper, we continue this line of research and extend proper+ KBs to include functions. We prove that their progression wrt local-effect, normal actions, and range-restricted theories, is first-order definable and efficiently computable. We then provide a new logically sound and complete decision procedure for certain kinds of queries.

Approaches to reasoning about knowledge in imperfect information games typically involve an exhaustive description of the game, the dynamics characterized by a tree and the incompleteness in knowledge by information sets. Such specifications depend on a modeler's intuition, are tedious to draft and vague on where the knowledge comes from. Also, formalisms proposed so far are essentially propositional, which, at the very least, makes them cumbersome to use in realistic scenarios. In this paper, we propose to model imperfect information games in a new multi-agent epistemic variant of the situation calculus. By using the concept of only-knowing, the beliefs and non-beliefs of players after any sequence of actions, sensing or otherwise, can be characterized as entailments in this logic. We show how de re vs. de dicto belief distinctions come about in the framework. We also obtain a regression theorem for multi-agent beliefs, which reduces reasoning about beliefs after actions to reasoning about beliefs in the initial situation.

We present a system for detecting and recognizing faces in images in real-time which is able to learn new identities in instants. In mobile service robotics, interaction with persons is becoming increasingly important, real-time performance is required and the introduction of new persons is a necessary feature for many applications. Although face detection and face recognition are well studied, only a few papers address both problems jointly and only few systems are able to learn to identify new persons quickly. To achieve real-time performance on modest computing hardware, we use random forests for both detection and recognition, and compare with well-known techniques such as boosted face detection and support vector machines for identification. Results are presented on different datasets and compare favorably well to competitive methods.