{'fraction_non_alphanumeric': 0.0377859778597786, 'fraction_numerical': 0.012669126691266913, 'mean_word_length': 4.7603797647725665, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 1, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI

Evaluating an explanation's faithfulness is desired for many reasons such as trust, interpretability and diagnosing the sources of model's errors. In this work, which focuses on the NLI task, we introduce the methodology of Faithfulness-through-Counterfactuals, which first generates a counterfactual hypothesis based on the logical predicates expressed in the explanation, and then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic (i.e. if the new formula is \textit{logically satisfiable}). In contrast to existing approaches, this does not require any explanations for training a separate verification model. We first validate the efficacy of automatic counterfactual hypothesis generation, leveraging on the few-shot priming paradigm. Next, we show that our proposed metric distinguishes between human-model agreement and disagreement on new counterfactual input. In addition, we conduct a sensitivity analysis to validate that our metric is sensitive to unfaithful explanations.


Introduction
How should we evaluate an explanation's faithfulness with respect to the task model? According to Jacovi and Goldberg (2020), faithful measures should focus on utility to the user and the idea that an explanation can be sufficiently faithful. 1 The goal of interpretability research is to increase warranted trust and identify the influence of certain variables and allow users to understand how a model will behave on given inputs (Doshi-Velez and Kim, 2017;Lipton, 2018).
In interpretable NLP, there is growing interest in tasks that require world and commonsense "knowl- * Work done while at internship at Meta AI Research, corresponding email ssia1@jhu.edu. 1 Jacovi and Goldberg (2020) originally posit that faithful explanations should "accurately represents the reasoning process behind the model's prediction", however also acknowledge that this is "impossible to satisfy fully". edge" and "reasoning" (Danilevsky et al., 2020). We focus on natural language inference (SNLI; Bowman et al. (2015)), where extractive explanations also known as rationales (DeYoung et al., 2020) are limited as they take a subset of the existing input. Instead, we require free-form natural language explanations to fill in the reasoning or knowledge gap for such tasks (Camburu et al., 2018;Rajani et al., 2019). Our setting is thus characterised by the post-hoc interpretation of black-box classification models via generative explanations. Our work follows the standard "predictand-explain" paradigm (Do et al., 2020). Here an explanation generator generates the explanations conditioned on the predicted task label. 2 Without faithfulness evaluations, the explanation approximately describes the internal process at best, and is generated from superficial similarities between the training data and the class label at worst. 3 2 Do et al. (2020) report little to no difference between jointly predict and explain compared to predict then explain. Note that the emphasis of this work is on evaluating the faithfulness of explanations rather than generating them. 3 Preliminary experiments show that flipping the input class label can change the form of the explanation.
The central contribution of this paper is a methodology grounded in first-order free logic (Lambert, 1967;Bencivenga, 2002), 4 to verify a given explanations' faithfulness. Our proposed approach generates a revised (counterfactual) hypothesis based on the logical propositions expressed in the explanation, and evaluates the logical satisfiability (Boolos et al., 2002) of the new hypothesis. Consider the following example:

Hypothesis:
The dog is barking at the girl. Explanation: The dog is an animal. Counterfactual: The animal is barking at the girl.
If the explanation is logically consistent (faithful) to the model, then the revised counterfactual hypothesis which replaces 'dog' with 'animal' in the original hypothesis, should be satisfiable, since 'dog is an animal'. However, if the explanation is inconsistent with the model, then the resulting hypothesis is unsatisfiable and the explanation is unfaithful. We describe this formally in Section 2.
Compared to previous automatic metrics ( LAS;Hase et al. (2020), LRA; ), our proposed method does not rely on an external verification model and therefore does not require explanation data for training. 5 Our method directly queries the task model in question while crucially avoiding the confound of "label leakage" 6 from the explanation (Hase et al., 2020). We expand on this discussion in Section 4. The contributions of this work are as follows: • We present a methodology for evaluating faithfulness of free form explanations for NLI, grounded in first-order free logic (Subsection 2.1, Subsection 2.2). Our method evaluates the satisfiability of logical relations expressed through a counterfactual hypothesis.
• We introduce an automatic metric (Subsection 2.3) and show its viability with human studies, indicating that a practical solution exists for the proposed (theoretical) method. We leverage few-shot priming for generating 4 This is an extension of predicate logic and should not be confused with either predicate or propositional logic. 5 "Faithfulness" measures which are tied to an external verification model are potentially problematic as given a fixed task model and explanation, one could in theory achieve two different faithfulness scores if the verification model changes. 6 Label leakage occurs because of superficial similarities between the syntatic form of the explanation and the task label. For instance the explanations "A is a B" and "A is not a B" are highly associated with the Entailment and Contradiction label.

Label Propositions Description
= ⇒ x hypothesis neither contradicts or is entailed by premise counterfactual hypothesis, achieving 0.71 − 0.88 METEOR score for human and generated explanations (Subsection 3.2).
• We further evaluate the effectiveness of the fully automated approach for the proposed metric in distinguishing when the model's prediction agrees and disagrees with gold labels on gold counterfactual hypothesis, and achieve 0.58 − 0.75 ρ-statistic on Wilcoxon rank-sum test (Subsection 3.3). A further sensitivity analysis indicates that our method is sensitive to pathological explanations that were generated by removing inputs to the explanation generator, as compared to other existing faithfulness metrics (Subsection 3.4).

Problem Formulation
Natural Language Inference (NLI) is typically cast as a classification task; given a premise u and a hypothesis x, the classifier f predicts the label y, where y ∈ {E, C, N}. Here E indicates entailment, C contradiction, and N neutral, for the relationship between u and x. f can therefore be viewed as a black-box function approximating the solution to a logical satisfiability problem.

Testing Predicate Relations in Explanations.
An explanation z can express one or more logical predicate relations (R), which describes the relationship between two variables A and B that are expressed in x and u respectively (see Table 2 col 4 for examples). This is denoted as R(A, B). A "faithful" explanation with respect to a task model f , is one that expresses predicate relations R(A, B) that are consistent with f 's predictions. The central idea of this work, is to automatically verify this using a counterfactual hypothesis, x cf and its derived associated counterfactual label (the expected satisfiability result). If f (u, x cf ) does not result in the associated counterfactual label, then the explanation is not faithful to f .  B] for y = N). The resulting counterfactual label y cf is logically derived from the propositions Subsection 2.2. Table 3 shows examples of this process.
First-order Free Logic in NLI. In order to deduce the associated label for x cf , we must address the issue of logical deduction for Neutral, which has no corresponding expression in classical predicate logic. We observe that the ternary label in NLI parallels first-order free logic, which has three distinct logical forms, positive, negative and neutral (Lambert, 1967;Nolt, 2021). In contrast to classical logic which requires each singular term to denote a Boolean variable in the domain, free logic may have formula which are truth-valueless (Nolt, 2021), i.e., it is not known whether they are True or False. 7 Table 1 shows the task label, propositions and their meaning in Free Logic.

Satisfiabilty of the Counterfactual
In this section, we derive what the counterfactual hypothesis and associated counterfactual label would be for each original label assuming logical formulas and discrete variables where exact substitution is possible. Subsection 2.4 describes our suggested approach to handle Natural Language where discrete substitution no longer holds. Axiom 1. Substitution for formulas (Fitting, 2012) For any variables A and B and any formula x [A] containing A, if x [B\A] is obtained by replacing any number of free occurrences of A in x with B, . Assumption 1. The hypothesis x and premise u contain n free variables, of which the variables A and B are members in u and x. We denote the membership of A ⊆ x as x [A] . Assumption 2. Given R(A, B), the counterfactual hypothesis can be constructed by applying Axiom 1 replacing A with B, denoted x [B\A] = x cf . 8 7 Truth-valueless formulas are often said to have "truthvalue gaps". Informally, this can be interpreted as there being insufficient information on the truth-values of logical variables to conclude the relationship between u and x (Nolt, 2021). 8 Equivalence formulas may be substituted for one another without changing that formula's truth value (Fitting, 2012).
Assumption 3. The predicate relation expressed in R(A, B) is a sufficient condition, to explain the model's predicted label.
We formally derive the associated counterfactual label y cf (expected satisfiability result) of the new counterfactual hypothesis x cf . Figure 1 and Table 3 show examples for this process. The proofs follow the following high-level structure: 1. Substitution of variables A and B (Axiom 1 and Assumption 1) to construct x cf (Assumption 2).

Examine the predicate relationship R(A, B)
and derive the logical relationship between the x cf and the premise u.
Proposition 1. If the original label is E, then the associated counterfactual label is E.
Proof. By Assumption 1, the logical proposition represented by E is u ⇒ x [A] . Since A ⇔ B, then u ⇒ x [B\A] , by Axiom 1, u ⇒ x cf . Therefore we have the resulting propositional formula and associated counterfactual label (u ⇒ x) ⇔ (u ⇒ x cf ), i.e. (y = E) ⇔ (y cf = E).
Proposition 2. If the original label is C, then the associated counterfactual label is E.
Proof. By Assumption 1, the logical proposition represented by C is (u ⇒ ¬x [A] ). Since ¬(A ⇔ B) is equivalent to (A ⇔ ¬B), then by Axiom 1, u ⇒ ¬(x [¬B\A] ). However it is not possible to test for the "negation of" variables as negation is not seen in training data for NLI. Under Assumption 3, 9 if the explanation ¬(A ⇔ B) sufficiently explains the label, then having x [B\A] negates (or 'flips') the label to Entailment u ⇒ ¬¬(x [B\A] ). Therefore we have the result (u ⇒ ¬x) ⇔ (u ⇒ ¬¬(x cf )), i.e., (y = C) ⇔ (y cf = E).
Original f (u, There are people playing the piano) → Contradict Counterfactual f (u, There are people playing woodwind instruments.) → Entail

Explanation
"The people in the photo are not playing the piano. They are instead playing other woodwind instruments." := ¬(playing the piano ⇔ playing other woodwind instruments) Original f (u, A man in safety equipment is working on a piece of metal.) → Entail Counterfactual f (u, A man in protective gear is working on a piece of metal.) → Entail

Explanation
"Protective gear is a piece of safety equipment" := (safety equipment ⇔ protective gear) Original f (u, Two kids walk home from school. → Neutral Counterfactual f (u, Two kids are walking down a sidewalk.) → Entail Counterfactual f (u, Two kids are going home from school.) → Neutral

Explanation
"Kids walking down a sidewalk are not necessarily going home from school." := ¬(walking down a sidewalk ⇒ going home from school) Proposition 3. If the original label is N, then there are two associated counterfactual labels, E, and N. Two conditions arise because ¬(A ⇒ B) ⇔ A AND ¬B. In the interest of space, we present the proof for Proposition 3 in the Appendix. Table 2 summarises the original propositional formula in the hypothesis x and premise u, the predicate relations R(A, B) and the associated y cf .

Proposed Metric: FTC
We introduce the metric Faithfulness-Through-Counterfactuals (FTC), to capture the difference in model predicted probabilities p(ŷ cf ) from the associated counterfactual label y cf .
Choice of Distance Function (d) We consider three metrics for d, 1[argmax(p(ŷ cf ))! = y cf ] denoted FTC-δ, KL Divergence (FTC-K) and Wasserstein distance (FTC-W) with symmetrical distance of 1 between E and C, and 0 ≥ α ≥ 1 between N and the two other labels.

Generating Counterfactual Hypotheses
In the previous section, we had assumed that the logical variables A and B are substitutable in x directly. Indeed generating a counterfactual hypothesis would be trivial if A and B could be directly extracted from the explanation, and directly substituted in the hypothesis. 10 However, open do-10 Consider the hypothesis: "the boy is outside" and the explanation: "A tire swing is usually installed outside". Naive substitution would result in "the boy is a tire swing".  Figure 2: Two step counterfactual rewriting of the hypothesis, according to the explanation. We implement extract and transform steps using regular expressions (regex) and few-shot priming (FSP) models.
Extract and Transform with Regex We adopt and extend templates identified by Camburu et al. (2020) for explanations, who noted that these templates are a "natural consequence of the task and dataset". Regex methods perform a rule-based span extraction and replacement (we allow for stemmed word replacement). Extraction rules are shown in Appendix (Tables 15 to 17).

Extract and Transform with Few-shot Priming
We compare the brittle regex pipeline with the modern paradigm of in-context few-shot priming. This is an attractive option in our setting where we do not have prior training data for generating counterfactual hypotheses, and the task appears to be related to manipulation of text strings.
We thus consider a two step process of 1) extracting the logical spans, i.e., A and B in Table 2 from the explanation, and 2) modifying the hypothesis given these extracted spans. 12 Given a sequence of priming examples of how to extract spans from the explanation in the prefix, the model should perform the extraction given a test explanation.
Reducing Natural Language Artifacts with x cf Previous attempts to test the explanation directly as input to a trained model, are subject to confounds of "label leakage" because of the close association between label and syntatic form of the explanation (Pruthi et al., 2020). Crucially, our proposed method sidesteps this confound by applying logical satisfiability checks via predicate relations R(A, B). In theory, the construction of x cf should preserve the syntatic structure of the original hypothesis, while only changing the semantics of A and B.

