Ein mathematisches Universum in einer Sandbox

Project Numina, eine in Paris ansässige gemeinnützige Organisation zur Förderung quelloffener KI für die Mathematik, gab heute bekannt, Tamás Hausel, Professor am Institute of Science and Technology Austria (ISTA), mit einem Project Numina Fellowship auszuzeichnen. Das Fellowship wird Hausel und sein Team bei der Entwicklung von „Project Sandbox“ unterstützen – einer eigenständigen digitalen Forschungsumgebung, in der menschliche Mathematiker:innen und KI-Agenten Seite an Seite arbeiten, um unerforschte Bereiche der Mathematik zu erschließen. Das Fellowship umfasst Rechenunterstützung und Softwarezugang im Wert von 50.000 Euro über einen Zeitraum von 12 Monaten.

Künstliche Intelligenz verändert die mathematische Forschung. Jüngste Fortschritte im Bereich KI für Mathematik haben unter Forschenden und in der Öffentlichkeit große Aufmerksamkeit erregt und den renommierten Mathematiker und Fields-Medaillengewinner Terence Tao dazu veranlasst, ein „rasches Umdenken“ für das gesamte Forschungsfeld zu fordern.

Doch anstatt KI-Modelle einfach seit Langem bestehende Probleme lösen und Vermutungen beweisen zu lassen, die Mathematiker:innen seit Jahrzehnten beschäftigen, könnten diese Fortschritte auch als neue Forschungswerkzeuge genutzt werden.

Mit dem Project Numina Fellowship wird Tamás Hausel, Professor am Institute of Science and Technology Austria (ISTA), „Project Sandbox“ entwickeln – eine kontrollierte digitale Forschungsumgebung, in der menschliche Mathematiker:innen und KI-Agenten an der Grenze des bisherigen mathematischen Wissens konstruieren, berechnen, beweisen und zusammenarbeiten, und zwar in einem Bereich, der bislang von keinem Beweisassistenten formalisiert wurde.

Ausgehend von einer Familie offener Vermutungen wird Project Sandbox eine neue Theorie entwickeln, um diese zu beweisen – wobei jeder Schritt unter der Leitung eines menschlichen Mathematikers maschinell überprüft wird. Laut Hausel diente der Numina-Lean-Agent, ein Anfang dieses Jahres vorgestellter interaktiver mathematischer Beweisassistent, als Inspiration und praktischer Ausgangspunkt für die Architektur von Project Sandbox.

Inzwischen hat das Team bereits ein interaktives Visualisierungswerkzeug entwickelt, das es „Eyepiece“ nennt, um die Sandbox in Aktion zu visualisieren. „Letztlich planen wir, das Eyepiece für virtuelle Realität anzupassen und Werkzeuge hinzuzufügen, die es Nutzer:innen ermöglichen, direkt mit den Berechnungen der Sandbox zu interagieren“, sagt Hausel.

Ein „Forschungsinstitut“ für KI-Agenten – in einer Sandbox

Mit spezialisierten Agentenrollen und einem klar definierten Arbeitsablauf wird Project Sandbox ähnlich wie ein digitales „Forschungsinstitut“ für KI-Agenten funktionieren – unter der Leitung eines menschlichen Mathematikers oder einer menschlichen Mathematikerin. „Die Sandbox wird funktionieren, als wäre sie ein Forschungsinstitut, das einem einzigen Forschungsbereich gewidmet ist“, erklärt Hausel. „Ein menschlicher Mathematiker legt die Forschungsagenda fest und bewertet, welche Ergebnisse wichtig sind, während die KI-Agenten die erforderlichen Werkzeuge entwickeln, Vermutungen formulieren, Beweise versuchen und die Arbeit der jeweils anderen überprüfen.“

Wichtig ist, dass Project Sandbox so konzipiert ist, dass nichts in die Dokumentation aufgenommen wird, bevor ein sogenanntes „Computer-Algebra-Orakel“ die Aussage geprüft und ein „Beweiskern“ den Beweis zertifiziert hat.

