OpenAI kondigt de oplossing aan van het Navier–Stokes Millennium-prijsprobleem betreffende existentie en gladheid. Het bewijs, gegenereerd door een krachtig intern AI-model, toont aan dat driedimensionale vloeistofbewegingen in een eindige tijd een singulariteit kunnen ontwikkelen, wat betekent dat vloeistofsnelheden onbeperkt kunnen groeien ondanks de aanwezigheid van viscositeit.
De oplossing werd bereikt via een complex systeem van ongeveer 10.000 coördinerende AI-agenten die gebruikmaakten van tools en onderlinge communicatie. Het proces begon met het oplossen van het eenvoudiger Euler-regulariteitsprobleem, waarna de middelen werden verschoven naar het Navier-Stokes-probleem. Het resultaat is zowel analytisch bewezen als geformaliseerd in de programmeertaal Lean.
Naast de wiskundige doorbraak benadrukt OpenAI dat dit resultaat dient als een indicator voor de snelle voortgang van AI-capaciteiten in complexe wetenschappelijke domeinen. Het bedrijf is niet van plan de Millennium-prijs te claimen, maar wil de wereld informeren over de huidige stand van zaken in de ontwikkeling naar AGI.
Over het Navier–Stokes Millennium-prijsprobleem
We delen een oplossing voor het Navier–Stokes-probleem betreffende existentie en gladheid (existence and smoothness), een van de Millennium-prijsproblemen. Dit bewijs, geproduceerd door een intern OpenAI-systeem, toont aan dat de dynamica van de Navier-Stokes-vergelijkingen voor vloeistofbeweging in een eindige tijd een singulariteit kunnen ontwikkelen. We delen zowel een beschrijving van het bewijs als een formalisering in Lean.
De Millennium-prijsproblemen vertegenwoordigen enkele van de diepste vragen op het front van de wiskunde. De vraag of een gladde driedimensionale vloeistofbeweging kan instorten, is ongeveer 90 jaar lang onopgelost gebleven.
Een belangrijk doel van ons werk is om wetenschappers in staat te stellen onderzoek en technologie te bevorderen waar de hele mensheid baat bij heeft. Om het Navier–Stokes-probleem op te lossen, hebben we gebruikgemaakt van een intern model dat aanzienlijk krachtiger is dan GPT-6 Astra. We vinden het belangrijk om de wereld te informeren over het tempo van de AI-vooruitgang en wat men kan verwachten van toekomstige modellen.
Het probleem
De Navier–Stokes-vergelijkingen maken gebruik van de tweede wet van Newton ("F=ma") om te beschrijven hoe vloeistoffen bewegen. Belangrijk is dat zij een vloeistof behandelen als een continu medium in plaats van individuele moleculen te volgen. Deze vergelijkingen worden gebruikt voor het ontwerp van vliegtuigen, weersvoorspellingen en de studie van de bloedstroom.
Een fundamentele open vraag voor deze dynamische vergelijkingen is of de continuümbenadering van de vloeistof kan instorten. Specifiek: kunnen de Navier–Stokes-vergelijkingen voor een driedimensionale, onsamendrukbare vloeistof met constante dichtheid een "singulariteit" ontwikkelen, zelfs wanneer de beweging glad begint? Hier betekent een singulariteit dat de dynamica leiden tot snelheden in de vloeistof die binnen een eindige hoeveelheid tijd onbeperkt groeien. De ontwikkeling van een singulariteit zou moeten plaatsvinden ondanks de aanwezigheid van viscositeit, die de neiging heeft beweging glad te strijken. Omdat een echte vloeistof niet oneindig snel kan bewegen, zou dit een breakdown betekenen in de manier waarop de vergelijkingen de vloeistof modelleren. Om het systeem vervolgens verder te modelleren, zou men het gedrag van elk deeltje individueel moeten volgen.
De vergelijkingen stammen uit het negentiende-eeuwse werk van Claude-Louis Navier en George Gabriel Stokes. In 1934 bewees Jean Leray dat oplossingen in een gegeneraliseerde zin bestaan, maar de vraag of ze altijd glad blijven, werd een centrale onbeantwoorde vraag. In 2000 wees het Clay Mathematics Institute het Navier–Stokes-probleem betreffende existentie en gladheid aan als een van de zeven Millennium-prijsproblemen.
Het resultaat
Ons systeem produceerde een analytisch bewijs en een Lean-formalisering dat een aanvankelijk gladde vloeistof in rust in een eindige tijd een singulariteit kan ontwikkelen. Er wordt een gladde kracht op de vloeistof uitgeoefend, en de energie blijft gedurende de gehele dynamica eindig, van rust tot de vorming van de singulariteit. Dit lost het Navier–Stokes Millennium-prijsprobleem op door bewering "C" (en ook "D") in de officiële Millennium-prijsformulering vast te stellen.
De oplossing is een vortex, een spinnende werveling van vloeistof, die naar binnen spiraalt en steeds meer langgerekt wordt, zoals spaghetti. Dit centrale gebied krimpt terwijl het versnelt, op zo'n manier dat de energie nog steeds eindig blijft, zoals vereist door de wetten van de fysica. De technische uitdaging is dat de vergelijkingen de instorting moeten ontwikkelen door de beweging van de vloeistof zelf, in plaats van bijvoorbeeld dat wij handmatig een oneindige kracht invoeren. Mathematisch gezien moeten de termen in de Navier–Stokes-vergelijkingen die de beweging beschrijven — versnelling, drukgradiënten, momentumoverdracht, viscositeit — zowel groot worden als elkaar op een precieze manier opheffen. Deze gedetailleerde balans zorgt ervoor dat een gladde externe kracht behouden blijft, zelfs terwijl de snelheid van de vloeistof onbeperkt groeit.
Bijschrift: Een momentopname van lokale onsamendrukbare beweging. Oranje markeert snellere hoekrotatie; groenblauw markeert langzamere rotatie. De circulerende snelheid hangt ook af van de straal. De trajecten tonen naar binnen spiraliseren en axiale stretching.
Hoe we het bewijs hebben gevonden
Sinds 28 augustus trainen we een nieuw intern model dat ongekende prestaties heeft getoond in onze benchmarks, waaronder wiskunde. De training van dit model is gaande en de prestaties blijven verbeteren.
Op dinsdag 1 september hoorden we geruchten dat twee Millennium-prijsproblemen waren opgelost. Geïnspireerd door deze geruchten en door de stap in prestaties van ons interne model, startten we een inspanning om het te evalueren op alle open Millennium-prijsproblemen en enkele andere problemen met een grote impact.
We maakten gebruik van een systeem van coördinerende agenten aangedreven door ons interne model. De agenten hadden toegang tot tools, zoals de mogelijkheid om te lezen uit een gecachte versie van het internet en de mogelijkheid om code uit te voeren. Agenten waren onderverdeeld in groepen met de mogelijkheid om binnen de groep te communiceren. De groepen varieerden in grootte; de groep die de Navier–Stokes-resolutie produceerde, bestond uit ongeveer 10.000 gelijktijdige agenten. Te allen tijde hielden we dezelfde strikte waarborgen aan die we toepassen op al onze evaluaties van frontier-modellen, inclusief monitoring en isolatie.
Voor elk probleem gaven we verschillende groepen agenten verschillende varianten van de probleemstelling, waarbij alle varianten van het probleem werden gedekt. Voor het Navier–Stokes-probleem suggereerden we versies "A" en "B" (specifieke vormen van het probleem die zouden resulteren in een bewijs) en versies "C" en "D" (die zouden resulteren in een weerlegging) aan afzonderlijke groepen agenten.
Naast de volledige Millennium-prijsproblemen vroegen we ons multi-agent-systeem om een set "makkelijkere" problemen te proberen. Een van deze problemen was een soortgelijke blowup-vraag voor de limiet van het Navier–Stokes-probleem waarbij de viscositeitsterm was verwijderd. Dit staat bekend als het regulariteitsprobleem voor de Euler-vergelijkingen, en onze agenten verrasten ons door deze vraag op te lossen. De specifieke variant die zij oplosten was de niet-gedreven versie, waarbij geen externe kracht op de vloeistof wordt uitgeoefend. Bijna 100 agenten werkten ongeveer 50 uur samen om onze weerlegging van de Euler-regulariteit te produceren.
Toen we de Euler-oplossing zagen, dachten we dat Navier–Stokes het meest veelbelovende probleem was om aan te werken. Daarom besloten we onze middelen aan Navier–Stokes te wijden. Om dit te doen, verplaatsten we agenten weg van de andere Millennium-problemen en voedden we deze agenten met de Euler-resolutie. Wanneer er gedurende de inspanning een verder getrainde versie van ons interne model beschikbaar kwam, werkten we onze agenten bij naar dat model.
We moedigden verschillende groepen agenten aan om een diversiteit aan benaderingen te verkennen. Na verloop van tijd kruisbestuifden we de agentgroepen door Codex te gebruiken om de meest nuttige inzichten van elke agentgroep te consolideren. Deze vervolgprompts maakten gebruik van de tussenresultaten van de agenten zelf. De groep die de oplossing voor Navier–Stokes vond, werd op deze manier begeleid.
De agenten kwamen tot hun resolutie op zaterdag 5 september, ongeveer 88 uur nadat de eerste agenten waren gelanceerd. De Lean-formalisering en verificatie namen nog eens 17 uur in beslag via GPT-6 Astra.
Over alle geprobeerde problemen heen stuurden de agenten 4,9 miljoen berichten en gebruikten ze ongeveer 300 miljard output-tokens. Tijdens het oplossen van het Navier–Stokes-probleem stuurden de agenten 2,7 miljoen berichten en gebruikten ze ongeveer 130 miljard output-tokens.
Gelijktijdig werk
Onze inspanning begon op 1 september nadat we een gerucht hadden gehoord dat later gerelateerd bleek te zijn aan Levent Alpöge, een medewerker van Anthropic, en Tristan Buckmaster, een professor in de wiskunde aan NYU. Na de voltooiing van ons volledige project en de Lean-verificatie (op 6 september), en in het geloof dat zij op basis van het gerucht ook een oplossing voor Navier–Stokes hadden, namen we contact met hen op om een gelijktijdige release van ons resultaat aan te bieden en hun prioriteit in een gezamenlijke aankondiging te erkennen. Op dat moment ontdekten we dat zij een resolutie hadden van het gedreven (forced) Euler-probleem. In deze discussies boden we hen inzicht in alle prompts die we gebruikten en later de mogelijkheid om het bewijs in te zien. We erkennen de prioriteit van hun werk aan de gedreven Euler en feliciteren hen met hun opmerkelijke wiskundige prestatie.
Wij (de onderzoekers en de agenten) hebben hun werk op geen enkele wijze ingezien totdat zij het publiekelijk vrijgaven — in het bijzonder is er geen specifieke gebruikersdata geraadpleegd om dit probleem op te lossen. Hoewel onwaarschijnlijk, kunnen we niet uitsluiten dat geanonimiseerde data afgeleid van hun gebruik van onze producten hebben geholpen onze modellen te verbeteren. Echter, onze bewijzen verschillen aanzienlijk en zelfs de precieze resultaten die zijn bewezen zijn verschillend in het Euler-geval (gedreven versus niet-gedreven).
Vooruitgang en verantwoordelijkheid
Ons doel bij het publiceren van dit resultaat is om te rapporteren over de aanzienlijke vooruitgang van onze AI-modellen. We zijn niet van plan de Millennium-prijs voor dit resultaat te claimen.
Deze mijlpaal vertegenwoordigt aanzienlijk werk van wiskundigen en AI-onderzoekers. Dit is echter geen culminatie, maar eerder een momentopname van de voortgang in AI-ontwikkeling.
We geloven dat we ons nu in de volgende periode van AI-vooruitgang bevinden, en de resultaten van vandaag leveren hiervoor verder bewijs. We concentreren ons op het begrijpen van dit model en het gebruiken van wat we leren om ons te helpen bepalen hoe we verdere vooruitgangen in capaciteit nastreven. Een van onze belangrijkste doelen is het bouwen van AI-systemen die stuurbaar, verantwoordelijk en verbonden zijn met mensen, wat bewuste keuzes over het tempo van de vooruitgang kan vereisen, terwijl we onze missie voortzetten om ervoor te zorgen dat AGI de hele mensheid ten goede komt.
***
Voetnoten
- Lees het paper over het Euler-bewijs · Link naar de Lean-geformaliseerde proof.
Over het Navier–Stokes Millennium-prijsprobleem
We delen een oplossing voor het Navier–Stokes-probleem betreffende existentie en gladheid (existence and smoothness), een van de Millennium-prijsproblemen. Dit bewijs, geproduceerd door een intern OpenAI-systeem, toont aan dat de dynamica van de Navier-Stokes-vergelijkingen voor vloeistofbeweging in een eindige tijd een singulariteit kunnen ontwikkelen. We delen zowel een beschrijving van het bewijs als een formalisering in Lean.
De Millennium-prijsproblemen vertegenwoordigen enkele van de diepste vragen op het front van de wiskunde. De vraag of een gladde driedimensionale vloeistofbeweging kan instorten, is ongeveer 90 jaar lang onopgelost gebleven.
Een belangrijk doel van ons werk is om wetenschappers in staat te stellen onderzoek en technologie te bevorderen waar de hele mensheid baat bij heeft. Om het Navier–Stokes-probleem op te lossen, hebben we gebruikgemaakt van een intern model dat aanzienlijk krachtiger is dan GPT-6 Astra. We vinden het belangrijk om de wereld te informeren over het tempo van de AI-vooruitgang en wat men kan verwachten van toekomstige modellen.
Het probleem
De Navier–Stokes-vergelijkingen maken gebruik van de tweede wet van Newton ("F=ma") om te beschrijven hoe vloeistoffen bewegen. Belangrijk is dat zij een vloeistof behandelen als een continu medium in plaats van individuele moleculen te volgen. Deze vergelijkingen worden gebruikt voor het ontwerp van vliegtuigen, weersvoorspellingen en de studie van de bloedstroom.
Een fundamentele open vraag voor deze dynamische vergelijkingen is of de continuümbenadering van de vloeistof kan instorten. Specifiek: kunnen de Navier–Stokes-vergelijkingen voor een driedimensionale, onsamendrukbare vloeistof met constante dichtheid een "singulariteit" ontwikkelen, zelfs wanneer de beweging glad begint? Hier betekent een singulariteit dat de dynamica leiden tot snelheden in de vloeistof die binnen een eindige hoeveelheid tijd onbeperkt groeien. De ontwikkeling van een singulariteit zou moeten plaatsvinden ondanks de aanwezigheid van viscositeit, die de neiging heeft beweging glad te strijken. Omdat een echte vloeistof niet oneindig snel kan bewegen, zou dit een breakdown betekenen in de manier waarop de vergelijkingen de vloeistof modelleren. Om het systeem vervolgens verder te modelleren, zou men het gedrag van elk deeltje individueel moeten volgen.
De vergelijkingen stammen uit het negentiende-eeuwse werk van Claude-Louis Navier en George Gabriel Stokes. In 1934 bewees Jean Leray dat oplossingen in een gegeneraliseerde zin bestaan, maar de vraag of ze altijd glad blijven, werd een centrale onbeantwoorde vraag. In 2000 wees het Clay Mathematics Institute het Navier–Stokes-probleem betreffende existentie en gladheid aan als een van de zeven Millennium-prijsproblemen.
Het resultaat
Ons systeem produceerde een analytisch bewijs en een Lean-formalisering dat een aanvankelijk gladde vloeistof in rust in een eindige tijd een singulariteit kan ontwikkelen. Er wordt een gladde kracht op de vloeistof uitgeoefend, en de energie blijft gedurende de gehele dynamica eindig, van rust tot de vorming van de singulariteit. Dit lost het Navier–Stokes Millennium-prijsprobleem op door bewering "C" (en ook "D") in de officiële Millennium-prijsformulering vast te stellen.
De oplossing is een vortex, een spinnende werveling van vloeistof, die naar binnen spiraalt en steeds meer langgerekt wordt, zoals spaghetti. Dit centrale gebied krimpt terwijl het versnelt, op zo'n manier dat de energie nog steeds eindig blijft, zoals vereist door de wetten van de fysica. De technische uitdaging is dat de vergelijkingen de instorting moeten ontwikkelen door de beweging van de vloeistof zelf, in plaats van bijvoorbeeld dat wij handmatig een oneindige kracht invoeren. Mathematisch gezien moeten de termen in de Navier–Stokes-vergelijkingen die de beweging beschrijven — versnelling, drukgradiënten, momentumoverdracht, viscositeit — zowel groot worden als elkaar op een precieze manier opheffen. Deze gedetailleerde balans zorgt ervoor dat een gladde externe kracht behouden blijft, zelfs terwijl de snelheid van de vloeistof onbeperkt groeit.
Bijschrift: Een momentopname van lokale onsamendrukbare beweging. Oranje markeert snellere hoekrotatie; groenblauw markeert langzamere rotatie. De circulerende snelheid hangt ook af van de straal. De trajecten tonen naar binnen spiraliseren en axiale stretching.
Hoe we het bewijs hebben gevonden
Sinds 28 augustus trainen we een nieuw intern model dat ongekende prestaties heeft getoond in onze benchmarks, waaronder wiskunde. De training van dit model is gaande en de prestaties blijven verbeteren.
Op dinsdag 1 september hoorden we geruchten dat twee Millennium-prijsproblemen waren opgelost. Geïnspireerd door deze geruchten en door de stap in prestaties van ons interne model, startten we een inspanning om het te evalueren op alle open Millennium-prijsproblemen en enkele andere problemen met een grote impact.
We maakten gebruik van een systeem van coördinerende agenten aangedreven door ons interne model. De agenten hadden toegang tot tools, zoals de mogelijkheid om te lezen uit een gecachte versie van het internet en de mogelijkheid om code uit te voeren. Agenten waren onderverdeeld in groepen met de mogelijkheid om binnen de groep te communiceren. De groepen varieerden in grootte; de groep die de Navier–Stokes-resolutie produceerde, bestond uit ongeveer 10.000 gelijktijdige agenten. Te allen tijde hielden we dezelfde strikte waarborgen aan die we toepassen op al onze evaluaties van frontier-modellen, inclusief monitoring en isolatie.
Voor elk probleem gaven we verschillende groepen agenten verschillende varianten van de probleemstelling, waarbij alle varianten van het probleem werden gedekt. Voor het Navier–Stokes-probleem suggereerden we versies "A" en "B" (specifieke vormen van het probleem die zouden resulteren in een bewijs) en versies "C" en "D" (die zouden resulteren in een weerlegging) aan afzonderlijke groepen agenten.
Naast de volledige Millennium-prijsproblemen vroegen we ons multi-agent-systeem om een set "makkelijkere" problemen te proberen. Een van deze problemen was een soortgelijke blowup-vraag voor de limiet van het Navier–Stokes-probleem waarbij de viscositeitsterm was verwijderd. Dit staat bekend als het regulariteitsprobleem voor de Euler-vergelijkingen, en onze agenten verrasten ons door deze vraag op te lossen. De specifieke variant die zij oplosten was de niet-gedreven versie, waarbij geen externe kracht op de vloeistof wordt uitgeoefend. Bijna 100 agenten werkten ongeveer 50 uur samen om onze weerlegging van de Euler-regulariteit te produceren.
Toen we de Euler-oplossing zagen, dachten we dat Navier–Stokes het meest veelbelovende probleem was om aan te werken. Daarom besloten we onze middelen aan Navier–Stokes te wijden. Om dit te doen, verplaatsten we agenten weg van de andere Millennium-problemen en voedden we deze agenten met de Euler-resolutie. Wanneer er gedurende de inspanning een verder getrainde versie van ons interne model beschikbaar kwam, werkten we onze agenten bij naar dat model.
We moedigden verschillende groepen agenten aan om een diversiteit aan benaderingen te verkennen. Na verloop van tijd kruisbestuifden we de agentgroepen door Codex te gebruiken om de meest nuttige inzichten van elke agentgroep te consolideren. Deze vervolgprompts maakten gebruik van de tussenresultaten van de agenten zelf. De groep die de oplossing voor Navier–Stokes vond, werd op deze manier begeleid.
De agenten kwamen tot hun resolutie op zaterdag 5 september, ongeveer 88 uur nadat de eerste agenten waren gelanceerd. De Lean-formalisering en verificatie namen nog eens 17 uur in beslag via GPT-6 Astra.
Over alle geprobeerde problemen heen stuurden de agenten 4,9 miljoen berichten en gebruikten ze ongeveer 300 miljard output-tokens. Tijdens het oplossen van het Navier–Stokes-probleem stuurden de agenten 2,7 miljoen berichten en gebruikten ze ongeveer 130 miljard output-tokens.
Gelijktijdig werk
Onze inspanning begon op 1 september nadat we een gerucht hadden gehoord dat later gerelateerd bleek te zijn aan Levent Alpöge, een medewerker van Anthropic, en Tristan Buckmaster, een professor in de wiskunde aan NYU. Na de voltooiing van ons volledige project en de Lean-verificatie (op 6 september), en in het geloof dat zij op basis van het gerucht ook een oplossing voor Navier–Stokes hadden, namen we contact met hen op om een gelijktijdige release van ons resultaat aan te bieden en hun prioriteit in een gezamenlijke aankondiging te erkennen. Op dat moment ontdekten we dat zij een resolutie hadden van het gedreven (forced) Euler-probleem. In deze discussies boden we hen inzicht in alle prompts die we gebruikten en later de mogelijkheid om het bewijs in te zien. We erkennen de prioriteit van hun werk aan de gedreven Euler en feliciteren hen met hun opmerkelijke wiskundige prestatie.
Wij (de onderzoekers en de agenten) hebben hun werk op geen enkele wijze ingezien totdat zij het publiekelijk vrijgaven — in het bijzonder is er geen specifieke gebruikersdata geraadpleegd om dit probleem op te lossen. Hoewel onwaarschijnlijk, kunnen we niet uitsluiten dat geanonimiseerde data afgeleid van hun gebruik van onze producten hebben geholpen onze modellen te verbeteren. Echter, onze bewijzen verschillen aanzienlijk en zelfs de precieze resultaten die zijn bewezen zijn verschillend in het Euler-geval (gedreven versus niet-gedreven).
Vooruitgang en verantwoordelijkheid
Ons doel bij het publiceren van dit resultaat is om te rapporteren over de aanzienlijke vooruitgang van onze AI-modellen. We zijn niet van plan de Millennium-prijs voor dit resultaat te claimen.
Deze mijlpaal vertegenwoordigt aanzienlijk werk van wiskundigen en AI-onderzoekers. Dit is echter geen culminatie, maar eerder een momentopname van de voortgang in AI-ontwikkeling.
We geloven dat we ons nu in de volgende periode van AI-vooruitgang bevinden, en de resultaten van vandaag leveren hiervoor verder bewijs. We concentreren ons op het begrijpen van dit model en het gebruiken van wat we leren om ons te helpen bepalen hoe we verdere vooruitgangen in capaciteit nastreven. Een van onze belangrijkste doelen is het bouwen van AI-systemen die stuurbaar, verantwoordelijk en verbonden zijn met mensen, wat bewuste keuzes over het tempo van de vooruitgang kan vereisen, terwijl we onze missie voortzetten om ervoor te zorgen dat AGI de hele mensheid ten goede komt.
***
Voetnoten
- Lees het paper over het Euler-bewijs · Link naar de Lean-geformaliseerde proof.
Groetjes,