ProofInfer: Generating Proof via Iterative Hierarchical Inference

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, linking an individual node to the proof step-by-step. However, these methods actually focus on generating several proof paths rather than a whole tree. To address this problem, we propose ProofInfer, which generates the proof tree via iterative hierarchical inference. At each step, ProofInfer generates the entire layer for proof tree, 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 avoid it. To this end, we propose a divide- and-conquer algorithm to encode the proof tree as the plain text recursively without structure information loss. Experimental results show that ProofInfer significantly outperforms the state-of-the-art (SOTA) models on several widely-used datasets. In addition, ProofInfer still performs well with data-limited, achieving comparable performance to the SOTA models with only 40% of the training data.