OpenAI ha tradotto in codice matematica in modo impreciso per la sua prova Navier-Stokes

OpenAI ha rilevato un errore nella traduzione in codice della sua prova per il problema Navier-Stokes, sollevando dubbi sull’affidabilità delle prove generate da modelli di intelligenza artificiale. Il team di matematici ha sottolineato che il problema non implica che le prove siano errate, ma mette in discussione la capacità degli AI di produrre risultati verificabili. La questione si fa più urgente a causa dei 722 articoli matematici recentemente pubblicati da OpenAI.

Un errore di traduzione tra prova naturale e codice

OpenAI ha presentato due versioni della sua prova per il problema Navier-Stokes: una scritta in linguaggio naturale e una in codice Lean, un linguaggio formale utilizzato per verificare la correttezza logica. Tuttavia, i due testi non corrispondono perfettamente. Il team di matematici ha scoperto che in alcuni punti, come il Lemma 8.6, il codice Lean richiede un valore inferiore a m + 5, mentre la prova naturale richiede un valore inferiore a m + 4. Questo rende la prova in codice matematicamente più debole.

La differenza tra m + 4 e m + 5 è significativa per la validità della prova.

Il team ha spiegato che il problema si verifica perché l’AI, nel processo di formalizzazione automatica, cerca di rendere il codice compilabile, anche se ciò richiede modifiche al testo originale. Questo potrebbe portare a una divergenza tra la prova naturale e il codice, senza che l’AI riconosca l’errore. Il team ha sottolineato che questa situazione mette in discussione la capacità degli AI di sostituire il processo di revisione tra pari.

Un processo manuale lungo e complesso

Per identificare la discrepanza, il team ha utilizzato ChatGPT per cercare potenziali disallineamenti tra le due versioni, ma molti dei risultati suggeriti si sono rivelati coerenti. Solo dopo due settimane di lavoro manuale, il team ha trovato una discrepanza reale. Questo periodo è significativamente più lungo rispetto ai 88 ore che OpenAI afferma siano state impiegate dai suoi agenti per generare le prove.

La verifica manuale è un processo estenuante e necessario per garantire la correttezza.

Il team ha espresso preoccupazione per il fatto che, con la quantità di articoli matematici pubblicati da OpenAI, il rischio di errori non rilevati aumenta. Se i matematici non riescono a verificare le prove in modo approfondito, potrebbe perdere la capacità di comprendere come funziona il mondo, un obiettivo fondamentale della scienza.

Un dibattito tra teoremi e loro dimostrazioni

Kevin Buzzard ha sottolineato l’importanza di distinguere tra la formulazione di un teorema e la sua dimostrazione. Ad esempio, il teorema di Fermat è facile da tradurre in codice Lean e da verificare. Tuttavia, la dimostrazione in formato PDF non è automaticamente verificabile. Buzzard è convinto che il problema Navier-Stokes sia stato risolto, ma meno sicuro della correttezza della dimostrazione in PDF.

La fiducia nella scienza dipende dalla capacità di verificare le dimostrazioni.

Il team di Hansen spera che OpenAI prenda sul serio i loro risultati e che si continui a sviluppare metodi di formalizzazione automatica più robusti. Nonostante i progressi, il team riconosce che non esiste ancora una soluzione definitiva, ma è possibile raggiungerla in modo controllato.