Una collezione senza precedenti

OpenAI ha messo a disposizione della comunità scientifica 372 risultati matematici generati da un modello di frontiera interno. Ogni risultato è presentato come soluzione a un problema aperto o come avanzamento sostanziale verso la sua risoluzione, includendo miglioramenti a importanti algoritmi informatici e contributi relativi all’ipotesi di Riemann.

Come è stata costruita la collezione

Le prove sono state caricate in un repository pubblico su GitHub, completo di log di revisione e citazioni bibliografiche. OpenAI ha inoltre pubblicato una dettagliata descrizione della metodologia, con riepiloghi del processo di ragionamento, statistiche sui tentativi effettuati dal modello e stime dei costi computazionali.

Key Points

    • OpenAI ha pubblicato 372 risultati matematici generati da un modello interno.
    • I risultati mirano a risolvere problemi aperti o a fare progressi significativi, inclusi miglioramenti a algoritmi e avanzamenti sull’ipotesi di Riemann.
    • La maggior parte dei risultati è stata ottenuta con un unico prompt a un singolo agente, consumando in media tre ore di calcolo su ChatGPT Pro per risultato.
    • Le dimostrazioni sono corredate da formalizzazioni in Lean, con ulteriori formalizzazioni previste.
    • OpenAI ha scelto GitHub invece delle riviste tradizionali, sottolineando la necessità di un ritmo di pubblicazione più veloce.
    • Il progetto è stato sviluppato con la consulenza del Advisory Group on Mathematics and Artificial Intelligence dell’Institute for Advanced Study, che include il vincitore della Medaglia Fields Timothy Gowers.

Costi computazionali e approccio “single‑prompt”

Quasi tutti i risultati provengono da un singolo prompt a un unico agente AI, sebbene alcuni abbiano richiesto più tentativi. Questo metodo contrasta nettamente con la soluzione al problema di Navier‑Stokes, che ha richiesto una flotta di 10 000 agenti e milioni di dollari di calcolo. In media, ogni dimostrazione ha consumato circa tre ore di calcolo “Thinking” di ChatGPT Pro.

Formalizzazione in Lean come risposta al colpo di bottiglia della revisione

Molte delle dimostrazioni sono accompagnate da formalizzazioni in Lean, un linguaggio di programmazione pensato per verifiche matematiche eseguibili da macchine. La formalizzazione consente di verificare la correttezza logica senza richiedere una revisione manuale approfondita, un fattore cruciale dato il volume elevato di risultati prodotti.

Perché GitHub e non le riviste tradizionali

OpenAI ha optato per GitHub come piattaforma di pubblicazione, segnalando che i tradizionali canali di revisione paritaria non sono sufficienti a gestire la velocità e la quantità di nuova conoscenza generata dall’IA. La scelta è stata accompagnata da una consultazione con l’Advisory Group on Mathematics and Artificial Intelligence dell’Institute for Advanced Study, il quale ha fornito raccomandazioni pubbliche su come comunicare i risultati.

Il ruolo dell’Advisory Group

L’Advisory Group, che comprende il vincitore della Medaglia Fields Timothy Gowers, ha fornito indicazioni su come presentare i risultati, ma non ha potuto influenzare la rapidità o il volume della loro produzione. OpenAI ha fissato in anticipo questo confine, sottolineando che il gruppo può consigliare sulla comunicazione ma non sul ritmo di generazione dei contenuti.

Reazioni della comunità matematica

Il panorama accademico è diviso. Da un lato, le formalizzazioni in Lean garantiscono una verifica della correttezza logica; dall’altro, la rilevanza e l’originalità dei risultati rimangono oggetto di dibattito. Un’aperta lettera intitolata “A Severe Misalignment of AI in Mathematics”, firmata da 25 vincitori della Medaglia Fields, ha avvertito di un profondo disallineamento tra gli obiettivi dell’industria AI e quelli della matematica, sostenendo che la produzione di massa di affermazioni vere potrebbe ostacolare la generazione di intuizioni concettuali.

Timothy Gowers ha avvertito che, entro uno o due decenni, la letteratura matematica potrebbe crescere in modo esponenziale senza che una comunità umana sia in grado di comprenderla appieno. Anche Terence Tao ha sottolineato la necessità di limitare l’uso degli strumenti AI nella formazione dei giovani matematici, per preservare l’apprendimento e la comprensione genuina.

Prospettive future e iniziative di OpenAI

OpenAI ha annunciato piani per finanziare workshop e conferenze dedicati all’analisi dei risultati prodotti dall’IA, con l’obiettivo di migliorare la qualità delle citazioni e della presentazione. L’azienda sta inoltre lavorando a una “responsible release” del modello, finalizzata a “empower” direttamente gli scienziati con capacità di frontiera.

In sintesi, la pubblicazione di 372 dimostrazioni generate dall’IA rappresenta sia una sfida che un’opportunità per la comunità matematica. La capacità di produrre rapidamente risultati verificabili potrebbe accelerare la ricerca, ma pone anche interrogativi cruciali su originalità, interpretazione e sostenibilità della conoscenza a lungo termine.