- Google entwickelte AlphaZero, das ĂŒbermenschliche FĂ€higkeiten im Brettspiel Go erlangte. AlphaProof, eine Kombination aus groĂem Sprachmodell und KI-Algorithmus, bewĂ€ltigt knifflige mathematische Beweise, darunter Aufgaben der Internationalen Mathematik-Olympiade 2024. AlphaGeometry, ein weiteres Programm, löst Geometrieprobleme und wurde kĂŒrzlich verbessert. Beide Programme bewiesen Ă€hnliche FĂ€higkeiten wie ein Silbermedaillengewinner der IMO. Die neuro-symbolische Methode kombiniert maschinelles Lernen mit konventioneller Programmierung und könnte die Logik und Vernunft von KI-Systemen in der Mathematik und anderen Bereichen verbessern.
Vor einigen Jahren entwickelte Google ein ungewöhnliches Programm, bevor die Ăra der Plaudertaschen begann. Dieses Programm, genannt AlphaZero, lernte durch unermĂŒdliche Ăbung, das Brettspiel Go mit ĂŒbermenschlicher Fertigkeit zu spielen. Nun haben Forscher der Firma eine Studie veröffentlicht, die die FĂ€higkeiten eines groĂen Sprachmodells (die KI hinter den heutigen Chatbots) mit denen von AlphaZero kombiniert, um Ă€uĂerst knifflige mathematische Beweise zu lösen.
Neues Konzept: AlphaProof
Ihr neues, frankensteinartiges Konstrukt namens AlphaProof zeigte seine FĂ€higkeiten, indem es mehrere Aufgaben der Internationalen Mathematik-Olympiade (IMO) 2024, einem renommierten Wettbewerb fĂŒr OberstufenschĂŒler, bewĂ€ltigte. AlphaProof nutzt das groĂe Sprachmodell Gemini, um natĂŒrlich formulierte Mathematikfragen in eine Programmiersprache umzuwandeln. Dies liefert das Trainingsmaterial fĂŒr einen zweiten Algorithmus, der durch Versuch und Irrtum lernt, wie man Beweise findet, die als korrekt bestĂ€tigt werden können.
Anfang dieses Jahres veröffentlichte Google DeepMind ein weiteres Programm namens AlphaGeometry, das ebenfalls ein Sprachmodell mit einem anderen KI-Ansatz kombiniert. AlphaGeometry verwendet Gemini, um Geometrieprobleme in eine Form zu ĂŒbertragen, die von einem Programm manipuliert und getestet werden kann, das mit geometrischen Elementen umgeht. Google kĂŒndigte heute auch eine neue und verbesserte Version von AlphaGeometry an.
Ergebnisse und Implikationen
Die Forscher fanden heraus, dass ihre beiden Mathematikprogramme Beweise fĂŒr IMO-Puzzles ebenso gut wie ein Silbermedaillengewinner liefern konnten. Von insgesamt sechs Problemen löste AlphaProof zwei Algebra-Probleme und ein Zahlentheorie-Problem, wĂ€hrend AlphaGeometry ein Geometrie-Problem löste. Manche Aufgaben wurden in Minuten gelöst, fĂŒr andere benötigte man jedoch mehrere Tage. Google DeepMind hat nicht offenbart, wie viel Rechenleistung fĂŒr die Probleme aufgewendet wurde.
Google DeepMind bezeichnet den fĂŒr AlphaProof und AlphaGeometry verwendeten Ansatz als “neuro-symbolisch”, da er das reine maschinelle Lernen (das die meisten Fortschritte in der KI der letzten Zeit bestimmt hat) mit der Sprache der konventionellen Programmierung kombiniert. “Was wir hier gesehen haben, ist, dass man den Ansatz, der so erfolgreich in Dingen wie AlphaGo war, mit groĂen Sprachmodellen kombinieren und etwas extrem FĂ€higes produzieren kann”, sagt der Google DeepMind-Forscher, der die Arbeit an AlphaZero leitete. Silver erklĂ€rt, die mit AlphaProof demonstrierten Techniken sollten theoretisch auf andere Bereiche der Mathematik ausgedehnt werden können.
Tendenzen und Zukunftsperspektiven
Die Forschung weckt die Aussicht, die schlimmsten Tendenzen groĂer Sprachmodelle zu ĂŒberwinden, indem Logik und Vernunft bodenstĂ€ndiger angewendet werden. So erstaunlich groĂe Sprachmodelle auch sein mögen, sie kĂ€mpfen oft damit, selbst grundlegende Mathematik zu erfassen oder logisch durch Probleme zu denken. In Zukunft könnte die neuro-symbolische Methode ein Mittel sein, um KI-Systemen zu ermöglichen, Fragen oder Aufgaben so zu formulieren, dass sie auf zuverlĂ€ssige Ergebnisse hingearbeitet werden. Auch OpenAI wird nachgesagt, an einem solchen System zu arbeiten.
Es gibt jedoch eine wesentliche EinschrĂ€nkung bei den heute vorgestellten Systemen, wie Silver anerkennt. Mathematische Lösungen sind entweder richtig oder falsch, wodurch AlphaProof und AlphaGeometry den richtigen Weg zur Lösung finden können. Viele reale Probleme â wie das perfekte Reiseprogramm zu erstellen â haben viele mögliche Lösungen und welche die beste ist, kann unklar sein. Silver meint, die Lösung fĂŒr unklare Fragen könnte darin liegen, dass ein Sprachmodell wĂ€hrend des Trainings versucht zu bestimmen, was eine “richtige” Antwort ausmacht. “Es gibt eine Vielzahl unterschiedlicher AnsĂ€tze, die ausprobiert werden können”, sagt er.
Silver betont auch, dass Google DeepMind Menschen Mathematikern nicht die Arbeit wegnehmen wird. “Wir streben danach, ein System zu schaffen, das alles beweisen kann, aber das ist nicht das Ende dessen, was Mathematiker tun”, sagt er. “Ein groĂer Teil der Mathematik besteht darin, Probleme zu stellen und zu finden, welche interessanten Fragen zu stellen sind. Man könnte dies als ein weiteres Werkzeug neben Rechenschieber, Taschenrechner oder computergestĂŒtzten Werkzeugen betrachten.”