Generating Natural Language Proofs with Verifier-Guided Search (2022)

Abstract: Reasoning over natural language is a challenging problem in NLP. In this work, we focus on proof generation: Given a hypothesis and a set of supporting facts, the model generates a proof tree indicating how to derive the hypothesis from supporting facts. Compared to generating the entire proof in one shot, stepwise generation can better exploit the compositionality and generalize to longer proofs but has achieved limited success on real-world data. Existing stepwise methods struggle to generate proof steps that are both logically valid and relevant to the hypothesis. Instead, they tend to hallucinate invalid steps given the hypothesis. In this paper, we present a novel stepwise method, NLProofS (Natural Language Proof Search), which learns to generate relevant steps conditioning on the hypothesis. At the core of our approach, we train an independent verifier to check the validity of the proof steps to prevent hallucination. Instead of generating steps greedily, we search for proofs maximizing a global proof score judged by the verifier. NLProofS achieves state-of-the-art performance on EntailmentBank and RuleTaker. Specifically, it improves the correctness of predicted proofs from 27.7% to 33.3% in the distractor setting of EntailmentBank, demonstrating the effectiveness of NLProofS in generating challenging human-authored proofs.

## introduction a fundamental goal of ai since its inception is automated reasoning @xcite : given explicitly provided knowledge as assumptions, we want the system to draw logically valid conclusions. research in automated reasoning has traditionally focused on structured domains such as formal logic @xcite . on the other hand, recent work suggests that free-form natural language can be a suitable vehicle for reasoning @xcite , because natural language represents knowledge without requiring labour-intensive formalization. however, reasoning in natural language is challenging, as it requires compositional generalization to novel examples @xcite )-a capability that state-of-the-art large language models struggle with @xcite . in this work, we focus on proof generation in natural language (fig. 1 ): given a hypothesis and a set of supporting facts in natural language, the model generates a proof tree indicating how the hypothesis is derived from a subset of the supporting facts. the proof tree may contain intermediate conclusions, which need to be generated by the model. existing methods generate the proof either in a single shot or step by step. stepwise methods leverage the compositionality of proofs, making it easier for the model to learn and generalize to longer proofs @xcite . however, existing stepwise methods suffer from a trade-off between generating valid steps and relevant steps. prior works @xcite have observed that, given the hypothesis, the model often learns to hallucinate invalid proof steps leading to the hypothesis, instead of performing valid logical inference (see examples in we introduce nlproofs, a novel method for stepwise proof generation. it generates proof steps conditioning on the hypothesis, enabling the model to learn to generate only relevant steps. to prevent hallucination, it trains an independent verifier based on roberta @xcite , which takes a single step (including multiple premises and one conclusion) as input and produces a score indicating its validity. during inference, instead of generating steps greedily, nlproofs searches for proofs h: solar is a kind of renewable energy for heating homes sent1: homes are buildings sent2: solar is renewable sent3: wind is a kind of energy sent4: solar is a kind of energy sent5: energy is used for heating buildings sent6: coal is nonrenewable … … hypothesis (ℎ): supporting facts (𝐶): sent1: homes are buildings h: solar is a kind of renewable energy for heating homes sent5: energy is used for heating buildings int1: energy is used for heating homes sent2: solar is renewable sent4: solar is a kind of energy int2: solar is a kind of renewable energy proof tree (𝑇): ## related work proof generation in natural language. when generating a proof step, prior work has observed that if the hypothesis is available, the model often uses it to hallucinate the intermediate conclusion instead of drawing valid logical inferences ( prover @xcite , proofwriter, and fairr have only evaluated on the simple ruletaker dataset @xcite . and it is nontrivial to extend them to real-world data. for example, fairr assumes sentences fall into two categories: rules and facts, which are tailored for ruletaker. @xcite introduce entailmentbank, a challenging benchmark of proofs authored by human experts, which is used to evaluate entailmentwriter, their method for single-shot proof generation. scsearch and @xcite also use entailmentbank but focus on different task settings that do not quantitatively evaluate the generated proofs. reasoning in other nlp tasks. multi-hop reasoning can also be found in open-domain qa @xcite , fact verification @xcite , and reading comprehension @xcite @xcite . compared to proof generation, reasoning chains in these tasks are much simpler, often consisting of only 2-3 supporting facts. also, they are more coarse-grained, involving large chunks of texts such as passages instead of simple, short sentences. ## generating natural language proofs task definition. now we define the proof generation task. as in fig. 1 (top), the input consists of a hypothesis h and a set of supporting facts @xmath0, sent 2 , . . . , sent n }. both h and sent i are natural language sentences. h can be derived from a subset of c through reasoning of one or multiple steps. the output is a proof tree t specifying how h is derived from c. the tree has h as its root and sent i as leaf nodes. the intermediate nodes are intermediate conclusions generated by the model. each non-leaf node u corresponds to a reasoning step with u as the conclusion and its children as premises. to successfully perform the task, the model must select relevant sentences from c, use them as leaf nodes to compose a valid proof tree leading to h, and fill in all the intermediate conclusions. singles-shot vs. stepwise generation. a simple and effective method for proof generation, popularized by proofwriter @xcite , is to finetune a pretrained t5 model @xcite to map the input (h and c) to the output (t ), either in a single shot or stepwise. to that end, the input/output must be encoded as text sequences, e.g., encoding the input by concatenating h and c as illustrated in fig. 1 . 3 the output proof tree can be encoded by post-order traversal. as in fig. 1 , nodes are labeled with identifiers: sent* for leaf nodes, int* for intermediate nodes, and hypothesis for the root. the output sequence is produced by traversing the tree in post-order, generating one proof step at each non-leaf node, using & for "and" and -> for "entails". the tree may correspond to multiple valid sequences due to different ordering between proof steps and between premises within a step. nevertheless, the evaluation metric can be calculated from the reconstructed trees instead of the raw text sequences. in single-shot generation, the model generates the output sequence of the entire proof (fig. 1 middle), whereas in stepwise generation, each time the model takes the current partial proof as input (besides h and c) and generates only the next step (fig. 1 bottom). ## our method: nlproofs now we present nlproofs, our method for generating natural language proofs. it has three main components: ## conclusion we have introduced nlproofs for stepwise proof generation in natural language. it learns to generate relevant proof steps conditioning on the hypothesis. to prevent hallucination, nlproofs searches for proofs that maximize a validity score judged by a verifier. our method has achieved state-of-the-art performance on en-tailmentbank and ruletaker, demonstrating the promise of stepwise proof generation for human-authored proofs. in the future, we hope to see increasing applications of verifiers and proof search in various reasoning tasks.