La reivindicació d’OpenAI sobre la demostració de Navier–Stokes, explicada

Les equacions de Navier–Stokes descriuen com es mouen fluids com l’aigua i l’aire. Són centrals per a la dinàmica de fluids, l’enginyeria i la física, però els matemàtics no han tingut una comprensió analítica completa del seu comportament en tres dimensions.

La versió del Premi del Mil·lenni pregunta, a grans trets, si unes condicions inicials suaus sempre porten a solucions suaus per a tot temps futur, o si les equacions poden «explotar» — produint una singularitat en què una quantitat com la velocitat esdevé infinita. El Clay Mathematics Institute va designar el problema com un dels set Problemes del Premi del Mil·lenni l’any 2000, cadascun associat a un premi d’$1 milió. Abans d’aquest anunci, només la conjectura de Poincaré havia estat resolta entre els set, tal com resumeix Wikipedia.

La reivindicació d’OpenAI, segons informa Quanta Magazine, és que agents d’IA autònoms executats sobre un model intern van trobar una singularitat en les equacions tridimensionals de Navier–Stokes. Quanta informa que el treball va utilitzar uns 10.000 agents, que els agents van trobar una demostració després de 88 hores, i que un altre model d’IA va formalitzar el resultat en Lean després de 17 hores addicionals. Els agents van intercanviar gairebé 5 milions de missatges, i Sébastien Bubeck, d’OpenAI, va estimar el cost computacional en diversos milions de dòlars, segons Quanta.

MIT Technology Review informa que OpenAI diu que no té previst reclamar el premi d’$1 milió. Segons Wikipedia, el contraexemple encara no ha estat verificat per matemàtics externs ni pel Clay Mathematics Institute.

Aquest últim punt importa. Una formalització en Lean és un senyal fort, però no és idèntica a l’acceptació de la comunitat. Quanta assenyala que les demostracions formals poden establir que un enunciat se segueix dins de l’assistent de demostració, mentre que els matemàtics encara han de comprovar que l’enunciat formalitzat és lògicament equivalent a la reivindicació matemàtica que es pretenia demostrar.

Les equacions diferencials descriuen relacions entre quantitats canviants. En mecànica de fluids, les equacions de Navier–Stokes combinen velocitat, pressió, viscositat, forces externes i conservació de la massa. Són prou fàcils d’escriure en notació estàndard, però el seu comportament a llarg termini pot ser extremadament difícil d’entendre.

La dificultat central no és si els enginyers poden simular fluids. Ho fan, constantment. La qüestió és si les equacions matemàtiques idealitzades tenen garantit un bon comportament sota les condicions especificades pel problema del Premi del Mil·lenni.

Una singularitat significaria que les equacions prediuen una ruptura: alguna part del fluid evoluciona cap a un estat matemàtic impossible. Tal com explica Quanta, això no implica un fracàs pràctic immediat en l’enginyeria del món real, perquè els fluids reals estan formats per molècules i àtoms, no per continus perfectament suaus. Però, com a matemàtiques, mostraria que les equacions idealitzades tenen un comportament més sorprenent del que molts esperaven.

El problema també connecta amb la turbulència, un dels fenòmens més difícils de la física. Wikipedia descriu la turbulència com un dels grans problemes no resolts de la física, malgrat la seva importància en la ciència i l’enginyeria. Una demostració d’explosió no «resoldria la turbulència» en el sentit pràctic, però remodelaria el que els matemàtics saben sobre les equacions que hi ha al darrere.

La controvèrsia se centra en la relació entre el treball d’OpenAI i el treball de Buckmaster i Alpöge.

Quanta informa que l’anunci d’OpenAI va arribar unes 12 hores després que Buckmaster anunciés resultats amb Alpöge sobre problemes estretament relacionats. El seu treball feia servir diversos models d’IA, incloent-hi models d’OpenAI. MIT Technology Review informa que Buckmaster i Alpöge havien treballat gairebé un any en el problema i que Buckmaster va publicar una demostració que mostrava que una versió simplificada de les equacions de Navier–Stokes pot trencar-se.

Tant el treball d’OpenAI com el de Buckmaster–Alpöge semblen recolzar-se en un enfocament associat amb Diego Córdoba i Luis Martínez-Zoroa. Quanta diu que tots dos equips van dependre molt del treball de Córdoba i Martínez-Zoroa, que van desenvolupar una estratègia que s’allunyava dels mètodes que feien servir la majoria de matemàtics. MIT Technology Review cita Javier Gómez-Serrano, professor de matemàtiques a Brown University, dient que aquest enfocament era un dels diversos que es consideraven prometedors per al problema.