In diesem Zusammenhang ist ein Orakel ein formales Werkzeug, das Antworten auf eine festgelegte Klasse von Fragen in einem einzigen Schritt liefern kann. Es überprüft konkrete, vom System benötigte rechnerische Behauptungen – ähnlich wie bei einer Hintergrundüberprüfung.

Ein Beweiskern hingegen ist ein relativ einfaches, unabhängiges Computerprogramm, das einem „Beweisprüfer“ ähnelt und wie ein automatisches Bewertungssystem für eine Matheprüfung funktioniert. Es bewertet weder die Eleganz eines Arguments noch entdeckt es Beweise oder beurteilt deren Bedeutung; es überprüft lediglich, ob ein formaler Beweis innerhalb eines festgelegten Systems gültig ist.

Eine KI-gestützte Brücke zwischen zwei mathematischen Disziplinen

Mit Project Sandbox wollen Hausel und seine Gruppe eine praktische Verbindung zwischen zwei Bereichen der Mathematik schaffen: der „Darstellungstheorie“ und der „äquivarianten Topologie“.

„Das Projekt wird prüfen, ob KI helfen kann, eine Beweis-erzeugende Brücke zwischen diesen beiden reichhaltigen mathematischen Welten zu bauen“, erklärt er. „Die Verknüpfung von Konzepten wie Quantengruppen und der Langlands-Klassifikation in der Darstellungstheorie mit affinen Schubert-Varietäten und GKM-Graphen in der äquivarianten Topologie wird uns letztlich dabei helfen, einen KI-gestützten Rahmen für die Übertragung von Ideen zwischen Algebra und Geometrie zu entwickeln.“

Als Hausel sein Projekt bei Numina im Juni präsentierte, erschien ihm das Bild eines „mathematischen Universums in einer Sandbox“ auf seiner Titelfolie noch wie Science-Fiction. „Erstaunlicherweise begann die Sandbox bereits nach nur drei Wochen Arbeit auf meinem Bürocomputer zu laufen, wie in der Illustration zu sehen ist“, sagt er. „Wir haben bereits ein wichtiges Ergebnis bewiesen und sind auf gutem Weg, dieses spezielle Forschungsgebiet zu verstehen.“

Numina: Eine internationale Initiative mit Sitz in Paris

Project Numina ist eine globale gemeinnützige Organisation mit Hauptsitz in Paris, Frankreich. Als ein sich der offenen Wissenschaft verschriebenes Projekt umfasst ihre Mission die Entwicklung von KI für formales Schlussfolgern sowie die Förderung der Zusammenarbeit zwischen Menschen und KI in der Mathematik. Numina bringt Olympiaden-Medaillengewinner:innen, junge Mathematiker:innen und Machine-Learning-Ingenieur:innen zusammen, um quelloffene KI zu entwickeln und die Grenzen der Mathematik weiter zu verschieben.

Das Project Numina Fellowship richtet sich an Forschungsgruppen weltweit, die ihre Forschung mit KI-Werkzeugen für mathematisches Schlussfolgern beschleunigen möchten. Das Fellowship unterstützt Teams bei der gemeinsamen Entwicklung von Lösungen für tiefgreifende und ambitionierte Forschungsprobleme an der Spitze der wissenschaftlichen und mathematischen Forschung.

Das Numina-Team wird von der Überzeugung geleitet, dass „die Mathematik die Intelligenz übersteigt wie ein endloser Ozean, den nur der Geist durchsegeln kann“ (Englisch, “mathematics transcends intelligence like an endless ocean only the mind can sail”). Mit diesem neuen Fellowship werden Hausel und seine Gruppe am ISTA nun ein KI-gestütztes System entwickeln, das ihnen helfen wird, neues, unerforschtes mathematisches Terrain zu erkunden.