LeanTutor: Towards a Verified AI Mathematical Proof Tutor

Dit paper introduceert LeanTutor, een proof-of-concept systeem dat de kracht van Large Language Models en theorem-provers combineert om een AI-gestuurde wiskundige bewijstutor te creëren die fouten minimaliseert en natuurlijke taalfeedback biedt, getest op de nieuwe PeanoBench-dataset.

De kern

Stel je voor dat wiskunde leren, en dan vooral het bewijzen van formules, een beetje lijkt op het bestijgen van een steile berg. Je hebt een kaart nodig (de theorie) en een gids die je stap voor stap meeneemt.

In de afgelopen jaren zijn er twee soorten "gidsen" opgedoken, maar beide hebben een groot probleem:

1. De slimme, maar onbetrouwbare chatbot (LLM): Dit is als een gids die fantastisch kan praten en heel vriendelijk is. Hij kan je in je eigen taal uitleggen wat er aan de hand is. Maar helaas, hij maakt vaak fouten. Soms zegt hij iets dat klinkt als een waarheid, maar is het gewoon een verzinsel (een "hallucinatie"). Of, nog erger: als je hem vraagt hoe je de berg beklimt, zegt hij direct: "Hier is de top!" in plaats van jou te helpen de weg te vinden. Voor een leerling is dat funest; je leert niets als je het antwoord gewoon krijgt.
2. De strenge, maar onbegrijpelijke computer (Theorema-bewijzer): Dit is een machine die 100% zekerheid biedt. Als hij zegt dat je bewijs klopt, klopt het. Maar om met deze machine te praten, moet je een heel moeilijke, vreemde taal spreken (zoals Latijn voor wiskundigen). Voor een student is dit vaak te moeilijk en te saai om te leren.

LeanTutor: De perfecte combinatie

De auteurs van dit paper hebben een nieuwe oplossing bedacht: LeanTutor. Ze hebben de twee bovenstaande gidsen samengevoegd tot één super-gids.

Hoe werkt dit? Stel je voor dat LeanTutor een tandem is met twee fietsers:

• De voorste fietser (De Chatbot): Deze fietser praat met de student in gewone, makkelijke taal. Hij hoort wat de student zegt, begrijpt de verwarring en praat terug in een vriendelijke toon. Hij is de "vertaler".
• De achterste fietser (De Computer): Deze fietser kan niet praten, maar hij is een genie in wiskunde. Hij kijkt naar wat de voorste fietser zegt, vertaalt het naar de strenge wiskundetaal, en checkt of het klopt. Hij is de "controleur".

De drie magische modules

LeanTutor bestaat uit drie onderdelen die samenwerken:

1. De Vertaler (Autoformalizer): Als een student zegt: "Ik denk dat ik hier moet beginnen met tellen vanaf nul", vertaalt de computer dit direct naar de strenge taal van de machine. Hij kijkt of die stap logisch is.
2. De Wegwijzer (Next Step Generator): Als de student vastloopt of een fout maakt, vraagt de computer: "Welke stap zou hier logisch op volgen?" Hij probeert 12 verschillende mogelijke stappen uit in zijn hoofd. Als hij een stap vindt die de machine accepteert, zegt hij: "Probeer deze stap eens!"
3. De Coach (Feedback Generator): Dit is het belangrijkste deel. Als de student een fout maakt, zegt de coach niet: "Het antwoord is X." Nee, hij zegt: "Kijk eens naar je vorige stap. Denk je dat die hier echt past? Wat zou er gebeuren als je dit anders doet?" Hij helpt de student om zelf op het juiste spoor te komen, zonder het antwoord te verklappen.

De proef: PeanoBench

Om te testen of dit werkt, hebben de onderzoekers een speciale testbaan gemaakt genaamd PeanoBench. Dit is een verzameling van 371 wiskundige puzzels (over getallen en optellen). Ze hebben voor elke puzzel een "perfecte" oplossing en ook een "menselijke" versie geschreven. Ze hebben zelfs "verkeerde" oplossingen gemaakt, alsof een student een stap over het hoofd ziet, om te kijken of LeanTutor die fout kan vinden en corrigeren.

Wat hebben ze ontdekt?

