Una congettura vecchia di trent'anni, un modello cinese e una dimostrazione verificata dalla macchina

Una congettura vecchia di trent'anni, un modello cinese e una dimostrazione verificata dalla macchina

Il 15 ottobre, Shanghai AI Laboratory (上海人工智能实验室) ha annunciato che un gruppo di ricerca ha dimostrato il caso tridimensionale della congettura di Ghys, un problema aperto nei sistemi dinamici che resiste dal 1995. Il lavoro è stato sviluppato con Intern-S2, il modello interno del laboratorio, e la dimostrazione finale è stata verificata formalmente in Lean da un gruppo della Peking University (北京大学).

La rilevanza non sta solo nel fatto che un problema difficile sia caduto. Sta nel fatto che l'annuncio è stato costruito attorno a un processo e non a un numero: un modello che produce derivazioni, ricercatori che scelgono su quali linee d'attacco concentrare l'attenzione e un assistente di dimostrazione che certifica ogni passo. Questa combinazione è quella che il settore promette da due anni, ed eccola qui, con un articolo allegato.

Che cosa chiede la congettura

Étienne Ghys ha posto il problema nel 1995. In termini generali, chiede se il comportamento dei sistemi dinamici caotici possa determinarne la classificazione geometrica, il che equivale a chiedere se il moto riveli la forma dello spazio in cui avviene.

Non è la domanda generale a essere stata risolta. Il gruppo ha dimostrato il caso di codimensione uno, cioè l'ambito tridimensionale, rimasto aperto per tre decenni. Questa distinzione conta per leggere l'affermazione con onestà: la congettura completa resta più ampia, ma il caso specifico che finora aveva resistito a tutti è ora chiuso.

La prima passata ha prodotto quattrocento pagine

La meccanica della collaborazione è più interessante del risultato, perché mostra come appare davvero la ricerca uomo-IA minuto per minuto.

La prima esplorazione del problema da parte di Intern-S2 ha prodotto un rapporto di derivazione di circa 400 pagine. Non è una risposta. È un mucchio di ragionamenti candidati, in parte utili e in parte no, esattamente la forma di output che si ottiene quando si chiede a un modello di pensare a qualcosa di genuinamente irrisolto invece di richiamare qualcosa di noto.

Da lì, il lavoro è passato attraverso sette cicli di ragionamento continuato. Il grafo del problema, una mappa delle sotto-affermazioni e di come dipendono l'una dall'altra, è cresciuto da 15 a 389 nodi. La produzione accumulata ha raggiunto circa mille pagine e ha incluso decine di approcci distinti. In ogni fase, i matematici hanno fatto ciò che il modello non può fare da solo: hanno esaminato le proposte, deciso quali aperture erano promettenti e orientato il ciclo successivo.

Xu Disheng, studioso in visita presso il laboratorio e professore alla Greater Bay University, e Zhang Jiesong, ricercatore post-dottorato che segue la congettura dai tempi del dottorato, hanno fornito quel giudizio. L'articolo di Zhang, pubblicato su arXiv il 29 settembre e rivisto il 13 ottobre, è un lavoro a autore singolo con una dichiarazione d'uso dell'IA: il modello ha aiutato a sviluppare le idee e gli argomenti attraverso molteplici cicli di dialogo, e lui ha verificato la matematica in modo indipendente.

La parte che lo rende più di una storia

Le affermazioni secondo cui l'IA risolve la matematica costano poco. Ciò che dà peso a questa è che la dimostrazione è stata formalizzata.

Il gruppo della Peking University, guidato da Bin Dong e Ruochuan Liu, ha usato il proprio framework SHEAF per formalizzare tutti e quattro i teoremi principali, più i risultati di supporto di Ghys da cui dipendono gli argomenti. Formalizzare significa tradurre definizioni, ipotesi e ragionamento in un linguaggio che un computer può controllare, dove ogni passo dell'argomento deve essere scritto esplicitamente invece di essere lasciato a un lettore esperto.

Il lavoro ha richiesto circa cinque giorni, con fino a 100 agenti che operavano in parallelo, e ha prodotto circa 550.000 righe di codice Lean. Lean è un dimostratore di teoremi interattivo. Non gli importa quanto qualcuno si senta sicuro. Controlla la logica e accetta la dimostrazione oppure no.

