T ab V er: Tabular Fact Verification with Natural Logic (2024)

Abstract: Fact verification on tabular evidence incentivizes the use of symbolic reasoning models where a logical form is constructed (e.g., a LISP-style program), providing greater verifiability than fully neural approaches. However, these logical forms typically rely on well-formed tables, restricting their use in many scenarios. An emerging symbolic reasoning paradigm for textual evidence focuses on natural logic inference, which constructs proofs by modeling set-theoretic relations between a claim and its evidence in natural language. This approach provides flexibility and transparency but is less compatible with tabular evidence since the relations do not extend to arithmetic functions. We propose a set-theoretic interpretation of numerals and arithmetic functions in the context of natural logic, enabling the integration of arithmetic expressions in deterministic proofs. We leverage large language models to generate arithmetic expressions by generating questions about salient parts of a claim which are answered by executing appropriate functions on tables. In a few-shot setting on FEVEROUS, we achieve an accuracy of 71.4, outperforming both fully neural and symbolic reasoning models by 3.4 points. When evaluated on TabFact without any further training, our method remains competitive with an accuracy lead of 0.5 points.

## introduction fact verification systems assess the veracity of claims based on evidence and provide an explanation for the prediction. in the case of tabular evidence, verification frequently relies on symbolic reasoning steps, such as the execution of arithmetic functions, to accurately predict whether a claim is supported by evidence @xcite . this incentivizes symbolic reasoning systems, where a logical representation of a claim and its tabular evidence (e.g., a lisp-style program) is executed to produce the veracity prediction @xcite . since the execution of these logical forms is deterministic, they serve as faithful explanations of the model's reasoning @xcite . however, these systems typically rely on well-formed tables, constraining their use in many scenarios, such as reasoning over diverse tabular structures as typically found on wikipedia. consequently, the majority of recently proposed verification models focus on neural entailment models that latently execute arithmetic functions @xcite or generate a natural language explanation alongside its prediction @xcite . while systems that produce natural language explanations are more flexible regarding the evidence format, they do not necessarily generate faithful explanations @xcite . an emergent symbolic reasoning paradigm for textual evidence focuses on logical inference by directly comparing claim and textual evidence via natural logic inference @xcite , achieving high prediction accuracy while maintaining faithful explanations @xcite . however, current natural logic systems are unable to handle tabular evidence since the semantic relationship captured between aligned claim-evidence spans via natural logic's set-theoretic operators does not extend to arithmetic functions @xcite . for instance, in figure 1 , no evidence in the table directly corresponds to the part of the claim that states three municipalities. instead, arithmetic computation on the table beyond the expressiveness of natural logic's set-theoretic operators is required (i.e., counting relevant cells). to this end, we propose tabver: tabular fact verification, a natural logic inference system that adds arithmetic reasoning capabilities to reason over tabular evidence directly in natural language. we define a set-theoretic interpretation of figure 1 : tabver proposes a set-theoretic view on numerals and arithmetic functions, which is integrated into natural logic proofs as arithmetic comparisons between claim and answers to questions (arithexps), resulting in deterministic inference (left). to generate arithexps, tabver asks questions about salient parts c i of a claim (middle), which are answered using tabular evidence e following the generation of a rationale and a set-theoretic compatible representation of the computation (right), serving as the answer a i aligned to c i . in a few-shot setting with 64 training instances on the tabular subset of the feverous dataset @xcite , tabver outperforms previous symbolic reasoning systems, including lpa @xcite , sasp @xcite , binder @xcite , and a state-of-the-art natural logic system @xcite by 10.5 accuracy points. moreover, tabver outperforms the highest-scoring neural entailment model by 3.4 accuracy points, including baselines such as tapas @xcite , tapex @xcite , pasta @xcite , and large language models of similar size as tabver. we confirm the tabular reasoning capabilities of tabver in a domain transfer setting to tabfact @xcite without further training annotations. our system performs competitively, leading over the strongest baseline by 0.5 accuracy points. our analysis reveals that tabver's reading of numerals is more sensitive to numerical inaccuracies and the pragmatic context of a claim (i.e., quantifiers and rounding) than a same-sized llm baseline, reflecting the annotator guidelines of feverous more accurately. finally, the arithmetic functions invoked in tabver's proofs are more accurate than the ones called in the logical form of our symbolic reasoning baselines. 1 2 related work symbolic reasoning systems for fact verification convert text into a logical form or executable program (sql/lisp-style). they typically involve a neural component, either to rank viable candidate programs consisting of hand-crafted functions @xcite or via neuralsymbolic models that generate programs directly @xcite . these programs are faithful explanations since the program's execution is the verdict. with the improved capabilities of large language models to generate code @xcite , @xcite and @xcite explore the use of sql, python, and fol to faithfully fact-check tabular claims, however, they only use proprietary models consisting of hundreds of billions of parameters. we show that tabver outperforms these approaches (when controlled for the language model), which we attribute to the suitability of natural logic to natural language in contrast to query languages like sql. the aforementioned symbolic executioners stand in contrast to the more prominent approach of using programs as features to neural systems, typically complemented by the original claim and table. for instance, lisp-style programs are used as a latent signal for a graph neural network @xcite @xcite , and sql queries and their executions are used as features to an llm serving as a verdict classifier @xcite @xcite . @xcite incrementally update an evidence table with lisp-style operations. alternatively to symbolic integration into neural systems, chen (2023) produce natural language explanations using chain-of-thought prompting @xcite . @xcite show that a 175b parameter gpt-3 model competes with fully supervised systems on tabular claims, yet its 6.7b variant performed only slightly above chance. this observation has been further confirmed by @xcite with llama2-chat-7b. finally, large-scale instruction-tuning on tabular tasks has been explored @xcite @xcite , however they do not produce explanations. conclusively, previous systems either rely on large proprietary models to achieve competitive performance or they sacrifice prediction explainability. in contrast to these explicit meaning representations, @xcite propose to use natlog @xcite for textual inference, operating directly on natural language by comparing texts in a premise with an associated hypothesis using set-theoretic relations. thus, as a framework of flexible compositional inference, it circumvents the requirement to convert statements into rigid logical forms, and typically independently from one another. these favorable properties of natural logic inference have subsequently recently been explored for fact verification, resulting in accurate predictions while maintaining transparency with plausible explanations @xcite . @xcite exploit natural logic's operations on natural language by casting the operators into a question-answering framework to leverage recent advances of instruction-tuned language models. this paper is the first attempt to extend natural logic inference for fact verification to the tabular domain. finally, tabular question answering @xcite is a common component to decompose a claim and reasoning processes. @xcite supplement the evidence with answers to questions generated via decomposition templates while @xcite supplement the evidence with information from a table-to-text model. more recently, @xcite use llms to decompose tables and questions. however, all three methods feed these modified tables into a pre-trained neural model @xcite , ultimately producing veracity predictions without explanations. finally, even for textual evidence, most previous work that generates questions conditioned on the claim does not construct proofs from the answers @xcite @xcite . ## method given a claim c and a set of evidence tables e, the task is to predict a veracity label ŷ p {supports, refutes, not enough information (nei)}, and to accompany the prediction with an explanation. since evidence might require arithmetic reasoning beyond the expressiveness of natural logic, as shown in figure 1 with three municipalities, tabver's explanation is a proof p " m 1 , . . . , m l , consisting of quintuples m i " pc i , e i , q i , a i , o i q, where o i describes the set-theoretic relation (natop) between a claim span c i and the result a i of arithmetic computations executed over relevant evidence e i . figure 2 : the finite state automaton (dfa), following natural logic inference @xcite . the transitions in the dfa denote natops and the states the veracity labels. the final state on which the the proof terminates determines the overall veracity. tabver performs arithmetic reasoning steps in a question-answering framework, producing an arithmetic expression (arithexp) with a i being the answer to a question q i for a claim span c i answered over evidence e i . the sequence of operators o " o 1 , . . . , o l is then the input to a finite state automaton that specifies the claim's veracity label ŷ " dfapoq. we follow the dfa for textual entailment described in @xcite , shown in figure 2 . to enable the assignment of natops o to arithexps, we need to expand the set-theoretic definition of these operators. to this end, we first discuss the set-theoretic relationship for numerals that occur in claim and evidence without the need for further computation (section 3.1). we subsequently expand this definition to arithexps where arithmetic functions are applied to evidence, by mapping function executions on relevant evidence to numerical representations (section 3.2). tab-ver produces its quintuples pc i , e i , q i , a i , o i q by first generating a question q i about a claim span c i that contains salient information (section 3.3). this question is answered using the evidence e by producing a rationale, consisting of extracted evidence e i , the execution of appropriate arithmetic functions on e i , and the final answer a i (section 3.4). finally, a proof generation model m p , trained on proofs containing arithexps and associated natops following our set-theoretic definitions, assigns a natop o i to the claim-answer pair. tabver follows qa-natver @xcite for the proof generation process by selecting over multiple proof candidates. ## limitations while the addition of arithmetic reasoning capabilities addresses a vital limitation of natural logic-based systems, tabver is not attempting to modify natural logic's model of compositional entailment itself (i.e., the dfa in figure 2 ). nat-log fails some inferences, such as de morgan's laws for quantifiers, generally having less deductive power than first-order logic @xcite . in contrast, tabver incorporates relevant reasoning processes in the generated proof either explicitly, e.g., arithexps and claim decomposition, or latently, e.g., the assignment of natops between an aligned claim and evidence span. moreover, inference rules that cannot be produced by nat-log affect the granularity of the proof: consider a natural-language instantiation of de morgan's law from @xcite where the claim ''some birds do not fly'' is entailed by the evidence ''not all birds fly''. due to natlog's limitations, the most fine-grained correct proof would be to align (not all, some do not), (birds, birds) and (fly, fly) to produce the proof s " ý ñ s " ý ñ s " ý ñ s ; thus the reasoning between the negations and quantifiers in the aligned pair required to arrive at the set-theoretic relation is omitted from the proof itself. therefore, the proofs of tabver are not necessarily fully comprehensive explanations, as they do not fully explain the production of the proof. moreover, proofs of tabver do not allow assigning natop sequences to individual claim spans, such as cat ñ dog ñ poodle, which can be a limitation for multi-hop claims where multiple pieces of evidence from one or more tables have to be combined for a single span beyond arithmetic functions. furthermore, proofs are produced and executed from left to right. however, natlog does not impose such constraints and is instead non-deterministic by design. this can lead to inconsistencies, as the rearrangement of a natop sequence o can lead to differently informative veracity predictions @xcite . for instance, consider a variation of the running example shown in figure 5 : ''in 2018, ortegal had three municipalities and a population larger than 12,000.''. assuming the same natop relations are assigned, an nei verdict would be produced: n . tabver mitigates this issue via two mechanisms: (i) using claim decomposition to avoid long proofs where such phenomena occur, and (ii) considering multiple proof candidates at different granularity levels, following @xcite (e.g., three municipalities and a population larger than 12,000 could be considered a single span with the ë natop). as shown in figure 5 , by breaking the original claims into atomic units of information, the individual subclaim verdicts (via dfa transitions s " ý ñ s " ý ñ s ë ý ñ r and s " ý ñ s " ý ñ s ď ý ñ s for subclaim 1 and 2, respectively) aggregate into the correct overall verdict. both mechanisms also help in dealing with complex, multi-clause claims, where multiple erroneous and independent facts can lead to nei predictions (double åae)-another weak point of natural logic's nondeterministic composition of natops. ## conclusion this paper presented tabver, a natural logic inference system that adds arithmetic reasoning capabilities for few-shot fact verification on tables. we presented a set-theoretic definition between numerals in a claim and answers calculated on evidence via arithexps. we proposed a method for leveraging llms to generate arithexps via claim-aware question generation and rationale-guided question answering with constrained decoding. tabver outperforms all baseline systems on feverous and in a domain-transfer setting on tabfact, highlighting our model's generalizability. we show that tabver has learned a nuanced understanding of numerals, more sensitive to the context of a claim than other baselines. future work investigates natural logic for scalar implicature on diverse datasets with different requirements for numerical precision. all other cases training & hyperparameters we fine-tune the question generation m qg and question answering m qa model using default hyperparameters. specifically, we use a learning rate of 2 ´4 and train for a total of 10 epochs across all models and experiments. the maximum generation length for m qg is set to 100 tokens for the generation of question, and the constraint answer selection is set to any-length span in c. for m qa the maximum length of e rel is 100 tokens between every generated number. we use adamw @xcite as the optimizer. we use a batch size of 1 during training with gradient accumulation, resulting in an effective batch size of 8. for lora, we use a rank r " 16 and apply it to the query and value vectors of the attention mechanism. for fine-tuning, we exclude tokens of the prompts from the loss computation that are not part of the gold answer, so we are not fine-tuning the instructions, only the answers that follow after the instruction. for our proof generation model m p we use the default hyperparameters of qa-natver @xcite . intended for use in english. all experiments are run on a single quadro 8000 with 48gb memory. to fine-tune m p with a flan-t5-3b backbone we use a single a100 80gb. baselines we use the available implementations for lpa, foot_5 sasp, 16 and binder. 17 identically to tabfact, all three models consider the the first table row of a feverous table as the header row. lpa was trained for 20 epochs since the default number of training epochs (10) was not sufficient to reach convergence. binder uses the default hyperparameters as specified for tabfact, but we use 4 instead of 18 in-context examples as mistralorca, with a full number of in-context examples, produced empty answers very frequently. we hypothesise that mistralorca generates the end of text token too early since the openorca dataset, on which mistralorca7b has been instruction-tuned, consists of gold answers which are in 93% of the cases shorter than 2.5k tokens. we train de-berta, pasta, tapex, and tapas using the huggingface trainer for 10 (100) epochs with full (few-shot) data and a learning rate of 1 ˆ10 ´5. 18 to sanity check our training pipeline, we trained tapas in a full supervision setting on tab-fact's 92,283 training instances, achieving a score of 82.1 accuracy points versus 81.59 points via the official model checkpoint. 19 to fine-tune the llm baselines with lora, we use huggingface's sfttrainer. 20