Quando l'intelligenza artificiale prende tre all'esame

Tempo di lettura: 5 mins

Crediti: Mike MacKenzie/Flickr. Licenza: CC BY 2.0

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 algoritmo1,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

 

altri articoli

Le notizie di scienza della settimana #104

Il biologo molecolare russo Denis Rebrikov ha dichiarato che ha intenzione di impiantare nell'utero di una donna embrioni geneticamente modificati con la tecnica CRIPSR entro la fine dell'anno. L'obiettivo sarebbe quello di prevenire che la madre, colpita da una forma di HIV resistente ai farmaci antiretrovirali, trasmetta il virus ai propri figli. Per farlo, Rebrikov userebbe la tecnica CRISPR-Cas9 per disattivare il gene CCR5, in modo simile a quanto fatto dallo scienziato cinese He Jiankui che lo scorso novembre aveva annunciato di essere stato il primo a far nascere una coppia di gemelle con questo procedimento (He voleva però evitare la trasmissione del virus dell'HIV dal padre alle figlie). La legislazione russa proibisce l'editing del genoma umano in senso generale, ma la legge sulla fertilizzazione in vitro non vi fa esplicito riferimento, e dunque Rebrikov potrebbe trovarsi di fronte un vuoto normativo che conta di colmare chiedendo l'autorizzazione di una serie di agenzie governative, a partire dal Ministero della salute. Scienziati ed esperti di bioetica si dicono preoccupati. La tecnologia non è ancora matura, motivo per cui qualche mese fa un gruppo di importanti ricercatori del campo avevano chiesto di mettere a punto una moratoria sul suo utilizzo in embrioni destinati all'impianto in utero. Non è chiaro poi se i rischi superino i benefici. In primo luogo, la disattivazione del gene CCR5 protegge dalla trasmissione del virus dell'HIV nel 90% dei casi. In secondo luogo, il rischio di mutazioni off-target e on-target indesiderate è ancora molto alto. Rebrikov sostiene che la sua tecnica ne riduca drasticamente la frequenza, ma finora non ha pubblicato alcuno studio scientifico che lo dimostri. Nell'immagine: lo sviluppo di embrioni umani geneticamente modificati con la tecnica CRISPR per correggere una mutazione responsabile della cardiomiopatia ipertrofica (lo studio, condotto nel laboratorio di Shoukhrat Mitalipov presso la Oregon Science and Health University di Portland, risale al 2017 ed è stato pubblicato su Nature). Credit: Oregon Science and Health University. Licenza: OHSU photos usage

Dove finisce la plastica dei ricchi?

Ogni anno gli Stati Uniti producono 34,5 milioni di tonnellate di rifiuti di plastica. 1 milione di tonnellate vengono spedite fuori dal continente. Fino a qualche anno fa la maggior parte veniva spedita in Cina e Hong Kong, ma nel 2017 la Cina ha chiuso le porte a questo tipo di importazioni, autorizzando solo l'arrivo della plastica più pulita e dunque più facile da riciclare.