OpenAI præsenterer GamePad: AI lærer at bevise matematiske teoremer
OpenAI har udviklet et nyt system kaldet GamePad, som anvender maskinlæring til at bevise matematiske teoremer i bevisassistenten Coq. Systemet repræsenterer et skridt mod at kombinere kunstig intelligens med formel matematisk bevisførelse.
GamePad fungerer som et læringsmiljø, hvor AI-modeller kan trænes til at konstruere maskin-verificerbare beviser trin for trin. I modsætning til traditionel automatiseret teorem-bevisførelse udnytter systemet menneskeligt tilsyn gennem interaktive beviser.
To centrale opgaver
Forskerne bag projektet har fokuseret på to hovedopgaver: Positionsevaluering, hvor systemet forudsiger antallet af bevistrin, der er tilbage, og taktikforudsigelse, hvor det forsøger at forudsige det næste trin i beviset.
I deres forskning har teamet testet GamePad på både simple algebraiske omskrivningsproblemer og mere avancerede formuleringer, herunder dele af den berømte Feit-Thompson-sætning – et centralt resultat inden for gruppeteori.
Potentiale for fremtiden
Projektet, som blev præsenteret i 2018, peger på potentialet i at anvende moderne maskinlæringsmetoder på formelle matematiske beviser. Interactive theorem provers som Coq giver en unik mulighed for at træne AI-systemer med struktureret, verificerbar feedback.
Forskningen er udført af Daniel Huang, Prafulla Dhariwal, Dawn Song og Ilya Sutskever og repræsenterer OpenAI’s fortsatte udforskning af AI’s anvendelse inden for komplekse, logiske domæner.
