Terence Tao nennt KI-gestützte Strömungsmechanik-Beweise «eine bemerkenswerte Leistung»

Der NYU-Mathematiker Tristan Buckmaster und der Anthropic-Forscher Levent Alpöge haben am Sonntag KI-gestützte und Lean-verifizierte Beweise veröffentlicht. Diese zeigen, dass mehrere Strömungsgleichungen unter glatter äußerer Anregung sogenannte Finite-Time-Blow-ups entwickeln können, also Punkte, an denen physikalische Größen gegen Unendlich streben. Fields-Medaillenträger Terence Tao bezeichnete die Arbeit als «eine bemerkenswerte Leistung» und erklärte, er sehe kein fundamentales Hindernis, die Methoden auf die Navier-Stokes-Gleichungen auszuweiten, eines der sieben ungelösten Millennium-Probleme der Mathematik.officechai+1

Was die Beweise zeigen

Die Ergebnisse decken die 3D-inkompressiblen Euler-, Boussinesq- und inkompressiblen Porous-Media-Gleichungen ab. Frühere Arbeiten der Mathematiker Diego Córdoba und Luis Martínez-Zoroa hatten gezeigt, dass ein Blow-up nur mit raueren, physikalisch weniger realistischen Anregungstermen möglich war. Buckmaster und Alpöge geben an, den Anregungsterm mit umfassender Unterstützung durch KI-Modelle und formale Verifikation in Lean bis hin zur Glattheit getrieben zu haben, was ein schwierigeres und bedeutenderes Ergebnis darstellt.terrytao.wordpress+2

In einem Blogbeitrag erläuterte Tao die zugrunde liegende Strategie: Die Konstruktion lagert iterativ kleine, hochfrequente Korrekturen über eine größere Hintergrundströmung. Der Hintergrund verstärkt diese Korrekturen exponentiell, bis sie stark genug sind, um die nächste Verstärkungsrunde auszulösen. Wiederholt man dies schnell genug, entsteht ein echter Finite-Time-Blow-up. Er merkte an, dass die Boussinesq-Arbeit allein trotz Bemühungen um Kürzung 76 Seiten umfasst.officechai+1

Ein Weg zu Navier-Stokes?

Tao erklärte, er sehe in der aktuellen Methode nichts, was einer Erweiterung auf die Navier-Stokes-Gleichungen grundsätzlich im Wege stünde. Zudem brachte er die Möglichkeit ins Spiel, dass der Anregungsterm letztlich ganz entfallen könnte, was das Ergebnis näher an die eigentliche Formulierung des Millennium-Problems bringen würde. Er warnte jedoch, dass zwischen den aktuellen Ergebnissen und einer vollständigen Lösung noch erhebliche technische Hürden liegen. Er sei nicht überrascht, wenn jemand diese Hürden mit ausreichend Rechenleistung und KI-Unterstützung schließlich überwinden würde, fügte jedoch hinzu, dass ihn diese Fleißarbeit persönlich kaum interessiere. Vielmehr begeistert ihn die Analyse der neuen Beweistechniken hinsichtlich ihres mathematischen Gehalts.terrytao.wordpress+1

Kontroverse um die Veröffentlichung

Die Veröffentlichung wurde von Vorwürfen Buckmasters begleitet, OpenAI habe versucht, während des Veröffentlichungsprozesses Druck auf ihn auszuüben, nachdem Gerüchte über einen möglichen Navier-Stokes-Durchbruch im Umlauf waren. Sebastien Bubeck von OpenAI wies jegliches Fehlverhalten in einer kurzen öffentlichen Reaktion zurück und versprach eine umfassendere Darstellung. Unabhängig davon gab eine Forschungsgruppe bei Anima AI bekannt, dass sie mit einem anderen Ansatz auf Basis physikinformierter neuronaler Netze an verwandten Blow-up-Ergebnissen für unangeregte inkompressible Euler-Gleichungen gearbeitet habe.anima-ai+2

Tao merkte an, dass er direkt mit Buckmaster telefoniert habe, um sich die Ideen erklären zu lassen, ein Detail, das er im Kontrast zur KI-vermittelten Kommunikation hervorhob und das menschliche Gespräch als «eine erfrischende Abwechslung» bezeichnete.officechai