OpenAI pubblica 722 manoscritti su problemi di matematica aperti

Un modello interno non ancora pubblicato ha prodotto 722 manoscritti su problemi di matematica mai risolti prima. Parte è verificata da un sistema automatico, parte no: la comunità matematica è divisa tra stupore e dubbi.

Perché conta

È il caso più esteso finora di un modello AI applicato alla ricerca matematica pura, ma anche un test delle sue debolezze: non tutto quello che l'azienda presenta come risolto è già verificato in modo indipendente, e la comunità matematica lo sta facendo notare apertamente.

In pratica

Non è uno strumento che si possa usare oggi: il modello che ha prodotto i risultati resta interno a OpenAI. Chi è curioso può comunque leggere i manoscritti e le formalizzazioni pubblicate gratis su GitHub.

Il 6 ottobre OpenAI ha pubblicato su GitHub 722 manoscritti matematici, raggruppati in 372 "famiglie" di risultati imparentati tra loro, che secondo l'azienda affrontano problemi di matematica rimasti aperti per anni. A produrli non è stato un modello che si può usare oggi, ma un modello interno di OpenAI, non ancora reso pubblico, lanciato su un elenco di problemi difficili e lasciato lavorare in media tre ore di calcolo per ogni risultato.

Alcuni dei problemi affrontati riguardano aree della matematica molto specialistiche, come la congettura di Barnette, sulla forma di certi grafi geometrici, e la Unique Games Conjecture, uno dei problemi aperti più citati dell'informatica teorica. Per una parte dei risultati, OpenAI ha pubblicato anche una dimostrazione formale in Lean, un linguaggio che permette a un programma, non a una persona, di controllare riga per riga se una dimostrazione matematica è corretta.

Qui arriva il primo limite, scritto dalla stessa OpenAI nel repository: non tutti i manoscritti hanno una dimostrazione Lean che li accompagna, e alcuni risultati non ancora formalizzati, avverte l'azienda, potrebbero contenere errori. Due aree, le dimostrazioni sulla funzione zeta di Riemann e sulla congettura di Hodge, seguono addirittura una procedura di verifica diversa da quella standard.

Nella discussione su Hacker News, i dubbi vanno oltre il singolo errore possibile. Alcuni commenti mettono in discussione il metodo con cui OpenAI ha scelto i problemi aperti da affrontare, basato sul confronto tra più modelli linguistici invece che sul giudizio di matematici: "sono scelte di progettazione, non probabilità misurate di correttezza", ha scritto un commentatore. Altri si chiedono se il modello stia davvero generalizzando tra campi diversi della matematica, o se stia sfruttando cicli verificabili con Lean, apprendimento per rinforzo e una quantità enorme di calcolo su problemi già vicini a quelli visti in addestramento.

Resta un dubbio più di fondo, sollevato da più voci nella discussione: una dimostrazione che nessun matematico riesce ancora a seguire e capire fa avanzare la matematica allo stesso modo di una dimostrazione tradizionale? Il repository, con licenza Apache 2.0, include comunque panoramiche in PDF e riassunti del ragionamento per dieci risultati scelti: un modo per chi è curioso di farsi un'idea senza dover leggere tutti e 722 i manoscritti.