Source-linked AI summary
End-to-End Differentiable Proving
Tim Rocktäschel, Sebastian Riedel
TL;DR
Knowledge-base completion needs both learned symbol similarities and multi-hop reasoning, but existing neural and symbolic approaches provide only part of this combination. The paper introduces differentiable Neural Theorem Provers inspired by Prolog, and reports stronger benchmark performance than ComplEx on three of four knowledge bases while inducing interpretable rules.
Problem
Existing neural link prediction models struggle with multi-hop reasoning, while symbolic provers lack learned subsymbolic representations for similar but nonidentical symbols.
Method
Neural Theorem Provers recursively mirror Prolog backward chaining and replace symbolic unification with differentiable RBF-kernel comparison of vector representations.
Results
NTPs outperform ComplEx on three out of four benchmark knowledge bases and induce interpretable rules, including transitivity rules on UMLS.
Takeaways & Limitations
The architecture combines learned subsymbolic representations with multi-hop logical reasoning and human-readable induced rules.
Takeaways & Limitations
Scaling NTPs to larger knowledge bases remains an open problem, and vanilla NTPs have severe computational limitations from representing possible proofs to a predefined depth.
Abstract
from arXiv · showhide
We introduce neural networks for end-to-end differentiable proving of queries to knowledge bases by operating on dense vector representations of symbols. These neural networks are constructed recursively by taking inspiration from the backward chaining algorithm as used in Prolog. Specifically, we replace symbolic unification with a differentiable computation on vector representations of symbols using a radial basis function kernel, thereby combining symbolic reasoning with learning subsymbolic vector representations. By using gradient descent, the resulting neural network can be trained to infer facts from a given incomplete knowledge base. It learns to (i) place representations of similar symbols in close proximity in a vector space, (ii) make use of such similarities to prove queries, (iii) induce logical rules, and (iv) use provided and induced logical rules for multi-hop reasoning. We demonstrate that this architecture outperforms ComplEx, a state-of-the-art neural link prediction model, on three out of four benchmark knowledge bases while at the same time inducing interpretable function-free first-order logic rules.
1 Introduction
The paper develops Neural Theorem Provers that combine Prolog-inspired multi-hop reasoning with learned subsymbolic representations. This design supports differentiable unification, rule induction, and benchmark knowledge-base completion.
- Differentiable unification: Differentiable unification replaces exact symbolic comparison with a vector-space similarity computation, allowing similar rather than identical symbols to participate in proofs.This addresses the local-scoring limitation of neural link prediction models while retaining learned representations.
- Motivation: The approach combines symbolic multi-hop reasoning and interpretable rules with vector-based similarities between predicates and constants.Variable binding remains symbolic, while non-variable symbols are compared through their subsymbolic representations.
- Approach: Neural Theorem Provers recursively construct differentiable proving networks from Prolog’s backward chaining algorithm.They learn symbol representations and parameters of function-free first-order rules through differentiable proof success.
- Learning and reasoning: NTPs learn representations of symbols and function-free first-order rules of predefined structure, enabling multi-hop reasoning on benchmark knowledge bases.The architecture also supports joint training with a neural link prediction model, batch proving, and approximate gradient calculation.
- Empirical contribution: NTPs outperform ComplEx on three out of four benchmark knowledge bases while inducing interpretable symbolic rules.The induced rules are intended to expose what the model has learned.
2 Background
The paper represents knowledge bases with atoms, terms, facts, rules, and substitutions. Prolog backward chaining proves a query by recursively matching rule heads and proving their body subgoals.
- Knowledge-base syntax: An atom contains a predicate symbol and a list of terms, with terms restricted to constants or variables in function-free first-order logic.For example, [grandfatherOf, Q, BART] contains one predicate, one variable, and one constant.
- Knowledge-base syntax: Rules have the form H :– B, where the head is an atom and the body is a possibly empty conjunction of atoms.A ground rule has no free variables, and a ground rule with an empty body is a fact.
- Backward chaining: Backward chaining uses OR to try rule heads and AND to prove every resulting body subgoal, updating substitutions during unification.For grandfatherOf, the example decomposes the goal into fatherOf and parentOf subgoals.
3 Differentiable Prover
NTPs recursively construct differentiable proving networks from proof states, replacing symbolic unification with vector-based comparison while retaining backward-chaining structure. The prover supports similarity-aware rule application, multi-step proof construction, and gradient-based rule induction.
- Neural proof-state construction: Each module maps discrete atoms, rules, and an upstream proof state to a list of new proof states.The proof state carries substitutions and a neural network computing partial-proof success.
- Unification: Differentiable unification compares corresponding terms using vector representations, updating substitutions while constructing proof-success computations.Non-variable symbols are compared through learned embeddings rather than exact equality; mismatched arity yields failure.
- Recursive proving: The OR module recursively applies knowledge-base rules to goals, instantiating AND submodules for rule bodies up to a predefined proof depth.Substitutions from rule-head unification are passed into the body subgoals.
- Unification: The unification module can match semantically similar predicates, allowing a grandfatherOf rule to answer a grandpaOf query when their representations are close under the RBF kernel.This extends symbolic rule application beyond exact symbol matching.
- Neural inductive logic programming: NTPs can induce function-free first-order rules by optimizing parameterized predicate representations with gradient descent rather than combinatorial rule search.Decoded predicates and RBF-based similarities provide interpretable induced rules and confidence scores.
4 Optimization
NTP training uses proof-success objectives and auxiliary optimization strategies to learn representations efficiently while addressing the computational cost of differentiable proving.
- 4.1 Training Objective: NTP training minimizes the negative log-likelihood of proof success scores for known and corrupted ground atoms.Corrupted atoms are sampled from constants and resampled each training iteration.
- 4.1 Training Objective: Known ground atoms are masked during training so the prover must infer them from other facts and rules rather than trivial self-unification.The unification score for the target fact is temporarily set to 0.
- 4.2 Neural Link Prediction as Auxiliary Loss: Random initialization and maximum-path gradient updates can make learning similar symbol representations and effective rule use slow.Early unification scores are noisy because all symbol representations initially lack structure.
- 4.2 Neural Link Prediction as Auxiliary Loss: Joint training with ComplEx accelerates representation learning by sharing subsymbolic representations while reserving multi-hop prediction for the NTP at test time.ComplEx scores ground atoms locally and acts as an auxiliary loss during training.
- 4.3 Computational Optimizations: Batch proving and truncated gradient computation reduce the number of proofs considered during optimization.These optimizations exploit GPUs and sparse gradients from min and max operations.
5 Experiments
Experiments evaluate ComplEx, NTP, and NTPλ across four benchmark knowledge bases using task-specific ranking or precision-recall metrics.
- Evaluation Setup: Experiments compare ComplEx, NTP, and NTPλ using AUC-PR on Countries and MRR and HITS@m on the other benchmark knowledge bases.The benchmark set comprises Countries, Kinship, Nations, and UMLS.
- Countries: The Countries KB contains 244 countries, 5 regions, 23 subregions, and 1158 facts about neighborhoods and locations.Countries are split into 204 training, 20 development, and 20 test countries.
- Countries: Countries S1 removes test-country-to-region facts, requiring region prediction through subregion transitivity.The evaluated rule is locatedIn(X, Y) :– locatedIn(X, Z), locatedIn(Z, Y).
- Countries: Countries S2 additionally removes test-country-to-subregion facts, requiring inference from neighboring countries’ locations.This task is harder because neighboring countries may belong to different regions.
- Kinship, Nations & UMLS: Nations, Kinship, and UMLS provide benchmark knowledge bases with differing predicate, constant, and fact counts for evaluating generalization.Unary atoms are removed from Nations because ComplEx cannot handle unary predicates.
6 Results and Discussion
NTPλ with ComplEx auxiliary training performs best across most tasks, while NTPs additionally provide inspectable induced rules for multi-hop reasoning.
- Results: NTPλ with ComplEx as auxiliary loss outperforms the other models in the majority of tasks.Vanilla NTPs outperform ComplEx only on Countries S3 and Nations, not on Kinship or UMLS.
- Results: p < 0.0001: NTPλ’s AUC-PR difference from ComplEx is significant for all Countries tasks.The comparison covers all three Countries tasks.
- Interpretability: NTPs produce inspectable induced rules that provide an interpretable representation of what the model learned.For Countries, NTP recovered rules needed for the three tasks; on UMLS, it induced transitivity rules.
- Interpretability: Transitivity relationships are particularly hard for local neural link prediction models such as ComplEx to encode.ComplEx is optimized to predict fact scores locally, whereas NTP reasoning steps are represented through explicit rules.
7 Related Work
Related work spans neural-symbolic systems, vector-space reasoning models, and inductive logic programming, while NTPs combine subsymbolic representations with gradient-based rule induction.
- Neural-Symbolic Learning: Earlier neural-symbolic networks were limited to propositional rules, while other first-order approaches did not learn subsymbolic vector representations from KB training facts.The paper places NTPs within a long tradition of combining neural and symbolic relational learning.
- Vector-Space Reasoning: Recent question-answering models encode reasoning chains in vector spaces without explicit rule representations, limiting incorporation of domain-specific knowledge.NTPs instead use explicit reasoning steps and subsymbolic representations for unification.
- Inductive Logic Programming: Unlike discrete ILP systems that search symbolic rule spaces, NTPs induce function-free rules from data using subsymbolic representations and gradient descent.NTPs are related to systems including FOIL, Sherlock, and Metagol.
- Limitations: Scaling NTPs to larger knowledge bases remains an open problem because a related differentiable rule-learning method is more scalable.The paper reports stronger baseline generalization on UMLS and Kinship but identifies scalability as future work.
8 Conclusion and Future Work
The paper presents an end-to-end differentiable prover that learns subsymbolic representations and function-free first-order logic rules from knowledge-base facts. It outperforms ComplEx on three of four benchmark knowledge bases while inducing interpretable rules, but computational limitations and unsupported function terms remain future-work boundaries.
- 8 Conclusion and Future Work: NTPs compute gradients of proof success with respect to symbol representations and rule parameters, enabling end-to-end training and rule induction by gradient descent.The prover uses Prolog’s backward chaining algorithm to recursively construct neural networks and introduces differentiable unification between vector representations.
- 8 Conclusion and Future Work: On benchmark KBs, NTPs outperformed ComplEx on three out of four KBs while inducing interpretable rules.
- 8 Conclusion and Future Work: The paper identifies computational limitations of the differentiable prover and plans to investigate hierarchical attention and reinforcement learning methods to address them.
- 8 Conclusion and Future Work: Future work includes supporting function terms and applying NTPs to automated mathematical theorem proving.
A Backward Chaining Pseudocode
The pseudocode expresses symbolic backward chaining through recursive OR and AND procedures that unify goals with rule heads and prove rule bodies. Unification updates substitutions when variables or equal terms match and fails otherwise.
- A Backward Chaining Pseudocode: OR iterates over rules, unifies the goal with each rule head, and calls AND to prove the resulting rule body.Any successful proof suffices because OR represents disjunction over applicable rules.
- A Backward Chaining Pseudocode: AND recursively proves body atoms, substituting the current bindings before invoking OR on each subgoal.
- A Backward Chaining Pseudocode: Unification fails when either input list is incompatible, including a nonempty list paired with an empty list or an explicit failure state.
B ComplEx
ComplEx represents symbols as complex vectors and scores candidate facts using their real and imaginary components. The NTP implementation batches unification across rule partitions, while the K max heuristic approximates gradients to reduce computational cost.
- B ComplEx: ComplEx represents each symbol as a complex vector and defines a neural link-prediction scoring function using its real and imaginary parts.
- B ComplEx: Complex-valued representations allow ComplEx to capture both symmetric and asymmetric relations.
- B ComplEx: NTPs batch-unify goals with rule heads within same-structure KB partitions on a GPU, using vectorized substitutions and per-goal min/max operations.
- B ComplEx: With 1,000 binary-predicate facts, a two-body rule can generate 1,000,000 proofs, making exact backpropagation computationally infeasible and limiting gradients under max aggregation.
- B ComplEx: The K max heuristic retains only the top K substitutions after the first body atom, reducing computation while providing an approximate rather than guaranteed exact gradient.
E Training Details
Training uses fixed optimization settings across experiments, while rule templates vary by dataset and structure. Countries uses progressively richer templates, whereas Kinship, Nations, and UMLS use three templates each.
- E Training Details: Models use ADAM with learning rate 0.001, mini-batches of 50, L2 regularization 0.01, gradient clipping to [-1.0, 1.0], Xavier initialization, and 100 epochs.Countries experiments are repeated ten times and statistical significance is tested with an independent t-test.
- E Training Details: Countries S1 uses three rule templates: symmetry and a two-hop rule repeating the same predicate.
- E Training Details: Countries S2 adds a two-hop rule combining two distinct predicates to the S1 templates.
- E Training Details: Countries S3 further adds a three-hop rule with two intermediate variables and three body predicates.
- E Training Details: Kinship, Nations, and UMLS each use templates for direct transfer, reversed relations, and two-hop reasoning.