AI olympisch

13.3.2024

Die Künstliche Intelligenz (Artificial Intelligence, AI) ist Anfang des Jahres mit einer Goldmedaille auf der Internationalen Mathematik Olympiade (IMO) ausgezeichnet worden. Ins Rennen geschickt wurde die AI-Anwendung "AlphaGeometry".

Zum Hintergrund:

Die hohe Kunst der Mathematik ist das Beweisen allgemeingültiger Sätze und Theoreme. Bislang konnten die Wissenschaftler an dieser Stelle kaum Hilfe durch Künstliche Intelligenz erwarten. Eine KI namens „AlphaGeometry“ verblüfft jetzt mit ihren Fähigkeiten. [3]

Einfache mathematische Berechnungen kann eine Künstliche Intelligenz wie ChatGPT problemlos bewältigen. Aber das war ja auch schon bislang mit Computern und Taschenrechnern möglich. Mathematiker fühlen sich indes grob missverstanden, wenn man ihre Kunst lediglich als einen professionellen Umgang mit Zahlen ansieht.

Das Besondere an mathematischen „Wahrheiten“ ist, dass sie – einmal korrekt bewiesen, für alle Ewigkeit gültig sind – während in den Naturwissenschaften jedes Wissen grundsätzlich vorläufig bleibt und unter dem Vorbehalt der Falsifizierung steht.

Dazu ein einfaches Beispiel aus dem Geometrie-Unterricht in der Schule. „In jedem Dreieck ist die Summe seiner drei Winkel 180 Grad.“ Dieses Theorem wurde bereits in der Antike bewiesen. An seiner Gültigkeit wird sich auch in Zukunft nichts ändern.

Das Beweisen von Theoremen gehört also zum Kerngeschäft von Mathematikern. Der Beweis bestimmter Aussagen ist dabei so kompliziert, dass Mathematiker bislang jahrelang daran arbeiten. Und es gibt eine Reihe „ungelöster Probleme“ für deren Bewältigung sogar Millionenbeträge ausgesetzt sind.

Das AI-System AlphaGeometry ist auf das Beweisen geometrischer Theoreme spezialisiert. Es kombiniert die Vorhersagekraft eines neuronalen Sprachmodells mit einer regelgebundenen Deduktionsmaschine, die zusammenarbeiten, um Lösungen zu finden. Und durch die Entwicklung einer Methode zur Generierung eines riesigen Pools synthetischer Trainingsdaten – 100 Millionen einzigartige Beispiele – lässt sich AlphaGeometry ohne menschliche Demonstrationen trainieren und so den Datenengpass umgehen.

Zwei Beispiele für Beweisführungen durch AlphaGeometry [2]:

Sei ABC ein beliebiges Dreieck mit AB=AC. Beweise, dass Winkel ABC= Winkel BCA ist.

Sei ABC ein spitzes Dreieck. Sei (O) sein Umkreis, H sein Orthozentrum und F der Fuß der Höhe von A. Sei M der Mittelpunkt von BC. Sei Q der Punkt auf (O), so dass QH1 QA und sei K der Punkt auf (O), so dass KH1 KQ. Beweise, dass die Umkreise (O,) und (O) der Dreiecke FKM und KQH tangential zueinander sind.
Die blauen Elemente sind hinzugefügte Konstrukte. Die Lösung von AlphaGeometry besteht aus 109 logischen Schritten.

Die Forschergruppe um Trieu H. Trinh berichtet in Nature [4]:

Bei einem Testsatz von 30 aktuellen Problemen auf Olympia-Niveau löst AlphaGeometry 25 und übertrifft damit die bisher beste Methode, die nur zehn Probleme löst, und nähert sich der Leistung eines durchschnittlichen Goldmedaillengewinners der Internationalen Mathematischen Olympiade (IMO).

und schließt mit der Feststellung:

AlphaGeometry ist das erste Computerprogramm, das die Leistung eines durchschnittlichen IMO-Teilnehmers beim Beweis der Sätze der euklidischen Ebenengeometrie übertrifft und starke Computeralgebra und Suchbasislinien übertrifft. Insbesondere haben wir mit AlphaGeometry einen neurosymbolischen Ansatz für den Theorembeweis durch groß angelegte Erkundungen von Grund auf demonstriert und dabei die Notwendigkeit von von Menschen kommentierten Beweisbeispielen und von Menschen kuratierten Problemstellungen umgangen. Unsere Methode zum Generieren und Trainieren von Sprachmodellen auf rein synthetischen Daten bietet einen allgemeinen Orientierungsrahmen für mathematische Bereiche, die mit dem gleichen Datenknappheitsproblem konfrontiert sind.

