Terence Tao hyllar AI-assisterade bevis i strömningsmekanik: «En enastående prestation»

Matematikern Tristan Buckmaster vid NYU och Anthropic-forskaren Levent Alpöge publicerade i söndags AI-assisterade och Lean-verifierade bevis som visar att flera vätskeekvationer kan utveckla «blow-ups» i ändlig tid, punkter där fysikaliska storheter går mot oändligheten, under slät yttre påverkan. Fields-medaljören Terence Tao kallade arbetet «en enastående prestation» och sade sig inte se några fundamentala hinder för att utöka metoderna mot Navier-Stokes ekvationer, ett av matematikens sju ulösta Millennieproblem.officechai+1

Vad bevisen visar

Resultaten omfattar 3D inkompressibel Euler-, Boussinesq- och inkompressibel porous media-ekvationer. Tidigare arbete av matematikerna Diego Córdoba och Luis Martínez-Zoroa hade visat att «blow-up» bara var möjligt med råare och mindre fysikaliskt realistiska påverkanstermer. Buckmaster och Alpöge uppger att de har drivit påverkanstermen ända till att vara slät, ett svårare och mer betydelsefullt resultat, med omfattande hjälp från AI-modeller och formal verifiering i Lean.terrytao.wordpress+2

I ett inlägg på sin blogg förklarade Tao den underliggande strategin: Konstruktionen lägger iterativt lager på lager av små, högfrekventa korrigeringar ovanpå ett större bakgrundsflöde, där bakgrunden exponentiellt förstärker korrigeringarna tills de blir tillräckligt starka för att utlösa nästa förstärkningsrunda. Om detta upprepas tillräckligt snabbt uppstår en reell «blow-up» i ändlig tid. Han noterade att Boussinesq-artikeln i sig omfattar 76 sidor trots försök att korta ned den.officechai+1

En väg mot Navier-Stokes?

Tao sade att han inte ser något i den nuvarande metoden som fundamentalt skulle hindra en utökning till Navier-Stokes ekvationer, och lyfte möjligheten att påverkanstermen i slutändan helt skulle kunna tas bort, vilket skulle föra resultatet närmare den faktiska Millennieproblem-formuleringen. Men han varnade för att betydande tekniska svårigheter återstår innan en fullständig lösning nås. Han sade att han inte skulle bli överraskad om någon slutligen tar sig igenom dessa svårigheter med tillräcklig beräkningskapacitet och AI-assistans, men lade till att det sifferarbetet inte intresserar honom personligen. Han är mer entusiastisk över att sätta sig in i de nya bevisteknikerna för deras matematiska innehåll.terrytao.wordpress+1

Kontroverser kring publiceringen

Publiceringen ledsagades av anklagelser från Buckmaster om att OpenAI försökte pressa honom under publiceringsprocessen efter att rykten spridits om att arbetet kunde vara ett genombrott för Navier-Stokes. OpenAIs Sebastien Bubeck förnekade felaktigheter i ett kort offentligt svar och utlovade en mer ingående redogörelse. Separat uppgav en forskargrupp vid Anima AI att de oberoende arbetat med relaterade «blow-up»-resultat för opåverkade inkompressibla Euler-ekvationer med hjälp av en annan metod baserad på fysikinformerade neuronala nätverk.anima-ai+2

Tao noterade att han talade direkt med Buckmaster per telefon för att få idéerna förklarade, en detalj han ställde i kontrast till AI-förmedlad kommunikation och kallade det mänskliga samtalet «ett uppfriskande ombyte».officechai