ProofInfer: Generating Proof via Iterative Hierarchical Inference

Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, pages 10883 - 10892 December 7-11, 2022 ©2022 Association for Computational Linguistics ProofInfer: Generating Proof via Iterative Hierarchical Inference Zichu Fei1,2, Qi Zhang1,2Xin Zhou1,2, Tao Gui3, Xuanjing Huang1,2,3 School of Computer Science, Fudan Unviersity1 Shanghai Key Laboratory of Intelligent Information Processing, Shanghai, China2 Institute of Modern Languages and Linguistics, Fudan University, Shanghai, China3 {zcfei19, qz, xzhou20, tgui,xjhuang}@fudan.edu.cn Abstract Proof generation focuses on deductive rea- soning: 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 conven- tional 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. 1 1 Introduction Automated reasoning is a fundamental goal of AI (Newell and Simon, 1956; McCarthy et al., 1960): the ability to draw valid conclusions from explicitly provided knowledge. Traditional research in automated reasoning focus on structured domains such as formal logic (Robinson and Voronkov, 2001; Musen and Van der Lei, 1988). Recently, (Clark et al., 2021) proposed a new version of 1Our code and models are publicly available at https://github.com/sion-zcfei/ProofInfer 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 (Saha et al., 2020; Sun et al., 2021) or step-by-step (Liang et al., 2021; Tafjord et al., 2021; Yang et al., 2022; Qu et al., 2022). Stepwise 10883 methods link an individual node to the proof step- by-step, which leverage the compositionality of proofs, making it easier for the model to learn and …

Content truncated to 500 words