KI-System ist Medaillenanwärter bei Mathematik-Olympiade

Die Internationale Mathematik-Olympiade findet seit 1959 jährlich und immer in einem anderen Land statt. Jeder Staat darf sechs Teilnehmer entsenden, die Aufgaben aus verschiedenen Gebieten der Mathematik wie Algebra, Kombinatorik, Geometrie und der Zahlentheorie zu lösen haben. Erreicht man beim Lösen der kniffligen und komplexen Probleme bestimmte Punktezahlen, gibt es dafür Medaillen in den aus dem Sport bekannten Varianten.

Mehr als ein Sprachmodell

Um in dem Wettbewerb zu bestehen, braucht es die Fähigkeit, komplexe mathematische Theorien anzuwenden und verlässlich überprüfen zu können. Damit hatten auf Künstlicher Intelligenz (KI) basierende Systeme bisher durchaus Schwierigkeiten, wie das Team, dem auch der lange Zeit bei Google DeepMind in London und nun beim US-KI-Unternehmen Anthropic tätige Softwareentwickler Julian Schrittwieser aus Niederösterreich angehörte, in der Publikation darlegt. Während etwa landläufig bekannte KI-Anwendungen, wie ChatGPT, auf sogenannten "Großen Sprachmodellen" beruhen, die wiederum die Prozesse und Logiken menschlicher Sprache mittels Wahrscheinlichkeitsberechnungen und viel Training mit riesigen Datensätzen nachahmen, braucht es zum erfolgreichen Bearbeiten von Mathematik-Aufgaben andere Kompetenzen.

Ein solches System muss unzählige mathematische Konzepte weitgehend selbstständig ableiten, mit ihnen umgehen und "strenge" mathematische Beweise in einem mehr oder weniger unendlich großen Problemfeld durchführen können, so die Wissenschafterinnen und Wissenschafter, zu denen u.a. auch Demis Hassabis, Mitbegründer des in London ansässigen, 2014 von Google übernommenen Unternehmens DeepMind und Chemie-Nobelpreisträger 2024, gehörte. Es brauche also einen Ansatz, der schon mehr in Richtung komplexes Schlussfolgern geht, als es ein Sprachmodell tut.

Mathe lernen, wie ein Spiel

Dafür hat das Team sein System entwickelt, das mittels Lernen durch Verstärkung - also dem ständigen Versuchen von Lösungen, die entweder Erfolg oder Misserfolg bringen, und damit entweder zu einer Art Belohnung oder eben nicht führen - innerhalb einer Mathematik-Software namens "Lean" agiert. Während Sprachmodelle derzeit ihre Ergebnisse eben in Sprachform ausgeben "und gerne halluzinieren, produziert AlphaProof formelle Beweise in Lean, die automatisch verifiziert werden können", erklärte Schrittwieser gegenüber der APA. Das heiße auch, dass man den Lösungen für komplizierte Probleme "auch wirklich vertrauen" könne, so der Forscher, der das Projekt zusammen mit dem Erstautor der Studie, Thomas Hubert, gestartet und weitestgehend umgesetzt hat.

Diese Herangehensweise des maschinellen Lernens ermöglicht es, dass ein System mehr oder weniger selbstständig Millionen Aufgaben durchrechnet. So erlernten Softwareentwicklungen von DeepMind unter Mithilfe Schrittwiesers auch schon die Brettspiele Go, Schach oder das Programmieren auf sehr hohem Niveau.

System hat "Rennen zum Mond" ausgelöst

Das gelang nun auch mit AlphaProof: In Kooperation mit dem Geometrie-KI-Programm "AlphaGeometry" konnte das System vier von sechs Aufgaben der IMO 2024 lösen, berichten die Forschenden. Diese Leistung hätte für eine Silbermedaille gereicht, was deutlich über den Kapazitäten vorhergehender einschlägiger Systeme gelegen habe, wie Schrittwieser betonte.

Mit der Entwicklung sei man einen Schritt weiter auf dem Weg zu einem KI-Werkzeug gekommen, das Mathematikerinnen und Mathematikern in Zukunft beim Bewältigen komplexer Problemstellungen helfen kann, heißt es in der Arbeit. In einem Perspektivenartikel dazu attestiert Talia Ringer von der University of Illinois (USA) AlphaProof tatsächlich eine Art "Rennen zum Mond" ausgelöst zu haben, das darin gipfelte, dass heuer bereits Systeme Goldmedaillen-Niveau bei der IMO erreicht haben. Selbst wenn sich das Feld seither rasant weiterentwickelt habe, habe sich das Warten auf die technischen Details des Pionier-Systems "gelohnt". Man sehe hier, dass der Ansatz, KI Mathematik ähnlich "wie ein Spiel" lernen zu lassen, funktioniere. Trotz mancher Einschränkung sei das System das erste seiner Art, "das ich zum Schreiben von Beweisen als tatsächlich nützlich empfunden habe", so Ringer.

(S E R V I C E - )

(APA)