Experiments and Results
We validate our automatic method through three sets of experiments.
i) Evaluating the quality of generated counterfactual hypotheses from a few-shot generator H model (Subsection 3.2).
ii) Evaluating the proposed metric (FTC) on goldmodel agreement of human generated x cf , and comparing this to existing faithfulness metrics in the literature (Subsection 3.3).
iii) Studying the sensitivity of our proposed approach compared to other metrics given pathological explanations (Subsection 3.4).

Quality of Counterfactual Hypotheses
As the feasibility of our automatic approach depends on the quality of counterfactual generation, we evaluatex cf ← H model (x, z) against gold counterfactuals, x cf * ← H human (x, z), where H human refers to the human annotator, H model refers to our automated hypothesis generator, z refers to explanations and x refers to the original hypothesis. We randomly sample 300 examples from the validation set (100 each for E, C, N) and ask annotators to write counterfactual hypothesis for human generated explanations, z * and model generated explanationsẑ. Annotators are asked to revise x such that the logic in z is expressed in the new counterfactual x cf (Appendix: Figure 3). We show annotators the same set of examples that were used to prompt  Table 4: METEOR scores for hypothesis generated by regex, GPT-Neo, or their combination, vs human generated hypothesis.
Bold is applied column-wise. We show the breakdown of revised hypothesis by class label (Contradiction C, Entailment E and Neutral N), and also whether the explanations are human or model generated. Note that there are two counterfactual hypothesis generated for N, N [A] and N [B] which correspond to x cf [A] and x cf [B] as described in Subsection 2.2: Proposition 3.
H model . We obtain three annotations per datapoint for multiple reference sentences. 15 Experiment Conditions As described in Subsection 2.4, we adopt a two-step process of 'extract' and 'transform' for generatingx cf ← H model (x, z).
We compare different combinations of either extracting and transforming with regex or H model . Our main results for the largest and best performing model (GPT-Neo2.7B) is shown in Table 4, and additional results for GPT-Neo1.3B and GPT2-XL in Appendix: Table 11.
Metric The evaluation metric used is METEOR (Banerjee and Lavie, 2005), that was found to correlate with human judgement (Kayser et al., 2021). METEOR computes harmonic mean of unigram precision and recall and accounts for stemming. As the validity of any text generation metric is debatable (Deng et al., 2021), we further quantify the downstream effects of the automated process through Subsection 3.3. Table 4). 1. The combination of using models for both extract and transform steps (last row) performs best in all cases with human explanations z * , and close to best with model explanations,ẑ.

