DMZ – WISSENSCHAFT ¦ Sarah Koller ¦ 
Die Fähigkeit, mathematische Theoreme auf Olympiadenniveau zu beweisen, stellt einen bedeutenden Meilenstein im automatisierten Denken auf menschlichem Niveau dar. Dies wird in der aktuellen Studie von Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He und Thang Luong verdeutlicht, die im Nature Journal veröffentlicht wurde.
Die Beweisführung mathematischer Theoreme auf Olympiadenniveau gilt als besonders schwierig und anspruchsvoll, insbesondere unter den besten Talenten der Welt im Bereich der voruniversitären Mathematik. Aktuelle maschinenlernbasierte Ansätze stoßen jedoch an Grenzen, da die Übersetzung menschlicher Beweise in maschinenverifizierbare Formate kostenintensiv ist. Dieses Problem verschärft sich im Bereich der Geometrie aufgrund einzigartiger Übersetzungsherausforderungen, was zu einem Mangel an Trainingsdaten führt. Die Autoren schlagen eine Lösung namens AlphaGeometry vor – einen Beweisführer für die euklidische Geometrie, der auf der Synthese von Millionen von Theoremen und Beweisen unterschiedlicher Komplexitätsgrade ohne menschliche Demonstrationen basiert.
AlphaGeometry ist ein neuro-symbolisches System, das ein neuronales Sprachmodell nutzt und von Grund auf auf großen synthetischen Daten trainiert wurde. Es leitet einen symbolischen Schlussfolgerungsmotor durch unendlich viele Verzweigungspunkte in schwierigen Problemen der Geometrie. In Tests mit 30 aktuellen Olympiadenniveau-Problemen löst AlphaGeometry beeindruckende 25, wobei es die bisher besten Methoden übertrifft. Es produziert menschenlesbare Beweise und nähert sich der Leistung eines durchschnittlichen Internationalen Mathematik-Olympiade (IMO) Goldmedaillengewinners an.
Die Autoren betonen, dass herkömmliche maschinenlernbasierte Methoden in der Beweisführung Schwierigkeiten haben, bedingt durch den Mangel an menschlichen Beweisen in maschinenverifizierbaren Sprachen. Insbesondere die Geometrie hat aufgrund von Übersetzungsschwierigkeiten einen Mangel an Beweisbeispielen in allgemeinen mathematischen Sprachen. AlphaGeometry umgeht diese Herausforderung, indem es synthetische Daten verwendet und die Notwendigkeit menschlicher Beweise eliminiert. Durch die Verwendung von symbolischen Engines auf einer Vielzahl von zufälligen Theorempremissen extrahieren die Autoren 100 Millionen synthetische Theoreme und ihre Beweise, wobei viele mehr als 200 Beweisschritte haben.
Der Beweisführer AlphaGeometry erzielt herausragende Ergebnisse und übertrifft den bisherigen Stand der Technik erheblich. Er demonstriert, dass die Verwendung von synthetischen Daten eine erfolgreiche Methode für die Beweisführung ist und stellt einen vielversprechenden Ansatz für die Anwendung in anderen Bereichen dar. Die Studie zeigt nicht nur die technologischen Fortschritte, sondern hebt auch die Bedeutung der automatisierten Beweisführung auf Olympiadenniveau hervor.
Überblick über das neuro-symbolisches AlphaGeometry und wie es sowohl ein einfaches Problem als auch das IMO 2015 Problem 3 löst.
Die obere Reihe zeigt, wie AlphaGeometry ein einfaches Problem löst. a, Das einfache Beispiel und seine Darstellung. b, AlphaGeometry startet die Beweissuche, indem es den symbolischen Schlussfolgerungsmotor ausführt. Der Motor leitet erschöpfend neue Aussagen von den Theoremprämissen ab, bis das Theorem bewiesen ist oder neue Aussagen erschöpft sind. c, Da der symbolische Motor keinen Beweis findet, konstruiert das Sprachmodell einen Hilfspunkt, um den Beweiszustand zu erweitern, bevor der symbolische Motor einen erneuten Versuch unternimmt. Die Schleife setzt sich fort, bis eine Lösung gefunden ist. d, Für das einfache Beispiel endet die Schleife nach der ersten Hilfskonstruktion "D als Mittelpunkt von BC". Der Beweis besteht aus zwei weiteren Schritten, die beide die Mittelpunkt-Eigenschaften nutzen: "BD = DC" und "B, D, C sind kollinear", hervorgehoben in Blau. Die untere Reihe zeigt, wie AlphaGeometry das IMO 2015 Problem 3 (IMO 2015 P3) löst. e, Die IMO 2015 P3 Problemstellung und das Diagramm. f, Die Lösung von IMO 2015 P3 hat drei Hilfspunkte. In beiden Lösungen ordnen wir die Ausgaben des Sprachmodells (blau) interleaved mit den Ausgaben des symbolischen Motors an, um ihre Ausführungsreihenfolge zu reflektieren. Beachten Sie, dass der Beweis für IMO 2015 P3 in f stark gekürzt und bearbeitet ist, um Illustrationszwecken zu dienen.
Kommentar schreiben