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

Tahreem Yasir; Arnav Mody; Xioayi Tian; Tiffany Barnes

cs.CLSep 18, 2026

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

Authors: Tahreem Yasir, Arnav Mody, Xioayi Tian, Tiffany Barnes

Organizations: North Carolina State University · Purdue University · Kennesaw State University

Abstract

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

Figures & tables

Figure 1: An illustrative example of one student action processed by all three pipelines. Both LLM detectors misdiagnose the action: B0 predicts wrong_arity , B1 predicts correct . The symbolic verifier correctly identifies it as antecedent_mismatch . Each row shows the resulting rationale and the feedback message shown to the student, tracing how an incorrect diagnosis propagates into misleading feedback.

Proof state	Rule	Label
1. $(\neg O\lor L)\to(M\land\neg N)$ 2. $\mathbf{\neg O}$ 3. $K\to N$	Add	correct
1. $(\neg O\lor L)\to(M\land\neg N)$ 2. $\neg O$ 3. $\mathbf{K\to N}$	MP	wrong_arity
1. $\mathbf{\neg(G\land A)}$ 2. $B\to A$	Equiv	antecedent_ mismatch
1. $K\to M$ 2. $Z\to R$ 3. $\mathbf{\neg(K\to R)}$	DeM	wrong_rule

Table 1: One student action per diagnosis class; the selected statement is bold.

Dimension	2	1	0
Quality judge (feedback vs. corresponding rationale)
Rationale faithfulness	Preserves the rationale’s diagnosis	Partial or vague	Contradicts or changes it
Non-revelation	No corrective rule, formula, or next step	Reveals a substantial clue	Explicitly reveals one
Pedagogical appropriateness	Concrete, relevant, appropriate depth	Generic or mismatched depth	Irrelevant or misleading
Diagnostic judge (feedback vs. reference diagnosis)
Diagnostic correctness	Communicates the reference class’s defining property	Compatible but underspecified	Contradicts it or targets another class

Table 2: Scoring rubric for the two feedback judges. Reference diagnosis denotes the verifier’s

c_{i}^{*}

	Zero-shot (B0)			SFT (B1)
Macro-F1	0.191			0.709
Class	P	R	F1	P	R	F1
correct	0.12	0.01	0.01	0.75	0.73	0.74
wrong_arity	0.29	0.19	0.23	0.98	0.82	0.89
antecedent_mismatch	0.25	0.43	0.31	0.81	0.37	0.51
wrong_rule	0.17	0.27	0.21	0.74	0.65	0.69

Table 3: Per-class precision, recall, and F1 for B0 and B1 on the 600-instance experiment set (150 per class).

System	$F_{\mathrm{sys}}$	$F_{\mathrm{gt}}$	$\overline{s}_{\mathrm{sys}}$	$\overline{s}_{\mathrm{gt}}$
Verifier (proposed)	94.3%	94.3%	0.977	0.977
B1 (SFT)	75.8%	60.3%	0.660	0.566
B0 (zero-shot)	73.5%	25.3%	0.573	0.256

Table 4: Rationale faithfulness by pipeline. For the verifier, label accuracy is 100%, hence

F_{\mathrm{sys}}=F_{\mathrm{gt}}

; the drop to 94.3% reflects label to rationale rendering loss.

Figure 2: Ground-truth confusion matrices for the rationale evaluation. Rows are verifier ground-truth classes, columns are NLI-assigned rationale classes. WA = wrong_arity , AM = antecedent_mismatch , WR = wrong_rule , C = correct .

System	Label	$N$	Faith.	Pedag.	Diag.
Verifier	–	600	1.710	1.292	1.775
B1	Overall	600	1.625	1.263	1.513
B1	Matched	386	1.672	1.332	1.734
B1	Mismatched	214	1.472	1.042	0.803
B0	Overall	600	1.617	1.040	1.060
B0	Matched	135	1.672	1.061	1.794

Table 5: Feedback faithfulness, pedagogical appropriateness, and diagnostic correctness on a 0–2 scale. Non-revelation is omitted because all rows score 2.000.

Appendix figures & tables10 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 3: Initial proof state and goal specification. The student is presented with the premises (top left) and the target conclusion ( $J\lor K$ ) at the bottom. Available inference rules are displayed on the middle. At this stage, no intermediate steps have been derived, and the student must choose a productive forward step toward the goal.