Results (Presented in
2. The performance of most methods are better onẑ than z * which might be explained by the more 'standardised' text format inẑ. Brahman et al. (2020) reported that generator models tend to follow a similar format, supporting this interpretation. The row regex-regex can be seen as a direct comparison of how 'standardised'ẑ is compared to z * as it indicates the performance for a brittle rule-based approach.
3. For ease of rewriting each class (column-wise), C > E > N for z * in most cases, which highlight the relative complexity (N tends to be expressed in a less 'straightforward' manner) of extracting and transforming hypothesis with different types of explanations.

Metric Validation for Predictions on Counterfactual Hypotheses
In this experiment, we compare faithfulness scores with human predictions on counterfactual hypotheses, assuming that humans are consistent with the logically derived answer (we describe the case when they are not in the next section). As described in Section 1, faithfulness metrics should focus on utility of explanations to the user (Jacovi and Goldberg, 2020). One practical utility is that humans should have a better handle of the model's predictions on slightly different input. 16 The domain of new input that we test, is the counterfactual hypotheses x cf ← H human (z * , x) that has been generated by humans using human explanations in Subsection 3.2. Faithfulness metrics should therefore be good at discriminating whether the gold predictions agree with the model predictions.
Since faithfulness metrics are real-valued, and agreement is discrete binary, we are interested in how well they can discriminate between the two groups. We use the Wilcoxon rank-sum test which is a nonparametric test for the null hypothesis that two groups (agreement vs disagreement) are equal. Recall that our FTC metric proposes to use H model to generate a counterfactual hypothesis from the explanations. If H model had produced exactly the same x cf as the human H human , then FTC should be very effective at separating the two outcome groups, and the test statistic ρ ∈ [0, 1] would be very close to 1. However we know this automated process is imperfect (Subsection 3.2), and the implications of a 0.7 or 0.8 METEOR score are unclear. We collect annotations for 100 data instances grouped by each original label-class, and obtain 3 annotations per instance. 17 Annotators are required to rate whether (x cf , u) entails, contradicts, or is neutral (Appendix: Figure 4). We compare with other faithfulness metrics namely Label Adjusted Simulation (LAS; Hase et al. (2020)) and Label Rationale Association (LRA; ), reviewed in Section 4 and Appendix: Table 8. Table 5) 1. FTC variants have the highest ρ ∈ [0, 1] statistic (higher is better and indicates a larger effect size), which indicates that it is the most discriminative metric for whether the human can simulate the model's prediction given new counterfactual inputs. This is expected as the simulation procedure is similar to how FTC is calculated.

