DeepMind erreicht Meilenstein bei der Lösung mathematischer Probleme – Die nächste große Herausforderung für KI

Nachdem Google DeepMind Menschen in alles besiegt hat, vom Spiel Go bis zu Strategie-Brettspielen,
behauptet es nun, kurz davor zu stehen, die weltbesten Schüler beim Lösen von Mathematikaufgaben zu schlagen.

Das in London ansässige Machine-Learning-Unternehmen verkündete am 25. Juli, dass seine künstliche Intelligenz (KI)-Systeme vier der sechs Aufgaben gelöst haben, die den Schülern bei der Internationale Mathematik-Olympiade (IMO) 2024 in Bath, Großbritannien, gegeben wurden. Die KI lieferte rigorose, schrittweise Beweise, die von zwei Top-Mathematikern bewertet wurden und erzielte eine Punktzahl von 28/42 – nur einen Punkt von Bereich der Goldmedaillen entfernt.

„Es ist offensichtlich ein sehr bedeutender Fortschritt“, sagt Joseph Myers, ein Mathematiker aus Cambridge, Großbritannien, der gemeinsam mit Fields-Medaillenträger Tim Gowers die Lösungen überprüft hat und bei der Auswahl der Originalprobleme für die diesjährige IMO geholfen hat.

DeepMind und andere Unternehmen sind im Rennen, um letztendlich Maschinen Beweise zu liefern, die wesentliche Forschungsfragen in der Mathematik lösen. Die bei der IMO gestellten Probleme, dem weltweit führenden Wettbewerb für junge Mathematiker, sind zu einem Maßstab für den Fortschritt in Richtung dieses Ziels geworden und werden als „große Herausforderung“ für das maschinelle Lernen betrachtet, so das Unternehmen.

„Dies ist das erste Mal, dass ein KI-System Leistungen auf Medaillenniveau erreichen konnte“, sagte Pushmeet Kohli, Vizepräsident für KI in der Wissenschaft bei DeepMind, in einer Pressebesprechung. „Dies ist ein wichtiger Meilenstein auf dem Weg zum Aufbau fortschrittlicher Beweisermittler“, sagte Kohli.

Erweiterung

Erst vor wenigen Monaten, im Januar, hatte das DeepMind-System AlphaGeometry Leistungen auf Medaillenniveau beim Lösen eines Typs von IMO-Problemen, nämlich denen in der euklidischen Geometrie, erreicht. Die erste KI, die auf Goldmedaillenniveau für den Gesamttest – einschließlich Fragen in Algebra, Kombinatorik und Zahlentheorie, die im Allgemeinen als anspruchsvoller als die Geometrie angesehen werden – arbeitet, ist berechtigt, einen Preis von 5 Millionen US-Dollar, den AI-Mathematik-Olympiade-Preis (AIMO), zu erhalten. (Der Preis hat strenge Kriterien wie die Offenlegung des Quellcodes und die Arbeit mit begrenzter Rechenleistung, was bedeutet, dass die aktuellen Bemühungen von DeepMind nicht qualifizieren würden.)

In ihrem neuesten Versuch verwendeten die Forscher AlphaGeometry2, um das Geometrieproblem in unter 20 Sekunden zu lösen; die KI ist eine verbesserte und schnellere Version ihres Rekordsystems, sagt der DeepMind-Computerspezialist Thang Luong.

Für die anderen Arten von Fragen entwickelte das Team ein völlig neues System namens AlphaProof. AlphaProof löste zwei Algebra-Probleme des Wettbewerbs sowie eines in Zahlentheorie, wofür es drei Tage brauchte. (Die Teilnehmer der tatsächlichen IMO haben zwei Sitzungen von jeweils 4,5 Stunden.) Es war nicht in der Lage, die zwei Probleme in der Kombinatorik, einem anderen Bereich der Mathematik, zu lösen.

Forscher haben gemischte Ergebnisse erzielt, wenn sie mathematische Fragen mit Sprachmodellen beantworten – die Art von System, die Chatbots wie ChatGPT antreiben. Manchmal geben die Modelle die richtige Antwort, können aber ihre Argumentation nicht rational erklären, und manchmal geben sie Unsinn aus.

