The promise and limits of LLMs in constructing proofs and hints for logic problems in intelligent tutoring systems

📄 arXiv: 2505.04736v2 📥 PDF

作者: Sutapa Dey Tithi, Arun Kumar Ramesh, Clara DiMarco, Xiaoyi Tian, Nazia Alam, Kimia Fazeli, Tiffany Barnes

分类: cs.AI

发布日期: 2025-05-07 (更新: 2025-11-21)

💡 一句话要点

利用LLM构建逻辑证明与提示，提升智能辅导系统性能，但需关注准确性。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 智能辅导系统 逻辑证明 提示生成 命题逻辑

📋 核心要点

  1. 现有智能辅导系统依赖模板化解释，缺乏个性化反馈，限制了教学效果。
  2. 利用LLM生成动态提示，旨在提供更个性化的逻辑证明辅导，提升教学质量。
  3. 实验表明DeepSeek-V3在逻辑证明构建中表现出色，准确率达86.7%，但在解释提示原因方面仍有不足。

📝 摘要（中文）

智能辅导系统在教授形式命题逻辑证明方面表现出有效性，但其对基于模板的解释的依赖限制了提供个性化学生反馈的能力。大型语言模型（LLM）为动态反馈生成提供了有希望的能力，但存在产生幻觉或教学上不健全的解释的风险。我们评估了LLM在构建多步符号逻辑证明中的逐步准确性，比较了四种最先进的LLM在358个命题逻辑问题上的六种提示技术。结果表明，DeepSeek-V3在逐步证明构建中表现出卓越的性能，准确率高达86.7%，尤其擅长较简单的规则。我们进一步使用性能最佳的LLM为来自逻辑ITS的1,050个独特的学生问题解决状态生成了解释性提示，并使用LLM评分器和人工专家评分（20%样本）在4个标准上对其进行评估。我们的分析发现，LLM生成的提示的准确率为75%，并且在一致性和清晰度方面受到人工评估者的高度评价，但在解释为什么提供提示或其更大的背景方面表现不佳。我们的结果表明，LLM可用于通过逻辑辅导提示来增强辅导系统，但需要进行额外的修改以确保准确性和教学上的适当性。

🔬 方法详解

问题定义：论文旨在解决智能辅导系统中，现有方法依赖于预定义模板，无法为学生提供个性化逻辑证明指导的问题。现有方法的痛点在于缺乏灵活性和适应性，难以根据学生的具体错误和理解程度提供针对性的帮助。

核心思路：论文的核心思路是利用大型语言模型（LLM）的强大生成能力，动态生成逻辑证明的步骤和提示。通过不同的prompting策略，引导LLM生成更准确、更具解释性的内容，从而为学生提供更有效的学习支持。

技术框架：整体框架包含两个主要阶段：1) 使用不同的prompting技术，利用LLM生成逻辑证明的步骤；2) 使用最佳LLM为学生在智能辅导系统中遇到的问题生成提示，并使用LLM评分器和人工专家对提示的质量进行评估。主要模块包括：LLM选择（DeepSeek-V3等），Prompting策略设计，逻辑问题集，LLM评分器，人工评估。

关键创新：最重要的技术创新点在于探索了LLM在逻辑证明生成和提示方面的潜力，并系统地评估了不同prompting策略对LLM性能的影响。与传统方法相比，该方法能够动态生成内容，具有更高的灵活性和适应性。

关键设计：论文比较了六种prompting技术，并选择了DeepSeek-V3作为最佳LLM。针对提示生成，论文设计了四个评估标准：准确性、一致性、清晰度和解释性。人工评估选取了20%的样本，并与LLM评分器的结果进行对比分析。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

实验结果表明，DeepSeek-V3在逐步证明构建中表现出卓越的性能，准确率高达86.7%，尤其擅长较简单的规则。人工评估表明，LLM生成的提示在一致性和清晰度方面表现良好，但解释性仍有提升空间。该研究验证了LLM在逻辑证明辅导方面的潜力，并为未来的研究方向提供了指导。

🎯 应用场景

该研究成果可应用于智能辅导系统，为学生提供个性化的逻辑证明指导。通过LLM生成的动态提示，可以帮助学生更好地理解逻辑规则和证明过程，提高学习效率。未来，该技术还可扩展到其他学科，例如数学、编程等，为更广泛的学习场景提供支持。

📄 摘要（原文）

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 up to 86.7% 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 require additional modifications to ensure accuracy and pedagogical appropriateness.