I computer sono estremamente bravi con i numeri, ma non hanno licenziato molti matematici umani. Fino a poco tempo fa, riuscivano a malapena a reggere il confronto nelle gare di matematica delle scuole superiori.
Ma ora il team DeepMind di Google ha sviluppato AlphaProof, un sistema di intelligenza artificiale che eguaglia le prestazioni dei vincitori di medaglie d’argento alle Olimpiadi internazionali di matematica del 2024, segnando solo un punto in meno dell’oro nella competizione di matematica universitaria più prestigiosa del mondo. E questo è un grosso problema.
Percezione vera
Il motivo per cui i computer ottengono scarsi risultati nelle gare di matematica è che, sebbene superino la capacità di calcolo dell’uomo, non sono altrettanto bravi nella logica e nel ragionamento richiesti per la matematica avanzata. In altre parole, sono bravi a fare i calcoli molto velocemente, ma di solito non capiscono il motivo per cui li stanno facendo. Sebbene qualcosa come l’addizione sembri semplice, le persone possono fare dimostrazioni semi-formali o optare per un formalismo completo basato sulla definizione di addizione. Aritmetica del pianoforte che definisce le proprietà dei numeri naturali e operazioni come l’addizione tramite assiomi.
Per eseguire una dimostrazione, le persone devono comprendere la struttura della matematica. Il modo in cui i matematici costruiscono le dimostrazioni, il numero di passaggi necessari per raggiungere una conclusione e l’intelligenza con cui li progettano testimoniano la loro genialità, ingegnosità ed eleganza matematica. “Sai, Bertrand Russell ha pubblicato un articolo di 500 pagine libro per dimostrare che uno più uno fa due”, ha affermato Thomas Hubert, ricercatore di DeepMind e autore principale dello studio AlphaProof.
Il team di DeepMind voleva creare un’intelligenza artificiale in grado di comprendere la matematica a questo livello. Il lavoro è iniziato risolvendo il solito problema dell’IA: la mancanza di dati di addestramento.
Traduttore di problemi di matematica
I grandi modelli linguistici che alimentano i sistemi di intelligenza artificiale come Chat GPT imparano da miliardi di pagine di testo. Poiché il loro database di formazione contiene testi di matematica, tutti i manuali e le opere di famosi matematici, mostrano un certo livello di successo nel dimostrare affermazioni matematiche. Ma sono limitati dal modo in cui funzionano: si basano sull’utilizzo di enormi reti neurali per prevedere la parola o il token successivo in una sequenza generata in risposta a un prompt dell’utente. Il loro ragionamento è statistico per definizione, il che significa che danno solo risposte corrette “a parole”.
