OpenAI ha offerto una prima panoramica di Astra, una famiglia di modelli non ancora rilasciata, progettata per affrontare problemi complessi che richiedono uno sforzo prolungato nel tempo. L’azienda afferma che una versione interna del sistema ha contribuito a 10 progressi nella matematica e nell’informatica teorica.
In un aggiornamento di ricerca, OpenAI ha dichiarato che non si erano registrati progressi sui risultati fondamentali di questi problemi da almeno 10 anni, mentre alcuni erano rimasti irrisolti per un periodo considerevolmente più lungo. Il lavoro ha riguardato aree come la geometria ad alta dimensionalità, la teoria dei codici, la complessità dei circuiti aritmetici, la teoria dei gruppi, la complessità quantistica, la crittografia basata sui reticoli e la combinatoria estremale.
OpenAI ha citato diversi risultati come esempi, tra cui lavori sui gruppi non sofic, una confutazione della congettura di rigidità di Connes, limiti migliorati per l’impacchettamento di sfere ad alta dimensionalità e soluzioni a diversi problemi associati al matematico Paul Erdős. L’azienda ha stimato che la generazione delle soluzioni abbia richiesto circa 2.000 dollari di utilizzo del modello alle tariffe dell’API di Sol.
La verifica formale faceva parte del processo
I ricercatori umani hanno utilizzato l’output del modello per sviluppare manoscritti matematici formali. Astra ha quindi tradotto ogni argomentazione in un certificato per Lean, un assistente alla dimostrazione in grado di verificare meccanicamente se il ragionamento formalizzato è valido. Questo ulteriore passaggio di verifica mira a distinguere le congetture o gli argomenti generati dalle macchine dalle dimostrazioni che possono essere controllate autonomamente dal software.
OpenAI ha descritto Astra come il suo “prossimo grande modello”, ma non ha annunciato una data di rilascio né il nome definitivo del prodotto. Anche alcune indiscrezioni pubblicate da The Information hanno indicato che l’azienda sta sviluppando una famiglia di modelli destinata a carichi di lavoro prolungati, compresi i compiti in cui gli agenti di IA suddividono tra loro parti di un problema più ampio.
Il nome commerciale e la disponibilità del modello restano ancora da definire. Secondo quanto riferito, potrebbe essere presentato come GPT-5.7, GPT-6 o con un nome diverso. OpenAI potrebbe inoltre offrire ampiamente una versione meno potente, limitando al contempo l’accesso alle varianti più avanzate, in modo simile alle politiche di sicurezza e accesso adottate da altre aziende di IA.
I risultati matematici riportati evidenziano il potenziale dei sistemi capaci di combinare ragionamento prolungato, collaborazione e verifica formale. Tuttavia, le affermazioni di OpenAI riguardano ricerche interne e dovranno essere valutate più approfonditamente quando saranno disponibili ulteriori dettagli tecnici, risultati verificabili in modo indipendente e informazioni sul prodotto.