Recerca
OpenAI reclama una solució al problema de Navier-Stokes amb 10.000 agents i obre una disputa per l'autoria
OpenAI va anunciar que un desplegament massiu d'agents d'IA va produir en 88 hores una proposta de solució al problema de Navier-Stokes, un dels set Millennium Prize Problems (Problemes del Mil·lenni) dotats amb un milió de dòlars. L'anunci va arribar acompanyat de formalitzacions en Lean i d'una polèmica immediata sobre el crèdit i el paper dels matemàtics humans que ja treballaven en el mateix terreny.
Rep el resum diari d'IA
Cada matí, l'essencial de la intel·ligència artificial al teu correu, sense fum. Al dia amb la IA.
En subscriure-t'hi acceptes rebre el butlletí d'AI Informator. Pots donar-te de baixa quan vulguis.
En resum
- OpenAI afirma haver emprat uns 10.000 agents coordinats durant 88 hores per a generar una proposta de demostració sobre Navier-Stokes.
- El cost declarat de l'operatiu ronda els 22 milions de dòlars i uns 300.000 milions de tokens de sortida.
- La companyia va publicar les formalitzacions en Lean de Navier-Stokes i Euler en un repositori públic de GitHub per a permetre'n la verificació.
- El matemàtic Tristan Buckmaster va difondre una declaració pública sobre la cronologia de la seva pròpia recerca, i va obrir una disputa sobre l'atribució de l'avenç.
El problema que fa gairebé un segle que es resisteix
Les equacions de Navier-Stokes descriuen el moviment de fluids viscosos: des de l'aigua que es remena en una tassa fins als corrents atmosfèrics. La pregunta oberta, formulada pel Clay Mathematics Institute com un dels seus Problemes del Mil·lenni, és si aquestes equacions admeten sempre solucions suaus o si poden desenvolupar una singularitat, un punt on les magnituds es disparen cap a l'infinit i el model deixa de tenir sentit.
Demostrar l'existència de singularitats en temps finit, o descartar-la, té conseqüències que van molt més enllà de les matemàtiques pures: afecta la fiabilitat de la simulació numèrica en aeronàutica, meteorologia i oceanografia. Per això la comunitat matemàtica tracta qualsevol reclamació en aquest terreny amb una cautela extrema i exigeix verificació independent abans de donar res per tancat.
La verificació formal és el punt clau de l'anunci
L'element més comprovable de l'anunci no és el resultat en si, sinó que OpenAI va publicar formalitzacions en Lean, un demostrador assistit per ordinador (proof assistant) que verifica mecànicament cada pas lògic d'una demostració. Una prova que compila en Lean no depèn de la confiança en qui la va escriure: el mateix sistema rebutja qualsevol salt injustificat.
Aquesta és la diferència substancial respecte a episodis anteriors de suposats avenços matemàtics generats per models de llenguatge. El repositori NavierStokesAndEuler permet a tercers executar la verificació pel seu compte. Fins que la comunitat no completi aquest escrutini i el Clay Mathematics Institute no es pronunciï, la proposta continua sent això: una proposta pendent de validació.
La disputa per l'autoria revela un problema estructural
Tristan Buckmaster, especialista reconegut en dinàmica de fluids i singularitats, feia temps que treballava en la mateixa direcció i va publicar una declaració que detalla la cronologia de la seva recerca. El desacord gira entorn de quina part del treball previ va alimentar el resultat, en quina mesura les línies d'atac ja publicades van orientar la cerca automatitzada i com s'ha de repartir el crèdit.
El cas exposa una tensió que la comunitat científica encara no ha resolt: quan un sistema automatitzat escala una idea humana prèvia fins a completar-la, no hi ha cap convenció clara d'autoria. Les normes de coautoria de les revistes científiques es van dissenyar per a persones, i cap no preveu l'estatus d'una infraestructura de còmput que consumeix milions de dòlars en una setmana.
El cost marca el veritable límit d'aquest enfocament
Els 22 milions de dòlars i els 300.000 milions de tokens declarats situen aquest experiment fora de l'abast de qualsevol departament universitari. L'estratègia consisteix essencialment en força bruta dirigida: llançar milers d'agents que exploren branques de l'espai de demostracions en paral·lel i filtrar després allò que sobreviu a la verificació formal.
Aquest model només és reproduïble per un grapat de laboratoris amb accés a còmput a aquesta escala, cosa que introdueix una asimetria inquietant en la recerca matemàtica. Si els grans resultats passen a dependre del pressupost de GPU disponible, la frontera del coneixement es desplaça cap a qui la pot pagar, no necessàriament cap a qui té la millor idea.
Conclusió
Convé separar dues coses que l'anunci barreja. La primera és tècnica i verificable: hi ha formalitzacions en Lean publicades que qualsevol pot comprovar, i aquest és un estàndard de rigor molt superior al de les demostracions en llenguatge natural que els models havien anat produint. La segona és institucional i està sense resoldre: com s'atribueix el mèrit, com es reconeix el treball humà previ i què significa investigar quan el factor limitant és el pressupost de còmput. El resultat matemàtic es validarà o caurà en les properes setmanes mitjançant l'escrutini de la comunitat. La pregunta sobre qui signa els descobriments de la dècada vinent trigarà bastant més a respondre's.
Fonts primàries
Rep el resum diari d'IA
Cada matí, l'essencial de la intel·ligència artificial al teu correu, sense fum. Al dia amb la IA.
En subscriure-t'hi acceptes rebre el butlletí d'AI Informator. Pots donar-te de baixa quan vulguis.
Comentarios