Einige Jahre bevor ChatGPT anfing, Unsinn von sich zu geben, hatte Google ein ganz anderes Programm für künstliche Intelligenz namens AlphaGo entwickelt, das durch unermüdliches Üben lernte, das Brettspiel Go mit übermenschlichen Fähigkeiten zu spielen.
Forscher des Unternehmens haben gerade eine Studie veröffentlicht, die die Fähigkeiten eines großen Sprachmodells (der KI hinter den heutigen Chatbots) mit denen von AlphaZero, einem Nachfolger von AlphaGo, der auch Schach spielen kann, kombiniert, um sehr heikle mathematische Beweise zu lösen.
Ihre neue Frankenstein-Kreation namens AlphaProof stellte ihr Können unter Beweis, indem sie mehrere Probleme der Internationalen Mathematikolympiade (IMO) 2024, einem prestigeträchtigen Wettbewerb für Oberstufenschüler, anpackte.
AlphaProof nutzt das Gemini-Sprachmodell, um natürlich formulierte mathematische Fragen in eine Programmiersprache namens Lean umzuwandeln. Dies liefert das Trainingsmaterial für einen zweiten Algorithmus, der durch Versuch und Irrtum lernt, Beweise zu finden, die als richtig bestätigt werden können.
Anfang des Jahres stellte Google DeepMind einen weiteren mathematischen Algorithmus namens AlphaGeometry vor, der ebenfalls ein Sprachmodell mit einem anderen KI-Ansatz kombiniert. AlphaGeometry verwendet Gemini, um Geometrieprobleme in eine Form umzuwandeln, die von einem Programm, das geometrische Elemente verarbeitet, manipuliert und getestet werden kann. Google hat heute außerdem eine neue und verbesserte Version von AlphaGeometry angekündigt.
Die Forscher fanden heraus, dass ihre beiden Mathematikprogramme Beweise für IMO-Rätsel sowie einen Silbermedaillengewinner liefern könnten. Die Programme lösten zwei Algebra-Aufgaben und eine Zahlentheorie-Aufgabe von insgesamt sechs. Ein Problem konnte er innerhalb von Minuten beheben, die anderen brauchten jedoch mehrere Tage. Google DeepMind hat nicht bekannt gegeben, wie viel Rechenleistung es zur Lösung dieser Probleme eingesetzt hat.
Google DeepMind nennt den für AlphaProof und AlphaGeometry verwendeten Ansatz „neurosymbolisch“, weil sie das reine maschinelle Lernen eines künstlichen neuronalen Netzwerks, der Technologie, die den neuesten Fortschritten in der KI zugrunde liegt, mit der Sprache der konventionellen Programmierung kombinieren.
„Wir haben hier festgestellt, dass es möglich ist, den so erfolgreichen Ansatz und Tools wie AlphaGo mit großen Sprachmodellen zu kombinieren und etwas äußerst Leistungsfähiges zu produzieren“, sagt Google-Forscher David Silver, der die Arbeit an AlphaZero leitete. Silver sagt, dass die mit AlphaProof demonstrierten Techniken theoretisch auch auf andere Bereiche der Mathematik anwendbar sein sollten.
Tatsächlich eröffnet diese Forschung die Aussicht, die schlimmsten Tendenzen wichtiger Sprachmodelle durch eine fundiertere Anwendung von Logik und Argumentation anzugehen. So wunderbar großartige Sprachmodelle auch sein können, oft haben sie Schwierigkeiten, auch nur grundlegende Mathematik zu verstehen oder Probleme logisch zu lösen.
Künftig könnte die neuronal-symbolische Methode es KI-Systemen ermöglichen, Fragen oder Aufgaben in ein begründbares Format umzuwandeln, das verlässliche Ergebnisse liefert. Auch OpenAI würde an einem solchen System arbeiten, unter dem Codenamen „Strawberry“.
Die heute vorgestellten Systeme weisen jedoch eine wesentliche Einschränkung auf, wie Silver einräumt. Mathematische Lösungen sind entweder richtig oder falsch, sodass AlphaProof und AlphaGeometry die richtige Antwort finden können. Für viele reale Probleme (z. B. die Suche nach der idealen Route für eine Reise) gibt es viele mögliche Lösungen, und es kann schwierig sein, zu wissen, welche die ideale ist. Silver sagt, die Lösung für die mehrdeutigen Fragen könnte darin bestehen, dass ein linguistisches Modell während des Trainings versucht, herauszufinden, was eine „gute“ Antwort darstellt. „Es gibt eine ganze Reihe verschiedener Lösungen, die man ausprobieren kann“, sagt er.
Silver betont außerdem sorgfältig, dass Google DeepMind Mathematiker nicht arbeitslos machen wird. „Unser Ziel ist es, ein System bereitzustellen, das alles beweisen kann, aber das ist noch nicht das Ende der Arbeit der Mathematiker“, sagt er. „In der Mathematik geht es oft darum, Probleme zu stellen und interessante Fragen zu finden. Dies könnte als weiteres Werkzeug betrachtet werden, genau wie ein Rechenschieber, ein Taschenrechner oder ein Berechnungstool. »