Finding Common Mistakes In Modelling With Mathematical Formalisms Using LLMs
Lilian Killich, Marko Schmellenkamp, Fabian Vehlken, Thomas Zeume
cs.CY · cs.AI · cs.LO
Quick verdict
Sound LLM-plus-validation workflow recovers known logic-modelling mistakes and extends them; CTL coverage is low and evaluation lacks statistical rigor.
Summary
The paper presents a tool-supported workflow for discovering common mistakes in student modelling with mathematical formalisms. Mistakes are represented as bug fixing transformations: tree-pattern rewrites mapping incorrect to correct syntax trees. GPT-OSS-120B proposes candidate transformations batch-by-batch (~50 pairs per prompt); each candidate is validated algorithmically (a single rewrite must exactly produce the target tree and explain at least delta=1% of the dataset), and the loop stops after ten fruitless iterations. A correlation graph over transformations, weighted by overlap of explained pairs, yields interpretable single/equivalent/hierarchical clusters that are visualized for educators. On 6106 propositional-logic pairs, the workflow explains 84.44% of pairs versus 71.57% for the hand-picked mistakes of Schmellenkamp et al. (SIGCSE 2023), exclusively explaining 15.03% (e.g., rho_xornand covering 114 pairs); 21 clusters explain 66.34%. Modal logic (12482 pairs) reaches 79.39% coverage; CTL (7210 self-collected pairs) only 35.89%. A single CS educator judged the >=0.5% clusters mostly feedback-suitable. Strengths are the propose-and-verify design that neutralizes LLM hallucination and the at-scale reproduction of prior hand analyses. Main limitations: purely descriptive evaluation without statistical uncertainty or repeated runs, no non-LLM baseline or runtime figures backing the scalability claim, low CTL coverage, single-rater usefulness assessment, and no explicit code release.
Review complete
Assessment at a glance
6
risk flags identified
● high 0
● medium 3
● low 3
4 strengths · 5 weaknesses · 5 author questions
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- The LLM-based workflow reproduces the hand-identified propositional-logic mistakes of Schmellenkamp et al. [13] and explains more pairs (84.44% vs. 71.57%), exclusively explaining 15.03% of pairs.
- Unlike SAT-based transformation mining [8], the LLM-based approach scales to large educational datasets (up to 12,482 pairs).
- The same pipeline generalizes to modal logic (79.39% explained) and CTL (35.89% explained) without formalism-specific engineering.
- Clustering via correlation graphs yields interpretable structures (single, equivalent, hierarchical clusters) that help educators select representative transformations for targeted feedback.
Strengths
Propose-then-verify design neutralizes LLM unreliability
The LLM only suggests candidates; Algorithm 1 validates each against the full dataset, accepting only transformations that exactly rewrite incorrect into correct syntax trees and explain >=delta=1% of pairs (Sec. 3.1). This directly addresses the reliability concerns the authors themselves cite for LLM feedback [16,17].
Reproduces and extends prior hand analysis at scale
On the same 6106-pair propositional dataset, found transformations explain 84.44% of pairs vs. 71.57% for hand-picked mistakes [13], exclusively explaining 15.03% (e.g., rho_xornand, 114 pairs, which the prior bi-implication-only xor mistake misses). Table 1 shows the disjunction-instead-of-conjunction mistake is 98.8% recovered by one cluster (330/334).
One pipeline generalizes across formalisms with a locally deployable model
Interpretable, data-grounded clustering
Weaknesses
Descriptive-only evaluation
Scalability claim lacks evidence
Generalization only partially demonstrated
Subjective usefulness assessment; visualization unevaluated
Spurious candidates in the long tail; minor inconsistencies
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
- All 4 strengths & 5 weaknesses, analyzed in detail
- 6 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What does the LLM do in this paper, and why isn't hallucination a problem?
The LLM only proposes candidate 'bug fixing transformations' - small tree-rewrite rules - from batches of about 50 student formula pairs. Every candidate is then checked algorithmically: it must exactly rewrite an incorrect formula's syntax tree into the correct one and explain at least 1% of the dataset to be kept. Unvalidated LLM output therefore never enters the results; the LLM is a proposal engine, the verifier is exact.
How well does the method perform compared to earlier manual analyses?
On a public dataset of 6106 propositional-logic student answers, the workflow's transformations explain 84.44% of answer pairs, versus 71.57% for the hand-picked mistakes of Schmellenkamp et al. (SIGCSE 2023) on the same data; 15.03% of pairs are explained only by the new workflow, and 2.16% only by the prior hand analysis.
Does the approach work for formalisms other than propositional logic?
Partly. The identical pipeline explains 79.39% of 12,482 modal-logic pairs, which is comparable to propositional logic, but only 35.89% of 7,210 CTL (computation tree logic) pairs. So generalization is strong for propositional and modal logic and noticeably weaker for CTL; regular expressions are shown only as a motivating example, not evaluated.
Are the code, data, and prompts available?
The prompts and very detailed per-transformation result tables are published in an anonymized OSF supplement, and the model used (GPT-OSS-120B) is open-weight and locally deployable. The underlying datasets come from prior published work plus the authors' own course data. However, the paper does not explicitly state that the validation/clustering code itself is released.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- Figure 1 (workflow diagram) and the correlation-graph figure of Example 3.1 could not be assessed from the extracted text, as graphics are lost in extraction.
- Appendix Table 38 is truncated mid-row in the extracted text (ends around T328), so a minority of propositional-logic cluster rows were unavailable for inspection.
- Per-cluster tables for modal logic and CTL are referenced as OSF supplementary material and could not be verified from the provided text.
- The anonymized OSF supplement (full prompts, detailed tables) was not accessed; judgments about reproducibility rely on what the paper text states.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.