Results (Presented in
2. As reported in Subsection 3.2 discrepancies in the automated rewriting process affect the scoring of the metric in ways which are not easily captured by sentence generation metrics (Table 4). The results show that the best-automatic rewriting process of adopting GPT-Neo2.7B achieves 0.58 to 0.75 ρ-statistic across C, E, N, giving us an indication of the downstream impact of 0.74 to 0.82 METEOR score.
3. KL-Divergence (FTC-K) and Wasserstein Distance (FTC-W) perform slightly better than the naive Identity function (FTC-δ). This indicates that a soft computation over probabilities can account for some of the errors in the x cf rewriting process. 4. With the exception of LAS on C and LRA on E, we find that other metrics have poorer ρ across C, E, N. This indicates that the metric is relatively poorer at distinguishing between the two outcome groups.
Examining Inconsistent Explanations In cases where the human NLI label does not correspond to the logically derived NLI class in Table 2, our method suggests that the human provided explanations themselves are not faithful to the human's 'internal NLI model'. Appendix:Subsection 7.6 shows examples of these cases, which we typically find to be due to explanations of low quality, supporting the central thesis of the paper. In the previous results, we filter out data points where majority of the annotators do not predict the logically derived NLI class. We report the non-filtered results in Subsection 7.6) which demonstrate negative results and a failure case when the 'gold' human explanations are themselves problematic. 18

Sensitivity Analysis
As a sanity check, good faithfulness metrics should be sensitive towards unfaithful explanations, i.e. they should perform worse on unfaithful explanations compared to faithful ones. We perform a sensitivity analysis on various faithfulness metrics by examining their raw scores on unfaithful explanations by construction. These are constructed by leaving out all but one type of input to the explanation generator. The 'complete' set of inputs are the entailment label (y), hypothesis (x), and premise (u). Note that the 'complete' set of inputs to the explanation generator does not guarantee faithful explanations, but they are guaranteed to be less pathological than leaving out all but one type of input. We additionally consider BertScore (Zhang et al., 2019) and METEOR (Banerjee and Lavie, 2005) which are text similarity metrics evaluated against the human explanation, and use FTC-K variant which has an upperbound of 1 and a high ρ-statistic in the previous experiment. 19 Results (presented in Table 6) 18 Quantifying the extent and range of annotation errors for explanations is outside of the scope of this work and we refer readers to Valentino et al. (2021) who report that explanations in SNLI are valid logical relations 60% of the time and other times they are either redundant or non-sensical due to annotation errors. 19 As described in Subsection 2.3, FTC-K is 1 − the KL term, which has lower bound 0 and no upper bound. Hence the upper bound on FTC-K is 1.  3. LAS scores are in the 'wrong' direction, namely that explanations generated with all of the relevant inputs perform worse than just having the label.

Related Work
We outline existing methods which evaluate freetext generated Natural Language explanations, their assumptions of faithfulness, and describe how they operationalise these assumptions. We focus on LAS and LRA, which are used in our experiments, and provided more discussion of related work in Appendix:Subsection 7.4.

Label Rationale Association
According to , "at a minimum, rationales must be implicitly or explicitly tied to the model's prediction.". Their method tests whether label and explanations are similarly robust to noise in the input. Although designed to be highly generalisable to generative framework of explanations, this assumption may be overly general for more rigorous notions of faithfulness. Consider the scenario where merely changing the label to the generator results in "sufficiently different" explanations being generated (Kumar and Talukdar, 2020), whether or not the original explanation was actually faithful, LRA will assign this a high score.

Natural Logic vs Free Logic
Previous work on "Natural Logic" (MacCartney and Manning, 2007) relies on natural language features to guide inferences. For instance, changing specific terms to more general ones preserves entailment. This sidesteps the difficulties of translating sentences into First-order-Logic. Natural logic systems (Angeli and Manning, 2014) have been used in explainable fact verification (Krishna et al., 2021) which constructs "explanations" by presenting logical steps for inference. However these approaches still require a knowledge base to train or mine truth values, e.g, "in Paris" ⊆ "in France". In contrast, our method does not require additional training and is a procedurally lightweight method relying on off-the-shelf pretrained models.

Conclusion
Measuring faithfulness of free-text explanations with respect to a task model is a challenging problem due to confounds introduced by testing explanations directly. In this work, we propose an approach to evaluating explanations for NLI tasks which uses the predicate logic expressed in explanations to construct counterfactual hypotheses, and tests the satisfiability of the resulting hypothesis. Our experiments on validating counterfactual hypothesis generation and the fully automated approach distinguishing when humans agree and disagree with the model's prediction on counterfactual hypotheses show that a proposed automatic pipeline is a viable approximation to the theoretical method. Further, we show that our metric is sensitive to pathologically unfaithful explanations.
6 Impact Statement

Potential Limitations
We document and discuss some potential limitations of our proposed approach. 1. The suggested implementation (Subsection 2.4) relies on pre-trained models which are opensource, 20 but requires GPU memory of >10Gb memory to host the 2.7B parameter model and <10Gb to host the 1.3B parameter model.
2. While it is reasonable to expect that applying the same approach using larger GPT models might generate better counterfactual hypotheses, we have opted to use models that can still be launched on a single GPU machine, and does not assume access to industry level 175B models.
3. Our metric is not directly differentiable as it involves discrete operations to generate the counterfactual hypotheses.
4. Since the method of generating counterfactual hypotheses is tied to the set of explanations, the generated counterfactual hypotheses are not meant to be an extensive set of counterfactuals that might be used to test a model, which has been explored in other work such as Ross et al. (2021). This is not strictly a limitation, but a note that the method focus on evaluating generated explanations, rather than generating counterfactuals extensively.

5.
While most classification problems can be reformulated into ternary logic of E, C, N, it is more challenging to extend the notion of logical satisfiability for tasks that require open-ended text generation, and so the current work is limited to NLI task explanations.

Potential Risks
The proposed work investigates an evaluation methodology for faithfulness of explanations. This work focuses on explanations for the NLI task, which has no influence on the actual classification algorithm of the NLI model. Extensions of the method which generate counterfactual hypothesis using other pretrained models may be subject to hallucinations in those models (which we did not currently encounter with the present models).

References
Gabor Angeli and Christopher D Manning. 2014. Naturalli: Natural logic inference for common sense reasoning. In Proceedings of the 2014 conference on empirical methods in natural language processing (EMNLP), pages 534-545.  If the original label is N, then there are two associated counterfactual labels, E, and N.
For N, as u (?)

= = ⇒ x is truth-valueless under Open
Universe Semantics (Russell, 2015)), the formula is either truth-valueless of every variables in x and u, or truth-valueless of some and false of others (Nolt, 2021). We start by considering the predicate relation R(A, B) = ¬(A ⇒ B) which we rewrite as A ∧ ¬B, so that the two variables are separately testable (due to ∧ relation). For A, applying Assumption 1, we verify the satisfiability of u ⇒ x cf [A] where the counterfactual hypothesis is x cf [A] = x [A\B] . We test the formula which excludes B but has A. The associated counterfactual result of y cf [A] = E. Next we consider ¬B, with the counterfactual hypothesis x cf [¬B] = x [¬B\A] . Since the original propositional formula was truth-valueless, the same conditions apply for u [¬B] which is still truth-valueless. The negation of a truth-valueless formula is still truth-valueless (Nolt, 2021)) hence u has the counterfactual label y cf = N.

