La matematica si è sempre avvalsa di due linguaggi distinti. Uno è il linguaggio naturale che usiamo per spiegare idee, raccontare storie e condividere intuizioni; è flessibile, ricco di contesto e spesso salta passaggi che sembrano ovvi a un lettore umano. L'altro è il linguaggio formale dei sistemi di prova assistita, sistemi informatici rigidi che controllano ogni singolo movimento logico per garantire che una conclusione sia innegabilmente vera. Per decenni, i ricercatori hanno lavorato per tradurre il primo linguaggio nel secondo, un processo chiamato autoformalizzazione. L'obiettivo era semplice: prendere una dimostrazione scritta da un essere umano e trasformarla in codice che un computer possa verificare. Ma rimaneva un problema critico. Un computer poteva spesso produrre una dimostrazione tecnicamente corretta, ma che non aveva alcuna somiglianza con l'argomentazione umana che l'aveva ispirata. Il computer poteva risolvere il problema utilizzando un percorso completamente diverso, nascondendo il ragionamento originale dietro un muro di scorciatoie automatizzate. Ciò creava un divario tra verità e comprensione. Se la dimostrazione del computer non segue i passaggi dell'uomo, non possiamo usarla per verificare se il ragionamento umano fosse effettivamente solido, né possiamo fidarci del fatto che ci insegni come funziona l'argomento.

Un team di ricercatori ha ora affrontato questo divario con un nuovo sistema progettato per mantenere la dimostrazione del computer fedele al processo di pensiero originale dell'uomo. Chiamano il loro sistema Pistis, un nome derivato dall'antico termine greco per fede o fiducia. I ricercatori hanno applicato questo sistema ai primi tre libri degli Elementi di Euclide, un testo fondamentale della geometria scritto oltre duemila anni fa. Il loro lavoro dimostra che è possibile tradurre questi antichi argomenti in un linguaggio informatico moderno senza perdere la logica originale, scoprendo al contempo errori nascosti nel testo che erano passati inosservati per secoli.

La sfida principale affrontata dal team era che il linguaggio naturale e la logica informatica operano su ritmi diversi. Una dimostrazione umana potrebbe dire: "Assumiamo che questo sia vero", e proseguire, aspettandosi che il lettore colmi la lacuna. Un computer, invece, esige che ogni singolo passaggio sia esplicitamente dichiarato e giustificato. I tentativi precedenti di tradurre le dimostrazioni spesso lasciavano che il computer riempisse queste lacune con la propria logica, riscrivendo di fatto l'argomento per renderlo più facile da risolvere per la macchina. Il risultato era una dimostrazione che compilava con successo ma non rifletteva l'intento dell'autore umano. Pistis è stato costruito per prevenire questo. Invece di chiedere al computer di trovare qualsiasi modo per dimostrare l'enunciato, il sistema costringe il computer a seguire il percorso specifico dell'uomo, frase per frase.

Per raggiungere questo obiettivo, i ricercatori hanno sviluppato un metodo che suddivide il processo di traduzione in due fasi distinte. Primo, una fase di mappatura analizza il testo in linguaggio naturale e lo suddivide in una sequenza di piccoli passi atomici. Identifica esattamente cosa afferma ogni frase e su quali assunzioni si basa. Questo crea un modello rigido che il computer deve seguire. Secondo, una fase di riempimento tenta di dimostrare ciascuno di questi piccoli passi individualmente. Il sistema utilizza una strategia di ricerca specializzata che impedisce al computer di prendere scorciatoie o saltare in avanti. Se il computer non può dimostrare un passaggio specifico utilizzando gli strumenti e i riferimenti esatti menzionati nel testo umano, non si limita a trovare un altro modo per risolvere il problema. Invece, segnala l'anomalia, rivelando che l'argomento umano originale potrebbe avere un buco o una parte mancante.

