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.

Disclaimer

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
locatedIn(palau,micronesia).
locatedIn(palau,oceania).
locatedIn(maldives,southern_asia).
locatedIn(maldives,asia).
locatedIn(brunei,south-eastern_asia).
locatedIn(brunei,asia).
neighborOf(brunei,malaysia).
locatedIn(japan,eastern_asia).
locatedIn(japan,asia).
locatedIn(netherlands,western_europe).

• *.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).

Running

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.

Test

nosetests

Contributors

• Tim Rocktäschel
• Sebastian Riedel
• Pasquale Minervini
• Matko Bosnjak
• Johannes Welbl

Citation

@inproceedings{rocktaschel2017end,
  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},
}