Experiment Details
Dataset

Our use of this dataset is compatible with original access conditions and in research contexts.
Package Details For all models, we used Huggingface's Transformers, v 4.12.2. For Meteor Score calculation, we used NLTK v 3.6.1 which lower cases tokens. For BertScore calculation, we used roberta-large and the metric implementation from Huggingface's datasets v 1.15.1. For training and validation loop, we used PyTorch Lightning, v 1.5.2.
Training Details Models are trained with Adam Optimizer (Kingma and Ba, 2015) with learning rate 10 −5 and batch size 64. Models were trained using with Early stopping was used with patience=5 and threshold=0.0001. We did not perform any hyperparameter search for this work, and used default values for training the models from the packages.
Computational Budget The largest model used was GPT-Neo 2.7B (2.7 Billion Parameters). The GPU hardware for the experiments used was NVIDIA's Quadro RTX 6000. The multimodal CLIP model takes about a day to fine-tune. To generate 14000 new counterfactual hypothesis using pretrained GPT-Neo 2.7B takes about 1-2 hours.
Prompt Selection Details We report results from a single run of random prompt selection, as hand-labelling multiple random prompt sets is manually intensive. A preliminary experiment comparing randomly sampled prompt sets, versus obtaining prompts using datapoints that are closest to the cluster centers from k-means clustering (where k=20) of the sentence unigram and bigram vectors, yielded nearly identical scores for Table 3. With a huge source dataset to sample from, we suspect that both types of prompt set selection might be close to random.

