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-gedreven wiskundige bewijstutor te creëren die zowel natuurlijk taalverkeer als wiskundige correctheid garandeert, geëvalueerd met de nieuwe PeanoBench-dataset.

De kern

Stel je voor dat wiskunde bewijzen schrijven een beetje is als het bouwen van een heel complexe, perfecte toren van Legoblokken.

In de wereld van vandaag hebben we twee soorten "bouwers":

1. De Talige Verteller (LLM's): Dit zijn slimme robots die heel goed kunnen praten en uitleggen hoe je de toren moet bouwen. Ze gebruiken mooie zinnen en klinken heel overtuigend. Maar ze maken vaak fouten. Ze kunnen zeggen: "Zet hier een rood blokje," terwijl dat blokje eigenlijk niet past en de hele toren laat instorten. Ze zijn goed in praten, maar slecht in controleren of het echt klopt.
2. De Strikte Bouwmeester (Lean): Dit is een computerprogramma dat onfeilbaar is. Als het zegt dat de toren staat, dan staat hij perfect. Maar deze bouwmeester spreekt een heel moeilijke, cryptische taal. Voor een student is het net als proberen een boek te lezen in een taal die je nooit hebt geleerd. Het is te moeilijk om zelf te leren.

LeanTutor is de oplossing die deze twee wereldjes samenbrengt. Het is als een slimme leerkracht die twee superkrachten heeft:

• De Vertaler: Deze vertaalt wat de student in gewone taal zegt (bijvoorbeeld: "Ik doe dit blokje hier") naar de strenge taal van de Bouwmeester, zodat die het kan controleren.
• De Hulp bij de Volgende Stap: Als de student vastloopt, denkt de leerkracht mee en zegt: "Probeer eens dit blokje hier," maar dan in de taal die de Bouwmeester begrijpt.
• De Vriendelijke Uitlegger: Als er een fout is, vertaalt de leerkracht de strenge waarschuwing van de Bouwmeester ("Fout: blokje 4 past niet op blokje 3") terug naar een vriendelijke zin in gewone taal die de student echt begrijpt.

Om te testen of dit werkt, hebben de makers van LeanTutor een speciale speelset gemaakt genaamd PeanoBench. Dit is een verzameling van 371 wiskundige puzzels (over getallen) die zowel in gewone taal als in de strenge taal zijn opgeschreven. Het is alsof ze een testexamen hebben gemaakt om te zien of hun nieuwe leerkracht echt kan helpen zonder de toren te laten instorten.

Kortom: LeanTutor is de perfecte assistent die de vriendelijkheid en begrijpelijkheid van een menselijke leraar combineert met de onfeilbare nauwkeurigheid van een computer, zodat iedereen wiskunde kan leren zonder bang te zijn voor fouten.

Technische samenvatting

Probleemstelling

Het paper adresseert een fundamenteel spanningsveld in het onderwijs van wiskundige bewijzen. Enerzijds bieden Grote Taalmodellen (LLMs) een naadloze interface voor communicatie in natuurlijke taal, maar zijn ze berucht om hun neiging tot hallucinaties en fouten in logische redenering. Anderzijds bieden theorema-proevers zoals Lean een omgeving voor wiskundig bewezen correctheid, maar is de leercurve voor studenten extreem steil en is de interactie vaak te formeel en onvriendelijk. Er is een behoefte aan een systeem dat de toegankelijkheid van LLMs combineert met de strikte correctheid van formele bewijssystemen.

Methodologie

De auteurs presenteren LeanTutor, een proof-of-concept-systeem dat de complementaire sterkten van LLMs en theorema-proevers integreert. Het systeem is architectonisch opgebouwd uit drie gespecialiseerde modules die samenwerken om een interactieve tutor te vormen:

1. Autoformalizer/Proof-checker: Deze module is verantwoordelijk voor het vertalen van natuurlijke taal-invoer van de student naar formeel Lean-code (autoformalisatie) en het verifiëren van de correctheid van het bewijs binnen de Lean-omgeving. Dit zorgt voor de "provable-correctness" (bewezen correctheid).
2. Next-step Generator: Wanneer een student vastloopt of een fout maakt, genereert deze module de volgende logische stap in het bewijs. Deze module fungeert als een gids die het bewijsproces structureert zonder de volledige oplossing direct te onthullen.
3. Natural Language Feedback Generator: Om de interactie toegankelijk te houden, vertaalt deze module de formele feedback van de Lean-prover (bijvoorbeeld typefouten of logische onvolkomenheden) terug naar begrijpelijke natuurlijke taal voor de student.

Om dit systeem te evalueren, hebben de auteurs PeanoBench geïntroduceerd. Dit is een nieuw dataset dat bestaat uit 371 bewijzen in Peano-aritmetiek. De dataset bevat zowel menselijk geschreven natuurlijke taalversies als de corresponderende formele Lean-versies, en is afgeleid van het bekende educatieve spel Natural Numbers Game.

Belangrijkste Bijdragen

• LeanTutor Systeem: Een geïntegreerd architectuurontwerp dat LLMs gebruikt voor interactie en taalverwerking, terwijl een formele theorema-prover (Lean) als "waarheidsgarant" fungeert voor elke stap in het bewijs.
• PeanoBench Dataset: De creatie van een gestandaardiseerde benchmark voor het evalueren van AI-systemen in het domein van wiskundige bewijzen, specifiek gericht op Peano-aritmetiek.
• Proof-of-Concept Validatie: Het aantonen dat het combineren van deze technologieën haalbaar is voor het bouwen van een tutor die zowel educatief waardevol als wiskundig betrouwbaar is.

Resultaten

Hoewel het paper voornamelijk een proof-of-concept presenteert, demonstreert het dat het LeanTutor-systeem in staat is om:

• Bewijzen in natuurlijke taal succesvol te vertalen naar Lean.
• Fouten in studentbewijzen te detecteren via de formele checker.
• Constructieve feedback te geven die de student helpt bij het vinden van de volgende correcte stap, waarbij de strengheid van de formele logica behouden blijft.
  De evaluatie met PeanoBench bevestigt dat het systeem effectief kan opereren binnen de beperkingen van Peano-aritmetiek.

Significantie

De bijdrage van dit paper is significant voor de toekomst van AI-ondersteund wiskundeonderwijs. Het biedt een oplossing voor het "hallucinati-probleem" van LLMs in kritieke domeinen door een formele verificatielaag toe te voegen. Door de hoge drempel van formele bewijssystemen te verlagen via natuurlijke taal-interactie, opent LeanTutor de deur voor studenten om complexe wiskundige concepten te leren met de zekerheid dat hun redenering wiskundig correct is. Dit markeert een stap in de richting van "Verified AI", waar AI-assistenten niet alleen suggesties doen, maar ook de waarheid van die suggesties kunnen garanderen.