P roo FV er: Natural Logic Theorem Proving for Fact Verification (2022)

Abstract: Fact verification systems typically rely on neural network classifiers for veracity prediction, which lack explainability. This paper proposes ProoFVer, which uses a seq2seq model to generate natural logic-based inferences as proofs. These proofs consist of lexical mutations between spans in the claim and the evidence retrieved, each marked with a natural logic operator. Claim veracity is determined solely based on the sequence of these operators. Hence, these proofs are faithful explanations, and this makes ProoFVer faithful by construction. Currently, ProoFVer has the highest label accuracy and the second best score in the FEVER leaderboard. Furthermore, it improves by 13.21% points over the next best model on a dataset with counterfactual instances, demonstrating its robustness. As explanations, the proofs show better overlap with human rationales than attention-based highlights and the proofs help humans predict model decisions correctly more often than using the evidence directly.1

## introduction fact verification systems typically comprise an evidence retrieval model followed by a textual entailment classifier @xcite . recent high-performing fact verification systems @xcite use neural models for textual entailment whose reasoning is opaque to humans despite advances in interpretablity @xcite . on the other hand, proof systems like naturalli @xcite provide transparency in their decision making for entailment tasks, by using explicit proofs in the form of natural logic. however, the accuracy of such approaches often does not match that of neural models @xcite . justifying decisions is central to fact verification @xcite . while models such as those developed for fever @xcite typically substantiate their decisions by presenting the evidence as is, more recent proposals use the evidence to generate explanations. here, models highlight salient parts of the evidence @xcite , generate summaries @xcite , correct factual errors @xcite , answer claim-related questions @xcite , or perform rule discovery @xcite ). an explanation is faithful only if it reflects the information that is used for decision making @xcite , which these systems do not guarantee. a possible exception here would be the rule discovery models, although, their performance often suffers due to limited knowledge base coverage and/or the noise in rule extraction from text @xcite . faithful explanations are useful as mechanisms to dispute, debug, or advise @xcite , which may aid a news agency for advice, a user to dispute decisions, and a developer for model debugging in fact verification. keeping both accuracy and explainability in mind, we propose proofver-proof system for fact verification-which generates proofs or refutations of the claim given evidence as natural logic-based inference. proofver follows the natural logic based theory of compositional entailment, originally proposed in natlog @xcite . in the example of figure 1 proofver generates the proof shown in figure 2 , for a given claim and evidence. here, at each step in the proof, a claim span is mutated with a span from the evidence. each such mutation is marked with an entailment relation, by assigning a natural logic operator (natop; @xcite figure 1 : the proof generator in proofver, generates the natural logic proofs using a seq2seq model. the natural logic operators from the proof are used as transitions in the dfa to determine the veracity of the claim. the states s, r, and n in the automaton denote the task labels supports, refutes, and not enough info, respectively. the transitions in the automaton are the natural logic operators (natops) defined in figure 2 : proof steps for the input in figure 1 . @xcite . a step in the proof can be represented using a triple, consisting of the aligned spans in the mutation and its assigned natop. in the example, the mutations in the first and last triples occur with semantically equivalent spans, and hence are assigned with the equivalence natop (≡). however, the mutation in the second triple results in a contradiction, as 'short story' is replaced with 'novel' and an item cannot be both. hence, the mutation is assigned the alternation natop ( ). the sequence of natops from the proof become the transitions in the dfa shown in figure 1 , which in this case terminates at the 'refute (r)' state, that is, the evidence refutes the claim. unlike other natural logic systems @xcite , proofver can form a proof by combining spans from multiple evidence sentences, by leveraging the entity mentions linking those sentences. the proof is generated by a seq2seq model trained using a heuristically annotated dataset, obtained by combining information from the publicly available fever dataset @xcite with ppdb @xcite , wordnet @xcite and wikidata @xcite . we heuristically generate the training data for the claims in three datasets, namely, fever, symmetric fever @xcite , and fever 2.0 @xcite . proofver is currently the highest scoring system on the fever leaderboard in terms of label accuracy and is the second-best system in terms of fever score. additionally, proofver has robustness and explainability as its key strengths. its veracity predictions are solely determined using the generated proof. hence by design, proofver's proofs, when used as explanations, are faithful by construction @xcite . similarly, it demonstrates robustness to counterfactual instances from symmetric fever and adversarial instances from fever 2.0. in particular, proofver achieved 13.21% higher label accuracy than that of the next best model @xcite for symmetric fever and similarly improves upon the previous best results @xcite on adversarial fever. to evaluate the robustness of fact verification systems against the impact of superfluous information from the retriever, we propose a new metric, stability error rate (ser), which measures the proportion of instances where superfluous information changes the decision of the model. proofver achieves a ser of 5.73%, compared with 9.36% of @xcite , where a lower ser is preferred. proofver's proofs as explanations, apart from being faithful, score high in their overlap with human rationales with a token overlap f1-score of 93.28%, 5.67 percentage points more than attention-based highlights from @xcite . finally, humans, with no knowledge of natural logic, correctly predict proofver's decisions 81.67% of the times compared with 69.44% when using the retrieved evidence. 1014 natural logic operates directly on natural language @xcite . thus it is appealing for fact verification, as structured knowledge bases like wikidata typically lag behind text-based encyclopedias such as wikipedia in terms of coverage @xcite . furthermore, it obviates the need to translate claims and evidence into meaning representations such as lambda calculus @xcite . while such representations may be more expressive, they require the development of semantic parsers, introducing another source of potential errors in the verification process. natural logic has been previously used in several information extraction and nlu tasks such as natural language inference (nli, @xcite , question answering @xcite , and open information extraction @xcite . natlog (mac-cartney and manning, 2007), building on earlier theoretical work on natural logic and monotonicity calculus @xcite , uses natural logic for textual inference. naturalli @xcite extended natlog by adopting the formal semantics of icard iii and moss (2014), and it is a proof system formulated for the nli task. it determines the entailment of a hypothesis by searching over a database of premises. the proofs are in the form of a natural logic based logical inference, which results in a sequence of mutations between a premise and a hypothesis. each mutation is marked with a natural logic relation, and is realized as a lexical substitution, forming a step in the inference. each mutation results in a new sentence, and the natural logic relation assigned to it identifies the type of entailment that holds between the sentences before and after the mutation. naturalli adopts a set of seven natural logic operators, as shown in to determine whether a hypothesis is entailed by a premise, naturalli uses a deterministic finite state automaton (dfa). here, each state is an entailment label, and the transitions are the natops (figure 1 ). the sequence of natops in the inference is used to traverse the dfa, and the state where it terminates decides the label of the hypothesis-premise pair. the decision mak- natop: name definition : alternation x∩@xmath0: cover x∩@xmath1: equivalence @xmath2: forward entailment x ⊂ y : negation x∩@xmath3: reverse entailment x ⊃ y : independence all other cases other proof systems that apply mutations between text sequences have been previously explored. @xcite explored how to transform a premise into a hypothesis using mutations, however their approach was limited to two-way entailment instead of three-way that is handled by naturalli. similar proof systems have used mutations in the form of tree-edit operations @xcite , transformations over syntactic parses @xcite , knowledge-based transformations in the form of lexical mutations, entailment rules, rewrite rules, or their combinations @xcite . ## proofver proofver uses a seq2seq generator that generates a proof in the form of natural-logic based logical inference, which becomes the input to a dfa for predicting the veracity of the claim. we elaborate on the proof generation process in section 3.1, and on the veracity prediction in section 3.2. ## generating proofs for training training datasets for evidence-based fact verification consist of instances containing a claim, a label indicating its veracity, and the evidence, typically a set of sentences @xcite @xcite . however, we need sequences of triples to train the proof generator of section 3.1. manually annotating them would be laborious; thus, we heuristically generate them from existing resources. as shown in figure 4 , we perform a twostep annotation process: chunking and alignment, followed by the natop assignment. ## limitations figure 7 shows three instances of incorrect proofs from proofver, which highlight some of the well known limitations in natural logic @xcite . in figure 7 .i, the claim uses two negation words, ''neither'' and ''nor'', both of which appear in different spans and lead to prediction of two negation natops. however, this natop sequence nullifies the effect of the negation natop and predicts support instead of refute. similarly, in figure 7 .ii the adverb ''mistakenly'' negates semantics of the verb. however, its effect is not captured in the second mutation and proofver predicts the forward entailment natop, leading to the support label. moreover, the natop sequence remains the same even if we remove the term ''mistakenly'' from the claim, demonstrating that the effect of the adverb is not captured by our model. similar challenges involving adverbs and non-subsective adjectives @xcite when performing inference in natural logic have been reported in prior work @xcite . in figure 7 .iii, the claim states a time period by mentioning its start and end years, which appear in two different claim spans. however, proofver does not capture the sense of the range implied by the spans containing @xcite instead, two similar 4-digit number patterns are extracted from the evidence and are directly compared to the claim spans, resulting in two alternation natops, thereby predicting not enough info. handling such range expressions is beyond the expressive power of the natural logic, and often other logical forms are needed to perform such computations @xcite . datasets like feverous @xcite , which consider semi-structured information present in tables, often require such explicit computations for which approaches purely based on natural logic are not sufficient. finally, proofver, due to its auto-regressive formulation, generates the corresponding evidence spans and natops for the claim spans sequentially from left to right. however, the steps in the natural logic based inference are not subject to any such specific ordering, and hence the order in which the natops are generated is non deterministic by default @xcite . proofver benefits from the implicit knowledge encoded in the pretrained language models, specifically bart, which follows auto-regressive decoding. nevertheless, in the future we plan to experiment with alternative decoding approaches, including some of the recent developments in non-autoregressive conditional language models @xcite and transformer-based proof generators @xcite . ## conclusion we presented proofver, a natural logic-based proof system for fact verification. currently, we report the best results in terms of label accuracy, and the second best results in fever score in the fever leaderboard. moreover, proofver is more robust in handling superfluous information from the retriever, and handling counterfactual instances. finally, proofver 's proofs are faithful explanations by construction, and improve the understanding of the decision making process of the models by humans.