Nachricht

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Maschinenherzbericht

Redaktion von Machine Heart

Mit dem großen Gemini-Modell und dem AlphaZero-Lernalgorithmus zur Verstärkung können Sie Geometrie, Algebra und Zahlentheorie beherrschen.

Für KI ist die Mathematikolympiade kein Problem mehr.

Am Donnerstag hat die künstliche Intelligenz von Google DeepMind eine Meisterleistung vollbracht: Sie nutzte KI, um meiner Meinung nach die eigentliche Frage der diesjährigen Internationalen Mathematikolympiade zu lösen, und war nur einen Schritt davon entfernt, die Goldmedaille zu gewinnen.

Der IMO-Wettbewerb, der gerade letzte Woche zu Ende ging, hatte sechs Fragen zu Algebra, Kombinatorik, Geometrie und Zahlentheorie. Das von Google vorgeschlagene hybride KI-System beantwortete vier Fragen richtig und erzielte 28 Punkte und erreichte damit die Silbermedaille.

Anfang dieses Monats hatte der UCLA-Professor Terence Tao gerade die KI-Mathematische Olympiade (AIMO Progress Award) mit einem Millionenpreis gefördert. Unerwarteterweise hatte sich das Niveau der KI-Problemlösung vor Juli auf dieses Niveau verbessert.

Meiner Meinung nach, beantworten Sie die Fragen gleichzeitig und stellen Sie die schwierigsten Fragen richtig.

IMO ist der älteste, größte und prestigeträchtigste Wettbewerb für junge Mathematiker, der seit 1959 jährlich stattfindet. In jüngster Zeit wurde der IMO-Wettbewerb auch weithin als große Herausforderung im Bereich des maschinellen Lernens anerkannt und hat sich zu einem idealen Maßstab für die Messung der fortgeschrittenen mathematischen Denkfähigkeiten von Systemen der künstlichen Intelligenz entwickelt.

Beim diesjährigen IMO-Wettbewerb gelang AlphaProof und AlphaGeometry 2, die vom DeepMind-Team gemeinsam entwickelt wurden, ein Meilenstein.

Darunter ist AlphaProof ein verstärkendes Lernsystem für formales mathematisches Denken, und AlphaGeometry 2 ist eine verbesserte Version des Geometrielösungssystems AlphaGeometry von DeepMind.

Dieser Durchbruch zeigt das Potenzial der künstlichen allgemeinen Intelligenz (AGI) mit fortschrittlichen mathematischen Denkfähigkeiten zur Erschließung neuer Bereiche der Wissenschaft und Technologie.

Wie hat das KI-System von DeepMind am IMO-Wettbewerb teilgenommen?

Vereinfacht ausgedrückt werden diese mathematischen Probleme zunächst manuell in eine formale mathematische Sprache übersetzt, damit das KI-System sie verstehen kann. Im offiziellen Wettbewerb reichen menschliche Teilnehmer ihre Antworten in zwei Sitzungen (zwei Tagen) ein, wobei die Zeitbegrenzung für jede Sitzung 4,5 Stunden beträgt. Das aus AlphaProof+AlphaGeometry 2 bestehende KI-System löste ein Problem in wenigen Minuten, die Lösung anderer Probleme dauerte jedoch drei Tage. Wenn Sie sich jedoch strikt an die Regeln halten, ist im System von DeepMind eine Zeitüberschreitung aufgetreten. Einige Leute spekulieren, dass dies eine Menge brutaler Gewalt zum Knacken beinhalten könnte.

Laut Google löste AlphaProof zwei algebraische Probleme und ein zahlentheoretisches Problem, indem es die Antworten ermittelte und deren Richtigkeit bewies. Dazu gehört das schwierigste Problem des Wettbewerbs, das bei der diesjährigen IMO nur fünf Teilnehmer gelöst haben. Und AlphaGeometry 2 beweist ein Geometrieproblem.

Lösung durch KI: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

Der IMO-Goldmedaillengewinner und Fields-Medaillengewinner Timothy Gowers und der zweifache IMO-Goldmedaillengewinner Dr. Joseph Myers, Vorsitzender des IMO 2024 Problem Selection Committee, bewerteten die Lösungen des kombinierten Systems gemäß den IMO-Bewertungsregeln.

