Bislang scheiterten Computer daran, komplizierte mathematische Aussagen zu beweisen. Doch nun gelang es der KI AlphaGeometry, dutzende Aufgaben der Mathematik-Olympiade zu lösen.
KÜNSTLICHE INTELLIGENZ
Die Internationale Mathematik-Olympiade (IMO) ist der wohl renommierteste Schülerwettbewerb. Um die begehrten Bronze-, Silber- und Goldmedaillen wetteifern jedes Jahr Schülerinnen und Schüler aus aller Welt (2023 nahmen 112 Länder teil) – und schon bald könnten ihnen KI-Programme Konkurrenz machen.
Ein Team um Trieu H. Trinh von Google DeepMind und der New York University hat am 17. Januar 2024 in der Fachzeitschrift »Nature« ein neues KI-Programm namens Alpha-Geometry vorgestellt, das 25 von 30 gestellten Geometrie-Aufgaben aus vergangenen Mathematik-Olympiaden erfolgreich lösen konnte. Damit hatte die KI eine ähnliche Erfolgsquote wie die besten menschlichen Teilnehmer und Teilnehmerinnen, die beim Wettbewerb eine Goldmedaille gewinnen konnten. Außerdem fand AlphaGeometry eine allgemeinere Lösung zu einem Problem von der IMO im Jahr 2004, die Fachleuten bisher entgangen war.
»Mathematik-Olympiaden sind die weltweit renommiertesten Wettbewerbe zum Lösen von Theoremen«, schreiben Trinh und seine Kollegen in ihrer aktuellen Veröffentlichung. An zwei Tagen müssen die Schülerinnen und Schüler jeweils drei Aufgaben aus verschiedenen mathematischen Gebieten bearbeiten. Teilweise sind die Probleme so kompliziert, dass selbst Fachleute sie nicht lösen können. Die Aufgaben besitzen in der Regel kurze, elegante Lösungen, die jedoch viel Kreativität verlangen. Das macht sie aus Sicht der KI-Forschung besonders interessant. Denn bisher versagten selbst große Sprachmodelle wie GPT-4 von OpenAI bei solchen Aufgaben.
Einer der Gründe dafür, warum KI-Programme bislang an höherer Mathematik scheiterten, sind die mangelnden Datensätze. Große Sprachmodelle wie GPT-4 werden mit zweistelligen Gigabyte an Textdateien trainiert, was etwa 20 Millionen gefüllten DIN-A4-Seiten entspricht. Zwar gibt es viele mathematische Arbeiten, aber einen Beweis in eine für Computer verständliche Programmiersprache wie »Lean« zu übersetzen, erfordert sehr viel Arbeit. Im Bereich der Geometrie fällt das extrem schwer ins Gewicht: Dort sind die Beweise meist noch schwieriger zu formalisieren. Es gibt zwar speziell für die Geometrie entwickelte Programmiersprachen, doch diese lassen kaum Methoden aus anderen Bereichen zu. Wenn ein Beweis also einen Zwischenschritt erfordert, bei dem etwa kompl
