AlphaGeometry: la macchina che sa dove tracciare la linea giusta

Chiunque abbia sudato su un problema di geometria conosce quel momento. La figura è lì, ferma, e per quanto la si guardi non ne esce nulla. Poi qualcuno traccia una linea che non c’era — congiunge due punti, disegna una parallela, aggiunge un cerchio — e all’improvviso tutto si incastra: la dimostrazione scivola via da sola. Quella linea in più si chiama costruzione ausiliaria, ed è il punto in cui la geometria smette di essere calcolo e diventa intuizione.

Nel gennaio del 2024, su Nature, un gruppo di Google DeepMind presenta AlphaGeometry: un sistema che affronta i problemi di geometria delle olimpiadi internazionali di matematica e ne risolve 25 su 30, avvicinandosi alla media di chi conquista una medaglia d’oro. La cosa interessante non è tanto il punteggio, quanto come ci arriva: separando il lavoro noioso dalla scintilla creativa, e affidando ciascuno a una macchina diversa.

Due modi di ragionare

Dimostrare un teorema di geometria richiede due capacità molto diverse. La prima è la deduzione paziente: da ciò che sai, ricavare meccanicamente tutte le conseguenze. Se due angoli sono uguali e questi due segmenti pure, allora questi due triangoli sono congruenti, allora quest’altra coppia di lati è uguale, e così via, all’infinito. È un lavoro da contabile: nessuna fantasia, solo regole applicate con precisione.

La seconda capacità è tutt’altra cosa: capire che, per sbloccarsi, bisogna aggiungere alla figura qualcosa che il problema non menzionava. Un punto medio, una perpendicolare, il centro di un cerchio. È un salto, non una deduzione — nessuna regola ti dice quale oggetto inventare, tra gli infiniti possibili. Un contabile, per quanto rapido, non ci arriverà mai. Serve qualcosa che assomiglia all’intuizione.

L’idea di AlphaGeometry è non chiedere a un unico strumento di fare entrambe le cose. Il lavoro da contabile lo dà a un motore simbolico. Il salto creativo lo dà a un modello linguistico. E li fa dialogare.

Il motore instancabile e il suggeritore

Il motore simbolico è un deduttore esaustivo: parte dalle ipotesi del problema e applica le regole della geometria in ogni modo possibile, accumulando tutti i fatti che ne discendono, finché non ne emergono di nuovi. A questo affianca un pezzo di ragionamento algebrico che macina uguaglianze tra angoli e rapporti tra lati. È velocissimo e non sbaglia mai un passaggio, ma ha un tetto: con le sole informazioni di partenza, prima o poi si ferma senza aver raggiunto la tesi.

Qui entra il modello linguistico, un transformer addestrato apposta. Quando il motore si blocca, il modello guarda lo stato del problema e propone una costruzione ausiliaria: «aggiungi il punto medio di questo lato», «traccia questa parallela». È un suggerimento, non una certezza. Ma basta introdurre quel nuovo oggetto perché il motore simbolico riparta, con nuove ipotesi da masticare, e magari stavolta arrivi in fondo. Se non ci arriva, si blocca di nuovo, il modello propone un’altra costruzione, e il ciclo continua.

La divisione dei compiti è netta e onesta. La correttezza è tutta del motore simbolico: ogni dimostrazione è verificabile passo per passo, niente è lasciato alla parola del modello linguistico. La creatività è tutta del modello: indovinare la mossa che sblocca. È come una coppia in cui uno è un calcolatore infallibile ma privo di fantasia, e l’altro ha lampi di intuizione ma va sempre controllato — insieme funzionano.

Il problema entra nel motore simbolico, che deduce tutte le conseguenze finché può. Quando si blocca, il modello linguistico propone una costruzione ausiliaria — qui il punto medio M — e il motore riparte. Il ciclo si ripete fino alla dimostrazione, sempre verificata passo per passo.

Imparare senza maestri umani

Un modello linguistico va addestrato su esempi, e per la geometria olimpica di dimostrazioni scritte da esperti ne esistono poche. Il gruppo di DeepMind aggira l’ostacolo con l’idea più elegante del lavoro: genera i propri dati da zero, senza usare una sola dimostrazione umana.

Il procedimento è quasi paradossale. Si parte da figure geometriche casuali; il motore simbolico deduce tutto ciò che ne discende, sfornando teoremi veri a milioni. Poi, per ciascuno, si ripercorre a ritroso quali passaggi sono stati necessari — e in particolare quali oggetti aggiunti sono serviti a chiudere la dimostrazione. Quegli oggetti diventano l’insegnamento: «in una situazione come questa, la mossa giusta era aggiungere quel punto». Il modello linguistico impara a suggerire proprio quelle mosse, allenandosi su un enorme corpus — dell’ordine dei cento milioni di esempi — che il sistema si è costruito da solo.

È come un allievo che imparasse le aperture degli scacchi non guardando partite di campioni, ma giocando da solo milioni di volte e annotando ogni volta quale mossa iniziale ha portato a un finale vinto. Nessun maestro, solo un motore di verità instancabile che genera lezioni.

25 su 30, e cosa vuol dire davvero

Sul banco di prova — trenta problemi di geometria tratti da olimpiadi recenti, tradotti nel linguaggio formale del sistema — AlphaGeometry ne risolve 25. Per confronto, un metodo automatico classico degli anni Settanta ne risolveva 10, e un modello linguistico generalista come GPT-4, provato sullo stesso insieme, non ne chiude nessuno da solo. La media di un medagliato d’oro alle olimpiadi si aggira intorno ai 26 problemi su 30: AlphaGeometry le si avvicina.

Conviene però leggere il risultato senza gonfiarlo. Il sistema fa una sola cosa: geometria piana euclidea, e per giunta solo la porzione esprimibile nel suo linguaggio formale. I problemi vanno tradotti a mano in quel formalismo prima di essere dati in pasto. Non affronta la teoria dei numeri, non le disuguaglianze, non la combinatoria; non è un matematico, è uno specialista strettissimo. La notizia non è «una macchina ora fa matematica», ma qualcosa di più preciso e più utile: un motore che garantisce la correttezza e una rete neurale che fornisce l’intuizione, cuciti insieme, battono di gran lunga ciascuno dei due preso da solo.

Il paper e chi l’ha scritto

L’articolo si intitola Solving olympiad geometry without human demonstrations, firmato da Trieu H. Trinh, Thang Luong e colleghi di Google DeepMind, pubblicato su Nature nel gennaio del 2024. Il codice e i dati sono stati rilasciati pubblicamente su GitHub, così che la comunità possa verificare e ripartire dal lavoro.

Perché ti riguarda, se non ti interessano né la geometria né le olimpiadi? Perché AlphaGeometry è una risposta concreta a una domanda che ci portiamo dietro da quando esistono i grandi modelli linguistici: come si fa a fidarsi del loro ragionamento? Qui la fiducia non poggia sulla loquacità del modello, ma su un motore che verifica ogni passo. Il modello linguistico serve per la parte in cui è bravo — proporre idee — e non per la parte in cui sbaglia — garantire la verità. È un’architettura del ragionamento che vale la pena tenere a mente ogni volta che si prova a costruire un sistema di cui ci si debba davvero fidare.