Evaluating Automatic Difficulty Estimation of Logic Formalization Exercises

TL;DR

This paper evaluates an automatic difficulty estimation algorithm for logic formalization exercises by correlating its predictions with empirical difficulty measures, identifying additional difficulty factors, and discussing implications for education and AI.

Contribution

It assesses the effectiveness of a difficulty estimation algorithm for logic exercises and identifies new difficulty factors through error analysis.

Findings

Moderate correlation between predicted and empirical difficulty measures.

Identification of predicate complexity, pragmatic factors, and typicality as additional difficulty sources.

Implications for improving logic teaching and explainable AI.

Abstract

Teaching logic effectively requires an understanding of the factors which cause logic students to struggle. Formalization exercises, which require the student to produce a formula corresponding to the natural language sentence, are a good candidate for scrutiny since they tap into the students' understanding of various aspects of logic. We correlate the difficulty of formalization exercises predicted by a previously proposed difficulty estimation algorithm with two empirical difficulty measures on the Grade Grinder corpus, which contains student solutions to FOL exercises. We obtain a moderate correlation with both measures, suggesting that the said algorithm indeed taps into important sources of difficulty but leaves a fair amount of variance uncaptured. We conduct an error analysis, closely examining exercises which were misclassified, with the aim of identifying additional sources of difficulty. We identify three additional factors which emerge from the difficulty analysis, namely predicate complexity, pragmatic factors and typicality of the exercises, and discuss the implications of automated difficulty estimation for logic teaching and explainable AI.