Related Work
Leakage Adjusted Simulatability For task inputs X = {x i }, model outputsŶ = {ŷ i }, and model explanations =Ê = {ê i }, Leakage Adjusted Simulatability (LAS) metric is computed as: We adopt the same set of final hyperparameters for dropout, 0.2 explanations only, 0.4 hypothesis and premise only, and 0.4 hypothesis, premise and explanations.
Label Rationale Association We adopt the "Robustness Equivalence measure" which tests whether both label and explanations are similarly or disimilarly robust to noise in the input. Following , we measure changes in label prediction as the number of predicted dev set labels that flip, i.e., change from their original prediction to something else, and measure changes in rationale quality using simulatability. Their approach aims to measure association between input perturbation and output explanation. They first add zero-mean Gaussian noise N (0, σ 2 ) to each input embedding at inference time, and measure the changes in label prediction by counting the number of predicted labels in the test set which flip. They then use the corresponding generated explanations, and get the task prediction change of a separate model that has been pretrained with explanations. The LRA is computed as: (2) Teacher-Student Paradigm Pruthi et al. (2020) introduce a student-teacher paradigm, where they target a notion of faithfulness being tied to the usefulness of explanations. They measure the extent to which explanations allow student models to simulate the teacher model on unseen examples for which explanations are unavailable. Student models incorporate explanations in training (but not prediction) procedures. The proposed framework for evaluating explanation quality suggests that explanations are effective if they help students learn about the teacher.
Erasure The vast majority of prior work that proposes models and evaluations of explanatory methods for faithfulness focus on removing tokens from the input text (DeYoung et al., 2020). This method directly intervenes in the input hypothesis by finding 'important' spans and is not applicable to free-text explanations. Our method has a similar spirit of doing direct interventions. However instead of removing tokens, we generate a counterfactual hypothesis which is grammatically close to the original hypothesis, but with propositions from the explanation.  Compared to the other models, our proposed method 'Faithfulness-through-Counterfactuals' directly tests the task model without relying on third party Human or model verification. The reliance on third party is via counterfactual hypothesis generator, which we validate the efficacy in Subsection 3.2. Additionally, our method relies a one-off manual prompts generation which is cheaper than gathering explanation training data or relying on human annotators.

