Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

DeepProofLog: Efficient Proving in Deep Stochastic Logic Programs

Ying Jiao, Rodrigo Castellano Ontiveros, Luc De Raedt, Marco Gori, Francesco Giannini, Michelangelo Diligenti, Giuseppe Marra

TL;DR

DeepProofLog introduces a scalable neurosymbolic reasoning framework by parameterizing the resolution process in stochastic logic programs with neural networks, operating under goal-conditioned guidance. By establishing a formal mapping between deep SLPs and Markov Decision Processes, it enables both exact dynamic programming and reinforcement learning to efficiently infer proofs over large knowledge bases. The approach demonstrates strong performance on MNIST addition and knowledge graph completion while preserving interpretability through explicit proof trees. This work advances NeSy scalability and explainability, offering a flexible framework that leverages both DP and RL techniques for complex reasoning tasks.

Abstract

Neurosymbolic (NeSy) AI aims to combine the strengths of neural architectures and symbolic reasoning to improve the accuracy, interpretability, and generalization capability of AI models. While logic inference on top of subsymbolic modules has been shown to effectively guarantee these properties, this often comes at the cost of reduced scalability, which can severely limit the usability of NeSy models. This paper introduces DeepProofLog (DPrL), a novel NeSy system based on stochastic logic programs, which addresses the scalability limitations of previous methods. DPrL parameterizes all derivation steps with neural networks, allowing efficient neural guidance over the proving system. Additionally, we establish a formal mapping between the resolution process of our deep stochastic logic programs and Markov Decision Processes, enabling the application of dynamic programming and reinforcement learning techniques for efficient inference and learning. This theoretical connection improves scalability for complex proof spaces and large knowledge bases. Our experiments on standard NeSy benchmarks and knowledge graph reasoning tasks demonstrate that DPrL outperforms existing state-of-the-art NeSy systems, advancing scalability to larger and more complex settings than previously possible.

DeepProofLog: Efficient Proving in Deep Stochastic Logic Programs

TL;DR

DeepProofLog introduces a scalable neurosymbolic reasoning framework by parameterizing the resolution process in stochastic logic programs with neural networks, operating under goal-conditioned guidance. By establishing a formal mapping between deep SLPs and Markov Decision Processes, it enables both exact dynamic programming and reinforcement learning to efficiently infer proofs over large knowledge bases. The approach demonstrates strong performance on MNIST addition and knowledge graph completion while preserving interpretability through explicit proof trees. This work advances NeSy scalability and explainability, offering a flexible framework that leverages both DP and RL techniques for complex reasoning tasks.

Abstract

Neurosymbolic (NeSy) AI aims to combine the strengths of neural architectures and symbolic reasoning to improve the accuracy, interpretability, and generalization capability of AI models. While logic inference on top of subsymbolic modules has been shown to effectively guarantee these properties, this often comes at the cost of reduced scalability, which can severely limit the usability of NeSy models. This paper introduces DeepProofLog (DPrL), a novel NeSy system based on stochastic logic programs, which addresses the scalability limitations of previous methods. DPrL parameterizes all derivation steps with neural networks, allowing efficient neural guidance over the proving system. Additionally, we establish a formal mapping between the resolution process of our deep stochastic logic programs and Markov Decision Processes, enabling the application of dynamic programming and reinforcement learning techniques for efficient inference and learning. This theoretical connection improves scalability for complex proof spaces and large knowledge bases. Our experiments on standard NeSy benchmarks and knowledge graph reasoning tasks demonstrate that DPrL outperforms existing state-of-the-art NeSy systems, advancing scalability to larger and more complex settings than previously possible.

Paper Structure

This paper contains 43 sections, 2 theorems, 22 equations, 1 figure, 4 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Logic Programming
  4. Stochastic SLD Resolution
  5. Markov Decision Processes
  6. DeepProofLog
  7. Goal Representation.
  8. Learning.
  9. Expressiveness.
  10. Markov Decision Processes for DeepProofLog
  11. SLD-resolution as MDP.
  12. Example.
  13. Learning in DeepProofLog
  14. Experiments
  15. MNIST Addition
  16. ...and 28 more sections

Key Result

Proposition 1

Any probability distribution over SLD Derivations can be approximated with arbitrary precision by DeepProofLog.

Figures (1)

  • Figure 1: (a) DeepProofLog uses goal-level parameterization: a neural policy conditioned on the goal to guide proving at each resolution step. In comparison, (b) SLPs assign scalar weights to clauses for probabilistic proof search without input adaptation, and (c) DeepStochLog uses neural nets conditioned on subsymbolic terms in the query, requiring a fixed output domain.

Theorems & Definitions (8)

  • Definition 1: Probability Distribution over SLD Derivations
  • Definition 2: Success Probability of a Query
  • Proposition 1: Universal Approximation
  • Proposition 2
  • Definition 3: Derivation Tree
  • Definition 4: Target and network distributions
  • proof
  • proof