DeepMinds KI löst Aufgaben der Internationalen Mathematik-Olympiade auf Silbermedaillen-Niveau

(deepmind.google)

3 Punkte von GN⁺ 2024-07-26 | 3 Kommentare | Auf WhatsApp teilen

Google DeepMinds AlphaProof und AlphaGeometry 2 haben Aufgaben der Internationalen Mathematik-Olympiade gelöst
- AlphaProof: ein auf Reinforcement Learning basierendes System für mathematisches Schlussfolgern
- AlphaGeometry 2: ein verbessertes System zum Lösen von Geometrieaufgaben
- Die beiden Systeme lösten bei der diesjährigen Internationalen Mathematik-Olympiade (IMO) 4 von 6 Aufgaben und erreichten damit ein Ergebnis auf Silbermedaillen-Niveau

KI-Erfolg beim Lösen komplexer mathematischer Probleme

Einführung in die IMO
- Der älteste und renommierteste Mathematikwettbewerb für Jugendliche, der seit 1959 jährlich stattfindet
- Die Wettbewerbsaufgaben stammen aus Algebra, Kombinatorik, Geometrie und Zahlentheorie
- Viele Fields-Medaillen-Gewinner haben an der IMO teilgenommen
Die IMO-Herausforderung für die KI-Systeme
- AlphaProof und AlphaGeometry 2 lösten die diesjährigen IMO-Aufgaben
- Die Aufgaben wurden nach den offiziellen Wettbewerbsregeln bewertet
- AlphaProof löste 2 Algebra-Aufgaben und 1 zahlentheoretische Aufgabe
- AlphaGeometry 2 löste 1 Geometrieaufgabe
- Die 2 kombinatorischen Aufgaben konnten nicht gelöst werden
- Insgesamt wurden 28 von 42 Punkten erreicht, was einem Ergebnis auf Silbermedaillen-Niveau entspricht

AlphaProof: ein formaler Ansatz für Schlussfolgerungen

Wie AlphaProof funktioniert
- Beweist mathematische Aussagen in der formalen Sprache Lean
- Kombination aus einem vortrainierten Sprachmodell und dem AlphaZero-Reinforcement-Learning-Algorithmus
- Übersetzt Aufgaben in natürlicher Sprache in formale Aussagen, um Probleme unterschiedlicher Schwierigkeit zu lösen
- Wenn eine Aufgabe vorgegeben wird, erzeugt AlphaProof Lösungskandidaten und beweist oder widerlegt sie
- Bewiesene Ergebnisse stärken das Sprachmodell von AlphaProof und verbessern so die Fähigkeit, schwierigere Probleme zu lösen
Trainingsprozess
- Trainiert durch das Beweisen oder Widerlegen von Millionen Aufgaben
- Auch während des Wettbewerbs wurde ein Trainingsloop angewendet, um Varianten der Aufgaben zu beweisen

Das wettbewerbsfähigere AlphaGeometry 2

Verbesserungen bei AlphaGeometry 2
- Ein auf Gemini basierendes Sprachmodell und ein neuro-symbolisches Hybridsystem
- Mit zehnmal mehr synthetischen Daten als die Vorgängerversion trainiert
- Verbesserte Geschwindigkeit und Genauigkeit beim Lösen von Geometrieaufgaben
- Verwendet beim Lösen neuer Aufgaben einen Mechanismus zum Wissensaustausch
Ergebnisse bei der IMO 2024
- Löste 83 % der Geometrieaufgaben der IMO aus den vergangenen 25 Jahren
- Löste Aufgabe 4 des diesjährigen Wettbewerbs in 19 Sekunden

Eine neue Frontier des mathematischen Schlussfolgerns

Experimente mit Systemen für Schlussfolgern in natürlicher Sprache
- Experimente mit einem auf Gemini basierenden System für Schlussfolgern in natürlicher Sprache
- Kann Probleme lösen, ohne sie in eine formale Sprache zu übersetzen
- Untersuchung der Möglichkeit, es mit anderen KI-Systemen zu kombinieren
Ausblick
- Mathematiker könnten gemeinsam mit KI-Tools neue Hypothesen erforschen, neue Lösungsansätze ausprobieren und den Beweisprozess verkürzen
- KI-Systeme wie Gemini verbessern mathematische und allgemeine Fähigkeiten zum Schlussfolgern

Zusammenfassung von GN⁺

