PaperlayerView exact revision on arXiv

Source-linked AI summary

ProoFVer: Natural Logic Theorem Proving for Fact Verification

Amrith Krishna, Sebastian Riedel, Andreas Vlachos

arXiv:2108.11357v2cs.CL

TL;DR

High-performing neural entailment models can be opaque, while transparent proof systems often do not match their accuracy; generated explanations also do not guarantee faithfulness. ProoFVer uses a seq2seq model to generate natural-logic proofs from claim and evidence spans, then determines veracity from the proof’s natural logic operator sequence. ProoFVer reports the FEVER leaderboard’s highest label accuracy and second-best FEVER Score, and 13.21% higher label accuracy than the next-best model on Symmetric FEVER.

  • Problem

    High-performing neural entailment models can be opaque, while transparent proof systems often do not match their accuracy; generated explanations also do not guarantee faithfulness.

    Source: §1 · p. 1

  • Method

    ProoFVer uses a seq2seq model to generate natural-logic proofs from claim and evidence spans, then determines veracity from the proof’s natural logic operator sequence.

    Source: §1 · p. 1

  • Results

    ProoFVer reports the FEVER leaderboard’s highest label accuracy and second-best FEVER Score, and 13.21% higher label accuracy than the next-best model on Symmetric FEVER.

    Source: §1 · p. 2, §8 · p. 12

  • Takeaways & Limitations

    ProoFVer’s proofs concern human understanding of models’ decision-making processes.

    Source: §8 · p. 13

    Natural logic can miss negation scope and range-expression computations, limiting its sufficiency for semi-structured tasks such as FEVEROUS that require explicit computations.

    Source: §7 · p. 12

Abstract

from arXiv · show

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 faces a tension between neural models’ accuracy and transparent but often less accurate proof systems. ProoFVer generates natural-logic proofs and uses them to determine claim veracity, reporting strong benchmark performance and faithful explanations.

1 Introduction

  • High-performing neural entailment models can be opaque, while natural-logic proof systems offer transparency but often do not match neural-model accuracy.Source: §1 · p. 1
  • ProoFVer generates natural-logic proofs by mutating claim spans with evidence spans, marking each mutation with a natural logic operator.The operator sequence drives a DFA that determines veracity, making the proof the basis of the decision.Source: §1 · pp. 1–2, Figure 1 · p. 2
  • ProoFVer combines spans from multiple evidence sentences and trains its seq2seq proof generator on heuristically annotated data assembled using FEVER, PPDB, WordNet, and Wikidata.Source: §1 · p. 2
  • ProoFVer reports the highest FEVER leaderboard label accuracy and second-best FEVER Score, with 13.21% higher label accuracy than the next-best model on Symmetric FEVER.It also improves on previous best results on Adversarial FEVER.Source: §1 · p. 2
  • ProoFVer’s Stability Error Rate is 5.73% versus 9.36% for Stammbach (2021), and its proofs reach 93.28% token-overlap F1, 5.67 points above attention-based highlights.A lower Stability Error Rate is preferred.Source: §1 · p. 2
  • Humans correctly predict ProoFVer’s decisions 81.67% of the time using proofs, versus 69.44% using retrieved evidence.Source: §1 · p. 2

2 Natural Logic Proofs as Explanations

Natural-logic proofs represent inference as lexical mutations labeled with natural logic relations. A deterministic automaton can use those relations to select an entailment label, making the inference steps transparent.

2 Natural Logic Proofs as Explanations

  • Natural logic has been used for natural language inference, question answering, and open information extraction, while NatLog applies it to textual inference.Source: §2 · p. 3
  • NaturalLI represents inference as lexical mutations between premise and hypothesis, each labeled with a natural logic relation, using seven natural logic operators.Source: §2 · p. 3, Table 1 · p. 3
  • NaturalLI traverses a deterministic finite state automaton using the sequence of natural logic operators, and the terminal state supplies the entailment label.Because the decision relies solely on the logical inference steps, those steps form faithful explanations.Source: §2 · p. 3
  • Earlier mutation-based proof systems include two-way entailment, tree-edit operations, syntactic transformations, and knowledge-based rewrites.Stern et al. (2012) explored premise-to-hypothesis mutations but was limited to two-way entailment, unlike NaturalLI’s three-way setting.Source: §2 · p. 3

3 ProoFVer

ProoFVer generates natural-logic proof steps from claims and retrieved evidence, then uses their operator sequence in a deterministic automaton to predict veracity. Its generation process can draw evidence spans from multiple sentences, and its fact-verification automaton distinguishes negation from alternation.

