Il nuovo modello di OpenAI di Astra lascia a bocca aperta i matematici

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.

I risultati coprono ambiti diversi, tra cui geometria ad alta dimensione, teoria dei codici, complessità computazionale, crittografia basata su reticoli e teoria dei grafi. Tra i progressi dichiarati figurano miglioramenti nel problema del sphere packing, nuovi limiti per codici binari e sferici, avanzamenti sul Closest Vector Problem e contributi nella teoria dei grafi e nei numeri di Ramsey. Alcuni di questi temi hanno implicazioni dirette anche in ambito pratico, come la crittografia post-quantistica.

OpenAI ha indicato che il costo computazionale complessivo per ottenere le dieci dimostrazioni sarebbe intorno ai 2.000 dollari in termini di utilizzo API, evidenziando come la potenza di calcolo resti un fattore chiave. L’azienda ha inoltre pubblicato i passaggi seguiti dal modello e i certificati Lean, favorendo la verifica indipendente.

Resta però necessario il processo di revisione scientifica tradizionale prima di considerare questi risultati come definitivi. OpenAI sottolinea che Astra non ha risolto problemi del Millennium Prize e che molti tentativi non hanno prodotto esiti utili. Più che un punto di arrivo, si tratta di un segnale concreto dell’evoluzione dell’AI nel supporto alla ricerca teorica, con un potenziale impatto significativo nei prossimi anni.