Elamur Research⌕
☰
home / papers / 2026 / NSF-CoT: Neuro-Symbolic Formal Verification of Chain-of-Thought Faithfulness in Contextual Question Answering

NSF-CoT: Neuro-Symbolic Formal Verification of Chain-of-Thought Faithfulness in Contextual Question Answering

Paper · 2026 · Vishal Pramanik, Maisha Maliha, Nathaniel D. Bastian et al.

Summary

Chain-of-thought explanations can sound convincing while not reflecting what actually drove a model's answer. Existing faithfulness tests mostly check whether editing the chain changes the output, or they depend on injected hints. They rarely confirm, step by step, that each claim is backed by the supplied evidence. NSF-CoT is a neuro-symbolic auditing pipeline for contextual QA that addresses this. An LLM parser translates context facts and each reasoning step into ground atoms over binary predicates modeled on ConceptNet relations. ContextCite-style fact ablation with a LASSO surrogate then estimates which facts the model leaned on for each step. A hybrid verifier pairs the Z3 SMT solver with an LLM entailment judge to rate every step on three criteria: groundedness (supported by the whole context), validity (supported by the relied-upon facts only), and utility (helps derive the answer). The product of these ratings gives a per-step faithfulness verdict. On OpenBookQA, QASC and HotpotQA, the method outperforms causal mediation, perturbation-probe and behavioral-monitoring baselines. It also produces a traceable record linking claims to supporting facts.

Key points

  • Each step's score is the product of groundedness, validity and utility (F_k = G_k · V_k · U_k), each in [0, 1]. The symbolic Z3 signals are fused with continuous scores from the LLM judge.
  • For attribution, the method samples fact-ablation masks and fits a sparse LASSO model (λ = 0.01). Facts are kept as relied-upon when their weight is at least τ = 0.5 times the mean positive weight.
  • Evaluation covers OpenBookQA, QASC and HotpotQA, using several models including Pythia, LLaMA-3.1-8B and Qwen2.5-72B-Instruct.
  • When flagged steps are used to correct reasoning at test time, the paper reports larger gains for smaller models (Pythia +10–11, LLaMA +9) than for Qwen (+7). This requires no retraining.
  • Stated limitations:
    • The first-order logic representation cannot capture all linguistic phenomena, so the method falls back on the LLM judge.
    • The approach needs token-level likelihoods and many repeated queries, which makes it practical mainly for open-weight models.
  • Code: github.com/VishalPramanik/NSF-CoT.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓University of Colorado BoulderBoulder · United States69 works · 51,069 citations🔬SRI InternationalMenlo Park · United States24 works · 12,175 citations🎓University of FloridaGainesville · United States36 works · 364 citations🎓University of OklahomaNorman · United States3 works · 256 citations

Also on the byline: United States Military Academy.

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksArts and Humanities · 17,450 worksLanguage and Linguistics · 17,296 works

🧭 Topics 2Research subjects and languages the work is about.Reasoning · 1,685 worksQuestion answering · 487 works

Cite

Cite as Vishal Pramanik, Maisha Maliha, Nathaniel D. Bastian, Alvaro Velasquez, Susmit Jha and Sumit Kumar Jha. 2026. NSF-CoT: Neuro-Symbolic Formal Verification of Chain-of-Thought Faithfulness in Contextual Question Answering. Findings of the Association for Computational Linguistics: ACL 2026.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.findings-acl.516

