# Correct Diagnosis, Better Feedback: A Symbolic-Verifier for Faithful LLM Tutoring Feedback in Logic Proofs

arXiv: https://arxiv.org/abs/2609.22553 · HTML: https://mlsanity.com/paper/2609.22553/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 19 of its 32 references that are in the map.
- First posted on arXiv 18 Sep 2026.

## Builds on (most cited first, 19 of 19)

- [BART: Denoising Sequence-to-Sequence Pre-training for Natural Language Generation, Translation, and Comprehension](https://mlsanity.com/paper/1910.13461/) (2019)
- [Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting](https://mlsanity.com/paper/2305.04388/) (2023)
- [Towards Faithfully Interpretable NLP Systems: How should we define and evaluate faithfulness?](https://mlsanity.com/paper/2004.03685/) (2020)
- [MathDial: A Dialogue Tutoring Dataset with Rich Pedagogical Properties Grounded in Math Reasoning Problems](https://mlsanity.com/paper/2305.14536/) (2023)
- [Faithfulness Tests for Natural Language Explanations](https://mlsanity.com/paper/2305.18029/) (2023)
- [CodeAid: Evaluating a Classroom Deployment of an LLM-based Programming Assistant that Balances Student and Educator Needs](https://mlsanity.com/paper/2401.11314/) (2024)
- [On Measuring Faithfulness or Self-consistency of Natural Language Explanations](https://mlsanity.com/paper/2311.07466/) (2023)
- [Walk the Talk? Measuring the Faithfulness of Large Language Model Explanations](https://mlsanity.com/paper/2504.14150/) (2025)
- [Stepwise Verification and Remediation of Student Reasoning Errors with Large Language Model Tutors](https://mlsanity.com/paper/2407.09136/) (2024)
- [The Probabilities Also Matter: A More Faithful Metric for Faithfulness of Free-Text Explanations in Large Language Models](https://mlsanity.com/paper/2404.03189/) (2024)
- [FaithLM: Towards Faithful Explanations for Large Language Models](https://mlsanity.com/paper/2402.04678/) (2024)
- [MalAlgoQA: Pedagogical Evaluation of Counterfactual Reasoning in Large Language Models and Implications for AI in Education](https://mlsanity.com/paper/2407.00938/) (2024)
- [LLMs cannot spot math errors, even when allowed to peek into the solution](https://mlsanity.com/paper/2509.01395/) (2025)
- [A Comprehensive Review of AI-based Intelligent Tutoring Systems: Applications and Challenges](https://mlsanity.com/paper/2507.18882/) (2025)
- [LeanTutor: Towards a Verified AI Mathematical Proof Tutor](https://mlsanity.com/paper/2506.08321/) (2025)
- [From Untamed Black Box to Interpretable Pedagogical Orchestration: The Ensemble of Specialized LLMs Architecture for Adaptive Tutoring](https://mlsanity.com/paper/2603.23990/) (2026)
- [MathEDU: Feedback Generation on Problem-Solving Processes for Mathematical Learning Support](https://mlsanity.com/paper/2505.18056/) (2025)
- [When Verification Hurts: Asymmetric Effects of Multi-Agent Feedback in Logic Proof Tutoring](https://mlsanity.com/paper/2603.27076/) (2026)
- [Confirming Correct, Missing the Rest: LLM Tutoring Agents Struggle Where Feedback Matters Most](https://mlsanity.com/paper/2605.16207/) (2026)

## Abstract (arXiv)

Effective LLM tutoring depends on correctly identifying the specific error in a student's reasoning before generating feedback. We study this problem in propositional-logic proof tutoring, where student actions can be checked against formal inference rules. We introduce a verifier-grounded architecture that separates diagnosis from language generation. Using 600 balanced student actions, we compare a zero-shot LLM detector, a fine-tuned detector, and a symbolic verifier. Each diagnosis is processed by shared rationale and feedback agents, isolating the effect of the initial diagnosis. The zero-shot detector achieves a macro-F1 of 0.191; fine-tuning raises this to 0.709 but retains systematic errors between structurally related classes. Rationales generally preserve the diagnosis supplied to them, showing that an incorrect diagnosis can be faithfully propagated through the pipeline. Feedback can likewise remain faithful to its rationale, non-revealing, and pedagogically appropriate while addressing the wrong error. Verifier-grounded feedback achieves the highest diagnostic correctness, and expert ratings largely uneven with the automatic feedback evaluations. These findings show that apparent feedback quality can conceal upstream diagnostic errors and that faithfulness must be evaluated separately from correctness. Our code is publicly available