Communications of the ACM

Probabilistic Theorem Proving

By Vibhav Gogate and Pedro Domingos

DOI: 10.1145/2936726

Abstract

Many representation schemes combining first-order logic and probability have been proposed in recent years. Progress in unifying logical and probabilistic inference has been slower. Existing methods are mainly variants of lifted variable elimination and belief propagation, neither of which take logical structure into account. We propose the first method that has the full power of both graphical model inference and first-order theorem proving (in finite domains with Herbrand interpretations). We first define probabilistic theorem proving (PTP), their generalization, as the problem of computing the probability of a logical formula given the probabilities or weights of a set of formulas. We then show how PTP can be reduced to the problem of lifted weighted model counting, and develop an efficient algorithm for the latter. We prove the correctness of this algorithm, investigate its properties, and show how it generalizes previous approaches. Experiments show that it greatly outperforms lifted variable elimination when logical structure is present. Finally, we propose an algorithm for approximate PTP, and show that it is superior to lifted belief propagation.

1. INTRODUCTION

Unifying first-order logic and probability enables uncertain reasoning over domains with complex relational structure, and is a long-standing goal of AI. Proposals go back to at least Nilsson, 17 with substantial progress within the community that studies uncertainty in AI starting in the 1990s (e.g., Bacchus, 1 Halpern, 14 Wellman25), and added impetus from the new field of statistical relational learning starting in the 2000s. 11 Many well-developed representations now exist (e.g., DeRaedt, 7 and Domingos10), but the state of inference is less advanced. For the most part, inference is still carried out by converting models to propositional form (e.g., Bayesian networks) and then applying standard propositional algorithms. This typically incurs an exponential blowup in the time and space cost of inference, and forgoes one of the chief attractions of first-order logic: the ability to perform lifted inference, that is, reason over large domains in time independent of the number of objects they contain, using techniques like resolution theorem proving. 20

In recent years, progress in lifted probabilistic inference has picked up. An algorithm for lifted variable elimination was proposed by Poole18 and extended by de Salvo Braz8 and others. Lifted belief propagation was introduced by Singla and Domingos. 24 These algorithms often yield impressive efficiency gains compared to propositionalization, but still fall well short of the capabilities of first-order theorem proving, because they ignore logical structure, treating potentials as black boxes. This paper proposes the first full-blown probabilistic theorem prover that is capable of exploiting both lifting and logical structure, and includes standard theorem proving and graphical model inference as special cases.

Our solution is obtained by reducing probabilistic theorem proving (PTP) to lifted weighted model counting. We first do the corresponding reduction for the propositional case, extending previous work by Sang et al. 22 and Chavira and Darwiche. 3 We then lift this approach to the first-order level, and refine it in several ways. We show that our algorithm can be exponentially more efficient than first-order variable elimination, and is never less efficient (up to constants). For domains where exact inference is not feasible, we propose a sampling-based approximate version of our algorithm. Finally, we report experiments in which PTP greatly outperforms first-order variable elimination and belief propagation, and discuss future research directions.

2. LOGIC AND THEOREM PROVING

We begin with a brief review of propositional logic, first-order logic and theorem proving.

The simplest formulas in propositional logic are atoms: individual symbols representing propositions that may be true or false in a given world. More complex formulas are recursively built up from atoms and the logical connectives ¬(negation), ∧;(conjunction), ∨ (disjunction), ⇒ (implication) and ⇔ (equivalence). For example, ¬A ∨ (B ∧ C) is true iff A is false or B and C are true. A knowledge base (KB) is a set of logical formulas. The fundamental problem in logic is determining entailment, and algorithms that do this are called theorem provers. A knowledge base K entails a query formula Q iff Q is true in all worlds in which all formulas in K are true, a world being an assignment of truth values to all atoms.

A world is a model of a KB iff the KB is true in it. Theorem provers typically first convert K and Q to conjunctive normal form (CNF). A CNF formula is a conjunction of clauses, each of which is a disjunction of literals, each of which is an atom or its negation. For example, the CNF of ¬A ∨ (B ∧ C) is (¬A ∨ B) ∧ (¬A ∨ C). A unit clause consists of a single literal. Entailment can then be computed by adding ¬Q to K and determining whether the resulting KB KQ is satisfiable, that is, whether there exists a world where all clauses in KQ are true. If not, KQ is unsatisfiable, and K entails Q. Algorithm 1 shows this basic theorem proving schema. CNF(K) converts K to CNF, and SAT(C) returns True if C is satisfiable and False otherwise.