OpenAI ha condiviso i primi risultati di Astra, una nuova famiglia di modelli di Intelligenza Artificiale ancora in sviluppo, presentandola come un passo concreto verso l’uso dell’AI nella ricerca matematica avanzata.
L’azienda afferma di aver ottenuto progressi su dieci problemi aperti tra matematica e informatica teorica, alcuni irrisolti da oltre dieci anni. L’aspetto più rilevante è la pubblicazione di dimostrazioni formalizzate e verificabili, un elemento che rafforza la credibilità scientifica dei risultati. Questo approccio segna una differenza rispetto ai precedenti modelli linguistici, spesso limitati nel ragionamento complesso e nella gestione di lunghe catene logiche.
OpenAI Astra e il ragionamento matematico avanzato
Secondo OpenAI, Astra è progettato per affrontare problemi che richiedono ragionamenti estesi, con migliaia o milioni di passaggi logici. Il modello utilizzato nei test è una versione interna, non ancora accessibile al pubblico, e rappresenta un’evoluzione rispetto ai sistemi attuali, soprattutto nella capacità di pianificare e verificare processi complessi nel tempo.
Le dimostrazioni sono state generate dal modello e successivamente rielaborate dai ricercatori in forma di articoli matematici. Un elemento centrale è l’uso di Lean, un assistente per dimostrazioni che consente di formalizzare ogni passaggio e verificarne automaticamente la correttezza. Questo riduce il rischio di errori e permette alla comunità scientifica di controllare in modo rigoroso i risultati. L’integrazione tra AI e strumenti di verifica rappresenta oggi uno dei punti più solidi nella ricerca, perché combina creatività computazionale e validazione formale.
