@inproceedings{pramanik-etal-2026-nsf,
    title = "{NSF}-{C}o{T}: Neuro-Symbolic Formal Verification of Chain-of-Thought Faithfulness in Contextual Question Answering",
    author = "Pramanik, Vishal  and
      Maliha, Maisha  and
      Bastian, Nathaniel D.  and
      Velasquez, Alvaro  and
      Jha, Susmit  and
      Jha, Sumit Kumar",
    editor = "Liakata, Maria  and
      Moreira, Viviane P.  and
      Zhang, Jiajun  and
      Jurgens, David",
    booktitle = "Findings of the {A}ssociation for {C}omputational {L}inguistics: {ACL} 2026",
    month = jul,
    year = "2026",
    address = "San Diego, California, United States",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-acl/2026.findings-acl.516/",
    pages = "10645--10663",
    ISBN = "979-8-89176-395-1",
    abstract = "Chain-of-thought (CoT) prompting makes language models write step-by-step explanations, but these steps may not match what the model actually used to choose its answer. Existing faithfulness checks often only test whether changing the written chain changes the answer, without verifying whether the steps are truly supported by the given evidence, or they require special prompts that do not generalize well. We present \textbf{NSF-CoT}, a neuro-symbolic formal verification method that checks CoT faithfulness step by step for contextual question answering. NSF-CoT (1) converts the provided context facts and each reasoning step into simple logical statements, (2) uses counterfactual attribution to estimate which context facts the model relied on while generating each step, and (3) verifies each step using a hybrid checker that combines an SMT solver with an LLM-based entailment judge. For every step, we score \textit{groundedness} (supported by the full context), \textit{validity} (supported by the facts the model relied on), and \textit{utility} (helps reach the final answer), and combine them into a faithfulness score. Across OpenBookQA, QASC, and HotpotQA, NSF-CoT consistently outperforms causal mediation, perturbation probes, and behavioral monitoring, and it identifies reasoning steps that are not only unfaithful but also harmful to the model{'}s final decision."
}