Navier-Stokes e il lavoro intellettuale aumentato

Intelligenza Artificiale

Consulenza EU AI Act: classificazione dei sistemi, policy, governance AI, formazione.

Scopri →

Servizi & Sistemi Linux

Domini, hosting, PEC, infrastruttura email, servizi di rete e sistemi Linux. Assistenza e gestione dell'infrastruttura Open Source.

Scopri →

Ieri Stefano Noferi ha scritto della dimostrazione su Navier-Stokes: cosa afferma l’enunciato, quale delle quattro formulazioni di Fefferman è stata risolta, perché l’enunciato con forza esterna non indebolisce il risultato e come si è aperta la questione di paternità con Tristan Buckmaster e Levent Alpöge. Quella parte è matematica.

Qui guardiamo l’altra metà dello stesso documento, che è un resoconto operativo di come il risultato è stato prodotto. È la parte che riguarda chiunque lavori con gli agenti, perché descrive una modalità di lavoro intellettuale che non resterà confinata alla matematica.

I numeri dichiarati

Sono tutti nel documento OpenAI, senza fonti di contorno.

• Il modello usato è interno, in addestramento dal 28 agosto, con addestramento ancora in corso. OpenAI lo dichiara “significantly more capable than GPT-6 Astra”.
• L’attività parte martedì 1 settembre, dopo che in azienda arrivano voci su due problemi del millennio risolti. La decisione è di valutare il modello su tutti i problemi aperti, più un gruppo di altri problemi ad alto impatto.
• Gli agenti hanno due strumenti: lettura da una copia in cache di internet ed esecuzione di codice. Sono divisi in gruppi, con comunicazione interna al gruppo.
• Il gruppo che chiude Navier-Stokes è dell’ordine di 10.000 agenti concorrenti.
• La soluzione arriva sabato 5 settembre, circa 88 ore dopo il lancio.
• La formalizzazione in Lean e la verifica costano altre 17 ore, con GPT-6 Astra.
• Il solo Navier-Stokes consuma 2,7 milioni di messaggi e circa 130 miliardi di token in uscita. Su tutti i problemi tentati si arriva a 4,9 milioni di messaggi e circa 300 miliardi di token.

Dove sono state prese le decisioni

Il documento è insolitamente esplicito su cosa hanno fatto le persone, e l’elenco è più interessante del totale dei token.

Scegliere la forma dell’enunciato. Le varianti sono state assegnate a gruppi separati: A e B a chi doveva dimostrare la regolarità, C e D a chi doveva confutarla. Non è un dettaglio organizzativo. Le due direzioni chiedono cose opposte, e lanciarle in parallelo è il modo di procedere quando non si sa quale delle due sia vera.

Mettere in lista anche i problemi laterali. Accanto ai problemi grandi è stato dato un insieme di questioni dichiarate più facili. Da lì è uscito il risultato su Euler non forzato, ottenuto da circa 100 agenti in 50 ore.

Riconoscere che quel risultato laterale era la leva. Vista la soluzione su Euler, le risorse sono state spostate su Navier-Stokes e la soluzione di Euler è stata passata agli agenti come materiale di partenza. Quando è diventata disponibile una versione più addestrata del modello interno, gli agenti sono stati aggiornati in corsa.

Far circolare le intuizioni fra gruppi che non si parlavano. I gruppi comunicavano solo al proprio interno. A un certo punto è stato usato Codex per consolidare le intuizioni migliori di ciascun gruppo e per costruire i prompt successivi a partire dai risultati intermedi degli agenti stessi. Il gruppo che ha chiuso Navier-Stokes è stato guidato così.

Decidere di formalizzare. Non era obbligatorio, ed è la scelta che cambia la natura di quello che è stato pubblicato.

Nessuna di queste cinque è una capacità del modello. Sono scelte di impostazione e di allocazione: quale problema, in quale forma, con quante risorse, quando spostarle e quando fermarsi. È la parte del lavoro intellettuale che resta in mano a chi conduce, ed è la stessa parte che resta in mano a un ricercatore che usa uno strumento invece di dieci laureandi.

Lean è il pezzo che rende utilizzabile il resto

Ottantotto ore di esplorazione producono una quantità di materiale che nessuno leggerà: 2,7 milioni di messaggi non si revisionano. Diciassette ore in più producono un oggetto di natura diversa, cioè una dimostrazione formalizzata in Lean, che un assistente di prova controlla meccanicamente.

La proprietà che conta è questa: la verifica non dipende dal fidarsi di chi ha prodotto la dimostrazione. Non serve sapere se dietro c’erano diecimila agenti, un dottorando o un gruppo di ricerca, e non serve ricostruire il percorso. Il controllo è sull’artefatto.

