Così l’intelligenza artificiale di Google risolverà i problemi irrisolti della matematica

Tra le cose che l'intelligenza artificiale sa fare meglio delle controparti umane presto potrebbero esserci anche complesse dimostrazioni matematiche che sfuggono anche alle menti migliori di questa generazione. È la speranza dei ricercatori di Google che stanno mettendo a punto un sistema basato su machine learning che al momento è già riuscito a dimostrare con successo più di 1.200 teoremi già noti nell'ambito dell'algebra lineare e del calcolo complesso. Il team ha pubblicato in questi giorni online i risultati del proprio studio, descrivendo nel dettaglio il procedimento che li ha portati a perfezionare il proprio software fino a raggiungere i risultati annunciati.

Come ogni sistema basato sul machine learning, l'algoritmo è stato inizialmente nutrito con una banca dati dal volume sterminato: in questo caso si è trattato di un insieme di 10.200 teoremi e dimostrazioni grazie alle quali il software, aiutato dai ricercatori, ha potuto farsi un'idea del processo davanti al quale si sarebbe trovato. In particolare gli sviluppatori hanno modellato le capacità dell'algoritmo in modo simile a come viene insegnato dai docenti nelle scuole: scomponendo i teoremi da dimostrare in blocchi di più semplice soluzione e utilizzando le dimostrazioni di teoremi già noti come grimaldelli per sbloccare ciascuna parte del problema posto.

Terminata la fase di apprendimento i ricercatori hanno verificato le abilità acquisite dall'algoritmo sottoponendogli altri 3.225 teoremi di verifica – dimostrazioni note al resto del mondo, ma sconosciute al software perché mai affrontate durante la prima fase. Come risultato l'intelligenza artificiale ha saputo dimostrarne correttamente 1.253, una prestazione lontana dalla perfezione ma comunque interessante, soprattutto per due motivi. Innanzitutto gli ingegneri responsabili dello sviluppo hanno già dichiarato di poter insegnare all'algoritmo altre strategie risolutive, nuovi strumenti che lo renderanno più efficace nel selezionare l'approccio più adatto ai problemi postigli. Soprattutto però – quando il software sarà perfezionato e capace di operare con margini di errore minori – potrà essere utilizzato con un altro scopo: la dimostrazione di teoremi alla cui soluzione i matematici in carne e ossa ancora non sono giunti.