Eine mathematische Herausforderung, der Terence Tao 18 Monate lang nicht gewachsen war, wurde von diesem "künstlichen Intelligenz-Gauß" in drei Wochen bewältigt.

Unglaublich! Dieser neue KI-Agent namens Gauss scheint voll auf Tour zu sein.

Er hat nämlich in nur drei Wochen die mathematische Herausforderung gelöst, die von Tao Zhexuan und Alex Kontorovich gestellt wurde –

die formale Darstellung des Starken Primzahlsatzes (Prime Number Theorem, PNT) in Lean.

Man muss bedenken, dass Tao Zhexuan und Kontorovich nach der Stellung der Herausforderung im Januar 2024 erst nach 18 Monaten (im Juli dieses Jahres) einen vorläufigen Fortschritt erzielten.

Woher kommt dieser Gauss überhaupt?

Hinter ihm steht ein KI-Unternehmen namens Math. Laut Angaben ist Gauss der erste automatische Formalisierungs-Agent (autoformalization), der Spitzenmathematikern bei der formalen Verifikation helfen kann:

Hierbei bezieht sich die Formalisierung darauf, dass mathematische Inhalte, die von Menschen geschrieben wurden, in eine maschinenlesbare, prüfbare und eindeutige Formsprache umgewandelt werden, und dann der Computer zur Überprüfung ihrer Richtigkeit herangezogen wird.

Der Grund, warum Tao Zhexuan und Alex Kontorovich bisher nur vorläufige Fortschritte erzielt haben, liegt an einem Kernproblem der Komplexen Analysis (complex analysis).

Als eine künstliche Intelligenz hat Gauss die Eigenschaft, ununterbrochen zu arbeiten, was die Arbeitsmenge, die früher nur von Spitzenformalierungsexperten bewältigt werden konnte, erheblich reduziert. Gleichzeitig hat Gauss auch die oben genannten fehlenden Schlüsselresultate der Komplexen Analysis formalisiert.

Das ist der Grund, warum er in drei Wochen eine mathematische Herausforderung lösen konnte, die Tao Zhexuan in 18 Monaten nicht bewältigen konnte.

Wie wurde Gauss realisiert?

Das Unternehmen Math hat bisher keinen detaillierten technischen Bericht veröffentlicht.

Aber aus den Ergebnissen zu urteilen, hat Gauss etwa 25.000 Zeilen Lean-Code erzeugt, die Tausende von Sätzen und Definitionen enthalten.

Man muss bedenken, dass eine solche formale Beweisführung früher oft Jahre dauert.

Das größte einzelne formale Projekt in der Geschichte (das oft sogar über 10 Jahre dauert) ist nur um eine Größenordnung größer (maximal 500.000 Zeilen Code).

Im Vergleich dazu hat die Standardmathematikbibliothek Mathlib von Lean etwa 2 Millionen Zeilen Code und enthält 350.000 Sätze, wurde aber von über 600 Mitwirkenden in 8 Jahren aufgebaut.

Um Gauss betreiben zu können, hat das Team auch mit Morph Labs an der Infrastruktur der Trinity-Umgebung gearbeitet.

Den Betrieb von Gauss in einem so großen Maßstab zu ermöglichen, erfordert Tausende von parallelen Agenten, und jeder Agent hat seine eigene Lean-Betriebsumgebung, was Terabyte an Cluster-Speicher verbraucht. Das ist eine extrem komplexe Systemtechnikherausforderung.

Das Math-Team hat auch erklärt:

Gauss wird die Zeit, die für große mathematische Projekte benötigt wird, erheblich verkürzen.

Mit fortschreitender Algorithmentwicklung planen wir, die Gesamtmenge an formaliertem Code in den nächsten 12 Monaten um das 100- bis 1.000-fache zu erhöhen.

Dies wird zum Übungsfeld für ein neues Paradigma werden – auf dem Weg zu einer „verifizierbaren Superintelligenz“ und einem „universellen Maschinenmathematiker“.

Gerade jetzt hat Tao Zhexuan selbst auf Mastodon einige Erklärungen zu Fragen der Formalisierung gegeben (im Folgenden Tao Zhexuans Aussage).