Erst letzte Woche hat ein Team von Forschern der Softwareunternehmen Numina und HuggingFace ein Sprachmodell verwendet, um einen Zwischen-AMIO-‚Fortschrittspreis‘ auf der Grundlage vereinfachter Versionen von IMO-Problemen zu gewinnen. Die Unternehmen haben ihre gesamten Systeme Open Source gemacht und anderen Forschern zum Download zur Verfügung gestellt. Doch die Gewinner sagten Nature, dass Sprachmodelle allein wahrscheinlich nicht ausreichen würden, um schwierigere Probleme zu lösen.

Einzige Klasse

AlphaProof kombiniert ein Sprachmodell mit der Technik des verstärkenden Lernens, das den von der Firma erfolgreich eingesetzten „AlphaZero“-Motor für Angriffsspiele wie Go sowie einige spezifische mathematische Probleme verwendet. Beim verstärkenden Lernen lernt ein neuronales Netzwerk durch Versuch und Irrtum. Das funktioniert gut, wenn seine Antworten anhand eines objektiven Maßstabs bewertet werden können. Zu diesem Zweck wurde AlphaProof darauf trainiert, Beweise in einer formalen Sprache namens Lean zu lesen und zu schreiben, die in der ‚Proof Assistant‘-Softwarepaket gleichen Namens beliebt bei Mathematikern verwendet wird. Dafür testete AlphaProof, ob seine Ausgaben korrekt waren, indem es sie im Lean-Paket ausführte, was half, einige der Schritte im Code auszufüllen.

Das Training eines Sprachmodells erfordert massive Mengen an Daten, doch nur wenige mathematische Beweise waren in Lean verfügbar. Um dieses Problem zu überwinden, entwickelte das Team ein zusätzliches Netzwerk, das versuchte, eine vorhandene Aufzeichnung von einer Million Problemen, die in natürlicher Sprache verfasst waren, aber ohne menschlich geschriebene Lösungen, in Lean zu übersetzen, sagt Thomas Hubert, ein DeepMind-Maschinenlern-Forscher, der die Entwicklung von AlphaProof mit leitete. „Unser Ansatz war, können wir lernen, zu beweisen, auch wenn wir ursprünglich nicht auf menschlich geschriebenen Beweisen trainiert haben?“ (Das Unternehmen ging ähnlich vor wie beim Go, wo seine KI gelernt hat, das Spiel zu spielen, indem sie gegen sich selbst gespielt hat, anstatt von der Art und Weise, wie Menschen es tun.)

Magische Schlüssel

Viele der Lean-Übersetzungen ergaben keinen Sinn, aber genug waren gut genug, um AlphaProof zu dem Punkt zu bringen, an dem es seine verstärkenden Lernzyklen starten konnte. Die Ergebnisse waren viel besser als erwartet, sagte Gowers bei der Pressebesprechung. „Viele Probleme bei der IMO haben diese Eigenschaft des magischen Schlüssels. Das Problem sieht zuerst schwer aus, bis man einen magischen Schlüssel findet, der es öffnet“, sagte Gowers, der am Collège de France in Paris tätig ist.

In einigen Fällen schien AlphaProof in der Lage zu sein, diesen zusätzlichen Schritt der Kreativität zu liefern, indem es einen korrekten Schritt aus einer unendlich großen Lösungsmöglichkeit lieferte. Aber es bedarf weiterer Analyse, um festzustellen, ob die Antworten weniger überraschend waren, als sie aussahen, fügte Gowers hinzu. Ein ähnlicher Diskurs entstand nach dem überraschenden ‚Zug 37‘, den DeepMinds AlphaGo-Bot bei seinem berühmten Sieg 2016 über den weltbesten menschlichen Go-Spieler machte – ein Wendepunkt für die KI.

Ob die Techniken perfektioniert werden können, um auf einem Forschungsniveau in der Mathematik zu arbeiten, bleibt abzuwarten, sagte Myers bei der Pressebesprechung. „Kann es sich auf andere Arten der Mathematik ausweiten, auf denen möglicherweise keine Millionen Probleme trainiert sind?“

„Wir sind an dem Punkt angelangt, an dem sie nicht nur offene Forschungsprobleme beweisen können, sondern auch Probleme, die sehr herausfordernd für die allerbesten jungen Mathematiker der Welt sind“, sagte der DeepMind-Computerspezialist David Silver, der Mitte der 2010er Jahre der führende Forscher bei der Entwicklung von AlphaGo war.