@inproceedings{pramanik2026nsf,
  title = {{NSF-CoT: Neuro-Symbolic Formal Verification of Chain-of-Thought Faithfulness in Contextual Question Answering}},
  author = {Vishal Pramanik, Maisha Maliha, Nathaniel D. Bastian, Alvaro Velasquez, Susmit Jha and Sumit Kumar Jha},
  booktitle = {Findings of the Association for Computational Linguistics: ACL 2026},
  year = {2026},
  doi = {10.18653/v1/2026.findings-acl.516},
  url = {https://doi.org/10.18653/v1/2026.findings-acl.516}
}

References

27 references, 15 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Iván Arcuschin, Jett Janiak, Robert Krzyzanowski, Senthooran Rajamanoharan, Neel Nanda, and Arthur Conmy. 2025. Chain-of-thought reasoning in the wild is not always faithful. arXiv preprint arXiv:2503.08679. find
  2. Bowen Baker, Joost Huizinga, Leo Gao, Zehao Dou, Melody Y Guan, Aleksander Madry, Wojciech Zaremba, Jakub Pachocki, and David Farhi. 2025. Monitoring reasoning models for misbehavior and the risks of promoting obfuscation. arXiv preprint arXiv:2503.11926.
  3. Stella Biderman, Hailey Schoelkopf, Quentin Gregory Anthony, Herbie Bradley, Kyle O’Brien, Eric Hallahan, Mohammad Aflah Khan, Shivanshu Purohit, USVSN Sai Prashanth, Edward Raff, and 1 others. 2023. Pythia: A suite for analyzing large language models across training and scaling. In International Co… find
  4. Yanda Chen, Joe Benton, Ansh Radhakrishnan, Jonathan Uesato, Carson Denison, John Schulman, Arushi Somani, Peter Hase, Misha Wagner, Fabien Roger, and 1 others. 2025. Reasoning models don’t always say what they think. arXiv preprint arXiv:2505.05410.
  5. James Chua and Owain Evans. 2025. Are deepseek r1 and other reasoning models more faithful? arXiv preprint arXiv:2501.08156. — [arXiv:2501.08156](https://arxiv.org/abs/2501.08156) find
  6. Benjamin Cohen-Wang, Harshay Shah, Kristian Georgiev, and Aleksander Madry. 2024. Contextcite: Attributing model generation to context. Advances in Neural Information Processing Systems, 37:95764– 95807. find
  7. Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pages 337–340. Springer. find
  8. Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, and 1 others. 2024. The llama 3 herd of models. arXiv preprint arXiv:2407.21783.
  9. Alon Jacovi and Yoav Goldberg. 2020. Towards faithfully interpretable nlp systems: How should we define and evaluate faithfulness? arXiv preprint arXiv:2004.03685.
  10. Tushar Khot, Peter Clark, Michal Guerquin, Peter Jansen, and Ashish Sabharwal. 2020. Qasc: A dataset for question answering via sentence composition. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 8082–8090. find
  11. Tamera Lanham, Anna Chen, Ansh Radhakrishnan, Benoit Steiner, Carson Denison, Danny Hernandez, Dustin Li, Esin Durmus, Evan Hubinger, Jackson Kernion, and 1 others. 2023. Measuring faithfulness in chain-of-thought reasoning. arXiv preprint arXiv:2307.13702.
  12. Shiyang Li, Jianshu Chen, Yelong Shen, Zhiyu Chen, Xinlu Zhang, Zekun Li, Hong Wang, Jing Qian, Baolin Peng, Yi Mao, and 1 others. 2022. Explanations from large language models make small reasoners better. arXiv preprint arXiv:2210.06726.
  13. Todor Mihaylov, Peter Clark, Tushar Khot, and Ashish Sabharwal. 2018. Can a suit of armor conduct electricity? a new dataset for open book question answering. In Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing, pages 2381–2391, Brussels, Belgium. Association fo… find
  14. Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. 2023. Linc: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Proceedings of the 2023 Conference on Empirical Methods in Natural Lan…
  15. Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. 2023. Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806–3824.
  16. Debjit Paul, Robert West, Antoine Bosselut, and Boi Faltings. 2024. Making reasoning matter: Measuring and improving faithfulness of chain-of-thought reasoning. arXiv preprint arXiv:2402.13950.
  17. Vishal Pramanik, Maisha Maliha, Nathaniel D. Bastian, and Sumit Kumar Jha. 2026a. Hessian-enhanced token attribution (heta): Interpreting autoregressive llms. Preprint, arXiv:2604.13258. — [arXiv:2604.13258](https://arxiv.org/abs/2604.13258) find
  18. Vishal Pramanik, Maisha Maliha, Susmit Jha, and Sumit Kumar Jha. 2026b. Jailbreaking the matrix: Nullspace steering for controlled model subversion. Preprint, arXiv:2604.10326. — [arXiv:2604.10326](https://arxiv.org/abs/2604.10326) find
  19. Robyn Speer, Joshua Chin, and Catherine Havasi. 2017. Conceptnet 5.5: An open multilingual graph of general knowledge. In Proceedings of the AAAI conference on artificial intelligence, volume 31. find
  20. Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. 2021. Proofwriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pages 3621–3634.
  21. Robert Tibshirani. 1996. Regression shrinkage and selection via the lasso. Journal of the Royal Statistical Society: Series B (Methodological), 58(1):267–288. find
  22. Miles Turpin, Julian Michael, Ethan Perez, and Samuel Bowman. 2023. Language models don’t always say what they think: Unfaithful explanations in chain-of-thought prompting. Advances in Neural Information Processing Systems, 36:74952–74965.
  23. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, and 1 others. 2022. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824– 24837.
  24. Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, and Wynne Hsu. 2024. Faithful logical reasoning via symbolic chain-of-thought. arXiv preprint arXiv:2405.18357.
  25. An Yang, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, and 1 others. 2024. Qwen2.5 technical report. arXiv preprint arXiv:2412.15115. find
  26. Zhilin Yang, Peng Qi, Saizheng Zhang, Yoshua Bengio, William Cohen, Ruslan Salakhutdinov, and Christopher D Manning. 2018. Hotpotqa: A dataset for diverse, explainable multi-hop question answering. In Proceedings of the 2018 conference on empirical methods in natural language processing, pages 2369–…
  27. You are a semantic parser that converts natural language sentences into first-order logic predicates. Available predicates (from ConceptNet): • IsA(X, Y): X is a type/instance of Y • PartOf(X, Y): X is a part of Y • AtLocation(X, Y): X is located in/at Y • HasProperty(X, Y): X has property Y • Capab… — SatLM: Satisfiability-Aided Language Models Using Declarative Prompting

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/pramanik-2026-nsf-cot-neuro-symbolic-formal/