3 ProoFVer

  • ProoFVer uses a seq2seq generator to produce a natural-logic inference that becomes the input to a deterministic finite state automaton for claim-veracity prediction.Source: §3 · pp. 3–4

3.1 Proof Generation

  • Each proof step is a triple containing a claim span, an evidence span, and a natural logic operator; applying the mutations left to right forms successive statements.Source: §3.1 · p. 4
  • The autoregressive generator can select evidence spans in any order from multiple sentences, and some retrieved evidence may not be used.Claim spans proceed successively through the triples, while the operators are represented by predetermined tokens.Source: §3.1 · p. 4
  • Dynamically constrained markup decoding switches among claim-span, evidence-span, and NatOp token search spaces to produce valid proof triples.The markup delimiters constrain claim spans to copied claim tokens, evidence spans to evidence tokens, and the token following an evidence span to a NatOp.Source: §3.1 · p. 4

3.2 Veracity Prediction

  • The DFA maps predicted NatOp sequences to SUPPORT, REFUTE, or NOT ENOUGH INFO, and ProoFVer treats negation and alternation as distinct operators.Unlike NaturalLI’s NLI setup, ProoFVer distinguishes the two relations for fact verification and does not use the cover operator.Source: §3.2 · p. 4

4 Generating Proofs for Training

The paper heuristically constructs proof-training sequences from existing fact-verification resources because those datasets do not contain proof triples. Its process aligns claim and evidence spans, assigns natural logic operators (NatOps), then filters candidate operator sequences using veracity labels and FEVER annotations.

4 Generating Proofs for Training

  • Because existing fact-verification datasets lack proof triples, training proofs are heuristically generated through chunking and alignment followed by NatOp assignment.Figure 4 depicts those two stages, with NatOp assignment itself involving initial assignment and two filtering steps.Source: §4 · pp. 4–5, Figure 4 · p. 5

4.1 Chunking and Alignment

  • For multiple evidence sentences, the highest-cosine-similarity span is generally selected, while linked entity mentions mark switches between evidence sentences.Claims are chunked and each evidence sentence is aligned separately; low-similarity alignments are replaced with DEL.Source: §4.1 · p. 5

4.2.1 Initial Assignment

  • Initial NatOps use lexical rules and PPDB, WordNet, and Wikidata relations; entity hierarchies map to entailment, siblings to alternation, and distant connected entities to independence.Wikidata aliases receive equivalence, while relation direction determines forward or reverse entailment.Source: §4.2.1 · p. 6

4.2.2 Filtering the Search Space

  • Partially assigned NatOp sequences are filtered against the training veracity label using the DFA, retaining only sequences that terminate in the matching label.A further filter uses FEVER claim-construction transformations to select likely NatOps; manual assignment was needed for 2.55% of FEVER claims when filtering left no candidates.Source: §4.2.2 · pp. 6–7

5 Experimental Methodology

Experiments use FEVER and related counterfactual and adversarial datasets, with label accuracy, FEVER Score, and a robustness metric for evaluation. The paper compares retriever and proof-generator configurations and tests replacing manual FEVER transformation annotations with classifier predictions.

5.1 Data

  • Training uses FEVER, Symmetric FEVER counterfactual instances, and FEVER 2.0 adversarial examples, with retrieved evidence supplying training proofs for NEI claims.The study also derives development-set rationales from FEVER annotation logs and identifies 300 claims meeting its rationale criteria.Source: §5.1 · p. 7

5.2 Evaluation Metrics

  • Evaluation reports label accuracy and FEVER Score, while Stability Error Rate measures claims whose SUPPORT or REFUTE decision changes when additional evidence is added.Symmetric FEVER results are reported as mean label accuracy and standard deviation across five random initialisations.Source: §5.2 · pp. 7–8

5.3 Baseline Systems

  • The baselines include KGAT’s graph-attention model, CorefBERT’s coreference-pretrained language model, and Stammbach’s token-scoring retriever with a DeBERTa classifier.KGAT and CorefBERT use evidence sentences as graph nodes, while Stammbach selects sentences by aggregating token scores.Source: §5.3 · p. 8

5.4 ProoFVer: Implementation Details

  • For comparability, ProoFVer uses established retrieval approaches and a fine-tuned BART proof generator, with five retrieved sentences as evidence.The default concatenates claim and evidence; variants process evidence separately or restrict mutation spans and search space.Source: §5.4 · p. 8

5.5 Heuristic Annotation Using Kepler

  • KEPLER predicts FEVER claim transformations from the claim, evidence sentence, and veracity label to reduce reliance on manual annotations.Training data ranges from 1,800 to 60,000 examples; ProoFVer-K uses gold transformed spans, while ProoFVer-K-NoS requires only that the predicted transformation appear in the NatOp sequence.Source: §5.5 · pp. 8–9

