OpenAI presenta Astra con dieci progressi nella ricerca matematica

🤖 Cosa cambia

• Astra ha ottenuto dieci risultati su problemi aperti di matematica e informatica teorica, alcuni studiati senza progressi decisivi da decenni.
• Gli argomenti sono stati trasformati in manoscritti con supervisione umana e formalizzati dal modello attraverso certificati verificabili con Lean.
• OpenAI definisce Astra il proprio prossimo grande modello, ma non ha comunicato disponibilità, prezzi o integrazione in ChatGPT.

OpenAI ha presentato i primi risultati ottenuti con una versione interna di Astra, indicato dall’azienda come il proprio prossimo grande modello di intelligenza artificiale. Il sistema ha risolto o fatto avanzare dieci problemi aperti di matematica e informatica teorica, attraversando settori come geometria ad alta dimensionalità, teoria dei codici, complessità computazionale, crittografia basata sui reticoli e combinatoria. Gli argomenti individuati dal modello sono stati trasformati in manoscritti con l’intervento di ricercatori umani e successivamente formalizzati attraverso certificati Lean, verificabili in modo automatico. OpenAI non ha ancora annunciato una data di lancio, un nome commerciale definitivo o le modalità con cui Astra potrebbe essere distribuito agli utenti.

Astra affronta problemi matematici aperti da decenni

La novità non consiste nel superamento di un benchmark costruito con domande già risolte, ma nell’impiego di un modello non ancora pubblico su problemi per i quali la comunità scientifica non disponeva di una soluzione completa o di progressi sostanziali. Nella presentazione ufficiale dei dieci risultati ottenuti con Astra, OpenAI afferma che il sistema ha lavorato su questioni appartenenti a geometria ad alta dimensionalità, teoria dei codici, complessità dei circuiti aritmetici, teoria dei gruppi, algebre degli operatori, complessità quantistica, crittografia lattice-based e combinatoria estremale. Tra i risultati figurano nuovi limiti superiori per l’impacchettamento di sfere in dimensioni elevate, miglioramenti esponenziali per codici binari e sferici, la costruzione di gruppi non sofici e una confutazione della congettura di rigidità di Connes. Astra ha inoltre prodotto nuovi limiti inferiori per il calcolo del permanente mediante circuiti aritmetici, un risultato sulla ripetizione parallela nei giochi quantistici e progressi relativi al closest vector problem, problema computazionale centrale anche per la sicurezza della crittografia post-quantistica. La raccolta comprende infine risultati sulla congettura del volume di Ehrhart, sui numeri di Ramsey multicolore e su due problemi formulati da Paul Erdős nella teoria estremale dei grafi. OpenAI presenta questi lavori come un avanzamento rispetto ai modelli generalisti destinati principalmente alla conversazione, alla programmazione e all’elaborazione dei documenti. La traiettoria era già visibile nell’evoluzione di GPT-5.6 Sol e delle sue capacità di ragionamento avanzato, ma Astra viene descritto come un sistema capace di sostenere attività di ricerca più lunghe, articolate e verificabili.

Lean verifica formalmente gli argomenti prodotti dal modello

Il punto più delicato riguarda la verifica delle dimostrazioni, perché un modello linguistico può generare argomenti plausibili contenenti errori logici, passaggi mancanti o riferimenti inesistenti. OpenAI ha organizzato il lavoro in più fasi: Astra ha individuato gli argomenti matematici, ricercatori umani li hanno trasformati in manoscritti e il modello ha successivamente formalizzato ogni soluzione attraverso un certificato Lean. Lean è un linguaggio e un proof assistant che verifica i singoli passaggi rispetto a un insieme esplicito di regole logiche, impedendo che una dimostrazione venga accettata soltanto perché appare linguisticamente convincente. Il documento tecnico pubblicato da OpenAI con i dieci lavori completi raccoglie gli argomenti, le definizioni e le costruzioni utilizzate nei diversi settori. La formalizzazione non sostituisce comunque la revisione scientifica. Un certificato può dimostrare che una conclusione segue correttamente dalle premesse formalizzate, ma la comunità deve ancora valutare l’importanza dei risultati, l’originalità delle tecniche, il rapporto con la letteratura precedente e l’eventuale presenza di ipotesi troppo restrittive. OpenAI ha riconosciuto direttamente questa responsabilità, precisando che l’emergere di sistemi capaci di contribuire alla ricerca matematica solleva questioni che non possono essere risolte da una singola azienda tecnologica. Il processo utilizzato con Astra riduce quindi il rischio di allucinazioni matematiche, ma non elimina la necessità di controllo umano, confronto tra specialisti e pubblicazione attraverso i normali canali accademici.