OpenAI ha reconegut, segons MIT Technology Review, que l’equip es va inspirar per abordar el problema després de sentir un rumor sobre els esforços de Buckmaster i Alpöge. La disputa gira al voltant de si els models o empleats d’OpenAI van tenir accés al treball de Buckmaster i Alpöge, s’hi van entrenar o se’n van beneficiar d’alguna altra manera.

MIT Technology Review informa que Buckmaster va publicar un document que descrivia interaccions amb empleats d’OpenAI. Segons el relat de Buckmaster, els empleats d’OpenAI van presentar dues possibilitats. Buckmaster i Alpöge podien publicar el seu treball i OpenAI publicaria la seva solució de Navier–Stokes l’endemà, o Buckmaster podia treballar amb OpenAI en un article sobre Navier–Stokes que excloïa Alpöge de l’autoria a causa de la seva afiliació amb Anthropic. MIT Technology Review també informa que OpenAI va negar que els seus empleats o agents accedissin a les transcripcions de Buckmaster i Alpöge.

Són acusacions serioses, però el registre públic és incomplet. La posició correcta és separar la reivindicació matemàtica de la disputa d’atribució. La demostració pot ser correcta mentre el procés continua sent èticament controvertit. O la demostració pot fracassar sota revisió mentre les preguntes d’atribució continuen important.

Lean és un assistent de demostració: un sistema per expressar enunciats matemàtics i comprovar que cada pas se segueix de regles formals. En matemàtiques d’alt risc, això pot eliminar una gran classe d’errors. També pot fer que les demostracions generades per IA siguin més fàcils d’auditar, perquè la demostració no és només prosa; és lògica formal executable.

Per això el component Lean és important. Si la formalització és sòlida i coincideix amb l’enunciat de Navier–Stokes previst, el resultat esdevé molt més difícil de descartar com una al·lucinació fluida. Per als creadors d’IA, aquesta és la diferència entre un model que escriu raonaments plausibles i un sistema que produeix artefactes que un altre programa pot comprovar.

Però Lean no resol tots els problemes de confiança. No estableix la prioritat. No revela com es va trobar la demostració. No explica si dades privades, transcripcions o idees no publicades van influir en la cerca. I no substitueix el paper de la comunitat matemàtica a l’hora d’interpretar la importància de la demostració.

Aquesta distinció hauria de resultar familiar a les persones que creen productes d’IA. Les sortides estructurades, les proves, les avaluacions i les comprovacions formals poden fer que els sistemes siguin més fiables, però per si soles no responen preguntes de governança. Si un agent d’IA pot cridar eines, inspeccionar registres, reutilitzar context privat o coordinar-se amb altres agents, el sistema necessita límits i pistes d’auditoria tant com capacitat bruta.

Aquesta és una de les raons per les quals el treball multiagent és un problema d’enginyeria, no només un truc de prompting. Tant si dissenyes agents de recerca com fluxos de treball empresarials, les preguntes pràctiques són similars: quins agents poden veure quin context, quines eines poden cridar, on es produeixen els traspassos i què queda registrat? Aquestes decisions de disseny importen en agents d’IA molt abans que les apostes arribin al territori dels Premis del Mil·lenni.

El detall operatiu més cridaner és l’escala. Quanta informa d’uns 10.000 agents, 88 hores de cerca, 17 hores més per a la formalització i gairebé 5 milions de missatges entre agents. MIT Technology Review informa que OpenAI va dir que l’execució va costar milions de dòlars.

Aquesta escala no està a l’abast de la majoria de grups acadèmics. Suggereix un possible futur en què el progrés matemàtic de frontera depèn de models interns, pressupostos privats de computació i infraestructura d’agents concentrats dins d’unes poques empreses d’IA.

MIT Technology Review ho emmarca com un punt d’inflexió per a les matemàtiques: si grans problemes oberts poden ser atacats per eixams privats d’agents, les normes de col·laboració acadèmica poden quedar tensionades. Els matemàtics sovint aprenen d’intents fallits, resultats parcials i camins equivocats. Si tot això passa dins de sistemes privats i mai no es fa públic, el camp pot obtenir respostes sense el camí compartit que tradicionalment crea noves eines i subcamps.

Quanta cita Charles Fefferman, matemàtic de Princeton que va escriure la descripció oficial del problema del Clay Institute, dient que estava encantat que el problema s’hagués resolt i identificant Córdoba i Martínez-Zoroa com els herois de la història. Aquesta atribució és un correctiu útil. Encara que el pas final fos automatitzat, el criteri de recerca — triar una direcció prometedora — va venir de treball matemàtic humà construït durant anys.

