PaperlayerView exact revision on arXiv

Source-linked AI summary

Probabilistic Theorem Proving

Vibhav Gogate, Pedro Domingos

arXiv:1202.3724v1cs.AI

TL;DR

The paper addresses the limited ability of existing lifted probabilistic inference methods to use first-order logical structure. It defines probabilistic theorem proving, reduces it to lifted weighted model counting, and reports theoretical and empirical advantages over prior lifted methods. An approximate version also outperforms lifted belief propagation in the reported experiments.

  • Problem

    Existing lifted probabilistic inference methods largely ignore logical structure, limiting their ability to combine first-order theorem proving with probabilistic inference.

  • Method

    The paper defines probabilistic theorem proving as computing query probabilities from probabilistic formulas and reduces it to lifted weighted model counting.

  • Results

    The proposed algorithms greatly outperform lifted variable elimination and belief propagation when logical structure is present, with correctness established for the weighted model-counting algorithm.

  • Takeaways & Limitations

    Probabilistic theorem proving provides a framework that includes logical theorem proving and graphical-model inference as special cases and extends lifted inference to logical structure.

  • Takeaways & Limitations

    The lifting schemes used for decomposition and splitting do not exhaust the space of possible probabilistic lifting rules.

Abstract

from arXiv · show

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.

1 INTRODUCTION

The paper targets the gap between probabilistic inference and first-order theorem proving, whose existing lifted methods ignore logical structure. It reduces probabilistic theorem proving to lifted weighted model counting and reports strong efficiency advantages.

  • Unifying first-order logic and probability supports uncertain reasoning over domains with complex relational structure, but inference remains less developed than representation.
  • Existing lifted variable elimination and belief propagation methods gain efficiency over propositionalization but treat potentials as black boxes and fall short of theorem proving.
  • The paper reduces probabilistic theorem proving to lifted weighted model counting and develops an algorithm for the resulting problem.
  • The proposed algorithm can be exponentially more efficient than first-order variable elimination and is never less efficient up to constants.
  • Experiments report that probabilistic theorem proving greatly outperforms first-order variable elimination and belief propagation, including through an approximate sampling-based algorithm.

2 LOGIC AND THEOREM PROVING

The paper reviews propositional and first-order theorem proving, emphasizing how first-order structure enables concise representations and lifted reasoning. Its setting assumes finite domains with Herbrand interpretations.

  • Theorem proving determines whether a knowledge base entails a query by testing whether the knowledge base augmented with the query's negation is unsatisfiable.
  • Davis-Putnam uses resolution, while DPLL replaces elimination with splitting and has linear space complexity.
  • First-order logic extends propositional atoms with predicates, arguments, and universal or existential quantification.
  • Finite first-order domains permit propositionalization, but first-order resolution instead resolves complementary literals that unify and removes existential quantifiers by skolemization.
  • First-order logic expresses knowledge far more concisely than propositional logic, motivating the paper's extension of theorem proving to uncertain domains.

3 PROBLEM DEFINITION

Probabilistic theorem proving computes query probabilities from probabilistic knowledge bases, and the paper reduces this task to weighted model counting. The framework contains logical theorem proving and graphical-model inference as special cases.

  • Probabilistic theorem proving determines the probability of a query formula given logical formulas and their probabilities.
  • A probabilistic knowledge base combines formulas, probabilities, and a maximum entropy assumption, equivalently forming a log-linear model with formula features.
  • Potential values represent formula truth conditions, with hard formulas assigned φ_i = 0 and soft formulas assigned φ_i > 0.
  • The task takes a probabilistic knowledge base and query formula as input and returns P(Q|K).
  • PTP reduces query probability computation to weighted model counting by comparing the partition functions with and without the query added as a hard formula.
  • Weighted model counting sums the weights of worlds satisfying a CNF, with world weights formed from products of true-literal weights.
  • The resulting lifted algorithm applies across the inference problems depicted in Figure 1, while weighted SAT and MPE require replacing sums with maxima and adding traceback.

4 PROPOSITIONAL CASE

The propositional case generalizes weighted model counting to probabilistic knowledge bases, evidence, and query formulas. Its recursive algorithm exploits decomposition and splitting to compute weighted counts correctly.

  • The propositional method generalizes Bayesian-network inference techniques to arbitrary propositional probabilistic knowledge bases, evidence, and query formulas.
  • Query probabilities are obtained from partition functions of the knowledge base with and without the query enforced as a hard formula.
  • Soft formulas are replaced by hard equivalences to new atoms, assigning the false-indicator literal weight φ_i.
  • Theorem 1 establishes that the partition function equals the weighted model count: Z(K) = WMC(WCNF(K)).
  • Weighted model counting returns zero for an unsatisfied clause, multiplies counts for atom-disjoint CNFs, and sums weighted branches produced by splitting.
  • Theorem 2 states that the recursive WMC algorithm correctly computes the weighted model count of a CNF under literal weights.

5 FIRST-ORDER CASE

