Si chiama “AlphaGeometry” ed è un tool di Intelligenza Artificiale presentato da DeepMind capace di fare dimostrazioni di problemi di geometria, come quelli che sorgono durante gli esercizi proposti nelle Olimpiadi Internazionali di Matematica. Come si legge sulla rivista Nature, infatti, AlphaGeometry è stato messo alla prova con 30 quesiti geometrici tratti da questa celebre competizione ed è riuscito a risolverne 25 (un risultato che gli avrebbe praticamente garantito la medaglia d’oro, almeno nel settore della geometria).

“Il fatto che sia riuscito a risolvere 25 problemi delle IMO, generando prove comprensibili dall’uomo, è davvero impressionante” ha commentato Kevin Buzzard, matematico dell’Imperial College di Londra. AlphaGeometry è riuscito non solo a dimostrare “congetture” su figure bidimensionali, come i poligoni, ma lo ha fatto in modo comprensibile, raggiungendo così un traguardo che, finora, era sfuggito ai suoi “predecessori” sviluppati da Google, come “Minerva”. Questo ChatBot creato per affrontare problemi matematici di livello scolastico di base, allenato su documenti e soluzioni matematiche avanzate, riusciva infatti molto spesso a fornire la risposta giusta ma non era capace di spiegare in modo corretto come era arrivato alla soluzione. La causa del difetto? Probabilmente il linguaggio naturale “su cui era stato addestrato, che gli ha fatto produrre un linguaggio naturale imperfetto e inaffidabile”, ha spiegato Trieu Trinh, informatico del Google DeepMind di Mountain View, California, coautore della nuova ricerca pubblicata su Nature.

Come si legge nel nuovo studio, infatti, Trinh e colleghi hanno approntato un linguaggio con una sintassi rigorosa come quella di un comune linguaggio computazionale, capace di essere facilmente verificata da un computer pur mantenendo ancora un senso quando letto da un uomo. In questo linguaggio, un programma ha generato in automatico 100 milioni di “passaggi logici”, delle “prove” che consistevano in sequenze casuali di passaggi semplici ma logicamente corretti. Queste venivano poi usate per addestrare AlphaGeometry: l’IA era in grado di risolvere i problemi fornendo un passaggio dopo l’altro in modo simile a come i chatbot producono testo. Il suo output era leggibile dalla macchina e facile da verificare: per ogni problema, l’IA produceva molte soluzioni, le controllava ed eliminava quelle errate.
AlphaGeometry combina il metodo statistico brute force dei modelli linguistici con il ragionamento simbolico, ed è probabilmente questo il principale segreto del suo successo. Inoltre, dato che non si addestra su miliardi di testi recuperati in Rete è impossibile che “imbrogli”, ossia che abbia trovato la domanda in giro su Internet e quindi ne vada a copiare la risposta.

Nonostante questi punti di forza, non sembra che i matematici debbano temere per il loro futuro (almeno quello imminente). Come spiega Buzzard: “Forse tra qualche anno queste o altre tecniche di apprendimento automatico potranno risolvere problemi di matematica a livello universitario che solo gli studenti più intelligenti possono affrontare ma, al momento, non ci sono macchine in grado di impegnarsi autonomamente con la matematica moderna del livello della ricerca”.