Da Google l’intelligenza artificiale che dimostra i teoremi matematici. Un’équipe di scienziati di Google ha insegnato a un’intelligenza artificiale come dimostrare teoremi matematici nell’ambito dell’algebra lineare e del calcolo complesso. E l’Ai ci è riuscita con successo
Ha mandato a memoria migliaia di pagine, dense di ipotesi, congetture, simboli e formule. Le ha comprese e digerite. E infine si è messo alla prova con oltre tremila teoremi mai visti prima, riuscendone a dimostrare quasi la metà. Non è un laureando in matematica, ma un’intelligenza artificiale appena messa a punto da un’équipe di scienziati di Google con lo specifico obiettivo, per l’appunto, di riuscire a dimostrare teoremi matematici di difficoltà crescente. L’Ai, al momento, si è cimentata solo con problemi la cui soluzione è già nota, ma gli autori del lavoro, pubblicato su ArXiv, sperano che in futuro possa essere usata anche per lavorare su teoremi che non sono ancora stati dimostrati.
Impara e ripeti
Seguendo l’ormai consolidato approccio dell’apprendimento automatico, il team di Google ha anzitutto “allenato” il proprio algoritmo facendogli studiare un database di oltre 10mila teoremi e relative dimostrazioni. Per ogni dimostrazione, in particolare, all’algoritmo venivano spiegate anche le “strategie” utilizzate e le proprietà matematiche sfruttate (per esempio la proprietà commutativa – il fatto che moltiplicare a per b è uguale a moltiplicare b per a – o la cosiddetta “regola della catena”, una tecnica che permette di calcolare le derivate di funzioni composte).
Dopo l’apprendimento, gli scienziati hanno sottoposto all’algoritmo 3225 teoremi di cui conosciamo già la dimostrazione: l’intelligenza artificiale è riuscita a dimostrarne ben 1253, e gli autori del lavoro sono convinti che insegnando al sistema altre “strategie” la percentuale di successo potrebbe salire ulteriormente.
Passo dopo passo
Per dimostrare ciascun teorema, l’intelligenza artificiale ha scomposto il ragionamento in una serie di passi successivi, ciascuno dei quali era risolvibile con una singola strategia: “Al momento, quasi tutti i passi”, spiega Christina Szegedy, uno degli autori, “sono relativamente semplici, e non richiedono ragionamenti complessi. Ma è comunque un buon punto di partenza: vogliamo arrivare a realizzare un sistema che possa replicare tutte le dimostrazioni in cui sono riusciti gli esseri umani. E poi vorremmo andare anche oltre”.
Al momento, in particolare, l’algoritmo è specializzato in teoremi nell’ambito dell’algebra lineare e del calcolo complesso, ma a Google sono convinti che con qualche miglioria sarà possibile ampliarne le potenzialità. “Tutto ciò che si può esprimere con il linguaggio della matematica”, ha commentato al New Scientist Jeremy Avigad, esperto della Carnegie Mellon University in Pennsylvania, “può essere agevolmente fatto comprendere ad algoritmi di questo tipo. L’importante è insegnargli quali sono le regole e le assunzioni alla base di ciascun passaggio”. Quando ci saremo riusciti con un tasso di successo abbastanza alto, potremmo finalmente chiedere all’Ai di provare a sviluppare strategie di risoluzione completamente ex novo.
Lascia un commento