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

TL;DR

This paper evaluates the use of large language models for generating proofs and hints in logic tutoring systems, highlighting their potential and current limitations in accuracy and pedagogical quality.

Contribution

It introduces a comparative analysis of prompting techniques for LLMs in proof construction and demonstrates their application in generating student hints with promising accuracy.

Findings

DeepSeek-V3 achieved up to 86.7% accuracy in proof stepwise construction.

LLM-generated hints were 75% accurate and rated highly by humans.

LLMs need modifications for better pedagogical appropriateness.

Abstract

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.