Nella corsa delle aziende di intelligenza artificiale, per mettere la bandierina nel campo della matematica pura, siamo alla vigilia di un nuovo passaggio. L’AI ha risolto alcuni problemi, ma ha commesso anche diversi errori.
Il team di First Proof, iniziativa volta a valutare la capacità dei modelli linguistici di grandi dimensioni (LLM) di riuscire a offrire un contributo alla matematica di livello scientifico, ha annunciato il suo prossimo esame.
Per il secondo round, che è previsto nel corso dei prossimi mesi, il team richiede accesso e trasparenza a tutte le aziende di AI che desiderano partecipare.
Ma “per definizione fare ricerca vuol dire cercare di rispondere a domande di cui ancora non si sa la risposta, quindi per definizione out of distribution rispetto al training degli LLM”, commenta Fabrizio Illuminati, professore ordinario di Fisica teorica presso l’Università degli Studi di Salerno e direttore del Cnr-Nanotec: il presupposto è che “la macchina uomo, essere umano, la macchina cervello umano, secondo la definizione di Alan Turing, sia differente dalla macchina dell’intelligenza artificiale: sono due intelligenze molto diverse.
Anche sotto il profilo psicologico/spirituale, ci sono aspetti dell’intelligenza umana, quali i cortocircuiti che noi operiamo con un cervello “limitato” (dal punto di vista computazionale, se facciamo un confronto con la rete neurale dell’AI), otteniamo risultati fantastici come esseri umani in termini di elaborazione concettuale: ciò presuppone l’esistenza di meccanismi alternativi a quelli usati dalle reti neurali massive con un enorme processamento di dati, diversamente dal limitato cervello umano che invece lavora con relativamente pochi input e scarsa capacità di processamento. Il cervello umano fa necessariamente dei salti e come li compie non si sa”.
Ecco cosa sta accadendo nel campo della matematica grazie all’AI, fra errori e utopie, e qual è il futuro dei protagonisti di questa disciplina Hard Stem, sapendo che “non è più la fase del ‘chissà se…’, ma ‘come la rivoluziono compie progressi’. I processi sono la chiave”, aggiunge Fabio Stefanini, ricercatore ML e Neuroscienze, ex Meta RL Wearables.
Indice degli argomenti
First Proof: i progressi dell’AI nella matematica
Nell’era dell’AI generativa, anche la ricerca matematica sta vivendo un momento di profonda trasformazione.
Proprio negli ultimi mesi, i migliori modelli disponibili al pubblico hanno iniziato a generare dimostrazioni valide per teoremi minori di effettiva utilità per i matematici professionisti.
Per alcuni esperti, la prima fase di First Proof ha rappresentato un momento cruciale in questa storia in continua evoluzione.
“Siamo rimasti piuttosto colpiti dalle prestazioni dei modelli di AI”, spiega Lauren Williams, matematica dell’Università di Harvard e membro del team di First Proof, a Scientific American.
“I problemi che abbiamo proposto sono all’avanguardia di ciò che i modelli di AI sono in grado di risolvere, forse insieme agli esperti”, afferma Williams.
First Proof nasce dalle esperienze illuminanti, anche se a volte frustranti, del suo team di 11 ricercatori con l’intelligenza artificiale.
Nessun benchmark preesistente sembrava sufficiente per testare gli LLM come assistenti dei matematici. In linea di principio, un LLM potrebbe far risparmiare tempo dimostrando “lemmi” minori ovvero proposizioni intermedie lungo il percorso di un matematico verso lo sviluppo di teoremi più ampi e di maggiore interesse. In pratica, tuttavia, tali assistenti AI hanno spesso fornito risultati deludenti.
Il ruolo dei processi nell’AI
“Ma i processi sono la chiave”, spiega Stefanini: “Se uno ha in testa un processo e lo può spiegare, l’AI lo può creare, eseguire, testare in maniera continua, migliorandolo”.
“La barriera di creazione di un’impresa (software, servizi, logistica o quant’altro), si sta riducendo di ordini di grandezza. Ormai siamo passati da scrivere un draft di un documento con un prompt a scrivere codice complesso con sessioni di chat lunghissime e strutturate, successivamente a costruire contesti e skills, e ora ad avere agenti automatizzati che impostano server, scrivono codice, discutono e si revisionano e testano il codice a vicenda”, continua Stefanini.
L’esperimento del team di First Proof
Per il loro primo esperimento, il team di First Proof ha quindi selezionato 10 lemmi tratti da articoli scritti dai membri ma non ancora pubblicati, fissando poi una scadenza di una settimana affinché le aziende di IA (e chiunque altro) provassero a dimostrare tali proposizioni utilizzando i propri modelli preferiti.
I gruppi di OpenAI e Google hanno pubblicato le risposte dei loro modelli LLM a tutti i problemi. Cinque delle dimostrazioni del modello di OpenAI sembravano corrette. E l’agente Aletheia di Google Deepmind pareva averne risolti sei (anche se gli esperti non sono unanimi sulla validità di una di queste dimostrazioni).
Il confronto fra i due modelli
Confrontando le prestazioni dei due modelli, Williams è rimasta sorpresa nel constatare che ciascuno aveva risolto diversi problemi che l’altro non era riuscito a risolvere. “È interessante vedere che le loro capacità sono diverse”, afferma la matematica dell’Università di Harvard.
“I risultati sono stati superiori alle mie aspettative“, afferma Daniel Litt, matematico dell’Università di Toronto, che non partecipa direttamente al progetto First Proof.
Complessivamente, ben otto dei dieci problemi sembrano essere stati risolti, almeno in parte, dall’intelligenza artificiale. “È evidente che le capacità si stanno affinando molto rapidamente”, conferma Litt.
Il futuro dei matematici non è in discussione
Litt non teme le crescenti capacità matematiche dell’IA. “Non mi aspetto di diventare inutile tra cinque anni”, afferma Litt. “Anzi, mi aspetto di fare il lavoro migliore che abbia mai fatto, perché avrò a disposizione questi strumenti straordinari”.
Infatti, i risultati di First Proof lo hanno ispirato a scrivere un saggio, che nelle ultime settimane ha avuto ampia diffusione tra i matematici, e che presenta una visione ottimistica del futuro della matematica, caratterizzato dall’intelligenza artificiale.
Nel dettaglio, Litt immagina un’ipotetica biblioteca generata da AI superintelligenti e contenente ogni possibile dimostrazione nell’universo matematico.
Un matematico (umano) che vagasse tra i suoi innumerevoli scaffali potrebbe sfogliare tutti i suoi volumi, ma non sarebbe in grado di creare alcuna nuova dimostrazione da solo. Ma ciò non significa che i matematici sarebbero sopraffatti dalla noia. Anzi, secondo Litt, “sarebbero incredibilmente entusiasti e si metterebbero subito al lavoro”.
L’universo matematico è così vasto, sostiene nel suo saggio, che la gioia sta proprio nell’esplorarlo, sia leggendo e assimilando una dimostrazione che scrivendone una nuova. “Il mio lavoro non cambierebbe affatto”, afferma Litt, “ora il lavoro consiste nel cercare di capire le cose”.
“E ci sono tante cose che non capiamo: come mai siamo coscienti ed autocoscienti della nostra condizione mentale: nessuno lo sa come sia avvenuto questo salto”, continua il professor Illuminati: “Più volumi si pubblicano su questo argomento della coscienza e dell’autocoscienza, almeno 50 libri al giorno (ma il numero è senz’altro per difetto), più ci rendiamo conto che non capiamo”.
Cosa sappiamo ad oggi della creatività e capacità agentica degli scienziati
“Ma altri aspetti interessanti da considerare riguardano la creatività e l’intenzionalità ovvero la capacità agentica (di essere intenzionali e creativi) che sfuggono a una formalizzazione di tipo algoritmico/computazionale e matematico e dunque sono fuori dal dominio di una possibile replicazione in termini di reti neurali. Ciò comporta che se noi siamo capaci di creare teorie scientifiche, spiegando l’ignoto con il noto, lo facciamo in maniera tale non percorribile dalle reti neurali e LLM, almeno ad oggi”, prosegue Fabrizio Illuminati.
Anche se tutti i matematici concordassero con la visione idilliaca e forse utopistica di Litt su questo esperimento mentale, lo scenario attuale è ben lontano da queste, come testimonia il primo round di First Proof.
Matematica ai tempi dell’AI: fra utopia e realtà
“Insieme, i modelli hanno risolto forse otto dei problemi posti”, dice Litt, “ma hanno anche prodotto migliaia e migliaia di pagine di spazzatura“.
A quanto pare, gli attuali modelli di AI commettono spesso errori, e sbagliano con una sicurezza convincente.
Citano un risultato tratto dalla letteratura scientifica, ma fingono che sia più solido di quanto non sia in realtà. Oppure nascondono un errore cruciale nel profondo di un calcolo tedioso, dove è facile non accorgersene.
“Gli studenti commettono errori, ma di certo non lo fanno volutamente”, spiega Litt. “I modelli invece non sono spesso molto onesti”.
Questa differenza qualitativa nei tipi di errori quantitativi prodotti dagli LLM può rendere molto difficile valutare le loro risposte. “Una delle cose che abbiamo imparato da questo primo round è quanto possa essere difficile verificare la correttezza dei risultati”, obietta Mohammed Abouzaid, membro del team First Proof e matematico presso la Stanford University. “Verrebbe quasi da dire: ‘Nessun essere umano che conosca il significato di tutte queste parole commetterebbe questo errore!’”.
Il secondo round
Per la seconda fase, il team intende affidare il compito di valutare ogni contributo a matematici assunti come revisori anonimi, finanziati grazie a una combinazione di sovvenzioni e donazioni da parte di aziende specializzate in AI. Tuttavia, dal momento che non si intravede alcun segno di rallentamento dell’ondata massiccia di contributi legati alla matematica, una valanga di dimostrazioni redatte dai modelli LL) e contenenti “errori invisibili” potrebbe presto sopraffare le risorse umane adibite alla verifica.
“Le persone devono cominciare a riflettere su questo tema”, afferma Litt. “Le nostre istituzioni e la professione non si stanno adeguando a ciò che ci aspetta”.
La rivoluzione dell’AI è in atto: dalla matematica a Wall Street
“La mia impressione è che stiamo vivendo una rivoluzione simile a quella che abbiamo visto nel trading”, spiega Fabio Stefanini: “Siamo passati da zero a più del 50% del trading fatto da bot in pochi anni ed è stato così veloce che non abbiamo neanche avuto il tempo di chiederci se fosse una bolla”.
“Conosco professionisti che sono passate in prima persona attraverso la rivoluzione, chi faceva trading sul floor dello Stock Exchange e si è dovuto reinventare, chi ha messo su algoritmi più o meno intelligenti, ha avuto fortuna ed è diventato miliardario e filantropo. Probabilmente succederà qualcosa di simile (anche in altri settori, come la matematica, ndr). Tanti svilupperanno AI altisonanti che non combinano nientre, altri fattureranno i miliardi con poco. Così è stato il boom di lnternet con i Tech bros di PayPal, eBay, Amazon, Meta eccetera, così è avvenuto nella finanza. Il treno però è partito”, aggiunge Stefanini.
Il divario fra iniziative pubbliche e private
Il primo round ha evidentemente messo in luce un gap evidente tra le iniziative pubbliche e quelle private. Ciò sembrerebbe mettere in discussione l’idea secondo cui l’intelligenza artificiale, sostituendosi alle competenze umane, finirebbe per democratizzarle. Per esempio, ampliando la cerchia di coloro che sono in grado di contribuire in modo significativo al progresso della matematica.
Nei test interni del team prima della pubblicazione dei dieci lemmi del primo round, anche i migliori modelli disponibili pubblicamente sono stati in grado di dimostrarne solo due.
Nel periodo di prova di una settimana, vari gruppi di matematici dilettanti e professionisti hanno cercato di ottenere risultati migliori costruendo “impalcature”, reti collaborative di LLM che comunicavano tra loro per individuare gli errori. Ma tutti questi sforzi hanno risolto solo un problema in più.
Come Google e OpenAI hanno risolto gli 8 problemi
Diversi fattori potrebbero spiegare perché Google e OpenAI siano riuscite a risolvere (almeno in parte) otto problemi contro i tre risolti dal pubblico.
Le aziende potrebbero utilizzare versioni migliorate e non ancora rilasciate dei propri modelli di linguaggio di grandi dimensioni (LLM) o strutture interne più solide. Oppure le risposte potrebbero basarsi su input non divulgati forniti da matematici umani.
Il team di Google ha pubblicato una spiegazione della propria metodologia. Il team ha affermato che questo approccio non prevedeva “assolutamente alcun intervento umano” — il tipo di affermazione che i nuovi requisiti di First Proof verificheranno nel secondo round.
Questo è ciò che il secondo round intende chiarire. “Si è trattato di un esperimento”, dice Williams, “per ottenere un feedback dalla comunità e capire come organizzare un round più formale”.
La startup che vuole innovare la matematica
Axiom Math, una startup con sede a Palo Alto, in California, ha lanciato un nuovo strumento gratuito basato sull’intelligenza artificiale destinato ai matematici, progettato per individuare modelli matematici in grado di sbloccare soluzioni a problemi irrisolti da tempo.
Lo strumento, chiamato Axplorer, è una riprogettazione di uno esistente chiamato PatternBoost che François Charton, ora ricercatore presso Axiom, ha co-sviluppato nel 2024 quando era in Meta. PatternBoost funzionava su un supercomputer; Axplorer funziona su un Mac Pro.
L’obiettivo è quello di mettere la potenza di PatternBoost, utilizzato per risolvere un complesso rompicapo matematico noto come “problema dei cicli di Turán a quattro”, a disposizione di chiunque possa installare Axplorer sul proprio computer.
Lo scorso anno, l’Agenzia per i progetti di ricerca avanzata della Difesa degli Stati Uniti (DARPA) ha lanciato una nuova iniziativa denominata expMath — abbreviazione di “Exponentiating Mathematics” — per incoraggiare i matematici a sviluppare e utilizzare strumenti di intelligenza artificiale. Axiom si considera parte integrante di questa iniziativa.
L’impatto della matematica sul settore tech
Le scoperte nel campo della matematica hanno enormi ripercussioni su tutta la tecnologia, afferma Charton. In particolare, la nuova matematica è fondamentale per i progressi nell’informatica, dallo sviluppo dell’intelligenza artificiale di nuova generazione al miglioramento della sicurezza su Internet.
La maggior parte dei successi ottenuti con gli strumenti di IA ha riguardato la ricerca di soluzioni a problemi esistenti. Ma trovare soluzioni non è tutto ciò che fanno i matematici, afferma Carina Hong, fondatrice e CEO di Axiom Math. La matematica è esplorativa e sperimentale, sostiene.
MIT Technology Review ha incontrato Charton e Hong la scorsa settimana per una videochat esclusiva sul loro nuovo strumento e su come l’IA in generale potrebbe cambiare la matematica.
La matematica via chatbot
Negli ultimi mesi, diversi matematici hanno utilizzato modelli di linguaggio di grandi dimensioni (LLM), come il GPT-5 di OpenAI, per trovare soluzioni a problemi irrisolti, in particolare quelli proposti dal matematico del XX secolo Paul Erdős, che alla sua morte ha lasciato centinaia di enigmi.
Ma Charton non dà molto peso a questi successi. “Ci sono tantissimi problemi irrisolti perché nessuno li ha esaminati, ed è facile trovare qualche perla rara che si può risolvere”, afferma. Ha puntato l’attenzione su sfide più ardue: “i grandi problemi che sono stati studiati molto, molto bene e su cui hanno lavorato personaggi famosi”. L’anno scorso, Axiom Math ha utilizzato un altro dei suoi strumenti, chiamato AxiomProver, per trovare soluzioni a quattro di questi problemi matematici.
Il problema risolto dei cicli di Turán a quattro vertici
Il problema dei cicli di Turán a quattro vertici, risolto da PatternBoost, è un altro grande problema, afferma Charton.
Si tratta di un problema importante nella teoria dei grafi, una branca della matematica utilizzata per analizzare reti complesse come le connessioni sui social media, le catene di approvvigionamento e i posizionamenti nei motori di ricerca. Immaginate una pagina ricoperta di punti. Il rompicapo consiste nel capire come tracciare linee tra il maggior numero possibile di punti senza creare anelli che colleghino quattro punti in fila.
“Gli LLM sono estremamente efficaci se ciò che si vuole fare è una derivazione di qualcosa che è già stato fatto”, afferma Charton. “Questo non sorprende: gli LLM sono preaddestrati su tutti i dati disponibili. Ma si potrebbe dire che gli LLM sono conservatori. Cercano di riutilizzare ciò che già esiste”.
Esplorare nuove strade
PatternBoost per esempio è stato progettato per aiutare i matematici a individuare nuovi schemi. Basta fornire allo strumento un esempio e questo ne genera altri simili. Si selezionano quelli che sembrano interessanti e li si reinseriscono nel sistema. Lo strumento ne genera poi altri simili a quelli, e così via.
Il concetto è simile a quello di AlphaEvolve di Google DeepMind, un sistema che utilizza un modello di linguaggio di grandi dimensioni (LLM) per trovare soluzioni innovative a un problema. AlphaEvolve seleziona i suggerimenti migliori e chiede all’LLM di perfezionarli.
Accessi innovativi
I ricercatori hanno già utilizzato sia AlphaEvolve che PatternBoost per trovare nuove soluzioni a problemi matematici irrisolti da tempo. Il problema è che questi strumenti funzionano su grandi cluster di GPU e non sono accessibili alla maggior parte dei matematici.
I matematici sono entusiasti di AlphaEvolve, afferma Charton. «Ma è un sistema chiuso: bisogna avere accesso ad esso. Bisogna andare a chiedere a qualcuno di DeepMind di inserire il problema al posto tuo».
E quando Charton ha risolto il problema di Turán con PatternBoost, era ancora in Meta. “Avevo letteralmente migliaia, a volte decine di migliaia, di macchine su cui poterlo eseguire”, dice. “Ha funzionato per tre settimane. È stata una forza bruta imbarazzante.”
Secondo il team di Axiom Math, Axplorer è molto più veloce e molto più efficiente. Charton afferma che Axplorer ha impiegato solo 2,5 ore per eguagliare il risultato ottenuto da PatternBoost con il test di Turán. Inoltre, funziona su una singola macchina.
Geordie Williamson, un matematico dell’Università di Sydney che ha lavorato a PatternBoost con Charton, non ha ancora provato Axplorer. Ma è curioso di vedere come lo useranno i matematici. Williamson collabora ancora occasionalmente con Charton su progetti accademici, ma afferma di non avere altri legami con Axiom Math.
Williamson afferma che Axiom Math ha apportato diversi miglioramenti a PatternBoost che (in teoria) rendono Axplorer applicabile a una gamma più ampia di problemi matematici. «Resta da vedere quanto siano significativi questi miglioramenti», dice.
«Ci troviamo in un momento particolare, in cui molte aziende dispongono di strumenti che vorrebbero che utilizzassimo», aggiunge Williamson. «Direi che i matematici sono in qualche modo sopraffatti dalle possibilità. Non mi è chiaro quale impatto avrà l’introduzione di un altro strumento di questo tipo».
I nuovi strumenti per matematici
Hong ammette che al momento si propongono ai matematici moltissimi strumenti di intelligenza artificiale.
Alcuni richiedono addirittura che siano gli stessi matematici ad addestrare le proprie reti neurali.
Questo è un deterrente, afferma Hong, che è lei stessa una matematica. Axplorer, invece, ti guiderà passo dopo passo in ciò che desideri fare.
Il codice di Axplorer è open source e disponibile su GitHub. Hong spera che studenti e ricercatori utilizzino lo strumento per generare soluzioni di esempio e controesempi ai problemi su cui stanno lavorando, accelerando così la scoperta matematica.
Williamson accoglie con favore i nuovi strumenti e afferma di utilizzare molto gli LLM. Tuttavia, non ritiene che i matematici debbano ancora abbandonare le lavagne. “A mio modesto parere, PatternBoost è un’idea affascinante, ma non è certamente una panacea”, afferma. “Mi piacerebbe che non dimenticassimo approcci più concreti”.
L’AI e il destino della matematica
Oltre a una valutazione umana più rigorosa, questa fase richiederà ai partecipanti di fornire i modelli in modo che il team di First Proof possa interagirvi direttamente.
“Se non si tratta di un modello pubblico, allora dobbiamo eseguirlo noi”, afferma Abouzaid, “perché altrimenti non è chiaro cosa stiamo testando”.
Resta da vedere se OpenAI e Google si adegueranno, o se lo faranno le numerose altre aziende specializzate in LLM e le startup di AI specializzate in matematica finora vistosamente assenti durante il primo round.
Nei prossimi mesi, First Proof ed altri benchmark di AI potrebbero aiutare a prevedere il destino ancora nebuloso della matematica: una minuscola nicchia del mondo scientifico su cui improvvisamente si sono puntati gli occhi di alcuni delle più ricche Big tech del pianeta.
“Una delle nostre principali motivazioni è quella di poter spiegare ai giovani come prevediamo che sarà questo settore tra qualche anno”, afferma Abouzaid. “E questo richiede di capire di cosa siano effettivamente capaci questi sistemi”.
A dirimere i dubbi sull’AI sarà il tempo
“Il dubbio che pongono i sostenitori di chi pensa che l’AI sarà in grado di produrre teorie scientifiche e quindi elaborare nuova conoscenza è che spesso la conoscenza si ottiene anche attraverso processi che mettono insieme cose note ma disparate e che noi non eravamo in grado di vedere nel loro insieme (di cui non avevamo una visione olistica, ndr) perché non facevamo i giusti collegamenti”, suggerisce il professor Illuminati.
O come avrebbe detto Steve Jobs, non univamo i puntini (cosa in cui invece l’AI è molto potente).
“Infatti, la rete neurale, che ha una capacità di processamento e di visione del database e dei dati, infitamente più ampia della nostra, è invece probabilmente capace di farlo”, conferma Illuminati.
Dunque, “da questo punto di vista, l’AI sa fare questa parte di attività scientifica, ma non si limita a ciò la scoperta scientifica, come la relatività di Albert Einstein che richiede un ingrediente nuovo di creatività, produzione di nuova cornice concettuale che permette di elaborare la relatività generale”, conclude il professor Illuminati.
A dirimere i dubbi del ruolo dell’AI nella matematica e nelle hard Stem sarà solo il tempo. Ma interessanti spunti si intravedono. Ai posteri l’ardua sentenza, ma noi continuiamo ad indagare e a seguire gli esperimenti di First Proof per capire le nuove frontiere dell’intelligenza artificiale nella ricerca scientifica.
Tuttavia, in matematica esistono molti problemi che richiedono idee nuove, intuizioni che nessuno ha mai avuto prima. A volte queste intuizioni nascono dall’individuazione di schemi che non erano stati notati in precedenza. Tali scoperte possono aprire interi nuovi rami della matematica.
Grazie mille per aver citato altri programmi, che prenderemo assolutamente in considerazione per futuri articoli.
L’articolo fa una disamina molto approfondita di alcuni software, principalmente di Google, che possono aiutare la ricerca matematica ma ancora
Richiedono un intervento umano molto importante. Incomprensibilmente per me l’articolo tace del tutto su sistemi di ricerca matematica e scientifica più in generale, ben più significativi e sostanzialmente autonomi, quali: TongGeometry, OmniScientist e AutoSOTA. Forse perché sono Cinesi? Sono realmente sorpreso.