Nature News: KI ist bei der Lösung von Mathematik-Olympiade-Aufgaben in der High School den menschlichen Goldmedaillengewinnern nah

Künstliche Intelligenz (KI) hat bei der Internationalen Mathematik-Olympiade gelernt, schwierige Probleme zu lösen und dabei ein Niveau erreicht, das dem menschlicher Goldmedaillengewinner nahekommt.

Dieses KI-Modell namens AlphaGeometry wurde von einem gemeinsamen Team von Google DeepMind und der New York University entwickelt. Es handelt sich um ein KI-System, das Geometrieprobleme auf dem Niveau der Internationalen Mathematik-Olympiade lösen kann und heute im renommierten Wissenschaftsjournal Nature veröffentlicht wurde .

Berichten zufolge hat AlphaGeometry 25 der 30 Probleme auf dem neuesten Olympiadenniveau (ein mathematischer Theorembeweiswettbewerb für herausragende Highschool-Schüler) durch die autonome Synthese von Millionen von Theoremen und Beweisen gelöst. Dies entspricht in etwa der durchschnittlichen Leistung der Goldmedaillengewinner der Internationalen Mathematik-Olympiade und übertrifft das beste bisherige automatisierte Theorembeweissystem bei weitem.

Dieser Durchbruch stellt einen bedeutenden Fortschritt in der Fähigkeit der KI dar, mathematische Probleme autonom zu lösen, und ermöglicht es ihr, komplexe geometrische Herausforderungen ohne menschliche Demonstration zu bewältigen .

Die Forschung zeigt, dass KI das Potenzial hat, komplexe logische Herausforderungen auf nahezu menschlichem Niveau zu lösen – ein Hauptziel der KI-Forschung.

Insbesondere kann AlphaGeometry für Menschen lesbare Beweise generieren und hat sogar eine neue Version eines Theorems aus der Internationalen Mathematik-Olympiade 2004 entdeckt .

Die zugehörige Forschungsarbeit mit dem Titel „Solving olympiad geometry without human demonstrations“ (Olympiade-Geometrie ohne menschliche Demonstrationen lösen) wurde gerade in Nature veröffentlicht.

Ist es für KI schwierig, Probleme der Mathematik-Olympiade zu lösen?

Das Streben nach besseren Möglichkeiten zum Beweisen von Theoremen ist seit den 1950er Jahren ein Schwerpunkt der KI-Forschung. Die Mathematik-Olympiade ist der weltweit berühmteste Wettbewerb zum Beweisen von Theoremen. Sie geht auf das Jahr 1959 zurück und spielt eine wichtige Rolle bei der Entdeckung herausragender Talente.

Die Fragen der Internationalen Mathematik-Olympiade beinhalten in der Regel tiefgründige mathematische Theorien und abstrakte mathematische Konzepte und erfordern eigenständiges Denken, kreative Problemlösung und den Einsatz von Intuition. Diese Probleme erfordern oft ein hohes Maß an logischem Denken und kreativem Denken, über das menschliche Mathematiker verfügen , das aber über den Anwendungsbereich traditioneller Methoden des maschinellen Lernens hinausgeht.

Darüber hinaus lässt sich der menschliche Prozess der Lösung mathematischer Probleme im Vergleich zu anderen Bereichen nicht so einfach in große Datensätze übertragen, die für das Training verwendet werden können. Geometrie ist besonders schwierig zu übersetzen und Beispiele für Beweise in gängigen mathematischen Sprachen sind rar. Und die Sprache der Geometrie hat sehr präzise Definitionen und kann viele menschliche Beweise nicht ausdrücken, die Dinge außerhalb der Geometrie verwenden, wie beispielsweise komplexe Zahlen.

Abbildung | Nebeneinanderstellung des menschlichen Beweises und des AlphaGeometry-Beweises von IMO2000P6. Dies ist ein schwierigeres Problem (durchschnittliche menschliche Punktzahl = 1,05/7) mit einer großen Anzahl von Objekten in der Problemstellung. Links: Die menschliche Lösung verwendet komplexe Zahlen. Durch eine sorgfältige Wahl des Koordinatensystems wird das Problem erheblich vereinfacht und die Lösung ergibt sich auf natürliche Weise durch algebraische Manipulation. Rechts: Die AlphaGeometry-Lösung umfasst zwei Hilfskonstruktionen und über 100 Ableitungsschritte, von denen viele für Menschen äußerst mühsam durchzuführen sind. In diesem Fall ist die suchbasierte Lösung viel weniger lesbar und intuitiv. Eine strukturiertere Organisation, d. h. eine Beweisübersicht auf hoher Ebene, könnte die Lesbarkeit der AlphaGeometry-Lösung erheblich verbessern. In AlphaGeometry sind viele Ableitungsregeln auf hoher Ebene integriert, was dazu beiträgt, Ableitungen auf niedriger Ebene zu reduzieren und Beweisschritte zu vereinfachen. (Quelle: Dieses Dokument)

Der Mangel an ausreichenden Beispieldaten, insbesondere der Lösungsprozesse menschlicher Mathematiker, erschwert es Modellen des maschinellen Lernens, die Methoden zur Problemlösung zu erlernen und zu verstehen . Daher basieren aktuelle geometrische Methoden immer noch hauptsächlich auf symbolischen Methoden und manuell entworfenen, fest codierten Suchheuristiken.

Lösen Sie komplexe Probleme autonom und ohne Menschen

Die wichtigste Innovation von AlphaGeometry in dieser Forschung ist seine Fähigkeit, Millionen von Theoremen und Beweisen unterschiedlicher Komplexität zu synthetisieren, die autonom mithilfe eines von Grund auf neu trainierten neuronalen Sprachmodells trainiert werden. Dies bedeutet, dass AlphaGeometry in der Lage ist, komplexe Probleme selbstständig zu erlernen und zu lösen, ohne auf menschliche Eingaben angewiesen zu sein.