• Het werkt! LeanTutor is veel beter in het vinden van fouten en het geven van nuttige hints dan een gewone chatbot die alleen maar praat.
• De vertaling is lastig: Het is moeilijk om menselijke taal (vaak vaag en creatief) om te zetten in strenge wiskundetaal (die heel precies moet zijn). Soms denkt de computer dat de student een fout maakt, terwijl de student eigenlijk gewoon anders heeft geformuleerd.
• De menselijke factor: Het systeem is nog niet perfect, maar het is een enorme stap vooruit. Het combineert het beste van twee werelden: de vriendelijkheid en begrijpelijkheid van een menselijke chatbot, met de onfeilbare nauwkeurigheid van een computer.

Conclusie

LeanTutor is als een slimme fietsles-instructeur. Hij laat je niet direct op de top van de berg staan, maar hij loopt met je mee, corrigeert je houding als je scheef zit, en geeft je tips om zelf de volgende helling te beklimmen. Het doel is niet om de wiskunde voor je te doen, maar om je te leren hoe je het zelf kunt doen, zonder dat je vastloopt in een taal die je niet begrijpt.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "LeanTutor: Towards a Verified AI Mathematical Proof Tutor" in het Nederlands.

Probleemstelling

Huidige Large Language Models (LLMs) zoals ChatGPT en Claude worden steeds vaker gebruikt door studenten voor wiskundige taken, maar ze zijn niet ideaal als tutor voor het leren van wiskundige bewijzen. De belangrijkste beperkingen zijn:

1. Pedagogische tekortkomingen: LLMs zijn vaak te "helpzaam" en geven direct het antwoord in plaats van de student te begeleiden naar een zelfstandige oplossing.
2. Hallucinaties: Zelfs geavanceerde modellen genereren overtuigende maar onjuiste antwoorden en redeneringen.
3. Gebrek aan foutdetectie: Modellen hebben moeite om fouten in redenering te identificeren en kunnen correcte antwoorden geven zonder de juiste onderliggende logica te tonen.
4. Formele bewijssystemen: Bestaande systemen gebaseerd op bewijshulpmiddelen (zoals Lean) zijn weliswaar wiskundig correct, maar vereisen een complexe syntaxis die voor studenten een hoge drempel vormt.

Er is dus behoefte aan een systeem dat de natuurlijke taalinteractie van LLMs combineert met de wiskundige zekerheid van formele bewijshulpmiddelen, zonder de student te overweldigen met formele syntax.

Methodologie: LeanTutor

De auteurs stellen LeanTutor voor, een proof-of-concept systeem dat drie modules combineert om een interactieve tutor te creëren die in natuurlijke taal (NL) communiceert maar "onder de motorkap" gebruikmaakt van de Lean-theoremaprover.

Het systeem bestaat uit drie kernmodules:

1. Autoformalizer & Proof Checker:

   • Deze module vertaalt de stap-voor-stap input van de student in natuurlijke taal naar Lean-code (formele taal).
   • Het proces is iteratief: elke stap wordt vertaald, direct gecompileerd in Lean, en gecontroleerd op fouten.
   • Als de compiler een fout rapporteert (bijv. een onbekende tactic), wordt de stap als foutief gemarkeerd en stopt het proces.
   • Het systeem maakt gebruik van een "Staff Solution" (een referentiebewijs) en een woordenboek van theorema's en tactics als context voor de LLM om de vertaling te verbeteren.

2. Next Step Generator (NSG):

   • Wanneer een bewijs onvolledig of foutief is, genereert deze module een volgend haalbaar bewijsstapje.
   • De module voert een door de LLM geleide depth-first search uit. De LLM genereert 12 kandidaat-tactics.
   • Deze kandidaten worden gefilterd via een "progress check": ze moeten compileren, geen verboden theorema's gebruiken (zoals het te bewijzen theorema zelf) en geen cyclische paden creëren.
   • De zoektocht stopt zodra een compleet bewijs is gevonden (met een maximale diepte van 8 stappen).

3. Natural Language Feedback Generator:

   • Deze module combineert de output van de vorige modules (de geformaliseerde bewijzen, compiler-foutberichten en de gevonden volgende stap) om pedagogisch waardevolle feedback te genereren.
   • De feedback omvat drie typen:
     1. Foutidentificatie: Waar ging het mis?
     2. Hints/Vragen: Een leidende vraag om de student naar de oplossing te sturen zonder het antwoord te geven.
     3. Expliciete volgende stap: Een "bottom-out hint" die de concrete volgende tactic aangeeft (vergelijkbaar met het vertalen van formele code terug naar natuurlijke taal).

Dataset: PeanoBench