Annotation Details
We recruited annotators from the pool of Amazon Mechanical Turk workers who are located in the United States. In the counterfactual hypotheses rewriting task (Subsection 3.2), we paid between $0.15 (for E and C) and $0.20 (for N) per single rewrite, estimating that a sufficiently experienced worker can perform the task in under 45 seconds, thus yield a minimum of $12 hourly rate. (We do not separately ask humans to extract logical spans.) In the NLI label collection task (Subsection 3.3), we paid $0.10 per single NLI label and estimated that each task should take a sufficiently experienced worker at most 30 seconds, thus yielding a minimum of $12 hourly rate.

Low Quality Explanations
We find that inconsistency between human NLI labels and the logically derived labels can be largely attributed to low quality human explanations from the dataset. The logically derived label is obtained from Table 2. Human NLI labels do not correspond to the derived counterfactual around 15 to 45% of the time, with the following breakdown.
Subsection 3.3 presents results for filtering out data points where the majority label from the annotators is consistent with the logically derived NLI class. We additionally report non-filtered results in Table 10 which reflect the failure case when the human (gold) generated explanation itself is not reliable.

Hypothesis
Man riding a motorcycle. Explanation The man is on a lake with a monoboard.  Table 11: METEOR scores for Hypothesis Revision by either using regex, GPT-Neo, or a combination of both. Bold is applied column-wise. We show the breakdown of revised hypothesis by class label (Contradiction C, Entailment E and Neutral N), and also whether the explanations are human or model generated. Note that there are two counterfactual hypothesis generated for N (N [A\B] and N [B\A] ) as described in Subsection 2.2: Proposition 3. As expected, the performance of Neo2.7B > Neo1.3B > regex for both z * andẑ when the same 'model' is used for both extract and transform. Considering a combination of approaches (row-wise), forẑ, the best combination of (regex + Neo1.3B) performs close to the best combination of (regex + Neo2.7B), which suggests that a smaller H model may be sufficiently competitive.