SHEAF ha organizzato il compito come un grafo orientato di definizioni, proposizioni e dipendenze, così che agenti separati potessero lavorare su pezzi collegati mentre il gruppo seguiva quali affermazioni avevano una dimostrazione e quali ne avevano ancora bisogno. È un tipo di divisione del lavoro genuinamente nuovo, e il framework ha anche dovuto colmare lacune nella libreria formale esistente per i sistemi dinamici, perché l'attrezzatura necessaria a questa dimostrazione semplicemente non esisteva ancora.

Umani e modello, compiti diversi

La divisione del lavoro descritta dal laboratorio merita di essere presa alla lettera, perché non è la versione lusinghiera per nessuna delle due parti.

Il modello ha setacciato la letteratura, ha spezzato la proposizione in pezzi, ha esplorato rami di dimostrazione in parallelo, ha controllato i passaggi logici e ha testato un gran numero di idee rapidamente. Gli umani hanno fissato la direzione, giudicato quali approcci valesse la pena perseguire e preso le decisioni che stabilivano dove spendere lo sforzo del ciclo successivo.

Nessuna delle due metà assomiglia all'altra. Il contributo del modello è scala e resistenza: riesce a tenere a mente decine di vicoli ciechi senza scoraggiarsi. Il contributo degli umani è il gusto, cioè la capacità di guardare cento pagine di ragionamento plausibile e sapere quali tre paragrafi contano.

C'è un aneddoto collegato, di cui la stampa cinese ha fatto gran caso. Un esperto di sistemi dinamici avrebbe sottoposto lo stesso problema a GPT-6 per curiosità, dopo aver sentito che un modello nazionale l'aveva risolto, e non ci è arrivato. Letto in senso stretto, è un confronto tra due sistemi su un problema, il che dimostra molto poco. Letto come segnale sulla dinamica competitiva, è il tipo di dettaglio che muove gli investimenti.

Perché la verifica formale cambia la posta in gioco

Per gran parte degli ultimi due anni, il collo di bottiglia della matematica assistita dall'IA non è stato generare argomenti candidati. I modelli sono bravi a produrre ragionamenti plausibili. Il collo di bottiglia è stato sapere quale parte sia corretta, perché controllare una dimostrazione è lento, richiede esperti e non si parallelizza bene.

Lean inverte questo. Una volta che un enunciato è formalizzato, la verifica è economica e rapida, e ci si può fidare perché è meccanica e non sociale. Le 550.000 righe sono la parte costosa, e il fatto che un gruppo più cento agenti abbiano potuto produrle in cinque giorni è il vero progresso qui. Suggerisce che il collo di bottiglia della verifica possa allentarsi proprio mentre quello della generazione era già allentato.

Il laboratorio dice che impacchetterà il flusso di lavoro come modulo riutilizzabile di verifica matematica sulla sua piattaforma di scoperta scientifica, collegando modello, agenti, dati e attrezzatura sperimentale. Cita anche un risultato precedente, in cui un gruppo della Wuhan University (武汉大学) ha usato la piattaforma per ridurre il ciclo di sviluppo di una sintesi elettrochimica da cinque a dieci anni a uno o due.

Che cosa trarne

Il riassunto onesto è che si tratta di un risultato reale con una dimostrazione reale, prodotto da un flusso di lavoro ancora molto intensivo in termini di persone. Sette cicli di guida esperta non sono un modello che gira da solo. Un articolo a autore singolo con dichiarazione d'uso dell'IA non è un modello che rivendica il merito.

Ciò che è cambiato è che ora il ciclo si chiude. Un modello può produrre ragionamento sufficiente a contare su un problema che nessuno ha risolto, gli umani possono guidarlo e un assistente di dimostrazione può certificare l'esito senza che nessuno debba fidarsi di un riassunto. È una pipeline, non una demo, e sono le pipeline a trasformare una capacità in una pratica.

La domanda successiva è se questo si generalizzi oltre i casi in cui la formalizzazione è persino possibile. La geometria e la dinamica hanno una struttura che si presta al controllo automatico. Gran parte del resto della scienza no, ed è in quel territorio più disordinato, in biologia, nei materiali e in medicina, che la promessa dell'IA come assistente di ricerca sarà davvero messa alla prova. Il risultato di Ghys dice che lo strumento può funzionare. Non dice ancora con quale frequenza.