Autoformalisatie: wiskunde vertalen naar een taal die computers kunnen controleren
Stel je een kookboek voor waarin een recept staat met de zin "voeg naar smaak wat zout toe en bak tot het gaar is". Een ervaren kok begrijpt precies wat hier bedoeld wordt, maar een robotarm kan hier niets mee: die heeft een exact stappenplan nodig, met precieze hoeveelheden en tijden. Autoformalisatie is in wezen hetzelfde probleem, maar dan voor wiskunde: het automatisch omzetten van menselijke, vaak losjes geformuleerde wiskundetaal naar een strikt, ondubbelzinnig format dat een computer regel voor regel kan controleren.
Wiskundigen schrijven bewijzen in een mengvorm van gewone taal en symbolen, en laten daarbij voortdurend stappen weg die zij "vanzelfsprekend" vinden: "het is duidelijk dat...", "met een soortgelijke redenering volgt...". Voor mensen werkt dat prima, maar een computer accepteert zulke aannames niet zomaar. Autoformalisatie probeert, met behulp van kunstmatige intelligentie, die informele redeneringen te vertalen naar volledig expliciete, computerchecking bare code. Het doel is niet dat computers voortaan wiskunde "begrijpen" zoals mensen dat doen, maar dat ze elk detail van een bewijs kunnen natrekken, zodat er geen verborgen fouten of gaten meer overblijven.
Wat is het precies?
Om te snappen wat autoformalisatie doet, helpt het om het verschil te kennen tussen informele en formele wiskunde. Informele wiskunde is wat je in een leerboek of vakartikel aantreft: natuurlijke taal doorspekt met symbolen, waarbij de lezer wordt vertrouwd om kleine stappen zelf in te vullen. Formele wiskunde wordt geschreven in een speciale programmeertaal voor zogeheten proof assistants, ook wel bewijsassistenten genoemd, zoals Lean, Coq (tegenwoordig Rocq geheten) of Isabelle. In zo'n taal moet werkelijk elke logische stap met naam en toenaam worden opgeschreven, van de allereerste definitie tot de laatste conclusie.
Een proof assistant heeft in de kern een klein, streng gecontroleerd programma dat de "kernel" wordt genoemd. Deze kernel is het enige onderdeel dat daadwerkelijk beslist of een bewijs klopt, volgens een handvol wiskundige basisregels. Omdat die kernel zo klein en overzichtelijk is, kunnen wiskundigen en informatici er relatief veel vertrouwen in hebben dat hij geen fouten doorlaat, zelfs als het bewijs zelf duizenden regels lang is en met hulp van AI is opgesteld.
Autoformalisatie zet hier grote taalmodellen (LLM's, de technologie achter chatbots als ChatGPL en vergelijkbare systemen) voor in. Zulke modellen worden getraind op grote hoeveelheden gekoppelde voorbeelden: een informele stelling of bewijs naast de bijbehorende formele versie in Lean of een vergelijkbare taal. Op basis daarvan leert het model patronen herkennen en zelf nieuwe, nog ongeziene informele teksten om te zetten in formele code.
Wat dit proces bijzonder maakt, is de feedback die je erbij krijgt. Bij de meeste taken die een taalmodel uitvoert, zoals het schrijven van een e-mail, is er geen objectieve maatstaf voor "correct". Bij autoformalisatie is dat anders: de proof assistant checkt mechanisch of de formele code klopt, en geeft een hard ja-of-nee-signaal. Die eigenschap maakt het mogelijk om modellen te trainen met reinforcement learning, een trainingsmethode waarbij een systeem beloond wordt voor pogingen die tot een geverifieerd correct resultaat leiden, en zo stap voor stap beter leert formaliseren en bewijzen.
Wat wil men ermee bereiken?
Een eerste drijfveer is kwaliteitscontrole. Peer review, de traditionele controle van wiskundige artikelen door vakgenoten, is nuttig maar niet feilloos: bewijzen van honderden pagina's kunnen subtiele fouten bevatten die jarenlang onopgemerkt blijven. Als een bewijs volledig geformaliseerd is en door een proof assistant geaccepteerd wordt, is de kans op zo'n verborgen fout vrijwel nihil, althans wat de logische structuur betreft.
Een tweede doel is het laten groeien van formele wiskundebibliotheken. Het bekendste voorbeeld is Mathlib, een enorme, gezamenlijk opgebouwde verzameling geformaliseerde definities en stellingen voor Lean. Het handmatig formaliseren van bestaande wiskunde is extreem tijdrovend; als AI-systemen een groot deel van dat werk kunnen versnellen, kan zo'n bibliotheek veel sneller groeien dan wanneer alleen mensen dat doen.
Een derde, meer toekomstgerichte reden is dat autoformalisatie wordt gezien als een tussenstap naar AI die niet alleen vloeiend klinkt, maar ook aantoonbaar correct redeneert. Taalmodellen zijn berucht om het overtuigend klinkende, maar soms feitelijk onjuiste antwoorden geven. Een systeem dat zijn redenering moet gieten in een vorm die een onafhankelijke checker goedkeurt, kan zichzelf niet zo makkelijk voor de gek houden.
Tot slot heeft dit onderzoek ook uitstraling buiten de zuivere wiskunde. Dezelfde technieken en proof assistants worden gebruikt om software, computerchips en beveiligingsprotocollen formeel te verifiëren, dus vooruitgang in autoformalisatie van wiskunde kan ook bijdragen aan betrouwbaardere verificatie van kritieke techniek.
Voorbeelden uit de praktijk
Een van de meest besproken voorbeelden is AlphaProof, een systeem van DeepMind waarover in de zomer van 2024 werd bericht. Het combineert het automatisch vertalen van olympiadeopgaven naar Lean met een zoekmethode die geïnspireerd is op de reinforcement-learningtechnieken achter eerdere DeepMind-systemen zoals AlphaZero. Volgens de gepubliceerde resultaten haalde het systeem op een selectie problemen van de Internationale Wiskunde Olympiade (IMO) van 2024 een score die ongeveer overeenkomt met een zilveren medaille op mensenniveau.
Rond dezelfde tijd, begin 2024, publiceerde DeepMind ook AlphaGeometry, een systeem gericht op meetkundeproblemen uit wiskundeolympiades, met resultaten die in het tijdschrift Nature zijn beschreven. Dit systeem werkt met een eigen formele, symbolische taal voor meetkundige redeneringen en zou volgens de makers goud-medailleniveau benaderen op de geteste opgaven.
Een ander voorbeeld komt uit de zuivere onderzoekswiskunde: in 2023 leidde de bekende wiskundige Terence Tao een gezamenlijk project om een bewijs rond de zogeheten polynomial Freiman-Ruzsa-conjecture, een resultaat uit de combinatorische getaltheorie, te formaliseren in Lean. Tientallen vrijwilligers uit de Mathlib-gemeenschap werkten hieraan mee, deels geholpen door AI-hulpmiddelen.
Kevin Buzzard, hoogleraar aan Imperial College London, is een van de drijvende krachten achter een langlopend project om (onderdelen van) het beroemde bewijs van de laatste stelling van Fermat in Lean te formaliseren, een project dat vanwege de omvang van het oorspronkelijke bewijs jaren in beslag zal nemen en waarbij formalisatiehulpmiddelen een steeds grotere rol spelen.
Ook buiten de grote techbedrijven wordt gewerkt aan open modellen voor dit doel: DeepSeek AI heeft met zijn DeepSeek-Prover-modellen een open-source alternatief neergezet, dat op de veelgebruikte miniF2F-benchmark, een verzameling olympiadeproblemen die is opgesteld om formele bewijssystemen onderling te vergelijken, sterke resultaten liet zien.
Hoe ver is de techniek?
De vooruitgang van de afgelopen paar jaar is opvallend snel geweest, grotendeels dankzij de opkomst van grote taalmodellen. Op benchmarks met wiskundeolympiadeproblemen, zoals miniF2F, zijn de scores van AI-systemen sterk gestegen. Dat is echter een gecontroleerde, relatief overzichtelijke testomgeving, met problemen die weliswaar moeilijk zijn maar wel een beperkte, bekende reikwijdte hebben.
Het volledig autonoom formaliseren van een willekeurig onderzoeksartikel uit de wiskundeliteratuur is een ander verhaal, en daarin zijn de huidige systemen nog verre van betrouwbaar. Natuurlijke taal blijft dubbelzinnig, notatieconventies verschillen sterk per vakgebied en zelfs per auteur, en veel bewijzen leunen op achtergrondkennis die nergens expliciet wordt opgeschreven maar bij vakgenoten als bekend wordt verondersteld.
Een specifiek en hardnekkig probleem is wat wel het "formalisatiegat" wordt genoemd: een formele stelling kan door de proof assistant als syntactisch correct worden geaccepteerd, terwijl ze bij nadere inspectie toch net iets anders beweert dan de oorspronkelijke, informele bewering. De computer controleert dan feilloos of de formele tekst logisch klopt, maar niet of die formele tekst wel een getrouwe vertaling is van wat de wiskundige oorspronkelijk bedoelde. Die controle blijft mensenwerk.
Daarnaast is het opbouwen van uitgebreide formele bibliotheken zoals Mathlib nog altijd kostbaar: grote delen van de moderne wiskunde, vooral in snel evoluerende deelgebieden, zijn simpelweg nog niet geformaliseerd, waardoor een AI-systeem daar ook niet op kan voortbouwen. Per saldo functioneert autoformalisatie op dit moment vooral als hulpmiddel, een soort co-piloot voor wiskundigen die routinematige stappen kan overnemen of suggesties kan doen, en niet als vervanging van menselijke expertise of oordeel.
Wie werken eraan?
Binnen de grote technologiebedrijven is DeepMind, onderdeel van Google in het Verenigd Koninkrijk, een van de meest zichtbare spelers, met AlphaProof en AlphaGeometry als bekendste projecten. OpenAI in de Verenigde Staten deed rond 2020 met een project genaamd GPT-f vroeg verkennend werk op het raakvlak van taalmodellen en formeel bewijzen. Het Chinese DeepSeek AI heeft met zijn DeepSeek-Prover-modellen een prominente, open-source bijdrage geleverd.
Daarnaast draait veel van dit onderzoeksveld op non-profitorganisaties en academische gemeenschappen. De programmeertaal en proof assistant Lean, oorspronkelijk gestart door onderzoeker Leonardo de Moura, wordt tegenwoordig onderhouden door de Lean FRO (Lean Focused Research Organization), een non-profitorganisatie. Rond Lean is een wereldwijde vrijwilligersgemeenschap actief die de Mathlib-bibliotheek beheert en uitbreidt.
Aan Imperial College London in het Verenigd Koninkrijk leidt Kevin Buzzard onderzoek naar grootschalige formalisatieprojecten, terwijl Terence Tao vanuit de University of California, Los Angeles (UCLA) in de Verenigde Staten een prominente pleitbezorger is van formele methoden in de onderzoekswiskunde. De alternatieve proof assistant Coq, tegenwoordig Rocq geheten, wordt ontwikkeld rond het Franse onderzoeksinstituut Inria, terwijl Isabelle/HOL zijn wortels heeft aan de TU München in Duitsland en de University of Cambridge in het Verenigd Koninkrijk. Zo strekt het onderzoeksveld zich uit over Noord-Amerika, Europa en Azië, met een mix van bedrijfslabs, universiteiten en onafhankelijke non-profitorganisaties.