Probabilistic Theorem Proving

Vibhav Gogate, Pedro Domingos
Proceedings of the 27th Conference on Uncertainty in Artificial Intelligence, PMLR R9:294-303, 2011.

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, 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 this 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 probabilistic theorem proving, and show that it can greatly outperform lifted belief propagation.

Cite this Paper

BibTeX
@InProceedings{pmlr-vR9-gogate11b, title = {Probabilistic Theorem Proving}, author = {Gogate, Vibhav and Domingos, Pedro}, booktitle = {Proceedings of the 27th Conference on Uncertainty in Artificial Intelligence}, pages = {294--303}, year = {2011}, editor = {Cozman, Fabio and Pfeffer, Avi}, volume = {R9}, series = {Proceedings of Machine Learning Research}, month = {14--17 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/r9/main/assets/gogate11b/gogate11b.pdf}, url = {https://proceedings.mlr.press/r9/gogate11b.html}, 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, 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 this 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 probabilistic theorem proving, and show that it can greatly outperform lifted belief propagation.}, note = {Reissued by PMLR on 04 October 2026.} }
Endnote
%0 Conference Paper %T Probabilistic Theorem Proving %A Vibhav Gogate %A Pedro Domingos %B Proceedings of the 27th Conference on Uncertainty in Artificial Intelligence %C Proceedings of Machine Learning Research %D 2011 %E Fabio Cozman %E Avi Pfeffer %F pmlr-vR9-gogate11b %I PMLR %P 294--303 %U https://proceedings.mlr.press/r9/gogate11b.html %V R9 %X 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, 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 this 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 probabilistic theorem proving, and show that it can greatly outperform lifted belief propagation. %Z Reissued by PMLR on 04 October 2026.
APA
Gogate, V. & Domingos, P.. (2011). Probabilistic Theorem Proving. Proceedings of the 27th Conference on Uncertainty in Artificial Intelligence, in Proceedings of Machine Learning Research R9:294-303 Available from https://proceedings.mlr.press/r9/gogate11b.html. Reissued by PMLR on 04 October 2026.

Related Material