Per decenni, i computer sono stati considerati semplici calcolatori ad alta velocità, strumenti incapaci di competere con l’intuizione e il ragionamento creativo dei matematici umani nelle competizioni più prestigiose.
Questa percezione è stata recentemente scardinata dai ricercatori di DeepMind, il laboratorio di intelligenza artificiale di Google, che hanno sviluppato AlphaProof, un sistema di IA in grado di eguagliare le prestazioni delle medaglie d’argento alle Olimpiadi Internazionali di Matematica del 2024.
Il sistema ha totalizzato un punteggio di soli un punto inferiore alla medaglia d’oro in quella che è universalmente riconosciuta come la competizione matematica universitaria più importante a livello globale, un traguardo che segna una svolta epocale nel campo dell’intelligenza artificiale.
Dalla pura potenza di calcolo alla comprensione della matematica
La ragione per cui, storicamente, i computer hanno ottenuto risultati deludenti nelle gare matematiche risiede in una distinzione fondamentale.
Sebbene le macchine superino di gran lunga le capacità umane nell’esecuzione di calcoli complessi, sono tradizionalmente rimaste indietro nelle abilità di logica e ragionamento deduttivo, competenze essenziali per la matematica avanzata.
In altre parole, un computer può eseguire milioni di operazioni al secondo, ma fatica a comprendere il perché quelle operazioni siano necessarie per arrivare a una dimostrazione.
Un’operazione come l’addizione può sembrare elementare, ma un matematico umano può costruire dimostrazioni semi-formali basate sulle definizioni o ricorrere all’aritmetica di Peano, che definisce le proprietà dei numeri naturali e delle operazioni attraverso un sistema assiomatico completamente formale.
L’arte della dimostrazione: un territorio umano per eccellenza
Per portare a termine una dimostrazione, è necessario comprendere la struttura stessa della matematica.
Il modo in cui i matematici costruiscono le prove, il numero di passaggi necessari per giungere a una conclusione e l’ingegnosità con cui questi passaggi vengono progettati sono una testimonianza della loro brillantezza e dell’eleganza matematica.
“Come sapete, Bertrand Russell pubblicò un libro di 500 pagine per dimostrare che uno più uno è uguale a due”, ha dichiarato Thomas Hubert, ricercatore di DeepMind e autore principale dello studio su AlphaProof.
L’obiettivo del team di DeepMind era proprio sviluppare un’intelligenza artificiale in grado di comprendere la matematica a questo livello profondo, spostando il focus dalla mera esecuzione di calcoli alla genuina comprensione dei principi.
La sfida dei dati e il traduttore di problemi matematici
Il lavoro è iniziato affrontando il solito problema che affligge lo sviluppo dell’IA: la carenza di dati di addestramento di alta qualità.
I grandi modelli linguistici che alimentano sistemi di IA come Chat GPT apprendono da miliardi di pagine di testo.
Poiché nei loro database di addestramento sono presenti anche testi di matematica, inclusi manuali e opere di matematici famosi, questi modelli mostrano un certo grado di successo nel dimostrare enunciati matematici.
Tuttavia, il loro approccio presenta dei limiti intrinseci: si basano sull’utilizzo di immense reti neurali per prevedere la parola o il token successivo in sequenze generate in risposta alle richieste dell’utente.
Il loro ragionamento è di natura statistica, il che significa che tendono a restituire risposte che “sembrano” corrette, senza una garanzia di rigorosa correttezza logica.
Per superare questa barriera, il team di DeepMind ha adottato una strategia innovativa, trasformando AlphaProof in una sorta di traduttore di problemi matematici.
Il sistema è stato progettato per convertire i problemi complessi delle Olimpiadi in un linguaggio formale che un altro sistema, chiamato AlphaGeometry, potesse elaborare e utilizzare per generare dimostrazioni verificabili e strutturate.
Questa simbiosi tra diverse abilità computazionali ha permesso ad AlphaProof di navigare con successo nel terreno insidioso della matematica olimpica, dove l’intuizione e la creatività sono tanto importanti quanto la precisione tecnica.
Il successo di AlphaProof non rappresenta solo un trionfo tecnico, ma solleva anche profonde questioni sul futuro della ricerca matematica e sul ruolo che l’intelligenza artificiale potrà svolgere come collaboratrice, e non solo come strumento, dei matematici umani.
