End-to-End Differentiable Proving
Switch branches/tags
Nothing to show
Clone or download
rockt Merge pull request #1 from pminervini/master
Remove source of randomness/unpredictability
Latest commit 5a242ea Feb 28, 2018
Failed to load latest commit information.
conf NTPv0.6 code release Feb 2, 2018
data added data Feb 2, 2018
docs NTPv0.6 code release Feb 2, 2018
models NTPv0.6 code release Feb 2, 2018
ntp set random.seed Feb 27, 2018
tests NTPv0.6 code release Feb 2, 2018
.gitignore NTPv0.6 code release Feb 2, 2018
LICENSE Initial commit Feb 2, 2018
README.md Update README.md Feb 2, 2018
requirements.txt NTPv0.6 code release Feb 2, 2018


End-to-End Differentiable Proving

This is an implementation of the paper End-to-End Differentiable Proving. For a high-level introduction, see the NIPS oral, slides and poster.


Please note that this software is not maintained. It is highly-experimental research code, not well documented and we provide no warranty of any kind. Use at your own risk!

Data Format

Data for the NTP is in nl format - basically Prolog syntax:

ntp$ head data/countries/countries.nl
  • *.nl files represent facts and rules (example of a rule: isa(X,Y) :- isa(X,Z), isa(Z,Y))

  • *.nlt files represent rule templates (example of a rule template: #1(X,Y) :- #2(X,Z), #3(Z,Y))

ntp$ cat data/ntp/simpsons.nlt
5   #1(X, Y) :- #2(X, Y).

5   #1(X, Y) :- #1(Y, X).

5   #1(X, Y) :-
    #2(X, Z),
    #2(Z, Y).


The main file for running NTP is ntp/experiments/learn.py which takes the path to a configuration file as argument.

Code Structure

The core implementation of the NTP can be found here.

The base models (neural link predictors) are implemented here.

Imortant "modules" are unify, this one and this one. It should pretty much reflect the pseudocode in the paper.

The tricky part is the tiling of batched representations for batch proving - check out this.

However, this tiling needs to happen at various points in the code, e.g. here

Implementation of tiling (and multiplexing) here and here.

An important trick in NTP for proving in larger KBs and usin complex rules, is the Kmax heuristic, implemented here.

There is a symbolic prover implementation here

  • it is probably worthwile to look at it first, and compare to NTP.





  author    = {Tim Rockt{\"{a}}schel and
               Sebastian Riedel},
  title     = {End-to-end Differentiable Proving},
  booktitle = {Advances in Neural Information Processing Systems 30: Annual Conference
               on Neural Information Processing Systems 2017, 4-9 December 2017,
               Long Beach, CA, {USA}},
  pages     = {3791--3803},
  year      = {2017},
  url       = {http://papers.nips.cc/paper/6969-end-to-end-differentiable-proving},