The first-order extension lifts probabilistic theorem proving by representing substitution constraints and exploiting decompositions and splits over first-order CNFs. The resulting LWMC algorithm is correct, can outperform FOVE exponentially, and also yields lifted theorem-proving procedures.

  • First-order LWMC: A (C, S) pair represents the ground CNF formed by grounding clauses consistently with substitution constraints S.The constraints can enforce equalities or inequalities among variables and constants, while unifiability is evaluated under those constraints.
  • First-order LWMC: LWMC extends weighted model counting to first-order CNFs by carrying substitution constraints through recursive inference.It operates on first-order CNFs, literal weights, and an initially empty constraint set that is extended along each branch.
  • Lifted decomposition: Lifted decomposition groups independent, identical first-order CNFs, allowing their weighted model counts to be computed recursively and combined by powers.The decomposition requires conjunction equivalence, no shared unifiable literals, and identity among repeated components up to renaming.
  • Lifted decomposition: A decomposer partitions a CNF by substituting a shared variable set with different constants, producing components that do not share unifiable literals.When unconstrained substitutions yield identical components, the repeated component count equals the number of domain constants.
  • Limitations and extensions: The algorithm's lifting rules are not exhaustive, leaving discovery of additional probabilistic lifting rules as an open research direction.The paper notes that other lifting rules exist and that both positive and negative results about liftability remain to be explored.
  • Properties and consequences: LWMC correctly computes weighted model counts, while PTP can be exponentially more efficient than FOVE and has the same worst-case complexity as FOVE with full caching.A constructive example shows PTP solving a CNF in polynomial domain-size time where FOVE requires exponential time; the framework also yields a lifted DPLL procedure.

6 APPROXIMATE INFERENCE

The paper develops Monte Carlo approximations for weighted model counting and lifts them to probabilistic theorem proving, preserving unbiasedness while exploiting logical decomposition.

  • Monte Carlo weighted model counting: MC-WMC samples truth assignments using a proposal distribution Q and produces an unbiased estimate of WMC under a support condition.The estimate is averaged over multiple runs to improve accuracy, with variance reduced by more samples or proposals close to the posterior.
  • Monte Carlo weighted model counting: The proposal distribution selects each ground atom using the numbers of clauses satisfied by true and false assignments, weighted by the atom’s literal weights.The ordering of ground atoms is selected randomly, and each conditional probability uses n_i,t and n_i,f together with the positive and negative weights.
  • Limitations: MC-WMC can suffer from rejection when a sample returns zero; backtracking or a backtrack-free distribution can address this problem.This is identified as a specific limitation of the basic importance-sampling procedure.
  • Lifted sampling: MC-LWMC extends MC-WMC by replacing lifted splitting with sampling over lifted splits while recursively conditioning on the sampled choice.The sampled lifted element is weighted with respect to Q before recursive evaluation.
  • Lifted sampling: MC-LWMC yields an unbiased estimate of WMC and has smaller variance than MC-WMC because decomposition samples one representative from each group of identical independent CNFs.For a lifted decomposition of size m_i > 1, this gives a factor of m_i speedup and allows more samples within a fixed time bound.

7 EXPERIMENTS

Experiments compare exact PTP with FOVE and approximate MC-LWMC with alternative inference methods across synthetic, link-prediction, entity-resolution, and collective-classification settings.

  • Exact inference: PTP’s advantage over FOVE increases with clause length: FOVE runs out of memory on large-clause instances, while unit propagation enables substantial pruning in PTP.With small clauses, PTP is only slightly better; with large clauses, it is substantially better.
  • Exact inference: FOVE runs out of memory above 40% evidence in the 100-object link-prediction setting, whereas PTP solves all problems and is much faster.The comparison is shown in Figure 2(a) on a logarithmic time scale.
  • Exact inference: Beyond 100 objects, FOVE cannot solve the link-prediction problems because of memory exhaustion, while PTP solves all problems in less than 100s.Figure 2(b) uses 20% observed atoms while varying the number of objects.
  • Approximate inference: Approximate inference evaluates test-set atom probabilities from evidence using negative log-likelihood across entity-resolution and collective-classification datasets.The results average performance over 10 runs and plot negative log-likelihood against time.
  • Approximate inference: MC-LWMC achieves the lowest negative log-likelihood by a large margin, significantly surpassing MC-WMC after about two minutes and outperforming lifted BP and MC-SAT.These comparisons are reported for both evaluation domains in Figure 3.

8 CONCLUSION

The paper presents PTP as a combination of theorem proving and probabilistic inference, implemented through lifted weighted model counting and supported by theoretical and empirical advantages.

  • Conclusion: PTP combines theorem proving and probabilistic inference through a reduction to lifted weighted model counting.The paper reports both theoretical and empirical advantages over previous lifted probabilistic inference algorithms.
  • Future research: Future work includes extending PTP beyond finite Herbrand domains and developing new lifting rules, heuristics, proposal distributions, and approximate methods.The proposed directions also include handling existentials, answering multiple queries simultaneously, and applications.
Loading 1202.3724v1…