A team of researchers built an LLM-powered tool that automatically finds the mistakes students repeatedly make when writing formal logical and mathematical models.
The workflow has three steps. First, it scans large sets of student submissions in formalisms like propositional logic to find candidate bug-fixing transformations - patterns that turn an incorrect formula into a correct one. An LLM generates those candidates, and an algorithm checks that each transformation actually does what it claims. The system then clusters similar candidates together and visualizes the clusters so instructors and computer-science-education researchers can spot recurring error types.
The researchers tested the tool against mistakes in propositional logic that education researchers had previously catalogued by hand, and it reproduced them. It also scaled to data sets too large for older algorithmic approaches, and the team applied it to other formalisms beyond logic to show the method isn't a one-trick fit. That matters for any interactive learning system trying to give students specific feedback - you flipped a negation - instead of a generic wrong answer.
It's a narrow use of LLMs, but a sensible one: the model proposes, an algorithm disposes, and nobody has to trust the AI's math unsupervised.