P roof I nfer: Generating Proof via Iterative Hierarchical Inference (2022)

Abstract: Proof generation focuses on deductive reasoning: given a hypothesis and a set of theories, including some supporting facts and logical rules expressed in natural language, the model generates a proof tree indicating how to deduce the hypothesis from given theories.Current models with state-of-the-art performance employ the stepwise method that adds an individual node to the proof step-by-step.However, these methods actually focus on generating several proof paths rather than a whole tree.During generation, they focus on the most relevant areas of the currently generated node while neglecting the rest of the proof tree. To address this problem, we propose ProofInfer, which generates the proof tree via iterative hierarchical inference.At each step, ProofInfer adds the entire layer to the proof, where all nodes in this layer are generated simultaneously. Since the conventional autoregressive generation architecture cannot simultaneously predict multiple nodes, ProofInfer employs text-to-text paradigm.To this end, we propose a divide-and-conquer algorithm to encode the proof tree as the plain text without losing structure information.Experimental results show that ProofInfer significantly improves performance on several widely-used datasets.In addition, ProofInfer still performs well with data-limited, achieving comparable performance to the state-of-the-art model with about 40% of the training data.

## introduction automated reasoning is a fundamental goal of ai @xcite : the ability to draw valid conclusions from explicitly provided knowledge. traditional research in automated reasoning focus on structured domains such as formal logic @xcite . recently, @xcite proposed a new version of figure 1 : an example of the proof generation task. the existing stepwise methods add the nodes and edges step by step. they focus on generating several proof paths instead of the whole proof tree, so they often link the wrong branches (the nodes with red text) and miss the critical branches (the nodes with other color text). the task by replacing the formal representations of rule-bases with natural language. given a hypothesis and a set of theories, including some supporting facts and logical rules expressed in natural language, the model generates a proof tree indicating how the hypothesis is deduced from a subset of the theories. existing works generates the proof either in a single shot @xcite or step-by-step @xcite @xcite . stepwise methods link an individual node to the proof stepby-step, which leverage the compositionality of proofs, making it easier for the model to learn and generalize to long proofs @xcite . however, the existing stepwise methods actually focus on generating several proof paths rather than a whole tree @xcite . during generation, these models only focus on the most relevant areas of the currently generated path while neglecting the rest of the proof tree. this problem makes the existing stepwise methods struggle to generate proof steps that are both valid and relevant @xcite as shown in figure 1 . to address this challenge, we propose proofinfer, which generates the proof tree via iterative hierarchical inference. unlike the stepwise methods to link nodes one-by-one, the iterative hierarchical inference takes the hypothesis as the root node and infers the proof tree layer-by-layer until each intermediate node in the tree finds its supporting facts. at each step, proofinfer adds the entire layer to the proof, where all nodes in this layer are generated simultaneously. since convention autoregressive generation architecture with teacherforcing @xcite @xcite cannot simultaneously predict the multiple nodes at each step @xcite , proofinfer employs the textto-text paradigm to generate the proof instead of generating the tree structure directly. in detail, we map the generated proof tree to a plain text and take it as input for a generation model to infer the proof text with a new layer, which can be decoded into the corresponding tree structure. text-to-text paradigm can ensure that all the nodes with the same depth in the proof tree are generated simultaneously. furthermore, the standard text-to-text paradigm loses the structure information hidden in the proof tree @xcite . to this end, we propose a divide-and-conquer algorithm to encode the plain text for the proof tree, ensuring that the plain text is unique for each tree and ultimately retains the structure information. we conduct experiments to evaluate our approach on several datasets widely used in previous studies with different settings. experimental results show that our proofinfer outperforms significantly more than the state-of-the-art (sota) models. in addition, proofinfer shows strong generalization ability and performs well with data-limited, achieving comparable performance to the sota models with about 40% of the training data. our main contributions are summarized as follows: ## related work existing methods for generating natural language proofs include single-shot and stepwise methods. single-shot methods generate the entire proof tree at once by predicting the nodes and edges in the proof. prover @xcite trains two binary classifiers to predict whether each node and each edge is a part of the proof, and it employs linear integer programming to ensure the proof is connected. similarly, probr @xcite employs a probabilistic graph to generate the proof via one-shot. on the other hand, stepwise methods link the node to the proof one by one, which leverages the compositionality of proofs, making it easier for the model to learn the long proof. evr @xcite splits the question into subquestions, using generated intermediate texts to guide proof generation step-by-step. proofwriter @xcite shares a similar idea but annotates the extra intermediate conclusions and a much more powerful t5-11b model @xcite for generation, which is hard to reproduce. in addition, proofwriter employs the text-to-text paradigm to generate the proof step-by-step, which ignores the structure information in the proof tree. to retain the structure information, recent works the iterative inference will end when all the nodes find their supporting facts. @xcite @xcite focus on training the module to guide the model to generate the proof path. however, prior works @xcite have observed that the stepwise methods struggle to generate valid and relevant proof steps. one reason is that the stepwise methods focus on generating the proof path instead of the proof tree @xcite . but the conventional generation model with teacher-forcing cannot generate multiple nodes simultaneously, making it inevitable that the model can only focus on the proof path. proofinfer employs the text-to-text paradigm to achieve the hierarchical inference, which generates the proof layer-by-layer and simultaneously generates the nodes with the same depth. this way, proofinfer focuses on the whole proof tree rather than the paths. in addition, to avoid structure information loss caused by the text-to-text paradigm @xcite , proofinfer uses a novel divide-and-conquer algorithm to encode the proof tree as a plain text without information loss. ## methodology in this section, we formalize the proof generation task and introduce our proofinfer. in particular, we first describe the proof generation framework via iterative hierarchical inference. following this, we describe the divide-and-conquer algorithm for proof encoding and proof decoding. the overall architecture of proofinfer is shown in figure 2 . ## experiments to evaluate the model's ability to generate the proof, following @xcite we conduct experiments on three datasets and four settings, including fully-supervised training, training using fewer samples, testing on out-of-distribution samples, and generalization to more complex proofs or language.