All'inizio di aprile, un team di scienziati di Google ha annunciato di aver sviluppato un'intelligenza artificiale per la dimostrazione automatica di teoremi matematici, che è stata in grado di ricavare senza alcun aiuto più di 1200 nuovi risultati corretti. Lungi dal temere di vedersi sostituiti con delle macchine, alcuni matematici hanno commentato positivamente il successo di Google: in un'intervista per New Scientist, Jeremy Avigad, professore della Carnegie Mellon University, ha affermato che la possibilità di assegnare alcuni compiti di routine a delle macchine permetterà ai ricercatori di lavorare su problemi innovativi e più emozionanti. Eppure, il rapporto tra matematica e intelligenza artificiale non è così semplice come sembra. Pochi giorni prima della notizia sulle capacità di dimostrazione dell'intelligenza artificiale di Google, i colleghi di DeepMind hanno ammesso una sconfitta dell'IA: una rete neurale addestrata appositamente per risolvere esami di matematica ha preso F, l'equivalente italiano del tre, in una verifica di seconda superiore.

Risultati apparentemente contraddittori

Questi risultati sembrano a prima vista contraddittori: qualsiasi matematico può confermare che il lavoro di ricerca richiede intuizione, tenacia, originalità, creatività, mentre la maggior parte delle verifiche scolastiche premiano abilità differenti, come la padronanza di procedure e la capacità di applicarle in modo corretto. Inoltre, la dimostrazione di nuovi teoremi richiede delle conoscenze profonde: proprio a causa della necessità di specializzarsi, la maggior parte dei matematici lavora su pochi ambiti di ricerca, spesso vicini tra loro. Al contrario, le verifiche della scuola superiore dovrebbero essere accessibili alla maggior parte degli alunni, anche quelli che non studiano con particolare dedizione. La dimostrazione di teoremi, insomma, sembra essere molto più difficile rispetto allo svolgimento di un compito in classe. Com'è possibile che l'attività più ostica per gli esseri umani risulti più semplice per le macchine, e viceversa?

Una risposta parziale viene fornita dalla storia della dimostrazione dei teoremi per mezzo dei computer. Infatti, se da un lato quest'attività richiede impegno e specializzazione da parte degli esseri umani, dall'altro lato la maggior parte della matematica moderna si può tradurre in termini algoritmici, quindi comprensibili anche da una macchina. Sfruttando questa rappresentazione, già nel 1929 il matematico polacco Mojżesz Presburger scrisse il primo programma per dimostrare automaticamente i teoremi che riguardano la somma tra numeri naturali, prima ancora che esistessero dei computer in grado di eseguire il suo algoritmo^1,2. A partire dagli anni Sessanta, lo studio delle dimostrazioni per mezzo dei computer è diventato una parte integrante della ricerca in matematica e in informatica. Dopo l'algoritmo di Presburger, infatti, sono stati creati numerosi programmi per automatizzare le dimostrazioni. Alcuni di questi sono ideati per affrontare un singolo problema, come nel caso della dimostrazione del teorema dei quattro colori, mentre altri, come DPLL o E, sono in grado di dimostrare numerosi teoremi di un ambito abbastanza ampio della matematica. Il contributo del team di Google consiste nell'aver modificato uno di questi programmi, HAL Light, aggiungendo una rete neurale in grado di automatizzare alcuni passaggi che nel programma originale devono essere eseguiti da ricercatori in carne e ossa.

La difficoltà non è nella matematica

Alla luce della relativa facilità con cui è possibile dimostrare alcuni teoremi in modo automatico, l'insuccesso del team di DeepMind risulta ancora più incomprensibile: un algoritmo tradizionale avrebbe saputo risolvere in un tempo brevissimo la verifica di seconda superiore sulla quale è inciampata la rete neurale. Questa considerazione suggerisce che le difficoltà nella risoluzione del test non fossero di natura matematica. L'intelligenza artificiale di DeepMind doveva innanzitutto "leggere" la verifica, cioè un insieme di parole, numeri e altri simboli tipici della matematica, e interpretarne il contenuto: un compito paragonabile all'identificazione degli oggetti raffigurati in un'immagine. Quest'analogia permette di capire come mai alcune risposte fornite dalla rete neurale variassero a seconda che la frase si concludesse con un punto fermo oppure no. Il riconoscimento delle immagini, infatti, soffre di un problema simile: già da alcuni anni è noto che delle modifiche impercettibili all'occhio umano possono portare a degli errori grossolani, come scambiare una tartaruga per un fucile. Alla luce di queste difficoltà, non stupisce che la corretta interpretazione dei testi d'esame sia stata identificata dal team di DeepMind come l'abilità sulla quale è necessario compiere i progressi maggiori. Altre competenze simulate in modo poco accurato sono state la pianificazione di una strategia risolutiva e l'utilizzo della cosiddetta "memoria di lavoro" per immagazzinare risultati intermedi. Paradossalmente, quest'ultima caratteristica è tipica dei programmi tradizionali, nei quali è spesso necessario usare la memoria di lavoro anche per svolgere calcoli semplici.

Tenendo conto delle difficoltà non matematiche affrontate dalla rete neurale di DeepMind, la differenza nelle performance delle due intelligenze artificiali non stupisce più. Nel valutare i due risultati, occorre anche considerare che il team di DeepMind non ha sviluppato la sua intelligenza artificiale per ottimizzare lo svolgimento degli esercizi di matematica. Al contrario, con questo esperimento ha voluto iniziare un'indagine su come le macchine affrontino gli stimoli pensati per gli esseri umani, e non semplificati o codificati in un linguaggio artificiale. In quest'ottica, le verifiche di matematica sono uno stimolo relativamente semplice, ma che può dare molti indizi sui modi di ragionare delle macchine. Prima affrontare delle forme di pensiero più complesse, però, l'intelligenza artificiale dovrà almeno imparare a prendere sei in matematica.

Note
1. Mojżesz Presburger, "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt" in Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, 1929
2. Ryan Stansifer, "Presburger's Article on Integer Arithmetic: Remarks and Translation", Technical Report TR84-639. Ithaca/NY: Dept. of Computer Science, Cornell University, 1984