Probabilistic Theorem Proving

摘要

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. Exist ing methods are mainly variants of lifted vari able 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 the-orem proving, their generalization, as the prob lem of computing the probability of a logical for mula given the probabilities or weights of a set of formulas. We then show how this can be reduced to the problem of lifted weighted model count ing, and develop an efficient algorithm for the lat ter. We prove the correctness of this algorithm, investigate its properties, and show how it gen eralizes previous approaches. Experiments show that it greatly outperforms lifted variable elimina tion when logical structure is present. Finally, we propose an algorithm for approximate probabilis tic theorem proving, and show that it can greatly outperform lifted belief propagation.