AlphaProof und AlphaGeometry 2 zeigen das Potenzial von KI im mathematischen Schlussfolgern
Das Ergebnis auf Silbermedaillen-Niveau bei der Internationalen Mathematik-Olympiade belegt die Fähigkeit von KI, mathematische Probleme zu lösen
Es eröffnet Mathematikern die Möglichkeit, gemeinsam mit KI neue Lösungsansätze für Probleme zu erforschen
Ein Projekt mit ähnlicher Funktionalität sind Modelle zur Verarbeitung natürlicher Sprache wie OpenAIs GPT-3

3 Kommentare

chabulhwi 2024-07-26

Je mehr Mathematiker zur Entwicklung formaler Mathematikbibliotheken beitragen, desto leichter wird es sein, leistungsfähige Mathematik-KI zu entwickeln. Soweit ich weiß, gibt es derzeit in Korea drei Personen, die mathematische Theorien, die sie selbst in der Sprache des Beweisassistenten Lean formalisiert haben, in Leans Mathematikbibliothek Mathlib übertragen.

Ich habe mich im vergangenen Jahr ein wenig an der Portierung von Mathlib von Lean 3 auf Lean 4 beteiligt und in diesem Jahr einen bislang unbewiesenen Satz in der Lean-4-Batteries-Bibliothek bewiesen.

GN⁺ 2024-07-26

Hacker-News-Kommentare

Erster Kommentar
- Ich bin sehr begeistert von diesem Projekt, aber es ist unklar, wie viel der Computer zum Prozess beigetragen hat, die Mathematikaufgaben in eine formale Sprache zu übersetzen.
- In den herunterladbaren Lösungen ist nicht klar ersichtlich, was im Übersetzungsprozess vom Menschen entschieden wurde und was der Computer gefunden hat.
Zweiter Kommentar
- Bei der IMO werden Medaillen an 50 % der Teilnehmenden vergeben, und das Verhältnis von Gold-, Silber- und Bronzemedaillen beträgt 1:2:3.
- Dass die AI die Aufgaben besser gelöst hat als 75 % der Schüler, ist beeindruckend.
- Da die Zeit, die die AI zum Lösen der Aufgaben brauchte, sich jedoch von der Prüfungszeit der Schüler unterscheidet, ist ein direkter Vergleich unangebracht.
Dritter Kommentar
- AlphaGeometry hat nur eingeschränkte Probleme gelöst, aber diese Methode wird Mathematik in viel breiterem Umfang beeinflussen.
- Es wird eine Pipeline implementiert, die natürlichsprachliche Mathematik in formalisierte Mathematik umwandelt, und sie kann auch lernen, grundlegende Theoriebildung aufzubauen.
- Das ist der heilige Gral der Beweisassistenz und wird Menschen helfen, Mathematik auf natürlichere Weise zu formalisieren.
Vierter Kommentar
- Wenn das System drei Tage gebraucht hat, um die Probleme zu lösen, unterscheidet sich das kaum von reinem Brute-Force-Vorgehen.
- Das ist kein echtes Schlussfolgern.
Fünfter Kommentar
- Es verwendet Lean.
- Das ist nicht nur für Mathematikprobleme wichtig, sondern allgemein, um sinnlose Ergebnisse zu vermeiden.
- Ich hoffe, dass mehr Menschen Typen in Systemen wie Lean schreiben.
Sechster Kommentar
- Ich beneide die Menschen, die an diesem Projekt beteiligt sind.
- Es muss sehr unterhaltsam und erfüllend sein, Spitzentechnologie voranzubringen.
Siebter Kommentar
- Die beste Diskussion findet im Zulip-Chat von LeanProver statt.
Achter Kommentar
- Der Fields-Medaillengewinner Tim Gowers liefert einen guten Überblick, der die wichtigsten Vorbehalte erklärt und Kontext bietet.
Neunter Kommentar
- Theorembeweisen ist ein Einzelspieler-Spiel mit einem sehr großen Suchraum.
- Die größten Beitragenden zu AlphaProof sind die Entwickler von Lean und Mathlib.
- Der Mangel an Formalisierung in mathematischen Arbeiten hat Automatisierungsversuche behindert.
Zehnter Kommentar
- Maschinen sind Menschen im Schach seit Jahrzehnten überlegen.
- Trotzdem schauen die Leute immer noch Magnus Carlsen zu.
- Menschen interessieren sich für das Verhalten anderer Menschen.
- Maschinen interessieren nur insofern, als sie für Menschen hilfreich sind.