Jede der sechs Fragen ist 7 Punkte wert, was einer maximalen Gesamtpunktzahl von 42 Punkten entspricht. Das System von DeepMind erhielt eine Endpunktzahl von 28, was bedeutet, dass alle vier gelösten Probleme eine perfekte Punktzahl erhielten – was der höchsten Punktzahl in der Silbermedaillenkategorie entspricht. Die diesjährige Goldmedaillenschwelle lag bei 29 Punkten und 58 der 609 Spieler im offiziellen Wettbewerb gewannen Goldmedaillen.

Diese Grafik zeigt die Leistung des künstlichen Intelligenzsystems Google DeepMind im Vergleich zu menschlichen Konkurrenten auf der IMO 2024. Das System erzielte 28 von insgesamt 42 Punkten und erreichte damit das gleiche Niveau wie der Silbermedaillengewinner des Wettbewerbs. Darüber hinaus können in diesem Jahr 29 Punkte die Goldmedaille gewinnen.

AlphaProof: eine formale Argumentationsmethode

Unter den von Google verwendeten hybriden KI-Systemen ist AlphaProof ein selbst trainiertes System, das die formale Sprache Lean nutzt, um mathematische Aussagen zu beweisen. Es kombiniert ein vorab trainiertes Sprachmodell mit dem AlphaZero-Algorithmus für verstärktes Lernen.

Unter diesen bieten formale Sprachen wichtige Vorteile für die formale Überprüfung der Richtigkeit mathematischer Argumentationsbeweise. Bisher war dies beim maschinellen Lernen nur begrenzt von Nutzen, da die Menge der von Menschen geschriebenen Daten sehr begrenzt war.

Im Gegensatz dazu liefern auf natürlicher Sprache basierende Methoden trotz des Zugriffs auf größere Datenmengen Zwischenschritte und Lösungen, die vernünftig erscheinen, aber falsch sind.

Google DeepMind schlägt eine Brücke zwischen diesen beiden komplementären Bereichen, indem es das Gemini-Modell verfeinert, um Problemstellungen in natürlicher Sprache automatisch in formale Aussagen zu übersetzen und so eine große Bibliothek formaler Probleme mit unterschiedlichen Schwierigkeitsgraden zu erstellen.

Bei einem mathematischen Problem generiert AlphaProof mögliche Lösungen und beweist diese dann, indem es nach möglichen Beweisschritten in Lean sucht. Jede gefundene und verifizierte Beweislösung wird verwendet, um das Sprachmodell von AlphaProof zu stärken und seine Fähigkeit zur Lösung nachfolgender anspruchsvollerer Probleme zu verbessern.

Um AlphaProof zu trainieren, hat Google DeepMind in den Wochen vor dem IMO-Wettbewerb Millionen mathematischer Probleme bewiesen oder widerlegt, die ein breites Spektrum an Schwierigkeiten und Themen abdeckten. Während des Wettbewerbs wird außerdem eine Trainingsschleife angewendet, um den Beweis selbst generierter Wettbewerbsproblemvarianten zu stärken, bis eine vollständige Lösung gefunden ist.

Infografik zum AlphaProof Reinforcement Learning-Trainingsschleifenprozess: Etwa eine Million informelle mathematische Probleme werden vom formalen Netzwerk in formale mathematische Sprache übersetzt. Der Löser durchsucht dann das Netzwerk nach Beweisen oder Widerlegungen des Problems und trainiert sich nach und nach selbst, anspruchsvollere Probleme mithilfe des AlphaZero-Algorithmus zu lösen.

Wettbewerbsfähigeres AlphaGeometry 2

AlphaGeometry 2 ist eine deutlich verbesserte Version der mathematischen KI AlphaGeometry, die dieses Jahr im Nature-Magazin erschien. Es handelt sich um ein neurosymbolisches Hybridsystem, bei dem das Sprachmodell auf Gemini basiert und von Grund auf auf einer Größenordnung mehr synthetischen Daten trainiert wird als sein Vorgänger. Dies hilft dem Modell, anspruchsvollere geometrische Probleme zu lösen, einschließlich solcher zu Objektbewegungen und Gleichungen für Winkel, Proportionen oder Entfernungen.

