Gli LLM riescono a risolvere problemi matematici complessi: cosa significa e perché è importante

Nonostante le capacità linguistiche e di ragionamento dei modelli di intelligenza artificiale, non è affatto scontato che un LLM riesca a risolvere un problema matematico complesso: la matematica di alto livello richiede coerenza logica, controllo preciso delle variabili, capacità di sostenere lunghe catene di ragionamento e attenzione ai casi particolari. Anche un piccolo errore in un passaggio intermedio può compromettere l'intera dimostrazione, e molti modelli finora si sono dimostrati più abili a riconoscere schemi e pattern nei testi che a comprendere realmente le regole della logica o della matematica astratta.

È proprio in questo contesto che il lavoro di Neel Somani assume un significato di particolare importanza. Lo scorso fine settimana, Somani, ingegnere informatico, ex ricercatore quantitativo e fondatore di una startup nell'ambito blockchain, stava mettendo alla prova le capacità matematiche del nuovo modello di OpenAI quando si è imbattuto in qualcosa di inatteso: "Volevo capire quale fosse una base di riferimento, cioè il punto a partire dal quale gli LLM riescono davvero ad affrontare problemi matematici aperti, e dove invece iniziano ad avere difficoltà», ha spiegato Somani. «La sorpresa è stata scoprire che, con il modello più recente, quella frontiera si è spostata un po' più in avanti".

Somani ha sottoposto un problema matematico a ChatGPT che, dopo aver lavorato per circa 15 minuti, ha prodotto una soluzione completa. La dimostrazione è stata esaminata e successivamente formalizzata utilizzando Harmonic, uno strumento di verifica formale che permette di controllare con rigore la correttezza delle dimostrazioni traducendole in un linguaggio logico comprensibile a un computer. Il processo si è concluso senza errori.

A rendere l'episodio ancora più notevole è stato il modo in cui ChatGPT ha costruito il ragionamento, richiamando strumenti classici della matematica come la formula di Legendre, il postulato di Bertrand e il teorema della Stella di David. Lungo il percorso, il modello ha individuato un post del 2013 su Math Overflow, in cui il matematico di Harvard Noam Elkies proponeva una soluzione elegante a un problema affine.

Il risultato finale di ChatGPT, però, non è stato una semplice riebolazione della soluzione di Elkies. La dimostrazione data dal modello di OpenAI si discostava in alcuni punti chiave e arrivava a una soluzione più completa di una variante del problema. Problema, tra l'altro, formulato da Paul Erdős, uno dei matematici più influenti del Novecento. I cosiddetti "problemi di Erdős" costituiscono una vasta collezione di quesiti aperti, spesso semplici da enunciare ma estremamente difficili da risolvere, che Erdős ha lasciato in eredità alla comunità matematica e che oggi rappresentano un banco di prova ideale per misurare il progresso, umano e artificiale, nella comprensione matematica.

I progressi dell'IA nell'affrontare problemi matematici complessi

La matematica, con i suoi problemi aperti e le dimostrazioni rigorose, è uno dei terreni più esigenti per testare un modello linguistico. Se un LLM riesce a muoversi con successo in questo spazio, non si limita a rielaborare soluzioni note, ma diventa uno strumento capace di esplorare territori nuovi, spingendo più in là i confini della conoscenza matematica e dimostrando la capacità di elaborare un vero ragionamento.

Somani ha concentrato l'attenzione sulla raccolta di oltre 1.000 congetture di Erdős. Il primo gruppo di soluzioni autonome era emerso a novembre grazie a un modello basato su Gemini chiamato AlphaEvolve, ma più recentemente anche GPT-5.2 ha mostrato una padronanza sorprendente della matematica di alto livello. Da Natale, 15 problemi sono stati aggiornati da “aperti” a “risolti” sul sito di Erdős, e in 11 casi le soluzioni riconoscono esplicitamente il contributo dei modelli di intelligenza artificiale.

Somani non è il solo ad aver usato GPT-5.2 per risolvere un problema di Erdős. Più o meno contemporaneamente anche il ricercatore Nat Sothanaphan ha pubblicato la soluzione di un altro problema di Erdős utilizzando l'LLM di OpenAI e gli strumenti di Harmonic.

