Google sembra fare sul serio: dopo i successi di AlphaZero, che ha imparato a giocare a scacchi testandosi in partite contro sé stesso ed è poi riuscito a sconfiggere i più potenti motori scacchistici (ben più forti del campione del mondo di scacchi), il colosso di Mountain View ha presentato un algoritmo in grado di dimostrare teoremi. La ricerca è stata recentemente pubblicata su ArXiv.
Dopo la fase di apprendimento in cui ha elaborato migliaia di documenti matematici (oltre 10.000 teoremi già dimostrati dall’uomo), l’algoritmo è stato testato con 3.225 teoremi, dimostrandone più di un terzo, 1.253. L’apprendimento automatico ha funzionato anche perché, oltre ai teoremi, sono stati anche spiegati all’algoritmo i concetti matematici di base (un vero e proprio corso di matematica) e le strategie con cui di solito si dimostrano i teoremi.
Andare oltre l’intelligenza umana
Di fronte a questi successi molti si chiedono se sia possibile andare oltre l’intelligenza umana; in fondo, con gli scacchi, Google ha fatto centro. In realtà, la situazione con gli scacchi è molto “facilitata”: gli scacchi non sono un gioco di intelligenza (tanto è vero che se si spiegano le regole a una persona geniale, molto intelligente, ma neofita del gioco, e la si fa giocare contro uno scacchista di intelligenza media, ma che gioca da anni, il nostro genio non avrà chance), ma un gioco dove, a parità di altri fattori, prevale l’intelligenza “matematica” e in cui gli altri fattori sono la velocità di elaborazione delle informazioni (che per molti umani è veramente penosa), la conoscenza di schemi di apertura e dei finali (enormi database che un uomo non è in grado di memorizzare) e, non ultima, la psicologia del giocatore (che può prendere decisioni errate per paura della sconfitta o per eccessivo ottimismo). Non a caso i motori scacchistici non basati su intelligenza artificiale sono comunque in grado di battere il campione del mondo umano.
Anche per la dimostrazione dei teoremi siamo in una situazione simile: l’algoritmo impara in pochissimo tempo quello che uno studente intelligente e preparato impara in anni di corso e poi “dimostra”.
Nei due casi, l’algoritmo sfrutta la sua velocissima capacità di apprendimento e si può pensare, che migliorandolo, possa dimostrare tutti e 3.225 teoremi. Paradossalmente, può dimostrare teoremi che noi umani non siamo riusciti a dimostrare (come il problema di Goldbach), ma solo se essi rientrano nello schema strategico da cui è partito l’approfondimento. Questa limitazione è peraltro comune a tutti gli ambienti dove si fissano assiomi di partenza: per esempio, già nel 1940 Gödel mostrò che l’ipotesi del continuo (in termini semplici, non è possibile trovare un insieme più grande degli interi e più piccolo dei reali) non poteva essere dimostrata a partire dagli assiomi standard della teoria degli insiemi.
Da un punto di vista pratico, queste applicazioni di intelligenza artificiale avranno, come primo risultato, non tanto quello di fare cose che l’uomo non sa fare, quanto di farle più velocemente e più efficientemente e questo sicuramente avrà un grande peso nel mondo del lavoro.
Per approfondimenti: Il problema di Goldbach – Curiosità logiche