Sensitivity Analysis
FTC-W FTC-δ FTC-K x u y gpt-gpt gpt-regex regex-gpt regex-regex gpt-gpt gpt-regex regex-gpt regex-regex gpt-gpt gpt-regex regex-gpt regex-regex  Table 12: Raw scores for FTC metric variants by perturbing inputs to the explanation generator (sensitivity analysis). x, u, and y refers to hypothesis, premise, and label respectively. We vary different parts of the extracttransform pipeline (either with regex-regex, regex-gpt, gpt-regex, gpt-gpt), using GPT-Neo2.7B. We find that all columns have the first row as the largest number as expected, but FTC-K produces larger difference between the first row and other rows.

Prompt templates
Explanation A B

Contradiction
Jail cells aren't pastel-colored or a classroom. jail cells pastel-colored or a classroom The two men cannot both be at a construction site and also never have been at a construction site. at a construction site never have been at a construction site.
One cannot be happy and angry at the same time. happy angry a dog is not a cat. dog cat Star is not balloon star balloon

Entailment
The guy on the phone is sitting at a desk. guy on the phone sitting at a desk People is a generalization of many people. people many people Jockeys are people, so jockeys riding horses are people riding horses. jockeys people If people are sitting on blankets and the blankets are in the park, then the people are sitting at the park as well, because they cannot be in a separate location from the blankets they are sitting upon.
people sitting on blankets people sitting on blankets in the park If your pausing for a photo then they are having their photo taken pausing for a photo having photo taken

Neutral
Looking on does not mean waiting for their turn and doesn't mean they are at a competition.
looking waiting for their turn and they are at a competition Just because a track athlete is carrying a large pole it does not mean they gets ready for their turn at the pole vault.
A track athlete is carrying a large pole A track athlete gets ready for their turn at the pole vault. There is no evidence that the women talking to the man outside the building are sad The women talking to the man outside the building the women are sad Just because he has a mop, does not mean he has a broom. he has a map he has a broom No way to know that is alone because he lost his friends in a war.
he is alone he lost his friends in a war

Contradiction / Entailment
They are waiting for parole in their jail cells. They are waiting for parole in their pastel-colored classroom jail cells pastel-colored classroom The two men have never been to a construction site.
The two men are at a construction site. at a construction site never been to a construction site an angry man grills vegetables on a barbecue.
A happy man grills vegetables on a barbecue. angry happy There is a cat running There is a dog running cat dog The young man is holding the balloon inside the large stone building.
The young man is holding the star inside the large stone building.
balloon star

Neutral
The skateboarders are waiting for their turn at a competition. There is an old man sitting alone because he lost his friends in a war.
A: There is an old man sitting alone; B: There is an old man who lost his friends in a war. he is alone he lost his friends in a war    Table 17: Regex for extracting logical variables "A" and "B" from Neutral (N).