Il ruolo dell’AI passa dall’assistenza alla scoperta scientifica

Astra rappresenta un cambiamento nel modo in cui OpenAI posiziona i propri modelli per la ricerca. I sistemi precedenti erano utilizzati soprattutto per riassumere pubblicazioni, cercare connessioni nella letteratura, generare codice, controllare calcoli o proporre ipotesi da verificare. Nei dieci lavori presentati, il modello viene invece descritto come il soggetto che ha prodotto gli argomenti centrali, mentre gli esseri umani hanno curato la preparazione dei manoscritti, la verifica e l’assunzione di responsabilità scientifica. Questa distinzione apre un problema di attribuzione: una scoperta non può essere ricondotta esclusivamente alla macchina, perché la selezione dei problemi, l’infrastruttura, la valutazione e la pubblicazione dipendono dal lavoro umano, ma non può neppure essere descritta come una normale ricerca assistita quando il nucleo dell’argomento viene generato dal modello. OpenAI collega Astra al programma ChatGPT for Academic Researchers, destinato a fornire a 100.000 scienziati e matematici accesso gratuito ai modelli più avanzati dell’azienda. La strategia amplia l’attività già avviata con strumenti dedicati alla ricerca e conferma la volontà di trasformare l’AI in un’infrastruttura scientifica, non soltanto in un prodotto di produttività. Questa evoluzione richiederà criteri più rigorosi per documentare il contributo delle macchine, conservare le tracce del processo di scoperta, distinguere le intuizioni originali dalla ricombinazione della letteratura esistente e impedire che risultati non verificati vengano presentati come teoremi acquisiti.

OpenAI non ha ancora annunciato il lancio di Astra

OpenAI definisce Astra il proprio prossimo grande modello, ma non ha comunicato se questo nome verrà mantenuto al momento del rilascio né se il sistema diventerà una nuova generazione della famiglia GPT. Non sono stati indicati prezzi, limiti di utilizzo, requisiti hardware o una data di integrazione in ChatGPT e nelle API. L’azienda ha dichiarato che la quantità complessiva di token necessaria per trovare le dieci soluzioni avrebbe avuto un costo di circa 2.000 dollari applicando le tariffe API di Sol, ma questa cifra non rappresenta il costo effettivo del progetto. Restano esclusi l’addestramento del modello, l’infrastruttura, lo sviluppo degli strumenti, i tentativi non riusciti e il lavoro dei ricercatori coinvolti. Il dato suggerisce tuttavia che, una volta disponibile un sistema sufficientemente avanzato, l’esplorazione di problemi matematici complessi potrebbe richiedere costi di inferenza accessibili anche a gruppi di ricerca privi di grandi infrastrutture computazionali. La capacità effettiva di Astra dovrà essere valutata su problemi selezionati da soggetti indipendenti e in condizioni differenti da quelle predisposte durante lo sviluppo interno. I dieci risultati mostrano una direzione precisa, ma non dimostrano ancora che il modello possa affrontare con la stessa efficacia qualsiasi problema matematico aperto. Astra emerge quindi come una piattaforma sperimentale orientata alla scoperta scientifica, la cui portata reale dipenderà dalla riproducibilità dei risultati, dalla revisione della comunità e dalle condizioni con cui OpenAI deciderà di renderla disponibile.