6 Results

ProoFVer performs strongly across fact verification, robustness, and explanation evaluations. Its results include high FEVER leaderboard placement, better accuracy on Symmetric FEVER than the next-best model, strong rationale overlap, and improved human prediction with proofs.

6.1 Fact Verification

  • ProoFVer-SB is the best-performing model in the experiments, with the highest FEVER leaderboard label accuracy and second-best FEVER Score.The second-best FEVER Score is behind the unpublished “mitchell.dehaven” model.Source: §6.1 · p. 9
  • ProoFVer’s default configuration outperformed the baselines and other Liu et al. retriever variants, with multi-sentence handling especially helping claims requiring multiple evidence sentences.On those claims, ProoFVer predicted 67.45% correctly versus 60.1% for ProoFVer-MV; dynamically inferred mutations also benefited overall performance.Source: §6.1 · p. 9

Impact of additional manual annotation

  • 79.67% label accuracy for ProoFVer-K and 78.61% for ProoFVer-K-NoS used KEPLER predictions from a configuration trained on 41.24% of FEVER claims.Without the final manually annotated NatOp filtering step, ProoFVer achieved 58.29% label accuracy; ProoFVer-K-NoS achieved 64.65% using KEPLER predictions trained on as few as 1,800 instances.Source: Impact of additional manual annotation · pp. 9–10, Table 4 · p. 9

6.2 Robustness

  • 81.70% mean accuracy on Symmetric FEVER was 13.21% above CorefBERT, the next-best model.After L2 regularization, ProoFVer had the highest accuracy on both FEVER and Symmetric FEVER; its accuracy drop was less than 3%, versus reductions above 9% for KGAT and CorefBERT after fine-tuning.Source: §6.2 · p. 10, Table 5 · p. 10
  • 82.79% label accuracy on FEVER 2.0 adversarial data exceeded Schuster et al.’s previously best reported 82.51%.ProoFVer was fine-tuned on heuristically generated proofs from participant data disjoint from the evaluation set, and on proofs from Symmetric FEVER.Source: §6.2 · p. 10
  • 5.73% Stability Error Rate for ProoFVer-SB was lower than the 9.36% reported for DominikS.ProoFVer’s rate was 6.21%; a lower SER is preferred, and the metric measures decisions changed by additional retrieved evidence.Source: §6.2 · p. 10

6.3.1 Rationale Extraction

  • ProoFVer achieved a token-level F-score of 93.28, compared with best F-scores of 87.61 for CorefBERT and 86.42 for KGAT, using attention-ranked words at top-1% and 5%-to-50% ranges.Source: §6.3.1 · p. 11

6.3.2 Human evaluation

  • 81.67% of human forward predictions matched ProoFVer’s decisions when subjects saw its proofs, versus 69.44% with evidence alone.For SUPPORT and REFUTE, proof-based predictions were correct 91.67% and 86.67% of the time, versus 73.33% and 70% with evidence; Fleiss κ was 0.7074 for proofs and 0.6612 for the baseline.Source: §6.3.2 · pp. 11–12

7 Limitations

ProoFVer's natural-logic proofs can mishandle negation and modifier scope, and natural logic cannot express some range computations. Its left-to-right autoregressive generation also imposes an ordering that the inference steps do not inherently have.

7 Limitations

  • Negation interactions and adverb scope can yield incorrect natural-logic inferences, including a SUPPORT prediction when the claim should be REFUTE.The examples include two negation words whose NatOps cancel and an uncaptured effect of “mistakenly.”Source: §7 · p. 12
  • Range expressions exceed natural logic's expressive power, while table-rich FEVEROUS claims often require explicit computations that purely natural-logic approaches cannot perform (Aly et al., 2021).A start-to-end year range is instead compared as separate year spans, producing NOT ENOUGH INFO.Source: §7 · p. 12
  • ProoFVer generates evidence spans and NatOps from left to right, although natural-logic inference steps have no prescribed order and their generation order is non-deterministic by default.The authors identify alternative decoding approaches as future work.Source: §7 · p. 12

8 Conclusion

ProoFVer reports the best label accuracy and second-best FEVER Score on the FEVER leaderboard, alongside robustness and faithful proofs. The proofs also improve human understanding of model decisions.

8 Conclusion

  • ProoFVer reports the FEVER leaderboard's best label accuracy and second-best FEVER Score.Source: §8 · p. 12
  • The conclusion reports greater robustness to superfluous retriever information and counterfactual instances.Source: §8 · p. 12
  • ProoFVer's proofs are faithful explanations by construction and improve human understanding of model decision-making.Source: §8 · pp. 12–13
Loading 2108.11357v2…