Jedes komplexe Projekt hat normalerweise klare, ausdrückliche Ziele und implizite, nicht ausdrückliche Ziele. Beispielsweise könnte das klare Ziel eines Lean-Formalisierungsprojekts die formale Beweisführung eines bestimmten mathematischen Satzes X sein. Aber es gibt auch oft unausgesprochene Ziele, wie etwa die Formalisierung der Schlüsselunteraussagen und Definitionen X1, X2, … von X auf eine Weise, die für die Integration in die Mathlib-Bibliothek geeignet ist; das Erlernen der Verwendung verschiedener kollaborativer Werkzeuge und die Aufgabenzuteilung; die organische Entdeckung einer feineren Struktur des Beweises von X, die in früheren informellen Beweisen möglicherweise nicht betont wurde; die praktische Ausbildung und das Sammeln von Erfahrungen für neue Formalisierer; und allgemeiner die Gründung einer menschlichen Gemeinschaft, die sich in der Kunst der Formalisierung bewandert.

In der Vergangenheit war es normalerweise nicht erforderlich, diese impliziten Ziele zu formulieren, da es eine starke empirische Korrelation zwischen der Erreichung dieser Ziele und der Erreichung der ausdrücklichen Ziele gab. Im Fall von Formalisierungsprojekten führte fast jeder menschliche Versuch, die ausdrücklichen Ziele zu erreichen, schließlich auch zur natürlichen Erreichung der meisten der oben genannten impliziten Ziele. Daher wurden die ausdrücklichen Ziele effektiv zu einem praktikablen Ersatz für die breiteren tatsächlichen Ziele.

Mit dem Aufkommen leistungsstarker KI-Werkzeuge ändert sich dies jedoch. Diese Werkzeuge verwenden eine völlig andere Methode als Menschen. Man kann diese Werkzeuge anweisen, ein ausdrückliches Ziel zu erreichen, ohne dass alle impliziten Ziele, die möglicherweise erreicht würden, wenn das Projekt von einem menschlichen Team durchgeführt würde, erreicht werden müssen. Tatsächlich können KI-Optimierungsalgorithmen aufgrund ihrer Natur sogar hohe Leistungen bei den ausdrücklichen Zielen erzielen, indem sie auf die Kosten aller impliziten Ziele gehen. (Siehe das Goodhart-Gesetz: „Wenn ein Maßstab zum Ziel wird, ist er kein guter Maßstab mehr.“)

Angesichts der zunehmenden Nutzung dieser Werkzeuge zeigt es mir, dass Projektorganisatoren jetzt größere Anstrengungen unternehmen müssen, um alle Ziele des Projekts, nicht nur die nominellen Ziele, klar zu formulieren. In einigen Fällen sind diese Ziele möglicherweise zunächst nicht einmal den Organisatoren selbst klar und erfordern möglicherweise einige Diskussionen zwischen den Teilnehmern. Externe Parteien, die an der Prüfung solcher Projekte mit ihren KI-Werkzeugen interessiert sind, sollten im Voraus mit den Organisatoren koordinieren, um zu vermeiden, dass sie ein oder mehrere Schlüsselimplizite Ziele übersehen, die ihre Werkzeuge nicht optimieren werden.

Der Gründer ist Autor des ICML’25 Time-Tested Award-Papiers

Es ist erwähnenswert, dass der Chef des Unternehmens Math auch ziemlich talentiert ist.

Er ist nämlich einer der Autoren des Papers, das diesen Jahres den ICML Time-Tested Award gewann, Christian Szegedy.

Dieses Paper wurde von ihm und einem anderen Autor, Sergey Loffe, 2015 vorgestellt: Batch Normalization (Batch-Normalisierung, kurz BatchNorm).

Heute hat dieses Paper über 60.000 Zitationen und ist ein Meilenstein in der Geschichte der Entwicklung des Deep Learning. Es hat die Ausbildung und Anwendung von tiefen neuronalen Netzwerken stark vorangetrieben.

Man kann sagen, dass es eine der Schlüsseltechnologien ist, die das Deep Learning von kleinen Experimenten zu einer großen praktischen und zuverlässigen Anwendung gebracht hat.

Natürlich haben die Netizens nach dem Blick auf Gauss zwar „Amazing“ gerufen, aber auch gefordert, dass das Unternehmen das Paper bald veröffentliche.

Wir können also auf weitere technische Details warten!

Referenzlinks: [1]https://x.com/mathematics_inc/status/1966194751847461309[2]https://www.math.inc/gauss[3]https://www.math.inc/vision

Teile deine Meinung im Kommentar!

Jin Lei, aus Aofeisi, Quantum Bit | Newsletter QbitAI

Dieser Artikel stammt aus dem WeChat-Newsletter „Quantum Bit“ (ID: QbitAI), Autor: Fokus auf Spitzentechnologie, veröffentlicht von 36 Krypton mit Genehmigung.