Probabilistic Theorem Proving

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.

References in corpus (4)

• Counting Belief Propagation
• Bisimulation-based Approximate Lifted Inference
• Constraint Processing in Lifted Probabilistic Inference
• Formula-Based Probabilistic Inference

Cited by in corpus (28)

• Skolemization for Weighted First-Order Model Counting
• Lifted Variable Elimination: Decoupling the Operators from the Constraint Language
• Automorphism Groups of Graphical Models and Lifted Variational Inference
• Quantum Enhanced Inference in Markov Logic Networks
• Markov Chains on Orbits of Permutation Groups
• Automorphism Groups of Graphical Models and Lifted Variational Inference
• Relational Approach to Knowledge Engineering for POMDP-based Assistance Systems as a Translation of a Psychological Model
• Tractability through Exchangeability: A New Perspective on Efficient Probabilistic Inference
• Closing the Gap Between Short and Long XORs for Model Counting
• Exploiting Uniform Assignments in First-Order MPE
• Understanding the Complexity of Lifted Inference and Asymmetric Weighted Model Counting
• First-Order Decomposition Trees
• Markov Logic Networks for Natural Language Question Answering
• Representing Meaning with a Combination of Logical and Distributional Models
• Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model
• Structured Message Passing
• Generating and Sampling Orbits for Lifted Probabilistic Inference
• Complex Markov Logic Networks: Expressivity and Liftability
• Why is Compiling Lifted Inference into a Low-Level Language so Effective?
• Lifted Inference in 2-Variable Markov Logic Networks with Function and Cardinality Constraints Using Discrete Fourier Transform
• Probabilistic Databases with MarkoViews
• Lifted Variable Elimination: A Novel Operator and Completeness Results
• Domain-Liftability of Relational Marginal Polytopes
• Approximate Lifted Inference with Probabilistic Databases
• Symmetric Weighted First-Order Model Counting
• Lifted Region-Based Belief Propagation
• Fusing First-order Knowledge Compilation and the Lifted Junction Tree Algorithm
• A Critical Look at the Applicability of Markov Logic Networks for Music Signal Analysis