AlphaGeometry 2 verfügt über eine symbolische Engine, die zwei Größenordnungen schneller ist als ihr Vorgänger. Wenn neue Probleme auftreten, ermöglichen neuartige Mechanismen zum Wissensaustausch erweiterte Kombinationen verschiedener Suchbäume, um komplexere Probleme zu lösen.

Vor dem diesjährigen Wettbewerb konnte AlphaGeometry 2 83 % aller historischen IMO-Geometrieprobleme der letzten 25 Jahre lösen, verglichen mit nur 53 % beim Vorgänger. In IMO 2024 löste AlphaGeometry 2 Problem 4 innerhalb von 19 Sekunden nach Erhalt seiner Formalisierung.

Ein Beispiel für Frage 4 erfordert den Nachweis, dass die Summe von ∠KIL und ∠XPY gleich 180° ist. AlphaGeometry 2 schlägt vor, Punkt E auf der Linie BI so zu konstruieren, dass ∠AEB = 90°. Punkt E hilft dabei, dem Mittelpunkt L des Liniensegments AB eine Bedeutung zu geben, wodurch viele Paare ähnlicher Dreiecke wie ABE ~ YBI und ALE ~ IPC entstehen, um die Schlussfolgerung zu beweisen.

Google DeepMind berichtet außerdem, dass Forscher im Rahmen der IMO-Arbeit auch mit einem neuen, auf Gemini basierenden System zum Schließen natürlicher Sprache und einem hochmodernen System zum Schließen natürlicher Sprache experimentieren, in der Hoffnung, erweiterte Fähigkeiten zur Problemlösung zu erreichen. Das System erfordert keine Übersetzung von Fragen in formale Sprache und kann mit anderen KI-Systemen kombiniert werden. Im Test der diesjährigen IMO-Wettbewerbsfragen zeigte es „großes Potenzial“.

Google erforscht weiterhin KI-Methoden zur Weiterentwicklung des mathematischen Denkens und plant, bald weitere technische Details zu AlphaProof zu veröffentlichen.

Wir freuen uns auf eine Zukunft, in der Mathematiker KI-Tools nutzen werden, um Hypothesen zu erforschen, mutige neue Ansätze zur Lösung langjähriger Probleme auszuprobieren und zeitaufwändige Elemente von Beweisen schnell fertigzustellen – und KI-Systeme wie Gemini werden dabei einen großen Unterschied machen Mathematik und mehr Der Aspekt des breiten Denkens wird noch wirkungsvoller.

Forschungsgruppe

Google sagte, die neue Forschung sei von der Internationalen Mathematikolympiade unterstützt worden, und außerdem:

Die AlphaProof-Entwicklung wurde von Thomas Hubert, Rishi Mehta und Laurent Sartran geleitet; zu den wichtigsten Mitwirkenden zählen Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser, Ottavia Bertolli, Borja Ibarz, Edward Lockhart, Edward Hughes, Mark Rowland und Grace Margand.

Unter ihnen waren Aja Huang, Julian Schrittwieser, Yannick Schroecker und andere Mitglieder vor 8 Jahren (2016) auch Kernmitglieder des AlphaGo-Papiers. Vor acht Jahren erlangte AlphaGo Berühmtheit, das sie auf Basis von Reinforcement Learning entwickelten. Acht Jahre später glänzt das verstärkende Lernen in AlphaProof erneut. Jemand beklagte sich im Freundeskreis: RL ist so zurück!

Die Arbeiten zu AlphaGeometry 2 und natürlicher Sprachinferenz werden von Thang Luong geleitet. Die Entwicklung von AlphaGeometry 2 wurde von Trieu Trinh und Yuri Chervonyi geleitet, mit wichtigen Beiträgen von Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang und Marcelo Menegali.

Darüber hinaus sind David Silver, Quoc Le, Hassabis und Pushmeet Kohli für die Koordination und Leitung des gesamten Projekts verantwortlich.

Referenzinhalt:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/