OpenAI ha pubblicato 722 risultati matematici derivati dall'IA. I matematici si chiedono a chi vada il merito.

OpenAI ha diffuso una raccolta di risultati matematici prodotti da un modello frontier interno, pubblicando un repository insieme alle formalizzazioni in Lean di molte delle dimostrazioni e ai protocolli per revisioni e citazioni. Il rilascio descrive 722 risultati, 162 dei quali verificati dalla macchina.

La reazione è stata meno incentrata sulla correttezza della matematica e più su che cosa garantisca davvero la verifica, e a chi appartengano i risultati.

Che cosa verifica Lean, e che cosa no

Lean è un assistente di dimostrazione. Verifica meccanicamente ogni passaggio di un argomento formale rispetto ad assiomi dichiarati, il che significa che una dimostrazione verificata non può contenere lacune logiche. Se compila, l'argomento segue dalle premesse.

È una garanzia forte e al tempo stesso limitata. Un assistente di dimostrazione verifica che l'enunciato formale segua. Non verifica che l'enunciato formale dica ciò che il testo che lo accompagna sostiene. Un essere umano deve comunque leggere ciascuno dei 162 risultati verificati dalla macchina e confermare che il file Lean codifichi il teorema che qualcuno ritiene codifichi. La formalizzazione è un passaggio di traduzione, e le traduzioni derivano.

Gli altri 560 risultati non hanno alcuna verifica di questo tipo, il che significa che la raccolta pubblicata mescola due categorie probatorie molto diverse. Riportare «722 risultati, 162 verificati» è più onesto che riportare il dato aggregato, ma significa anche che il numero di copertina sovrastima il sottoinsieme verificato di circa quattro volte e mezzo.

Il problema del merito ha una nuova forma

I matematici discutono dell'attribuzione dei meriti da quando esiste la disciplina, e le discussioni riguardano di solito chi ha posto la domanda, chi ha trovato il passaggio chiave e chi l'ha messo per iscritto. I risultati generati dall'IA introducono una versione del problema senza precedenti.

Se un modello produce la dimostrazione di un problema aperto di lunga data, chi è l'autore? Il modello, che peraltro non può essere un autore legale secondo gli attuali quadri normativi sul diritto d'autore? I ricercatori che lo hanno sollecitato con i prompt? Il team che ha curato l'elenco dei problemi? L'organizzazione che ha addestrato il modello e che non ne rilascia i pesi?

OpenAI afferma di lavorare a un rilascio responsabile del modello sottostante. Fino ad allora, la comunità non può riprodurre i risultati sullo stesso sistema, ispezionare i dati di addestramento né valutare se il successo del modello sia dipeso dall'aver visto problemi simili durante l'addestramento. Pubblicazione e riproducibilità sono promesse diverse, e questo rilascio mantiene la prima senza la seconda.

C'è un'ulteriore complicazione specifica della matematica: l'attribuzione in questo campo si basa sulla comprensione. Una dimostrazione riceve credito in parte per l'idea che introduce, e il modo in cui un'idea matematica si diffonde passa per le persone che la leggono, la trovano utile e la estendono. Una dimostrazione generata da una macchina che nessuno comprende appieno è un risultato che non può propagarsi in quel modo. Può essere citata. Non è facile costruirci sopra.

C'è anche un'asimmetria pratica che complicherà la peer review per anni. Un matematico umano che pubblica una dimostrazione difettosa è generalmente ritenuto aver commesso un errore in buona fede. La conseguenza reputazionale è proporzionata. Un modello che pubblica 722 risultati, alcuni corretti e altri no, produce un corpus di lavori in cui il rapporto tra corretti e scorretti è esso stesso ignoto, e in cui nessun individuo può essere ritenuto responsabile di quelli sbagliati. Le riviste non sono fatte per gestire sottomissioni la cui paternità è diffusa e il cui tasso di errore è una distribuzione anziché un singolo episodio.

Il problema delle citazioni ne consegue direttamente. Il progresso matematico dipende dal sapere su quali risultati precedenti si possa fare affidamento. Un risultato verificato dalla macchina in Lean è un candidato forte. Un risultato asserito da un modello e revisionato da nessuno non lo è, e mescolare le due categorie in un unico rilascio rende più difficile costruire su entrambe.

