The Pulse
OpenAI pubblica 722 manoscritti di matematica prodotti da un modello non ancora rilasciato
OpenAI ha pubblicato 722 manoscritti di matematica su GitHub il 6 ottobre, affermando che i risultati sono stati prodotti da un modello interno non ancora rilasciato. La raccolta comprende alcune formalizzazioni di dimostrazioni in Lean, ma
AI.info Team · Scritto con l’IA ·
«Rendere pubblico questo lavoro è un primo passo. Questa pubblicazione segna l’inizio, non la conclusione, del processo attraverso cui le persone comprenderanno il lavoro e lo integreranno nelle conoscenze matematiche.»
The Advisory Group on Mathematics and Artificial Intelligence
OpenAI ha pubblicato 722 manoscritti di matematica su GitHub il 6 ottobre, affermando che i risultati sono stati prodotti da un modello interno non ancora rilasciato. L’azienda ha organizzato i manoscritti in 372 famiglie di lavori correlati e ha pubblicato alcune formalizzazioni di dimostrazioni in Lean, un linguaggio di programmazione che consente ai computer di verificare le dimostrazioni matematiche.
La pubblicazione mette a disposizione dei matematici un’ampia raccolta di ricerche generate dall’IA da esaminare, ma il repository di OpenAI sottolinea che i lavori si trovano in fasi diverse di verifica. Il repository precisa che non tutti i manoscritti sono accompagnati da formalizzazioni in Lean e l’azienda avverte che alcuni risultati non formalizzati potrebbero presentare problemi. Il modello stesso non è incluso nella pubblicazione.
Da circa 4.000 problemi a 722 manoscritti
OpenAI afferma di aver sottoposto circa 4.000 problemi al modello interno durante la valutazione. I manoscritti così prodotti si distribuiscono in 372 famiglie, ciascuna delle quali può contenere un risultato principale, argomentazioni correlate, conseguenze o dimostrazioni alternative. Secondo l’azienda, ogni risultato ha richiesto in media risorse di calcolo equivalenti a circa tre ore di ragionamento di ChatGPT Pro con il modello interno.
Questa cifra indica una media, non una quantità di risorse di calcolo identica per ogni risultato. OpenAI segnala due eccezioni alla sua procedura generale: un lavoro su una regione priva di zeri per la funzione zeta di Riemann e una dimostrazione della congettura di Hodge per le varietà abeliane CM. Aggiunge inoltre che un testo riguardante la funzione zeta è stato rivisto da persone per renderlo più leggibile.
Il repository comprende 10 sintesi abbreviate dei ragionamenti del modello, insieme a informazioni sui problemi affrontati e a stime delle risorse di calcolo impiegate. OpenAI afferma che conserverà la cronologia della pubblicazione e registrerà le revisioni come nuove versioni, mantenendo accessibili quelle precedenti.
Le formalizzazioni in Lean riguardano solo una parte della raccolta
Gli artefatti in Lean possono consentire ai lettori di verificare una dimostrazione formalizzata mediante un sistema verificabile da un computer. OpenAI afferma che molte dimostrazioni sono state formalizzate e promette di aggiungerne altre man mano che saranno disponibili. La precisazione del repository è importante: un manoscritto privo di formalizzazione non è stato sottoposto a quel particolare tipo di verifica, e una formalizzazione non dice di per sé ai lettori quanto un risultato sia significativo o comprensibile.
La raccolta su GitHub precisa che i suoi articoli presentano risultati in fasi diverse di verifica e riconosce che i lavori non formalizzati potrebbero presentare problemi. OpenAI afferma che cercherà di risolverli rapidamente. Nella pubblicazione, l’azienda non ha indicato il nome del modello né annunciato una data in cui lo renderà disponibile; afferma di essere al lavoro per rilasciarlo in modo responsabile.
Secondo i consulenti, la pubblicazione dà inizio alla valutazione da parte delle persone
L’Advisory Group on Mathematics and Artificial Intelligence, un gruppo indipendente che OpenAI afferma di aver consultato, ha dichiarato che la pubblicazione non deve essere interpretata come un’approvazione dei risultati o del processo che li ha prodotti. Il gruppo ha affermato che solo la comunità matematica può valutare il lavoro e ha sottolineato che la pubblicazione dà inizio, anziché porre fine, all’impegno per comprenderlo e integrarlo nella matematica.
Nelle sue raccomandazioni di settembre, il gruppo ha invitato le aziende di IA a pubblicare responsabilmente i risultati matematici significativi, fornire dettagli su come sono stati prodotti, formalizzare le dimostrazioni ove possibile e sostenere il lavoro che aiuta le persone a comprenderli. Nella dichiarazione del 6 ottobre, il gruppo ha affermato di aver discusso quelle raccomandazioni con OpenAI, ma ha lasciato ai matematici il giudizio su quanto l’azienda le abbia seguite.
OpenAI afferma che finanzierà workshop, conferenze e altri programmi dedicati alla comprensione dei principali risultati prodotti dall’IA. Non ha ancora annunciato i dettagli di questi programmi. Per ora, i 722 manoscritti della raccolta sono disponibili per essere esaminati, con l’avvertenza, contenuta nel repository dell’azienda stessa, che non tutti sono corredati da formalizzazioni in Lean e che alcuni risultati non formalizzati potrebbero contenere errori.