A confermare l'impatto crescente dell'IA nella matematica interviene Terence Tao, matematico australiano di origini sino-irlandesi e vincitore della Medaglia Fields. Sulla sua pagina GitHub elenca otto problemi di Erdős in cui i modelli di IA hanno compiuto progressi autonomi significativi e altri sei casi ottenuti combinando l'analisi dei modelli con ricerche precedenti. Rimane molta strada da percorrere prima che i sistemi di IA possano fare matematica completamente da soli, ma diventa chiaro che i modelli di grandi dimensioni non sono più strumenti passivi: stanno assumendo un ruolo attivo nel plasmare il modo in cui si esplorano e si risolvono problemi complessi.

Tao ha inoltre sottolineato che la natura scalabile dei sistemi di IA li rende "particolarmente adatti ad affrontare in modo sistematico la 'coda lunga' di oscuri problemi di Erdős, molti dei quali possiedono in realtà soluzioni relativamente semplici". "Di conseguenza molti di questi problemi più accessibili hanno oggi maggiori probabilità di essere risolti con metodi basati interamente sull'IA, piuttosto che attraverso approcci umani o ibridi".

Il salto osservato con GPT-5.2 diventa ancora più significativo se confrontato con i modelli precedenti, che erano molto meno efficaci nel risolvere problemi complessi. Prima, gli LLM funzionavano bene per generare testi coerenti, ma mostravano limiti evidenti nel ragionare passo passo su concetti astratti o costruire dimostrazioni rigorose. I problemi matematici di alto livello richiedono lunghe catene di ragionamento, con controllo preciso di variabili e condizioni. I modelli precedenti tendevano a perdere coerenza, commettendo errori logici o saltando passaggi cruciali. Senza strumenti di formalizzazione in grado di tradurre il ragionamento in un linguaggio logico verificabile, le risposte potevano sembrare plausibili ma risultare sostanzialmente errate. Grazie a progressi nell'architettura dei modelli, a una maggiore capacità di memoria contestuale e all'integrazione con strumenti come Harmonic, gli LLM più recenti hanno superato questi limiti, affrontando problemi di matematica aperta con rigore e profondità prima impensabili.

Tutto va quindi inteso come il segnale di un cambiamento più ampio e non come la dimostrazione di capacità isolate. Risultati di questo tipo sono difficili da liquidare come mere curiosità, perché si inseriscono in un contesto in cui l'intelligenza artificiale è già parte integrante del lavoro matematico quotidiano: dai modelli orientati alla formalizzazione delle dimostrazioni, come Aristotele di Harmonic, fino agli strumenti di analisi e revisione della letteratura scientifica, come la ricerca approfondita di OpenAI. Con il rilascio di GPT-5.2, che Somani descrive come "aneddoticamente più abile nel ragionamento matematico rispetto alle versioni precedenti", il volume e la qualità dei problemi affrontati con successo iniziano a tracciare una linea di continuità con quanto osservato nei singoli casi.

La formalizzazione automatizzata

Un elemento che accelera ulteriormente i progressi è il passaggio alla formalizzazione delle dimostrazioni, un compito tradizionalmente laborioso ma che rende il ragionamento più facile da verificare e da estendere. La formalizzazione non richiede necessariamente l'uso di IA o computer, ma strumenti automatizzati hanno semplificato enormemente il processo.

In particolare, il proof assistant open source Lean, sviluppato da Microsoft Research nel 2013, è diventato uno standard per tradurre le dimostrazioni in linguaggio logico rigoroso. Strumenti di IA come il già citato Aristotele di Harmonic promettono di automatizzare gran parte del lavoro, collegando la potenza dei modelli linguistici alla precisione formale richiesta dalla matematica di alto livello.

Tudor Achim, fondatore di Harmonic, osserva che l'aumento dei problemi di Erdős risolti è meno significativo del segnale culturale che esso rappresenta: i più grandi matematici del mondo stanno iniziando a prendere sul serio questi strumenti: "Ciò che mi interessa di più è vedere professori di matematica e informatica usare concretamente l'intelligenza artificiale. Queste sono persone con una reputazione consolidata, quindi quando dichiarano di impiegare Aristotele o ChatGPT, diventa una prova tangibile del valore reale di questi strumenti" ha spiegato Achim. In questo senso, l'adozione accademica si lega direttamente ai progressi osservati sui problemi di Erdős e alla crescente integrazione della formalizzazione automatizzata nel lavoro matematico di alto livello.