Figure 4: Rule application with guided simplification. After deriving an intermediate conjunction via Modus Ponens, the student applies the Simplification rule. The interface prompts the learner to select the appropriate resulting literal ( $G$ or $\lnot H$ ), illustrating fine-grained, step-level decision making supported by rule constraints.

Figure 5: Successful proof completion. The student derives $J$ via Disjunctive Syllogism and applies the Addition rule to reach the target conclusion $J\lor K$ . The system confirms completion, reinforcing correct rule sequencing and alignment with the goal state.

Abbrev.	Rule Name	Form
MP	Modus Ponens	$P\rightarrow Q,\;P\Rightarrow Q$
MT	Modus Tollens	$P\rightarrow Q,\;\neg Q\Rightarrow\neg P$
Conj	Conjunction	$P,\;Q\Rightarrow P\land Q$
Simp	Simplification	$P\land Q\Rightarrow P$ (or $Q$ )
Add	Addition	$P\Rightarrow P\lor Q$
DS	Disjunctive Syllogism	$P\lor Q,\;\neg P\Rightarrow Q$

Appendix

Table 6: Propositional inference rules used in this work.

Panel of Figure 6 — Figure 6: Training and evaluation loss curves for llama8b_error_classifier_v5 over 6 epochs.

System	Dimension	$p$	$r$
B1	Faithfulness	$1.05\times 10^{-5}$	0.204
B1	Pedagogy	$3.36\times 10^{-11}$	0.288
B1	Diagnostic Correctness	$8.01\times 10^{-45}$	0.676
B0	Faithfulness	$0.178$	0.065
B0	Pedagogy	$0.201$	0.027
B0	Diagnostic Correctness	$9.78\times 10^{-36}$	0.668

Appendix

Table 7: Mann-Whitney

U

test comparing matched vs. mismatched instances within B1 and B0, by dimension.

Class	Hypotheses
wrong_arity	(1) The student selected the wrong number of formulas for the clicked rule. (2) The rule needs a different number of prior lines than were selected. (3) Too few or too many formulas were selected for this rule. (4) The number of selected formulas does not match what the rule requires. (5) The student selected an incorrect count of formulas.
antecedent_mismatch	(1) The student’s selected formulas do not satisfy the structural pattern of the clicked rule. (2) The selected formulas do not satisfy the structural pattern of the clicked rule. (3) The formulas do not match the antecedent requirements of the clicked rule. (4) The arity is correct but the formulas do not structurally match the clicked rule. (5) The clicked rule cannot be applied because the formula types do not match its pattern.
wrong_rule	(1) The student chose an inference rule that does not apply to the selected formulas. (2) The clicked rule cannot produce a valid derivation from these formulas. (3) A different rule should have been chosen for these selected formulas. (4) The student applied the wrong inference rule to otherwise valid formula selections. (5) The rule clicked does not match the logical form of the selected formulas.
correct	(1) The student’s attempted proof step is correct. (2) The selected formulas validly support applying the clicked rule. (3) The clicked rule is correctly applied to the selected formulas. (4) The student’s selected formulas satisfy the requirements of the clicked rule. (5) The attempted inference is valid and contains no structural error.

Appendix

Table 8: Hypotheses used for the NLI-based assignment of generated rationales to the four diagnostic classes. Each generated rationale is used as the NLI premise, and each sentence listed above is evaluated as a hypothesis.

Figure 7: Interface used for error-taxonomy annotation.

Figure 8: Interface used for rationale-faithfulness annotation.

Figure 9: Interface used for feedback annotation.

Intelligent Tutoring Systems

Intelligent tutoring systems model learner knowledge and adapt instruction, practice, hints, and feedback to support learning.

See all 154 papers

Mar 28, 2026

When Verification Hurts: Asymmetric Effects of Multi-Agent Feedback in Logic Proof Tutoring