AlphaGeometry-Teammitglieder, von links, Yuhuai Wu, Trieu H. Trinh, Quoc V. Le und Thang Luong vor Googles Gradient Canopy-Gebäude in Mountain View, Kalifornien.

Thang Luong, rechts, bespricht das I.M.O. 2015 Problem 3, das AlphaGeometry letzten Monat mit seinen Mathematiklehrern für die Olympiade, Trinh Le, Mitte, und Dung Tran in Ho-Chi-Minh-Stadt, Vietnam, gelöst hat.

Evan Chen (Mathematiklehrer und Olympiad Goldmedaillengewinner): „Die Ergebnisse von AlphaGeometry sind beeindruckend, weil sie sowohl überprüfbar als auch sauber sind. Frühere KI-Lösungen für beweisbasierte Wettbewerbsprobleme waren manchmal ein Glücksfall (die Ergebnisse sind nur manchmal korrekt und müssen von Menschen überprüft werden). AlphaGeometry hat diese Schwäche nicht: Seine Lösungen haben eine maschinenüberprüfbare Struktur. Dennoch ist die Ausgabe immer noch für Menschen lesbar. Man hätte sich ein Computerprogramm vorstellen können, das Geometrieprobleme mithilfe von Brute-Force-Koordinatensystemen löst: Denken Sie an Seiten um Seiten langwieriger algebraischer Berechnungen. AlphaGeometry ist das nicht. Es verwendet klassische Geometrieregeln mit Winkeln und ähnlichen Dreiecken, genau wie die Schüler es tun.“

Anfang Dezember besuchte Dr. Luong seine alte High School in Ho-Chi-Minh-Stadt, Vietnam, und zeigte AlphaGeometry seinem ehemaligen Lehrer und I.M.O. Trainer, Le Ba Khanh Trinh. Dr. Lê war der beste Goldmedaillengewinner der Olympiade 1979 und gewann einen Sonderpreis für seine elegante Geometrielösung. Dr. Lê analysierte einen der Beweise von AlphaGeometry und fand ihn bemerkenswert, aber unbefriedigend. Dr. Luong erinnerte sich: „Er fand ihn mechanisch und sagte, ihm fehle die Seele, die Schönheit einer Lösung, nach der er sucht.“

Dr. Trinh hatte zuvor Evan Chen, einen Mathematik-Doktoranden am M.I.T., I.M.O. Trainer und Olympia-Goldmedaillengewinner, gebeten, einige der Arbeiten von AlphaGeometry zu überprüfen. Das sei alles korrekt, sagte Herr Chen und fügte hinzu, dass ihn die Art und Weise, wie das System die Lösungen gefunden habe, fasziniert habe.

„Ich würde gerne wissen, wie die Maschine darauf kommt“, sagte er. „Aber ich meine, im Übrigen würde ich auch gerne wissen, wie Menschen zu Lösungen kommen.“ [1]

Danksagungen
Dieses Projekt ist eine Zusammenarbeit zwischen dem Google DeepMind-Team und der Informatikabteilung der New York University. Zu den Autoren dieser Arbeit gehören Trieu Trinh, Yuhuai Wu, Quoc Le, He He und Thang Luong. Wir danken Rif A. Saurous, Denny Zhou, Christian Szegedy, Delesley Hutchins, Thomas Kipf, Hieu Pham, Petar Veličković, Edward Lockhart, Debidatta Dwibedi, Kyunghyun Cho, Lerrel Pinto, Alfredo Canziani, Thomas Wies, He He's Forschungsgruppe, Evan Chen , Mirek Olsak, Patrik Bak für ihre Hilfe und Unterstützung. Wir möchten uns auch bei der Führung von Google DeepMind für die Unterstützung bedanken, insbesondere bei Ed Chi, Koray Kavukcuoglu, Pushmeet Kohli und Demis Hassabis.

Quellen:

[1] https://www.nytimes.com/2024/01/17/science/ai-computers-mathematics-olympiad.html
[2] https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/
[3] https://www.welt.de/wissenschaft/article249677660/AlphaGeometry-Mathematik-Goldmedaille-fuer-Kuenstliche-Intelligenz.html
https://imo-grand-challenge.github.io
[4] https://www.nature.com/articles/s41586-023-06747-5 <-- Original Artikel in Nature
https://www.unite.ai <-- AI-Tools (Cryptohandel u.a.)
https://www.p-domain.de/ratgeber-lifestyle/mathe.html