Per als creadors, la lliçó no és «fes servir més agents». És que els sistemes agèntics amplifiquen la qualitat de l’espai de cerca que se’ls dona. Models millors i pressupostos més grans ajuden, però l’enquadrament del problema, la selecció de context, l’accés a eines i els bucles de verificació encara determinen si el sistema explora territori útil o crema computació.

Si encamines treball entre múltiples models, el mateix principi s’aplica a menor escala. Fes servir el millor model per a cada tasca, però no tractis l’elecció del model com si fos tot el sistema. El flux de treball que l’envolta — recuperació, restriccions, comprovacions, aprovacions i registres — és d’on ve la fiabilitat. En altres paraules, la capacitat ve de tot el flux de treball, no d’una tria en un rànquing.

El primer que cal seguir és la validació matemàtica. Els matemàtics externs i el Clay Mathematics Institute necessitaran temps per avaluar si la demostració és correcta, si la formalització en Lean coincideix amb la reivindicació prevista i com encaixa el resultat amb el treball previ.

El segon és l’atribució. Els relats públics d’OpenAI, Buckmaster, Alpöge i matemàtics externs encara no formen un registre assentat. Les preguntes centrals són factuals: a què van accedir els agents o empleats d’OpenAI, amb què es van entrenar, què sabien i quan ho sabien?

El tercer és si això es converteix en una plantilla. Si els laboratoris d’IA de frontera poden apuntar eixams massius d’agents a problemes famosos no resolts, vindran més anuncis. Alguns seran nets. Alguns seran disputats. Alguns fracassaran sota revisió. Els camps afectats necessitaran normes per al crèdit, la divulgació, la computació privada i les reivindicacions de prioritat assistides per IA.

Per a les persones que creen amb IA fora de les matemàtiques pures, el missatge és prou clar: la capacitat s’està desplaçant cap als sistemes, no cap als prompts individuals. Agents, eines, encaminament de models i verificació s’estan convertint en la unitat de treball. Els equips que gestionin bé la procedència i la revisió estaran en una posició millor que els equips que només persegueixin sortides més grans.

Continuarem seguint la història de verificació i atribució a mesura que evolucioni. Si vols notícies d’IA amb el context tècnic inclòs, et pots subscriure al butlletí de LIA.

• OpenAI afirma que agents d’IA autònoms van trobar una singularitat en les equacions tridimensionals de Navier–Stokes i van produir una formalització en Lean.
• El resultat encara no ha estat verificat per matemàtics externs ni acceptat pel Clay Mathematics Institute.
• Una demostració en Lean pot reduir molts errors de comprovació de demostracions, però els revisors encara han de confirmar que l’enunciat formal coincideix amb la reivindicació matemàtica prevista.
• L’anunci està embolicat en una disputa d’atribució que implica treball de Tristan Buckmaster, Levent Alpöge, Diego Córdoba i Luis Martínez-Zoroa.
• L’escala reportada de l’execució posa de manifest una bretxa de recursos entre els laboratoris d’IA de frontera i la majoria de grups acadèmics.
• Per als creadors d’IA, l’episodi mostra que els agents necessiten procedència, pistes d’auditoria, bucles de verificació i límits clars, no només més computació.

Aquesta secció respon les preguntes pràctiques darrere de la reivindicació d’OpenAI sobre Navier–Stokes: les respostes següents cobreixen l’anunci, el paper de Lean i les parts que encara necessiten revisió independent. També separa les implicacions matemàtiques de la disputa d’atribució al voltant del treball.

OpenAI diu que té una solució generada per IA, però la reivindicació encara necessita revisió matemàtica externa i avaluació per part del Clay Mathematics Institute.

Segons els informes citats, OpenAI afirma que els seus agents van trobar una singularitat en les equacions tridimensionals de Navier–Stokes i que un altre model va formalitzar el resultat en Lean.

Lean pot comprovar que cada pas formal se segueix de les regles, cosa que fa que la demostració sigui més difícil de descartar com a prosa plausible. Els matemàtics encara han de verificar que l’enunciat formalitzat coincideix amb la reivindicació prevista sobre Navier–Stokes.

La disputa tracta de si el treball d’OpenAI es va beneficiar de recerca assistida per IA de Tristan Buckmaster i Levent Alpöge sense el crèdit adequat. OpenAI ha negat que els seus empleats o agents accedissin a les seves transcripcions, segons MIT Technology Review.

No. Una demostració d’explosió remodelaria la comprensió matemàtica de les equacions darrere del moviment dels fluids, però no resoldria directament la turbulència com a problema pràctic d’enginyeria.