Source-linked AI summary
ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language
Oyvind Tafjord, Bhavana Dalvi Mishra, Peter Clark
TL;DR
ProofWriter addresses the limited ability of natural-language reasoning systems to generate implications and reliable proofs. It uses iterative generation of one-step inferences and proofs, enabling deeper proof construction, implication enumeration, and restricted abduction. The approach achieves a reported +9% absolute improvement over prior proof-generation methods while supporting faithful proofs and broader reasoning capabilities.
Problem
Existing transformers reliably classify candidate implications over natural-language theories, but implication generation is un demonstrated and reconstructed proofs are imperfect.
Method
ProofWriter iteratively generates 1-step implications and their proofs, adds implications to the theory for deeper reasoning, and assembles full proofs from these fragments.
Results
+9% absolute proof-generation accuracy over the prior state of the art, with faithful proofs, implication enumeration, and restricted abduction demonstrated across natural-language reasoning tasks.
Takeaways & Limitations
The results improve the viability of neural methods for systematically reasoning over language by generating proofs, implications, and abductive inferences.
Takeaways & Limitations
The iterative approach is inefficient, proves everything before answering a particular question, and risks exceeding the transformer’s input token limit as theories grow.
Abstract
from arXiv · showhide
Transformers have been shown to emulate logical deduction over natural language theories (logical rules expressed in natural language), reliably assigning true/false labels to candidate implications. However, their ability to generate implications of a theory has not yet been demonstrated, and methods for reconstructing proofs of answers are imperfect. In this work we show that a generative model, called ProofWriter, can reliably generate both implications of a theory and the natural language proof(s) that support them. In particular, iterating a 1-step implication generator results in proofs that are highly reliable, and represent actual model decisions (rather than post-hoc rationalizations). On the RuleTaker dataset, the accuracy of ProofWriter's proofs exceed previous methods by +9% absolute, and in a way that generalizes to proof depths unseen in training and on out-of-domain problems. We also show that generative techniques can perform a type of abduction with high precision: Given a theory and an unprovable conclusion, identify a missing fact that allows the conclusion to be proved, along with a proof. These results significantly improve the viability of neural methods for systematically reasoning over natural language.
1 Introduction
ProofWriter addresses the limitations of natural-language reasoning systems by generating faithful proofs, enumerating logical implications, and performing restricted abduction. Evaluations report state-of-the-art proof generation and strong baselines for implication enumeration and abduction.
- 1 Introduction: Natural-language reasoning systems should generate verifiable proofs, not only assign true/false labels to candidate implications.
- 1 Introduction: ProofWriter generates faithful proofs by iteratively producing 1-hop inferences, adding implications to the context, and assembling deeper proofs from proof fragments.The approach is generation-based rather than classification-based, so the proofs reflect the model’s internal inference decisions.
- 1 Introduction: The generative approach enables implication enumeration and restricted abduction over natural-language theories.Abduction identifies a missing fact that makes an otherwise unprovable conclusion provable, together with its proof.
- 1 Introduction: ProofWriter achieves state-of-the-art proof-generation results and strong baselines for implication enumeration and abduction across RuleTaker datasets and new variants.
- 1 Introduction: The work introduces methods for faithful proof generation, implication generation, abduction, and new datasets for research on formal reasoning over language.The authors state that these results improve the viability of neural methods for formal reasoning over language.
2 Related Work
ProofWriter builds on neural deduction over natural language while differing from prior proof, rationale, and explanation systems. It generates explicit deductive chains from natural-language rules rather than reconstructing post-hoc or merely supportive explanations.
- 2 Related Work: RuleTaker showed that transformers can emulate deductive reasoning directly over natural language, bypassing formal representation languages.
- 2 Related Work: PRover assembled proofs with classification and ILP consistency constraints, but its post-hoc proofs did not necessarily represent the model’s actual decisions.
- 2 Related Work: ProofWriter differs from rule-induction and formal-theorem-proving approaches by generating proofs from explicit natural-language rules that may vary across problems.
- 2 Related Work: Rationale and explanation methods typically provide supporting evidence without an explicit account of why it leads to the answer or a fully formed reasoning chain.ProofWriter instead produces a deductive chain from known information to the conclusion using explicit reasoning rules.
3 Approach
ProofWriter formalizes reasoning over natural-language theories as proof, implication-enumeration, and restricted-abduction tasks, using structured proof representations and generative models. Its Iterative approach builds deeper proofs by repeatedly generating one-step implications and adding them to the context.
- Task definitions: The paper defines proof, enumeration, and restricted-abduction tasks over natural-language theories, questions, answers, proofs, and implications.Proof predicts an answer and proof; enumeration generates logical consequences; abduction identifies an extra fact that makes a conclusion true.
- Semantics: Facts are true when explicitly known or recursively supported by rules, under either closed-world or open-world Datalog semantics.The open-world setting permits Unknown answers and explicit negative facts or rule conclusions.
- Proof representation: A proof is a directed acyclic graph whose nodes alternate between facts and rules, including known, negation-as-failure, and rule-concluded facts.Intermediate conclusions are represented inside the proof rather than omitted.
- Proof encoding: Proofs are linearized with identifiers and operators so a generative model can output rule applications, conjunctive conditions, and intermediate conclusions.The encoding uses fact, naf, and conc identifiers, together with %, &, and # symbols and Polish notation.
- Generative models: The Iterative model generates one-step implications and proofs, adds each implication to the theory, and repeats until no further implication is found.Training examples are arranged so every generated inference has depth 1, while test-time iteration supports deeper reasoning.
- Inference procedure: At test time, generated implications are searched for the question or its negation to determine the answer and retrieve a proof.If neither is found, the answer follows the relevant closed- or open-world convention.
4 Datasets
The evaluation uses RuleTaker-derived datasets spanning closed- and open-world semantics, reasoning depths, and natural-language variations. It also evaluates proof-generation quality and out-of-distribution transfer.
- Dataset variants: The evaluation includes original RuleTaker data and CWA and OWA variants that differ in their treatment of negation and Unknown answers.The datasets are denoted D*(orig), D*(CWA), and D*(OWA).
- Annotations: Each example contains a theory, question, answer, and all possible proofs when provable, with auxiliary annotations for proofs of all implications.The domain is small enough to enumerate proofs, although some D5 questions have over 3000 possible proofs.
- Dataset scale and depth: The D* datasets contain D0, D1, D2, D3, and D5 subsets with 100k questions each and required reasoning depths from 0 to 5.Questions are expressed in templated English and include positive or negated facts.
- Evaluation results: Table 2 reports proof-generation accuracy by required proof depth on D5(orig), where ProofWriter achieves a new state of the art for all depths.
- Dataset splits: The datasets use a 70/10/20 train/dev/test split.
- Generalization datasets: Birds-Electricity and ParaRules test transfer to real-world hand-written theories and crowdsourced paraphrased natural language, respectively.Birds-Electricity contains six test-only datasets, while ParaRules contains 40k questions over 2k theories.
5 Experiments and Results
ProofWriter achieves strong proof-generation accuracy, including improved out-of-domain and unseen-depth generalization, while its iterative approach supports faithful and verifiable proofs.
- Proof generation: +9% absolute proof correctness over PRover on the RuleTaker comparison.
- Out-of-domain generalization: Both ProofWriter variants outperform PRover on Birds-Electricity, with the Iterative model reaching 97% proof correctness versus 84.5% for All-At-Once and 80.5% for PRover.
- Out-of-domain generalization: ProofWriter obtains 3% more correct proofs than PRover on ParaRules.
- IID comparison: Both ProofWriter versions achieve more than 95% proof correctness on the D5 test set, including complex proofs.
- Unseen-depth generalization: The Iterative model generalizes more robustly than All-At-Once to proof depths unseen during training.
- Proof verification: Iterative proofs are always verified, whereas verification of All-At-Once proofs drops rapidly at unseen depths.
- Implication enumeration: The Iterative model outperforms All-At-Once for implication enumeration on problems with depths unseen during training.
- Abduction: Abduction scores exceed 85% overall on D3-Ab and D5-Ab, but performance on complex Electricity theories drops to 64% F1 and 62% Accuracy.
6 Discussion
The Iterative approach generalizes robustly to deeper proofs because its highly reliable 1-step inferences keep accumulated errors small. Its main costs are inefficiency and limits on theory size.
- 6.1 All-At-Once vs. Iterative Strategies: The Iterative approach generalizes robustly beyond training proof depths despite error accumulation across iterations.Its high 1-step inference reliability keeps accumulated errors small.
- 6.1 All-At-Once vs. Iterative Strategies: The approach is inefficient and unguided because it proves everything possible before seeking a particular answer and proof.Guided forward-chaining or backward-chaining could address this limitation.
- 6.1 All-At-Once vs. Iterative Strategies: Growing the theory by one fact per iteration risks exceeding the transformer’s default 512-token input limit.Larger theories may require retrieval to manage available facts and rules.
- 6.2 Abduction and Implicit Knowledge: Abduction could materialize implicit facts needed to generate proofs when models use both explicit and implicit knowledge.The proposed combination applies abduction before ProofWriter proof generation.
7 Summary and Conclusion
ProofWriter applies generative techniques to produce proofs, implication enumerations, and abductive inferences over natural language. The work reports improved proof generation and broader reasoning capabilities, while its datasets include deeper implications and abductive questions.
- 7 Summary and Conclusion: ProofWriter generates proofs, implication enumerations, and abductive inferences over natural language.The paper reports these capabilities as improving the viability of neural methods for systematic reasoning over language.
- 7 Summary and Conclusion: +9% absolute proof-generation accuracy over prior state of the art is reported.
- 7 Summary and Conclusion: The Iterative ProofWriter generalizes to deeper proofs and more varied language than seen in training, while producing faithful proofs.
- 7 Summary and Conclusion: The datasets include theories with up to 20 or more implications and implication proof depths up to 10.Question proof depths remain limited to the corresponding dataset depth in the associated questions.
- 7 Summary and Conclusion: Abduction datasets allow zero or more missing facts as answers, with proof depths reaching 11.
- 7 Summary and Conclusion: The updated open-world datasets recompute truth values as True, False, or Unknown using hard negation rather than negation-as-failure.
A.3 The Birds-Electricity Datasets
The Birds-Electricity datasets cover hand-converted abnormality reasoning and toy circuit reasoning, while ParaRules tests reasoning over paraphrased natural language. ParaRules therefore broadens linguistic variation beyond the other described datasets.
- A.3 The Birds-Electricity Datasets: The Birds rulebase contains six rules, seven facts, and forty questions illustrating abnormality predicates.Birds1 and Birds2 differ only in English wording.
- A.3 The Birds-Electricity Datasets: ProofWriter obtains 3% higher proof correctness when trained on D3 plus ParaRules and tested on ParaRules.
- A.3 The Birds-Electricity Datasets: The Electricity datasets use fixed circuit-rule sets ranging from five rules in Elec1 to twelve in Elec4.Each example adds two to five circuit facts and questions about the circuit.
- A.3 The Birds-Electricity Datasets: ParaRules contains 40k questions against 2k theories written in paraphrased natural language.Crowdworkers rephrased templated facts and rules into more varied language.
- A.3 The Birds-Electricity Datasets: ParaRules tests reasoning over more human-like paraphrased language than the synthetic-language datasets.
B.1 Results on the OOD ParaRules Dataset
The ParaRules out-of-domain evaluation tests proof generation on more complex linguistic expressions after training on D3 and ParaRules training data. ProofWriter achieves higher proof correctness than the comparison system.
- B.1 Results on the OOD ParaRules Dataset: Training on D3 plus ParaRules and testing only on the ParaRules test partition evaluates robustness to varied natural language.
- B.1 Results on the OOD ParaRules Dataset: 3% higher proof correctness is obtained by ProofWriter on the ParaRules test partition.
B.2 Abduction: Generalization to New Tasks
Abductive reasoning achieved perfect zero-shot performance on simple Birds rulebases but declined as Electricity theories became more complex, so the task remains only partially solved.
- Perfect zero-shot performance was achieved on the simple Birds abductive rulebases.
- Performance progressively decreased on the Electricity theories as their complexity increased.
- The abductive task remains only partially solved by the generative model.
C Results with T5-large
The paper compares smaller T5-large models with the main T5-11B models, finding generally small score decreases and competitive performance, with some higher-depth proof degradation.
- 770 million-parameter T5-large models generally score lower than the 11-billion-parameter T5-11B models, typically by a small amount.
- T5-large is slightly worse on higher-depth proof accuracy for All-At-Once models trained on D3 and evaluated on D5, but otherwise remains competitive.
- The main experiments use T5-11B fine-tuned for 40k steps with batch size 8 and checkpoint selection by validation score.
- T5-11B is systematically slightly better than T5-large for Iterative ProofWriter trained on D0-D3 and evaluated on D5.
- The text-to-text task format can reach T5’s default 512-token limit when iterative models add implications to the theory.
D.1 All-At-Once Proof Generation
ProofWriter uses text-to-text generation for proof generation, single-hop implication generation, implication enumeration, and single-fact abduction over natural-language theories.
- All-At-Once Proof Generation: Proof generation takes a theory and question as input and produces a True, False, or Unknown answer with intermediate proof steps.
- All-At-Once Proof Generation: Single-hop inference generation asks the model to produce one valid depth-1 implication, or “None” when no such implication exists.
- All-At-Once Proof Generation: Iterative generation appends each inferred implication to the theory and repeats the question, allowing later proofs to reference earlier derived facts.
- All-At-Once Proof Generation: Implication enumeration asks the model to output all valid implications of a theory without generating proofs.
- All-At-Once Proof Generation: A theory can contain multiple valid implications, with the example containing 9 and some D5 theories containing up to 21.
- All-At-Once Proof Generation: Single-fact abduction outputs alternative missing facts that can separately be added to prove a target implication, with the example having two sufficient alternatives.