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.
Algorithm 1 TP(KB K, query Q)
KQ ← K ∪ {¬Q}
return ¬SAT(CNF(KQ ) )
The original version of this paper was published in the
Proceedings of the 27th Conference on Uncertainty in Artificial
Intelligence, 2011, AUAI Press, 256–265.