In un mondo dove l’intelligenza artificiale si vende come miracolo al grammo, il paper “Limitations of GPT-4 for formal mathematics” pubblicato da OpenAI e ambientato nei laboratori aridi della matematica formale, arriva come un’aspra doccia scozzese su chi crede che stiamo per sostituire i matematici con dei transformer addestrati a suon di GPU e caffeina. L’oggetto? L’analisi chirurgica delle performance di GPT-4 nel regno della matematica formale, usando Lean, il sistema di proof assistant sviluppato per togliere il sonno a filosofi e informatici da tastiera.
L’illusione è evidente fin dalla prima pagina: ci hanno venduto GPT-4 come un oracolo, ma messo davanti a problemi veri, rigorosi, con regole, assiomi e deduzione pura… inciampa come uno stagista al primo giorno di lavoro. Altro che AGI dietro l’angolo.
Il cuore pulsante del paper è l’abilità, o meglio l’inabilità, di GPT-4 di interagire con Lean 3. Parliamo di scrivere e correggere proofs formali, non di risolvere espressioni da liceo. OpenAI ha collegato GPT-4 a una REPL (Read-Eval-Print Loop) di Lean, dotandolo di capacità di editing iterativo. In pratica, un copilota intelligente che può tentare, sbagliare, rileggere l’errore del compilatore e provare a correggersi. L’output non è valutato in modo soggettivo, ma solo se la prova compila in Lean – criterio binario, oggettivo, inesorabile. O è vero, o è sbagliato. Fine.
Eppure, anche con un sistema di interazione raffinato, con feedback automatico e correzione iterativa, GPT-4 fallisce miseramente sulla matematica avanzata. Su un benchmark da 800 problemi selezionati dal mathlib di Lean, un modello vanilla (senza interazione) raggiunge un misero 20% di success rate. Il metodo iterativo “search” arriva a malapena al 35%. E stiamo parlando di problemi già risolti in Lean – quindi con una soluzione perfettamente nota e formalizzabile.
Tradotto: GPT-4, anche se collegato a un assistente logico, riesce a risolvere un terzo di problemi per cui esistono già le risposte. Gli altri due terzi restano nel limbo dell’incapacità. Ora, provate a immaginare cosa succede su un problema realmente nuovo. Esatto: il buio.
A peggiorare la situazione c’è un’altra scoperta tragicamente ironica. Le performance di GPT-4 su questi task formali non sembrano correlate con la difficoltà percepita dagli umani. Tradotto: GPT-4 si perde in bicchieri d’acqua e ogni tanto risolve problemi da Olimpiadi. Non c’è coerenza, non c’è mappa cognitiva, solo interpolazione e salti nel buio. Un comportamento che, più che intelligenza, sembra l’equivalente algoritmico del lancio dei dadi.
E non è tutto. Quando GPT-4 tenta di correggersi dopo un errore, spesso produce versioni nuove… e sbagliate. Quasi mai risolve il problema dopo un fallimento. L’abilità metacognitiva, il “capire dove si è sbagliato”, è ridicolmente scarsa. In molti casi, le iterazioni successive peggiorano la situazione. Una dinamica che ricorda certi middle manager: tanto zelo, poca efficacia.
In una parte del paper che sa quasi di commedia, viene analizzato un approccio in stile “active learning” – far votare a GPT-4 le sue stesse risposte e scegliere quella con il punteggio più alto. L’efficacia? Marginale. Una specie di referendum tra dilettanti, in cui il meno peggio vince. Ma la verità matematica non è una democrazia. Un teorema non diventa vero perché GPT-4 lo vota a maggioranza.
La morale, neanche troppo nascosta, è che i modelli di linguaggio come GPT-4 hanno una comprensione superficiale della matematica formale. Brillano nell’imitazione, non nella deduzione. Sono eccellenti pappagalli stocastici, ma falliscono quando il significato va oltre la forma. Possono generare testo che sembra un teorema, ma raramente riescono a chiudere un ragionamento logico fino al “qed”.
Nel settore tech ci piace raccontarci favole sul prossimo salto quantico, sull’AGI che sta per sbucare da una release di ChatGPT. Ma questo paper smonta con freddezza da sala operatoria quella narrazione. Il vero ragionamento formale – quello dei logici, dei matematici puri, dei sistemi come Lean – resta ancora lontano dall’essere replicabile da modelli linguistici.
Un’osservazione da bar, tanto per bilanciare il tutto: in fondo, ci aspettavamo che un modello addestrato su internet – dove la matematica è un’opinione e le dimostrazioni si fanno su Reddit – fosse in grado di scrivere proof formalmente corrette in Lean? È come sperare che uno chef stellato impari a cucinare guardando solo TikTok. L’apparenza c’è, la sostanza manca.
Intanto, nei laboratori, si continua a perfezionare questi modelli, con la speranza che la prossima versione capisca davvero cosa sta facendo. Ma la matematica non perdona. E l’intelligenza, quella vera, non si improvvisa.
Quindi sì, GPT-4 è brillante, sorprendente, a tratti geniale. Ma messo davanti al rigore della matematica formale, mostra la sua natura più profonda: quella di un illusionista, non di un matematico.