Intelligent tutoring systems have demonstrated effectiveness in teaching formal propositional logic proofs, but their reliance on template-based explanations limits their ability to provide personalized student feedback. While large language models (LLMs) offer promising capabilities for dynamic feedback generation, they risk producing hallucinations or pedagogically unsound explanations. We evaluated the stepwise accuracy of LLMs in constructing multi-step symbolic logic proofs, comparing six prompting techniques across four state-of-the-art LLMs on 358 propositional logic problems. Results show that DeepSeek-V3 achieved superior performance with 84.4% accuracy on stepwise proof construction and excelled particularly in simpler rules. We further used the best-performing LLM to generate explanatory hints for 1,050 unique student problem-solving states from a logic ITS and evaluated them on 4 criteria with both an LLM grader and human expert ratings on a 20% sample. Our analysis finds that LLM-generated hints were 75% accurate and rated highly by human evaluators on consistency and clarity, but did not perform as well explaining why the hint was provided or its larger context. Our results demonstrate that LLMs may be used to augment tutoring systems with logic tutoring hints, but requires additional modifications to ensure accuracy and pedagogical appropriateness.

本研究解决了智能辅导系统在提供个性化反馈方面的缺口，因其依赖模板化的解释。研究提出了一种评估其在构建多步骤逻辑证明中的准确性的方法，发现DeepSeek-V3在步骤证明构建中表现优越，准确率达84.4%。结果表明，LLM生成的提示在一致性和清晰度上得分较高，但在解释提示原因和背景时表现不佳，显示出LLM在增强逻辑辅导系统方面的应用潜力，同时需增加修改以确保其准确性和教育适宜性。

大型语言模型在智能辅导系统的逻辑问题证明和提示构建中的潜力与局限