검증이 오히려 악영향을 미치는 경우: 논리 증명 튜터링에서의 다중 에이전트 피드백의 비대칭적 효과

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

대규모 언어 모델(LLM)은 자동 튜터링에 점점 더 많이 사용되고 있지만, 구조화된 기호 영역에서의 신뢰성은 여전히 불확실합니다. 본 연구에서는 명제 논리 증명에 대한 단계별 피드백을 조사합니다. 단계별 피드백은 학습자의 현재 증명 상태와 정확하게 일치하는 정교한 기호 추론을 요구합니다. 우리는 지식 그래프 기반의 벤치마크를 구축했습니다. 이 벤치마크는 516개의 고유한 증명 상태를 포함하며, 각 상태는 단계별 주석과 난이도 지표를 가지고 있습니다. 기존의 튜터링 평가가 모델 자체 평가 또는 이진 정확도에 의존하는 것과는 달리, 본 연구의 프레임워크는 검증된 해결 경로에 대한 피드백 품질의 세분화된 분석을 가능하게 합니다. 우리는 세 가지 역할별 특화 파이프라인을 평가했습니다. 이 파이프라인은 해결책 접근 권한이 서로 다릅니다. 즉, 튜터(부분적인 해결책 접근), 교사(전체 유도 과정 접근), 그리고 심판(튜터 피드백 검증)입니다. 연구 결과는 놀라운 비대칭성을 보여줍니다. 즉, 상위 피드백의 오류율이 70% 미만인 경우, 검증은 결과 향상에 기여하지만, 피드백의 신뢰도가 85%를 초과하는 경우, 과도한 규정으로 인해 성능이 4~6% 포인트 감소합니다. 중요한 점은, 모든 모델과 파이프라인이 복잡도 4~5를 초과하는 증명 상태에서 안정적으로 성공하지 못한다는 공통적인 복잡도 한계가 존재한다는 것입니다. 이러한 결과는 검증기 추가 또는 풍부한 컨텍스트가 항상 튜터링을 향상시킨다는 가정에 도전하며, 추정된 복잡도와 상위 피드백 신뢰도를 기반으로 문제를 분류하는 적응형, 난이도 인지 아키텍처의 필요성을 강조합니다.

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.