“Het is vaak gemakkelijker om een model voor wiskunde te trainen als je een manier hebt om de antwoorden ervan te controleren (bijvoorbeeld in formele taal), maar er zijn relatief minder formele wiskundige gegevens online vergeleken met natuurlijke taal in vrije vorm (informele taal)”, zegt onderzoeker Katie. Collins van de Universiteit van Cambridge, gespecialiseerd in wiskunde en kunstmatige intelligentie, maar was niet bij het project betrokken.
Het overbruggen van deze kloof was het doel van Google DeepMind bij het creëren van AlphaProof, een op versterkend leren gebaseerd systeem dat is getraind om wiskundige uitspraken te bewijzen in de formele programmeertaal Lean. De sleutel is een versie van DeepMind’s Gemini AI die is verfijnd om wiskundige problemen die zijn geformuleerd in natuurlijke, informele taal automatisch te vertalen naar formele uitspraken, die gemakkelijker door AI kunnen worden verwerkt. Hierdoor ontstond een grote bibliotheek met formele wiskundeproblemen met verschillende moeilijkheidsgraden.
Het automatiseren van het proces van het vertalen van gegevens in een formele taal is een grote stap voorwaarts voor de wiskundige gemeenschap, zegt Wenda Li, docent hybride AI aan de Universiteit van Edinburgh, die het onderzoek beoordeelde maar niet bij het project betrokken was.
“We kunnen veel meer vertrouwen hebben in de juistheid van gepubliceerde resultaten als ze dit bewijssysteem kunnen formuleren, en het kan ook meer collaboratief worden”, voegt hij eraan toe.
Het Gemini-model werkt samen met AlphaZero – een versterkend leermodel dat door Google DeepMind is getraind om spellen als Go en schaken onder de knie te krijgen – om miljoenen wiskundige problemen te bewijzen of te weerleggen. Hoe meer problemen het met succes oploste, hoe beter AlphaProof werd in het oplossen van problemen van toenemende complexiteit.
Hoewel AlphaProof is getraind om problemen op te lossen in een breed scala aan wiskundige onderwerpen, is AlphaGeometry 2 – een verbeterde versie van het systeem aangekondigd door Google DeepMind in januari – geoptimaliseerd voor het oplossen van problemen die verband houden met de beweging van objecten en vergelijkingen met betrekking tot hoeken, verhoudingen en afstanden. . Omdat het op aanzienlijk meer synthetische gegevens was getraind dan zijn voorganger, kon het veel uitdagendere geometrievragen aan.