Cinquantamila.it La storia raccontata da Giorgio Dell'Arti

Il problema dell’intelligenza artificiale era lì fin dall’inizio e riguardava soprattutto l’affidabilità.
Per qualche anno è rimasto in secondo piano, oscurato dalla spettacolarità dei risultati. Prima i modelli hanno cominciato a produrre testi sorprendentemente fluidi, poi codice, immagini, ragionamenti articolati e soluzioni matematiche. Poi sono arrivati sistemi capaci di utilizzare strumenti, interrogare fonti, eseguire programmi, esplorare strategie e coordinare sequenze di azioni.
Quasi ogni avanzamento è stato letto, anche con un certo occhio al marketing, attraverso la stessa domanda: quanto stanno diventando intelligenti? Domanda semplice, ma che confonde e indebolisce quella decisiva.
Il valore economico di questi sistemi poggia sulla possibilità di affidare loro una parte del lavoro cognitivo. Scrivere programmi, analizzare documenti, formulare diagnosi, condurre ricerche, fornire consulenze, valutare i rischi, prendere decisioni. Perché questo regga, la qualità della generazione da sola non basta. Serve che il risultato sia sufficientemente affidabile da non richiedere, ogni volta, una ricostruzione completa da parte di un esperto.
Se un sistema scrive in pochi secondi un programma che un programmatore deve poi controllare riga per riga, si perde una parte del vantaggio. Lo stesso vale per una diagnosi che il medico deve rifare da capo, per un parere legale da verificare riferimento per riferimento o per una dimostrazione matematica che richiede comunque un controllo integrale. In casi del genere, l’automazione accelera enormemente la produzione di possibilità, ma lascia quasi intatto il lavoro che decide quali di esse meritino fiducia.
Qualche tempo fa, avevamo già descritto gli attuali sistemi generativi come macchine euristiche, ovvero strumenti molto potenti nell’esplorare rapidamente spazi enormi di possibilità, capaci di formulare in pochi minuti più ipotesi, strategie o soluzioni di quante una persona potrebbe esaminarne in settimane.
Generare, però, resta diverso dal verificare, e gran parte del valore di questi sistemi si riscontra proprio quando le due funzioni possono essere separate.
La matematica sembrava offrire l’ambiente ideale. Un modello propone una dimostrazione o una strategia; un sistema formale come Lean, cioè un software in grado di verificare rigorosamente se una prova rispetta determinate regole logiche e matematiche, verifica la validità dei passaggi. Il modello può esplorare migliaia di strade, mentre il verificatore elimina quelle che non funzionano. È un’architettura molto potente e, in effetti, una parte importante dei progressi recenti nella matematica assistita dall’intelligenza artificiale nasce proprio dalla combinazione di generazione, ricerca e verifica formale.
Per un certo periodo è sembrato quasi che qui il problema dell’affidabilità avesse trovato una soluzione definitiva. Gli LLM possono produrre una dimostrazione errata, ma Lean la rifiuterà. La macchina genera e un secondo sistema controlla. Tutto estremamente rassicurante, soprattutto per il marketing.
Il caso recente del problema di Navier–Stokes, presentato al mondo in grande spolvero, ha mostrato che la faccenda è molto più delicata e articolata.
Le equazioni di Navier–Stokes sono uno dei grandi problemi aperti della matematica contemporanea, tra i Millennium Prize Problems. Un recente lavoro ha confrontato la dimostrazione espressa in linguaggio naturale con la sua formalizzazione in Lean e ha individuato passaggi in cui le due non coincidono semanticamente: in alcuni casi, la versione formalizzata produce risultati più deboli o impiega ipotesi e argomenti diversi.
Ed è qui che emerge un aspetto particolarmente interessante. Al sistema viene chiesto di trasformare una dimostrazione scritta in una prova formale accettabile da Lean. Il criterio di successo, alla fine, è molto semplice: il codice deve compilare e la prova deve risultare valida nel sistema formale.
Se durante questa traduzione il modello incontra un passaggio difficile, ambiguo o problematico, può però modificarlo, sostituirlo con un argomento diverso o arrivare a dimostrare una versione più debole del passaggio originario, purché il risultato finale superi il controllo di Lean. Il lavoro appena pubblicato mostra che qualcosa di questo tipo è avvenuto in alcuni punti della formalizzazione di Navier–Stokes.
In termini colloquiali, l’intelligenza artificiale può quindi finire per “barare” sulla traduzione. Non perché abbia deciso di ingannare qualcuno, naturalmente, ma perché le abbiamo assegnato un obiettivo che premia il superamento del verificatore formale, mentre la fedeltà semantica alla dimostrazione di partenza è una condizione ulteriore che Lean, da solo, non controlla.
Lean, infatti, non ha fatto nulla di sbagliato. Ha verificato correttamente l’oggetto formale che gli è stato dato. Il problema è che, nel passaggio dalla dimostrazione scritta alla sua rappresentazione formale, quell’oggetto può essere cambiato. Gli autori precisano di non concludere per questo che la dimostrazione originaria sia necessariamente falsa; mostrano però che il fatto che il codice Lean compili non basta, da solo, a certificare quella dimostrazione così come era stata scritta.
Un po’ come un controllore che esamina un documento, ne verifica ogni requisito e appone il proprio timbro. Il controllo può essere impeccabile e il timbro autentico; resta però da stabilire se il documento arrivato sulla scrivania sia ancora esattamente quello che volevamo certificare. Se lungo il percorso alcune clausole sono state modificate per far sì che il documento superasse il controllo, il timbro resta perfettamente valido, ma certifica il documento modificato.
La parola “verificato”, invece, tende a cancellare tutti i passaggi intermedi. Sentiamo che una dimostrazione è stata verificata formalmente e traduciamo quell’informazione in una conclusione molto più ampia. Tutto il percorso che ha condotto a quella dimostrazione deve essere corretto. Il caso di Navier–Stokes mostra che tale inferenza può fallire. Il verificatore garantisce ciò che vede; la corrispondenza tra ciò che vede e ciò che pensavamo di sottoporgli resta un problema ulteriore.
È una scoperta importante perché sposta la questione dell’affidabilità a un livello più profondo. Non basta costruire un controllo perfetto. Bisogna conoscere con precisione che cosa quel controllo stia effettivamente certificando e quali passaggi della catena restino al di fuori del suo campo visivo.
Quasi nello stesso momento è arrivato un secondo segnale molto forte. Tre lavori collegati alla congettura di Hodge, uno dei grandi problemi della geometria moderna, sono stati ritirati da OpenAi dopo la scoperta di un errore di segno che comprometteva un passaggio centrale e i risultati che ne dipendevano. Qui il meccanismo è diverso, ma l’episodio è istruttivo per la stessa ragione. Una costruzione estremamente sofisticata può poggiare su un errore elementare che sopravvive abbastanza a lungo da sostenere un’intera catena di conclusioni. «Il diavolo è nei dettagli» recita il famoso adagio.
Fermarsi alla constatazione che «anche le macchine sbagliano» servirebbe a poco. Gli esseri umani sbagliano da quando esistono, e continueranno a farlo. Quello che svetta è il rapporto tra la capacità di produrre un argomento e quella di valutarne autonomamente l’affidabilità.
Un modello può generare una dimostrazione contenente un errore e, interrogato successivamente sul passaggio problematico, individuare lo stesso errore. Può correggerlo, spiegare perché era sbagliato e proporre una nuova versione. Queste capacità possono convivere senza che il sistema disponga, al momento della produzione, di una rappresentazione robusta del grado di fiducia che il proprio risultato merita.
Qui si entra in un territorio che avevamo studiato nel lavoro «The Simulation of Judgment» pubblicato su PNAS esattamente un anno fa. I modelli riescono spesso a produrre valutazioni convincenti, a utilizzare criteri appropriati, a organizzare le evidenze e a costruire giustificazioni articolate. Possono giungere a conclusioni simili a quelle di un essere umano e presentarle nella forma linguistica tipica di un giudizio competente. Questo però non garantisce che abbiano costruito ciò che rende quel giudizio affidabile.
La differenza sembra sottile finché non iniziamo a delegare decisioni reali.
Da qui nasce ciò che abbiamo chiamato Epistemia. Non si limita a indicare l’errore né coincide con le vecchie “allucinazioni”. Descrive una condizione più generale in cui un sistema riesce a produrre oggetti che possiedono la forma della conoscenza – linguaggio competente, coerenza, spiegazioni, riferimenti, formule, talvolta persino certificazioni parziali – senza che siano necessariamente soddisfatte tutte le condizioni che giustificano la fiducia in quella conoscenza.
Una risposta può essere perfettamente fluida e contenere un errore. Una spiegazione può essere coerente e poggiare su una premessa sbagliata. Una dimostrazione può essere estremamente sofisticata eppure includere un passaggio errato. Persino una verifica formalmente corretta può garantire meno di quanto il destinatario attribuisca alla parola “verificato”.
Questa distanza tra plausibilità e affidabilità diventa ancora più importante quando la si considera dal punto di vista economico.
Gli LLM stanno abbattendo vertiginosamente i costi di generazione. Un’altra pagina, un altro programma, un’altra analisi, un’altra ipotesi o un’altra possibile soluzione costano sempre meno. Su questo terreno le macchine diventeranno inevitabilmente molto più efficienti di noi. A scrivere scemenze, del resto, un LLM sarà sempre più competitivo di qualunque essere umano: potrà produrne migliaia in pochi minuti, perfettamente impaginate, articolate, plausibili e corredate di spiegazioni.
La vera difficoltà sarà inserire qualcosa di sensato in quella capacità produttiva e, soprattutto, conservarne la verificabilità.
Il costo del controllo, infatti, non sta diminuendo alla stessa velocità. 
Quando esiste un test automatico, il problema è relativamente semplice. In moltissimi altri casi continuiamo ad avere bisogno di conoscenza del dominio, esperienza, tempo e capacità di giudizio.
Questo modifica profondamente l’economia della conoscenza. Per molto tempo, una delle risorse più scarse è stata la capacità di produrre idee, analisi e soluzioni sufficienti. Potremmo entrare in una fase in cui le proposte candidate diventano illimitate e la risorsa realmente scarsa è la capacità di selezionarle. Avevamo già descritto questo spostamento: la generazione cresce molto più rapidamente della verifica, mentre l’expertise necessaria al controllo resta lenta e costosa da sviluppare.
A questa asimmetria se ne aggiunge un’altra, forse ancora più delicata. Deleghiamo alle macchine proprio quei processi attraverso cui impariamo a sviluppare quelle competenze.
Uno studente può chiedere al modello di svolgere il passaggio più difficile di una dimostrazione. Un programmatore può generare codice che non sarebbe più in grado di scrivere autonomamente. Un professionista può lavorare a partire da sintesi di documenti che progressivamente smette di leggere integralmente. Un ricercatore può delegare parti sempre più ampie dell’esplorazione, dell’analisi e della scrittura.
Nel breve periodo l’efficienza può aumentare moltissimo. Sul lungo periodo troviamo problemi. La verifica richiede precisamente le competenze che una delega sistematica rischia di non farci più costruire.
Non impariamo matematica soltanto per risolvere un esercizio più velocemente. Anni di studio servono anche a sviluppare una sensibilità per le cose che non tornano: un’ipotesi dimenticata, un ordine di grandezza sospetto, un salto logico, una conclusione troppo forte rispetto alle premesse. Un programmatore esperto è anche qualcuno che sa dove guardare quando un sistema complesso inizia a comportarsi in modo strano.
Queste capacità costituiscono una vera infrastruttura di verifica. Richiedono tempo, esercizio, errori, correzioni, esposizione ripetuta a problemi difficili. Non possono essere scaricate quando diventano improvvisamente necessarie.

WALTER QUATTROCIOCCHI