L'altra storia dello stesso giorno

Il rilascio matematico di OpenAI è arrivato in una settimana con diverse dichiarazioni di prima parte e non molta verifica di terze parti.

Mistral ha lanciato Large 4, un modello da mille miliardi di parametri presentato come la più forte risposta occidentale ai sistemi cinesi a pesi aperti, con confronti di benchmark che un thread di risposte ha verificato riga per riga rispetto ai punteggi pubblicati da Artificial Analysis, trovandoli carenti: nello specifico, l'accusa di aver scelto selettivamente una variante di un concorrente e di aver riportato in modo errato un dato di terze parti pubblicato.

Reflection ha rilasciato Beam, un modello a pesi aperti puntato alla stessa battaglia, con i pesi in arrivo più avanti nel mese.

E Anthropic ha ampliato l'accesso a un modello che individua vulnerabilità del software, con i propri numeri di prima parte.

Lo schema ricorrente della settimana è che le dichiarazioni di capacità arrivano più in fretta della capacità di verificarle. arXiv ha risposto a una diversa manifestazione della stessa pressione limitando gli autori a due articoli al mese, dopo aver ricevuto un record di 40.363 sottomissioni a settembre, il doppio rispetto a due anni prima.

La competizione riguarda il rendere utilizzabili le dichiarazioni

Esiste una versione della storia IA-e-matematica che viene inquadrata come un tabellone: quanti problemi aperti riesce a chiudere un modello. L'inquadratura più utile riguarda ciò che rende un risultato utilizzabile da una comunità di ricerca, e questo implica diverse cose che un rilascio di modello non fornisce da solo.

I revisori devono capire l'argomento. L'attribuzione deve essere tracciabile. Altri ricercatori devono poter costruire sul risultato senza doverlo ri-derivare. E la comunità più ampia ha bisogno di un accesso sufficiente al sistema generativo per eseguire i propri test.

È su quest'ultimo punto che il rilascio si ferma. Una raccolta di risultati prodotta da un sistema che nessun altro può eseguire è più una dimostrazione che un contributo. Mostra ciò che è possibile. Non consegna al campo nulla su cui possa costruire in modo indipendente.

La matematica non è la parte difficile di questa transizione. La parte difficile è che la capacità dell'IA sta ora superando le istituzioni che esistono per verificarla (peer review, replica dei benchmark, norme di paternità, pratiche di citazione) e quelle istituzioni funzionano su scale temporali umane. Un modello può generare 722 risultati in un ciclo di addestramento. Stabilire quali contino, chi meriti il credito e che cosa ne consegua si misura ancora in anni.

C'è una tesi alternativa che vale la pena esporre, perché non è irragionevole. Una dimostrazione formale che compila è una dimostrazione, a prescindere da chi o da che cosa l'abbia prodotta. La matematica ha sempre accettato i risultati per il loro valore e non per la loro provenienza, e se Lean verifica un argomento, l'argomento regge. Secondo questa tesi, il dibattito sul merito è un problema sociologico che il campo dovrebbe risolvere nei modi ordinari, e l'insistenza sulla riproducibilità è la richiesta di un tipo di accesso che ai matematici umani non è mai stato chiesto di fornire. Nessuno chiede a un autore umano di rendere pubblico il proprio processo di pensiero.

La contro-obiezione è che agli autori umani si può chiedere di spiegare il proprio lavoro, e che è nella spiegazione che risiede la comprensione. Una dimostrazione che arriva senza spiegazione è una scatola nera che per caso ha un output verificato. Il campo può citarla e non può insegnarla, il che è una perdita reale anche se il teorema è vero.

Il consiglio pratico emerso dalla settimana vale per chiunque acquisti capacità di IA e non specificamente matematica: chiedete di vedere le prove, i permessi e il percorso da una dimostrazione riuscita a un lavoro ripetibile. Un risultato di benchmark e un sistema funzionante sono artefatti diversi, e il divario tra i due è dove si annidano le sorprese.