Questo approccio si è rivelato straordinariamente efficace quando testato sulla geometria di Euclide. I ricercatori hanno generato dimostrazioni formali per 92 proposizioni attraverso i primi tre libri. Quando hanno confrontato queste nuove dimostrazioni con i tentativi precedenti, la differenza era netta. Le nuove dimostrazioni compilavano più di trentatré volte più velocemente, un miglioramento significativo dell'efficienza che suggerisce come il nuovo metodo eviti i calcoli pesanti e lenti dei sistemi più vecchi. Ancora più importante, gli esperti umani che hanno revisionato le dimostrazioni hanno preferito l'output del nuovo sistema con un ampio margine. In uno studio in cieco, i revisori hanno ritenuto le nuove dimostrazioni molto più trasparenti e migliori rappresentazioni degli argomenti del libro di testo originale. Un giudice basato sull'intelligenza artificiale, addestrato per valutare la qualità della traduzione, è concordato, favorendo le nuove dimostrazioni rispetto alle vecchie con un rapporto di oltre cinque a uno.

Oltre a tradurre semplicemente il testo, il sistema ha agito come un controllore rigoroso che ha esposto reali difetti nel materiale sorgente. Poiché il sistema insiste nel seguire esattamente la logica umana, non può nascondere gli errori. In un caso, il sistema ha identificato un errore di citazione in una traduzione moderna di Euclide. Il testo faceva riferimento a una proposizione riguardante il dimezzamento di una linea, ma la citazione puntava a una proposzione riguardante il dimezzamento di un angolo. Il sistema ha segnalato questa discrepanza, mostrando che la traduzione aveva collegato l'idea sbagliata al passaggio sbagliato. In un altro caso, il sistema ha trovato una lacuna nel ragionamento di Euclide dove uno scenario specifico era stato lasciato non affrontato. I ricercatori sono stati in grado di dimostrare formalmente che l'argomento originale era incompleto, una scoperta che sarebbe stata difficile da fare senza uno strumento che aderisca strettamente alla struttura originale.

Il successo di Pistis suggerisce che la formalizzazione fedele non è solo un esercizio tecnico, ma un potente strumento per verificare la conoscenza umana. Costringendo il computer a percorrere lo stesso cammino dell'uomo, il sistema può confermare se il ragionamento regge o dove si interrompe. I ricercatori hanno scoperto che il loro metodo poteva accettare argomenti validi, confutare quelli invalidi e individuare esattamente dove una dimostrazione andava sbagliata. Questa capacità si estende oltre l'antica geometria; il framework è progettato per lavorare con qualsiasi argomento matematico scritto in linguaggio naturale. Il lavoro mostra che non dobbiamo scegliere tra la flessibilità della spiegazione umana e il rigore della verifica delle macchine. È possibile avere entrambi, a patto che la macchina sia guidata a rispettare la voce e la logica originale dell'uomo.

Lo studio ha anche evidenziato i limiti dell'attuale tecnologia. Sebbene il sistema funzionasse bene per i primi tre libri di Euclide, non poteva gestire ogni singola proposizione dei libri successivi senza ulteriore guida umana. Alcune proposizioni richiedevano concetti geometrici che il sistema informatico sottostante non sapeva ancora come gestire, come ad esempio misurare la lunghezza di una linea curva. I ricercatori hanno osservato che il loro sistema si affida a un essere umano o a un'intelligenza artificiale avanzata per agire come un oracolo, verificando che la mappatura iniziale del testo sia corretta. Ciò significa che il processo non è ancora completamente automatico, ma riduce significativamente il lavoro manuale richiesto rispetto ai metodi precedenti.

In definitiva, l'articolo presenta un nuovo standard per il modo in cui interagiamo con le dimostrazioni matematiche nell'era dell'intelligenza artificiale. Si va oltre la domanda se un computer possa dimostrare un teorema, spostandosi verso la domanda più profonda se il computer comprenda l'argomento. Garantendo che la dimostrazione formale rispecchi l'argomento in linguaggio naturale passo dopo passo, i ricercatori hanno creato uno strumento che può validare il ragionamento dietro una conclusione, non solo la conclusione stessa. Ciò consente ai matematici e agli studenti di fidarsi del fatto che il computer non stia solo trovando una soluzione, ma stia realmente seguendo la logica della persona che ha scritto la dimostrazione. Il lavoro offre una strada percorribile in cui l'intuizione umana e la precisione della macchina lavorano insieme, preservando l'integrità della scoperta matematica pur sfruttando la potenza della moderna verifica.