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

Tahreem Yasir; Sutapa Dey Tithi; Benyamin Tabarsi; Dmitri Droujkov; Sam Gilson Yasitha Rajapaksha; Xiaoyi Tian; Arun Ramesh; DongKuan

cs.AIMar 28, 2026

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

Authors: Tahreem Yasir, Sutapa Dey Tithi, Benyamin Tabarsi, Dmitri Droujkov, Sam Gilson Yasitha Rajapaksha, Xiaoyi Tian, Arun Ramesh, DongKuan,

Organizations: DK · North Carolina State University Raleigh, NC, USA

Abstract

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.

Figures & tables

Figure 1: Multi-agent Tutoring with KG-grounded varying hints (a) Student solution is partially correct (using incorrect rule) Tutor echoes student’s incorrect rule, validates partial correctness (b) Teacher reveals solutions prematurely and students anchors (c) Judge correctly identifies the error in students reasoning (using incorrect rules and statements for derivations)

Dataset	Task	Step	Branching	Student	Difficulty
ProofWriter ( Tafjord et al., 2021 )	Proof Gen.	✗	✗	✗	✗
FOLIO ( Han et al., 2024 )	NLI	✗	✗	✗	✗
ProntoQA ( Saparov and He, 2022 )	CoT	✓	✗	✗	✗
LogicLearner ( Inamdar et al., 2025 )	Proof Gen.	✗	✗	✗	✗
Ours	Next-Step	✓	✓	✓	✓

Table 1: Comparison of existing reasoning benchmarks. Step : step-level evaluation. Branching : annotated solution space at multiple branches. Student : real learner data. Difficulty : instance-level complexity metrics.

Model	Pre (%)	Rule Acc.	Post (%)			$\Delta$	Mean Complexity			UIC over Teacher
	Student	Tutor (%)	Tutor	Teacher	Judge	pp	Tutor	Teacher	Judge	UIC	Gap
GPT-4.1	21.31	58.30	42.82	61.24	75.38	54.07	1.8	2.21	2.7	89	1.63
GPT-o3	24.80	60.10	48.25	61.24	75.58	50.78	2.04	2.26	2.65	84	1.4
Gemini-1.5-pro	52.52	85.8	73.92	78.79	72.95	20.43	3.73	3.17	3.65	23	2.22
Deepseek-R1	56	84.9	76.55	84.30	79.84	23.84	3.49	3.06	3.37	17	3.19
Mistral-Large	23.74	54.80	38.41	41.69	56.37	32.63	1.86	1.85	2.43	103	0.95

Table 2: Pipeline performance across seven LLMs (

N=516

), bold values indicate best Post accuracy per model.

Appendix figures & tables16 assets

Supplementary material from the paper’s appendix.

Appendix

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 3: Propositional inference rules used in this work.

Panel of Figure 2 — Figure 2: Illustrative proof instance showing intermediate derivations and differential hint access for Tutor and Teacher agents.

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.

Difficulty	Proof States	Avg. Statements
2 (Introductory)	48	5.86
3 (Basic)	111	7.73
4 (Intermediate)	148	7.94
5 (Advanced)	85	5.64
6 (Expert)	95	6.41
Total	516	6.72

Appendix

Table 4: Dataset distribution across practice levels (2-6)

Panel of Figure 6 — Figure 6: Base System Prompt for Student

Panel of Figure 7 — Figure 7: Base system prompt for student update

Panel of Figure 8 — Figure 8: Base System prompt for Tutor

Panel of Figure 9 — Figure 9: Base System prompt for Teacher

Panel of Figure 10 — Figure 10: Base System prompt for Judge

Panel of Figure 11 — Figure 11: Sample problem instance and corresponding correct student response

Model	Org.	API	Context	Param
GPT-4.1	OpenAI	OpenAI	1M	-
GPT-o3	OpenAI	OpenAI	1M	-
Gemini 1.5 Pro	Google	Vertex	128K	-
Qwen-3-32B	Alibaba	Groq	32K	32B
LLaMA-3.3-70B	Meta	Groq	128K	70B
Mistral Large	Mistral	Mistral	256K	675B

Appendix

Table 5: Models used in our experiments

Model	Main Effect	Interaction with Pipeline
	Complexity	Tutor $\times$ Comp.	Teacher $\times$ Comp.	Judge $\times$ Comp.
GPT-4.1	$-0.35^{***}$	$-0.02^{ns}$	$+0.08^{ns}$	$+0.22^{***}$
GPT-o3	$-0.42^{***}$	$+0.18^{*}$	$+0.13^{ns}$	$+0.24^{**}$
Gemini-1.5	$-0.55^{***}$	$+0.55^{***}$	$+0.65^{***}$	$+0.61^{***}$
DeepSeek-R1	$-0.36^{***}$	$+0.28^{***}$	$+0.36^{***}$	$+0.56^{***}$
Qwen-3	$-0.53^{***}$	$+0.33^{***}$	$+0.37^{***}$	$+0.39^{***}$

Appendix

Table 6: Effects of proof complexity on correctness and feedback pipelines (Logistic Regression Coefficients, significance: ***

p<.001

, **

p<.01

, *

p<.05

)

Model	Tutor		Teacher		Judge
	Count	Complexity	Count	Complexity	Count	Complexity
GPT	295	3.97	200	4.61	127	4.90
GPT-o3	267	4.14	200	4.64	126	5.23
Gemini	134	4.79	109	5.73	139	4.82
DeepSeek	121	4.74	81	6.12	104	5.08
LLaMA	383	3.44	332	3.60	307	3.60

Appendix

Table 7: Feedback hurts student performance with corresponding mean complexity

Rule	Actual	GPT-4.1	GPT-o3	Gemini	Mistral	Deepseek	Qwen	Llama-3.3
Simp	90	87	86	94	73	96	76	18
Add	61	81	77	78	62	85	92	23
MP	61	70	77	96	45	91	75	55
DS	53	43	45	81	60	77	90	17
MT	40	50	55	82	70	87	77	10
Impl	38	47	52	86	65	81	54	21

Appendix

Table 8: Tutor rule inference accuracy by rule type and model (%), best values are bolded across all rows

Intelligent Tutoring Systems

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

See all 154 papers

Correct Diagnosis, Better Feedback: A Symbolic-Verifier for Faithful LLM Tutoring Feedback in Logic Proofs
Sep 18, 2026Tahreem Yasir, Arnav Mody, Xioayi Tian +1Intelligent Tutoring Systems Language Model Error Detection
North Carolina State University · Purdue University · Kennesaw State University
Confirming Correct, Missing the Rest: LLM Tutoring Agents Struggle Where Feedback Matters Most
May 15, 2026Tahreem Yasir, Wenbo Li, Sam Gilson +3Educational Feedback Generation Intelligent Tutoring Systems
North Carolina State University
Evaluating Research-Level Math Proofs via Strict Step-Level Verification
Jun 9, 2026Yifeng SunLLM Answer Verification Automated Theorem Proving
Independent Researcher

Sep 18, 2026J/K move · Enter open · S save

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

Tahreem Yasir, Arnav Mody, Xioayi Tian, Tiffany Barnes

North Carolina State University · Purdue University · Kennesaw State University

Intelligent Tutoring Systems Language Model Error Detection Faithfulness of Language Model Explanations

Open paper AskPDF 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

Abstract

Intelligent Tutoring Systems

Explore similar work

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

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

Evaluating Research-Level Math Proofs via Strict Step-Level Verification