Neuronale Sprachmodelle eignen sich hervorragend zur Steuerung symbolischer Deduktionsmaschinen, die in der Lage sind, bei schwierigen Problemen eine große Anzahl von Verzweigungspunkten zu suchen. Durch die Einführung neuronaler Modelle ist AlphaGeometry in der Lage, bei der Lösung anspruchsvoller Probleme präzisere Schlussfolgerungen zu ziehen. Diese Methode der Kombination einer symbolischen Deduktionsmaschine und eines neuronalen Sprachmodells ist eine der wichtigsten Innovationen dieser Forschung.

Abbildung | Übersicht über AlphaGeometry und wie es einfache Probleme löst, sowie IMO2015-Problem 3. Die oberste Reihe zeigt, wie AlphaGeometry ein einfaches Problem löst. a) Einfaches Beispiel und sein Diagramm. b) Das Modell leitet die Beweissuche ein, indem es die symbolische Deduktionsmaschine ausführt. Die Engine leitet aus den Theoremprämissen erschöpfend neue Aussagen ab, bis das Theorem bewiesen ist oder die neuen Aussagen erschöpft sind. c) Da die symbolische Engine keinen Beweis findet, erstellt das Sprachmodell einen Hilfspunkt, um den Beweisstatus zu erhöhen, bevor die symbolische Engine es erneut versucht. Die Schleife wird fortgesetzt, bis eine Lösung gefunden ist. d) Für das einfache Beispiel endet die Schleife nach der ersten Hilfsstruktur „D als Mittelpunkt von BC“. Der Beweis besteht aus zwei weiteren Schritten, die beide die Mittelpunktseigenschaften ausnutzen: „BD = DC“ und „B, D und C sind kollinear.“ Die untere Reihe zeigt, wie AlphaGeometry das IMO 2015-Problem 3 (IMO 2015 P3) löst. e) IMO 2015 P3 Problemstellung und Diagramm. f Die Lösung von IMO 2015 P3 hat 3 Hilfspunkte. (Quelle: Dieses Dokument)

Obwohl AlphaGeometry beim Lösen von Geometrieproblemen auf olympischem Niveau bemerkenswerte Erfolge erzielt hat, weist es auch einige Einschränkungen auf .

Dem Artikel zufolge konzentriert sich AlphaGeometry hauptsächlich auf die Lösung von Geometrieproblemen auf olympischem Niveau und hat einen relativ engen Anwendungsbereich . Dies schränkt die Verallgemeinerung dieser Methode auf andere mathematische Bereiche oder praktische Probleme ein. Zukünftige Forschung muss untersuchen, wie die Methode erweitert werden kann, um ein breiteres Spektrum mathematischer Felder abzudecken.

Darüber hinaus nutzte das Forschungsteam groß angelegte künstliche synthetische Daten, um AlphaGeometry zu trainieren. Obwohl dem Modell dadurch eine große Bandbreite an Lernmaterialien zur Verfügung gestellt wurde, decken die synthetischen Daten möglicherweise immer noch nicht die gesamte Vielfalt und Komplexität echter mathematischer Probleme ab . Daher kann die Leistung des Modells in realen Szenarien durch unzureichende Daten beeinträchtigt werden.

Darüber hinaus ist AlphaGeometry zwar in der Lage, für Menschen lesbare Beweise zu generieren, die generierten Ergebnisse können jedoch bei extrem komplexen Schlussfolgerungen schwer verständlich werden. Dies macht es in manchen Fällen schwierig, den Denkprozess des Modells nachzuvollziehen und zu erklären .

KI hat großes Potenzial bei der Lösung mathematischer Probleme

In den letzten Jahren war der Einsatz von KI-Technologie zum Verstehen und Beweisen mathematischer Theoreme eine der Forschungsrichtungen, auf die sich Wissenschaftler konzentriert haben.

Beispielsweise können mithilfe von KI automatisierte Theorembeweissysteme entwickelt werden, die selbstständig mathematische Theoreme ableiten und beweisen können. Dieser Ansatz zielt darauf ab, den Aufwand manueller Beweise zu reduzieren und eine effizientere Beweismethode bereitzustellen.

Darüber hinaus kann KI auch zum Erstellen mathematischer Wissensgraphen verwendet werden, was dabei hilft, die Beziehungen zwischen mathematischen Konzepten in Graphstrukturen zu modellieren. Mithilfe dieses Graphen können die Argumentation und der Beweis von Theoremen verbessert werden, sodass das System das Wissenssystem im Bereich der Mathematik besser verstehen kann.

KI bietet auch Platz für die Entwicklung kreativen Denkens. In einigen Forschungsarbeiten werden generative Modelle wie Generative Adversarial Networks (GANs) verwendet, um neue Theoreme zu generieren, die mathematischen Strukturen und Spezifikationen entsprechen . Dieser Ansatz trägt dazu bei, das kreative Denken im Bereich der Mathematik zu erweitern und neue mathematische Konzepte und Schlussfolgerungen einzuführen.

Natürlich ist es noch ein weiter Weg, bis die KI in der Mathematik die gleiche Leistung erbringen kann wie die besten menschlichen Mathematiker.

Dennoch zeigt AlphaGeometry das Potenzial für die Anwendung von KI in der Mathematik. Diese Errungenschaft bringt nicht nur Innovationen in den Bereich der Mathematik, sondern eröffnet auch neue Möglichkeiten für die Anwendung von KI in anderen Bereichen.

Link zum Artikel: https://www.nature.com/articles/s41586-023-06747-5