Skip to content
End-to-End Differentiable Proving
NewLisp Python
Branch: master
Clone or download
Latest commit 23687f5 Nov 21, 2018
Type Name Latest commit message Commit time
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
tests NTPv0.6 code release Feb 2, 2018
.gitignore NTPv0.6 code release Feb 2, 2018
LICENSE Initial commit 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/
  • *.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/ 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       = {},
You can’t perform that action at this time.