Om het systeem te evalueren, hebben de auteurs PeanoBench ontwikkeld, een dataset van 371 bewijzen in Peano-arithmetiek.

• Bron: Afgeleid van de "Natural Numbers Game" (NNG4).
• Structuur: Elk bewijs heeft een menselijk geschreven versie in natuurlijke taal en een semantisch equivalente versie in Lean.
• Variatie: De dataset bevat "Staff Solutions" (correcte referenties) en gegenereerde bewijzen met verschillende "persona's" (bijv. algebraïsch of justifiërend).
• Fouten: Onjuiste bewijzen zijn gegenereerd door logische stappen (zoals het toepassen van de inductiehypothese) te overslaan, wat een veelgemaakte fout van studenten nabootst.

Resultaten

De evaluatie werd uitgevoerd met de gpt-4o-mini LLM en vergeleken met een baseline-model.

1. Autoformalisatie:

   • Het stap-voor-stap benadering met een "Staff Solution" in de context presteerde significant beter dan het vertalen van het hele bewijs in één keer.
   • Voor correcte bewijzen steeg de tactic-nauwkeurigheid van ~33% (baseline) naar ~57% (met staff solution).
   • Voor onjuiste bewijzen was de stap-voor-stap methode 8% beter dan de "whole proof" methode, wat cruciaal is voor een tutor die vaak met fouten te maken krijgt.
   • Een nieuwe metriek voor "faithful autoformalization" werd ontwikkeld die niet alleen op string-matching, maar ook op de syntactische identiteit van de bewijstoestand (na normalisatie van variabele namen) baseert.

2. Systeemevaluatie (Feedback):

   • Menselijke evaluators (docenten) beoordeelden de feedback op vier assen: Nauwkeurigheid, Relevantie, Leesbaarheid en "Answer Leakage" (het onbedoeld geven van het antwoord).
   • LeanTutor presteerde significant beter dan de baseline op Nauwkeurigheid en Relevantie.
   • De Leesbaarheid was vergelijkbaar voor beide modellen.
   • Answer Leakage was lager bij LeanTutor, wat aangeeft dat het systeem beter in staat is om hints te geven zonder het volledige antwoord te onthullen (hoewel dit bij "next step" feedback nog steeds een uitdaging blijft).
   • Een evaluatie met een LLM als "judge" (gpt-4) gaf tegengestelde resultaten (baseline won), wat de auteurs als onbetrouwbaar beschouwen in vergelijking met menselijke beoordelingen.

Belangrijke Bijdragen

1. Architectuur voor Verifieerbare Tutors: Een werkend bewijs van concept dat LLMs koppelt aan een formele theoremaprover (Lean) om pedagogische feedback te geven die wiskundig gegarandeerd correct is.
2. PeanoBench Dataset: Een nieuwe dataset met parallelle natuurlijke taal en formele bewijzen, inclusief systematisch gegenereerde fouten, specifiek ontworpen voor de evaluatie van tutoring-systemen.
3. Nieuwe Metriek: Een methode om de kwaliteit van autoformalisatie te meten door de bewijstoestand te vergelijken in plaats van alleen de tekstuele output, rekening houdend met variabele-namen.
4. Pedagogische Focus: Het systeem is ontworpen om de "happy medium" te vinden tussen de directe feedback van LLMs en de strikte correctheid van formele systemen, waarbij het vermijden van het geven van volledige antwoorden centraal staat.

Significantie en Toekomstperspectief

Dit paper is significant omdat het een brug slaat tussen twee vaak gescheiden werelden: de toegankelijkheid van generatieve AI en de strikte correctheid van formele verificatie. Het toont aan dat het mogelijk is om studenten te helpen met complexe wiskundige bewijzen zonder hen de complexe syntax van bewijshulpmiddelen te laten leren.

De auteurs erkennen beperkingen, zoals de afhankelijkheid van een bestaande "staff solution" en de uitdagingen bij het vertalen van zeer complexe, niet-lineaire redeneringen. Toekomstig werk richt zich op het implementeren van backtracking in de next-step generator, het verbeteren van de autoformalisatie zonder volledige referentiebewijzen, en het testen van het systeem in echte undergraduate wiskundecursussen (zoals discrete wiskunde en lineaire algebra).

Kortom, LeanTutor biedt een veelbelovend kader voor de ontwikkeling van toekomstige AI-tutors die niet alleen "helpzaam" zijn, maar ook wiskundig verantwoord.