Large language models (LLMs) are increasingly used for automated tutoring, but their reliability in structured symbolic domains remains unclear. We study step-level feedback for propositional logic proofs, which require precise symbolic reasoning aligned with a learner's current proof state. We introduce a knowledge-graph-grounded benchmark of 516 unique proof states with step-level annotations and difficulty metrics. Unlike prior tutoring evaluations that rely on model self-assessment or binary correctness, our framework enables fine-grained analysis of feedback quality against verified solution paths. We evaluate three role-specialized pipelines with varying solution access: Tutor (partial solution access), Teacher (full derivation access), and Judge (verification of Tutor feedback). Our results reveal a striking asymmetry: verification improves outcomes when upstream feedback is error-prone (<70% accuracy), but degrades performance by 4-6 percentage points through over-specification when feedback is already reliable (>85%). Critically, we identify a shared complexity ceiling; no model or pipeline reliably succeeds on proof states exceeding complexity 4-5. These findings challenge the assumption that adding verifiers or richer context universally improves tutoring, motivating adaptive, difficulty-aware architectures that route problems by estimated complexity and upstream reliability.

Tahreem Yasir, Sutapa Dey Tithi, Benyamin Tabarsi +7

DK · North Carolina State University Raleigh, NC, USA

Intelligent Tutoring Systems LLM Evaluation LLM Reliability Multi-Agent LLM Systems Logical Reasoning

Ask PDF

May 15, 2026

Confirming Correct, Missing the Rest: LLM Tutoring Agents Struggle Where Feedback Matters Most

Effective tutoring requires distinguishing optimal, valid but suboptimal, and incorrect student solutions, a distinction central to intelligent tutoring systems (ITS) but untested for LLM-based tutors. As LLMs are increasingly explored as conversational complements to ITS, evaluating their diagnostic precision is essential. We present a benchmark of seven LLM feedback agents in propositional logic using knowledge-graph-derived ground truth across 10,836 solution--feedback pairs and three feedback conditions. Models achieved near-ceiling performance on optimal steps but systematically over-rejected valid but suboptimal reasoning and over-validated incorrect solutions, precisely where adaptive tutoring matters most. These failures persisted across models regardless of solution context, suggesting architectural rather than informational limits. Moreover, accurate diagnosis did not reliably produce pedagogically actionable feedback, revealing a gap between diagnostic judgment and instructional effectiveness. Our findings suggest that LLMs are better suited for hybrid architectures where KG-grounded models handle diagnosis while LLMs support open-ended scaffolding and dialogue.

Tahreem Yasir, Wenbo Li, Sam Gilson +3

North Carolina State University

Educational Feedback Generation Intelligent Tutoring Systems Educational Assessment LLM Agent Evaluation Generative AI in Education

Ask PDF

Aug 9, 2026

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification

Large language models (LLMs) increasingly serve as data-driven reasoners, yet their chains-of-thought (CoT) can be unfaithful even when final answers are correct. Most existing

verification'' signals are not diagnostic: answer matching observes only the outcome, LLM-as-judge provides subjective and non-verifiable critiques, and scalar rewards (e.g., PRMs/RMs) offer little insight into where a multi-step derivation fails.We propose **SymDiag**, a neuro-symbolic framework that **reframes reasoning verification as structured failure diagnosis**. SymDiag translates natural-language CoT into symbolic constraints and performs step-level satisfiability/entailment checks to (i) localize failing steps and (ii) produce verifiable diagnostic evidence, including counterexamples, inconsistency witnesses, and missing-premise indicators. A central challenge is that apparent

logic violations'' can be caused either by genuine reasoning defects or by neural-to-symbolic translation noise. SymDiag therefore incorporates a Self-Auditor that disentangles TranslationError from ReasoningError via dual symbolic encodings consistency checks, enabling robust diagnosis under partial observability. Across diverse mathematical, logical, scientific, and general reasoning benchmarks, SymDiag improves detection of unfaithful reasoning and provides substantially more effective feedback for multi-round reasoning repair than outcome-only verification and LLM-based judging, offering a principled foundation for trustworthy and scalable reasoning diagnosis.

Wenyao Cui, Huaping Zhang, Yongyi Huang +6

Beijing Institute of Technology Beijing, China · Zhongguancun Academy Beijing, China · Xinjiang Future Enterprise Incubator Co., Ltd. Xinjiang, China +1

CoT Faithfulness LLM Answer Verification Symbolic Reasoning Neuro-Symbolic Reasoning

Ask PDF

Abstract

Intelligent Tutoring Systems

Explore similar work

When Verification Hurts: Asymmetric Effects of Multi-Agent Feedback in Logic Proof Tutoring

Confirming Correct, Missing the Rest: LLM Tutoring Agents Struggle Where Feedback Matters Most

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification