MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

Stel je voor dat je een briljante maar ietwat onhandige robot probeert te leren spreken in de taal van de pure logica. Deze robot, een Large Language Model (LLM), is geweldig in het lezen van verhalen, het schrijven van gedichten en het oplossen van wiskundige puzzels in gewoon Engels. Maar er is een addertje onder het gras: om een wiskundig theorema met absolute zekerheid te bewijzen, kun je niet alleen woorden gebruiken; je moet het schrijven in een superstrikte computertaal genaamd Lean 4. Denk aan Lean 4 als een hoogbeveiligde kluis waar elk woord, symbool en elke regel perfect moet zijn, anders gaat de deur van de kluis niet open. Het probleem is dat de robot wel wiskunde kent, maar niet het specifieke "regelboek" (genaamd Mathlib) dat Lean 4 gebruikt. Het is alsof je een chef vraagt die weet hoe hij een perfect biefstuk bereidt, om een recept te volgen dat geschreven is in een taal die hij nog nooit heeft gezien, met ingrediënten waarvan hij de namen niet kent. Hij kan gokken, maar hij zal waarschijnlijk de fout in gaan.

Dit is waar "autoformalizatie" om de hoek komt kijken: de kunst van het vertalen van menselijke wiskunde naar deze strikte computercode. Lange tijd probeerden onderzoekers de robot simpelweg de wiskunde te laten "vertalen", in de hoop dat hij de regels uit zijn training zou onthouden. Maar de robot bleef fouten maken, zoals het gebruik van de verkeerde ingrediënten of het vergeten van een cruciale stap, omdat hij probeerde te vertrouwen op zijn geheugen alleen. De nieuwe paper, MathForm, betoogt dat deze "gokken en hopen"-aanpak kapot is. In plaats daarvan hebben ze een systeem gebouwd waarbij de robot de mogelijkheid heeft om het regelboek op te zoeken voordat hij begint met schrijven, en als hij een fout maakt, een strikte editor het werk niet zomaar weggooit—maar hem precies vertelt wat er misging en hem laat het opnieuw proberen totdat hij het goed heeft.

De onderzoekers achter MathForm realiseerden zich dat om een robot de taal van de formele wiskunde perfect te laten spreken, je niet zomaar een concept kunt laten schrijven en hopen op het beste. Ze bouwten een assemblageproces van drie stappen om de workflow van de robot te verbeteren. Ten eerste, voordat de robot een enkele regel code schrijft, scant een "Researcher"-agent de enorme Mathlib-bibliotheek om de exacte definities en regels te vinden die de robot nodig heeft voor dat specifieke probleem. Het is alsof je de chef de specifieke pagina uit het kookboek voor "Biefstuk" geeft voordat hij zelfs maar een mes oppakt. Ten tweede schrijft de robot zijn code, en daarna controleert een "Inspector" deze. Als de code een syntactische fout bevat (zoals een ontbrekende komma), wijst de Inspector dit aan. Als de code compileert maar de verkeerde betekenis heeft (zoals zeggen "alle getallen" terwijl het probleem "alleen positieve getallen" bedoelde), legt de Inspector de semantische fout uit. Derde, in plaats van op te geven, gebruikt de robot deze feedback om zijn code te herschrijven. Hij blijft doorlopen in deze "schrijven-controleren-verbeteren"-cyclus totdat de code perfect is.

Met behulp van deze slimme lus creëerde het team een enorme nieuwe dataset genaamd FormalVerse, die ongeveer 367.000 geverifieerde wiskundige voorbeelden bevat. Ze trainden vervolgens een nieuw model, MathForm-8B, op deze data. De resultaten waren verrassend: dit relatief kleine model (8 miljard parameters) werd beter in het formaliseren van wiskunde dan veel grotere, gespecialiseerde modellen (32 miljard parameters) die vertrouwden op de oude "gokken en hopen"-methoden. Op zes verschillende moeilijke wiskundetests slaagde MathForm-8B voor de strikte "Consistency Check" (wat betekent dat de code daadwerkelijk betekende wat het menselijke probleem zei) in ongeveer 72,4% van de gevallen, waarmee het de vorige beste modellen versloeg. Zelfs bij de moeilijkste, meest abstracte algebraproblemen presteerde het aanzienlijk beter dan zijn grotere rivalen. De paper suggereert dat door het model de juiste hulpmiddelen te geven om informatie op te zoeken en de kans om van zijn fouten te leren, je geen gigantisch brein nodig hebt om een wiskundig genie te zijn; je hebt alleen een slimme workflow nodig.