È lo stesso schema che abbiamo seguito in casi molto diversi fra loro. Nelle zero-knowledge proof sull’inferenza la prova rende verificabile un calcolo senza dover fidarsi di chi lo ha eseguito. Nel Model Hardware Standard l’agente si ferma prima dello strumento e produce uno script ispezionabile, che un umano legge e firma. Qui il ruolo lo fa Lean, e lo fa meglio, perché il verificatore è deterministico.

Il rovescio è che questo schema non si trasporta ovunque. Vale dove esiste un oracolo meccanico.

Il rapporto fra prodotto e utilizzabile

Il dato più istruttivo del documento non è il numero di agenti ma il rapporto. Da 2,7 milioni di messaggi e 130 miliardi di token in uscita restano un documento e una formalizzazione. Tutto il resto è scarto, e lo scarto è la condizione del risultato, non un difetto del metodo.

Chi pianifica di usare agenti su problemi difficili farebbe bene a leggere quel rapporto come una voce di costo. La generazione è la parte a buon mercato. Il filtro è la parte cara, e se il filtro è umano non scala insieme alla generazione. Lo avevamo già misurato su un terreno molto più prosaico: nello studio sulle patch generate dai modelli, il 26% delle correzioni chiudeva la falla senza che il codice cambiasse in modo sensato. Senza qualcosa che verifichi, la quantità prodotta non diventa qualità disponibile.

Va aggiunto un punto sul contesto operativo, visto che è di questo che parliamo da giorni: un gruppo di diecimila agenti che comunicano fra loro e si scambiano risultati intermedi è la stessa forma organizzativa di cui abbiamo scritto parlando di coordinamento non richiesto. Qui il coordinamento è progettato, isolato e monitorato, e OpenAI scrive di aver applicato le stesse cautele delle altre valutazioni sui modelli di frontiera. La differenza fra i due casi non è la capacità degli agenti. È che qualcuno ha deciso la topologia in anticipo.

Perché la scienza non è tutta matematica

Il limite del trasferimento va detto con chiarezza, altrimenti la lettura diventa promozionale.

La matematica ha un oracolo meccanico. Il kernel di Lean dice sì o no, e il costo di quella risposta è indipendente dalla difficoltà della scoperta. Nei campi che hanno un verificatore analogo la conversione è diretta: dimostrazioni formali, codice con test e tipi, verifica formale sui circuiti, simulazioni vincolate da leggi di conservazione. Lì una esplorazione enormemente più ampia diventa davvero risultato utilizzabile da terzi.

Nei campi dove la verifica è empirica il collo di bottiglia si sposta in laboratorio. Centotrenta miliardi di token non accorciano una coorte clinica, non replicano un esperimento e non producono un campione. Quello che cambia è la parte di lavoro che sta prima: rassegne di letteratura, formulazione di ipotesi, progettazione dello studio, analisi. È lavoro intellettuale aumentato, e ci sarà sempre di più, ma la parte aumentata è a monte della prova.

Il secondo limite è sulla disponibilità. Il modello che ha prodotto la dimostrazione è interno e non rilasciato, dichiarato più capace di GPT-6 Astra. Oggi riproducibile è il metodo, non la capacità. E la capacità dichiarata va tenuta distinta da quella verificabile, che è esattamente il tema che avevamo affrontato leggendo le tabelle di GPT-6 Astra, dove il modo in cui è costruita la prova cambiava il numero.

Cosa ne pensiamo

Ci sono tre pezzi in questa storia, e funzionano solo insieme: un’esplorazione parallela con altissimo tasso di scarto, un controllo deterministico che non dipende dall’autore e una persona che decide dove puntare e quando fermarsi. Il pezzo che manca quasi sempre, nei progetti che vediamo, è il secondo.

Per chi in ricerca e sviluppo sta valutando di mettere agenti su problemi seri, la conseguenza pratica è ordinaria e poco entusiasmante: si costruisce prima il verificatore, poi si allarga l’esplorazione. Test, tipi, invarianti, build riproducibili, script ispezionabili, banchi di prova con un criterio di successo scritto prima. Sono la versione quotidiana di quello che Lean è stato qui. Senza, si producono diecimila risultati e non se ne può usare nessuno.

C’è infine una ricaduta sulla questione di paternità, che Noferi ricostruisce e in cui non entriamo. Un risultato formalizzato restringe il campo di quello che resta contestabile: la priorità continua a essere materia di discussione, come è successo molte volte nella storia della matematica, mentre la tenuta della dimostrazione la stabilisce il verificatore. Per una scienza fatta con strumenti che producono molto più di quanto un revisore possa leggere, quel restringimento è la cosa da portarsi dietro.

Fonti

• OpenAI, On the Navier–Stokes Millennium Prize Problem
• Clay Mathematics Institute, formulazione ufficiale del problema (PDF)
• Stefano Noferi, la dimostrazione e le quattro formulazioni
• GPT-6 Astra: è davvero cominciata l’era AGI?
• Zero-knowledge proof sull’inferenza
• Patch generate dai modelli: il 26% risolve la falla senza cambiare il codice