ProofWriter

Aristo • 2020
These datasets accompany the paper "ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language". They contain updated RuleTaker-style datasets with 500k questions, answers and proofs over natural-language rulebases, used to show that Transformers can emulate reasoning over rules expressed in language, including proof generation. It includes variants using closed- and open-world semantics. Proofs include intermediate conclusions. Extra annotations provide data to train the iterative ProofWriter model as well as abductive reasoning to make uncertain statements certain.
License: CC BY

The ProofWriter dataset contains many small rulebases of facts and rules, expressed in English. Each rulebase also has a set of questions (English statements) which can either be proven true or false using proofs of various depths, or the answer is “Unknown” (in open-world setting, OWA) or assumed negative (in closed-world setting, CWA).

The dataset includes full proofs with intermediate conclusions, which models can try to reproduce.

The dataset supports various tasks:

  • Given rulebase + question, what is answer + proof (w/intermediates)?
  • Given rulebase, what are all the provable implications?
  • Given rulebase + question without proof, what single fact can be added to make the question true?

Here is a simple example from the depth-2 dataset D2(OWA):

Rulebase:

triple1: The cow is big.  
triple2: The cow needs the dog.  
triple3: The dog sees the rabbit.  
triple4: The rabbit chases the cow.  
triple5: The rabbit chases the dog.  
triple6: The rabbit is big.  
triple7: The rabbit sees the dog.  
rule1: If the cow is blue and the cow needs the rabbit then the cow needs the dog.
rule2: If the cow chases the dog then the cow sees the rabbit.
rule3: If something is big then it chases the dog.

Question with answer + proof:

Question: The cow sees the rabbit?
Answer: true
Proof: (((triple1) -> (rule3 % int2))) -> (rule2 % int1) ; with int1 = The cow sees the rabbit. ; int2 = The cow chases the dog.

Generate all implications (only 2 in this case, can be as high as 21 in D5 theories):

All implications: The cow chases the dog. The cow sees the rabbit.

Use abduction to find a missing fact which will make something true:

Question to make true: The dog chases the dog.
Missing fact: The dog is big.   (denoted tripleM)
Proof: (tripleM) -> rule3

Authors

Oyvind Tafjord, Bhavana Dalvi Mishra, Peter Clark