💻 computer science

Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations

Questo articolo presenta un calcolo meccanizzato in Lean 4 e un sistema a doppio piano ("hurdy-gurdy") che consente a LLM non fidati di generare traduzioni auto-certificanti e con grado di fedeltà tra linguaggi di programmazione, garantendo che un grafo di fiducia in continua evoluzione e verificato dall'uomo converga su quesiti di programmazione decidibili con una sicurezza sempre crescente.

Autori originali: Christoph Kirsch

Pubblicato 2026-07-20

📖 7 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Christoph Kirsch

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Il dilemma del detective: quando non puoi fidarti del messaggero

Immagina di cercare di risolvere un mistero riguardante una macchina complessa, come il motore di un'auto o il comportamento di un personaggio di un videogioco. Hai una domanda: "L'auto si schianterà se premo l'acceleratore a 50 mph?". Per rispondere, non puoi limitarti a guardare l'auto; devi tradurre la sua meccanica disordinata e reale in un linguaggio che un risolutore informatico super intelligente possa comprendere, come un'equazione matematica. Ma ecco il problema: la persona che traduce l'auto in matematica potrebbe commettere un errore. Magari ha dimenticato un ingranaggio, o forse ha frainteso il funzionamento dei freni. Se il traduttore sbaglia, il risolutore matematico ti darà la risposta perfetta a una domanda sbagliata.

Nel mondo dell'informatica, questo è il problema della "traduzione". Spesso dobbiamo spostare un programma da un linguaggio (come C o Python) a un altro (come un puzzle logico per un risolutore) per verificare se è sicuro. Tradizionalmente, gli scienziati hanno cercato di risolvere questo problema cercando di dimostrare che il traduttore fosse perfetto una volta per tutte, come certificare la sicurezza di un ponte prima che chiunque vi transiti. Ma questo è incredibilmente difficile, specialmente quando i traduttori sono complessi o persino scritti da un'intelligenza artificiale. Questo articolo pone una domanda diversa: e se smettessimo di cercare di dimostrare che il traduttore è perfetto e costruissimo invece un sistema capace di intercettare gli errori del traduttore mentre è in funzione? È la differenza tra fidarsi di una singola guida per attraversare una foresta e avere un team di guide che controllano reciprocamente le proprie mappe, con una regola secondo la quale, se non sono d'accordo, ci si ferma e si capisce chi ha torto.

La macchina "Hurdy-Gurdy": una fabbrica di risposte affidabili

Questo articolo presenta un sistema chiamato hurdy-gurdy (chiamato così in onore di uno strumento musicale che produce melodie, ma qui produce risposte), un nome che richiama l'organetto a manovella. Gli autori, guidati da Christoph Kirsch, propongono un nuovo modo di gestire i programmi informatici: trattarli come una partita al "telefono senza fili" dove ogni passaggio è controllato e ogni risposta arriva con una ricevuta.

L'idea centrale è semplice ma potente: non fidarti del traduttore; fidati del processo.

Immagina di avere una domanda su un programma scritto in C. Invece di inviarlo a un solo traduttore, il sistema lo invia lungo due percorsi differenti.

La Traduzione: Il programma viene tradotto in un linguaggio logico più semplice (come trasformare un romanzo in un'equazione matematica).
Il Doppio Controllo: Il sistema esegue il programma originale e la versione tradotta affiancati. Controlla se si comportano nello stesso modo. Se lo fanno, ottimo! Se non lo fanno, il sistema indica esattamente il punto in cui sono divergenti, come un arbitro che fischia un fallo nel momento esatto in cui un giocatore commette l'infrazione.
Il Trucco del "Testimone": Se il risolutore dice: "Sì, un incidente è possibile", il sistema non si limita a prendere il risolutore per buono. Prende la "prova" (le condizioni specifiche che causano l'incidente) e la fa ripercorrere all'indietro attraverso la traduzione. Alimenta il programma originale con quelle stesse condizioni. Se il programma originale effettivamente subisce l'incidente, allora la risposta è reale al 100%. Il sistema ha "riprodotto" la scena del crimine.

I Due Piani: Costruire e Usare

Il sistema ha due modalità distinte, come un piano di fabbrica e uno showroom:

Il Piano di Utilizzo (Lo Showroom): È qui che avvengono le risposte. Qui, un'IA (o un essere umano) pone domande. Il sistema non tira a indovinare; sceglie un percorso, controlla la traduzione e, se la risposta è "Sì, è possibile", esegue la riproduzione per provarlo. Se la risposta è "No, è impossibile", il sistema si affida a una serie di controlli: molteplici traduttori, molteplici risolutori e persino certificati matematicamente verificati per esserne certi.
Il Piano di Evoluzione (La Fabbrica): È qui che il sistema cresce. Se il sistema non riesce a rispondere a una domanda, non si limita ad arrendersi. Scrive il motivo per cui ha fallito (ad esempio: "Non abbiamo un traduttore per questo specifico tipo di ciclo"). Successivamente, utilizza un'IA per costruire un nuovo traduttore che colmi quella lacuna. Una volta costruito, il nuovo traduttore viene testato contro quelli esistenti. Se supera il test, viene aggiunto al registro. Se fallisce, viene corretto. Questo ciclo avviene all'infinito, rendendo il sistema più intelligente e affidabile nel tempo, ma crucialmente, il processo di crescita non risponde mai alle domande in sé. Esso costruisce solo gli strumenti per rispondere.

Il colpo di scena degli "Autori inaffidabili"

La parte più sorprendente dell'articolo è che i traduttori stessi sono stati costruiti da agenti IA inaffidabili. Gli autori non hanno codificato manualmente i traduttori; hanno chiesto a modelli di IA di scriverli basandosi su una descrizione di una pagina. Di solito, questo sarebbe un disastro. Ma poiché il sistema controlla ogni passaggio, gli errori dell'IA vengono intercettati immediatamente.

Per esempio, in un test, un traduttore IA ha saltato un'istruzione specifica, causando un comportamento diverso rispetto al programma originale. Il "controllo quadrato" del sistema (il confronto affiancato) ha individuato l'errore istantaneamente, puntando esattamente alla riga e alla variabile errata. Il sistema ha poi corretto il traduttore. L'articolo dimostra che anche con autori IA che potrebbero sbagliare, l'architettura del sistema garantisce che le risposte finali siano affidabili.

Cosa ha scoperto il sistema (e cosa non ha scoperto)

Gli autori hanno testato questo sistema su un fermo immagine del loro lavoro di luglio 2026. Ecco cosa hanno misurato:

Copertura: Hanno tradotto con successo programmi da 13 linguaggi diversi (inclusi C, Python e persino reti di reazioni chimiche) in risolutori logici. Per il linguaggio dei processori RISC-V, hanno coperto 96 tipi di istruzioni su 96, il che significa che il sistema poteva gestire ogni singola istruzione di quel set senza perdere il controllo.
Accordo: Quando hanno inviato la stessa domanda lungo due percorsi di traduzione differenti (uno basato su un manuale, l'altro su un modello formale), le risposte concordavano il 100% delle volte sui casi di test.
Difetti Intercettati: Il sistema ha individuato 24 difetti specifici nei propri traduttori e strumenti. Alcuni erano semplici errori di battitura, altri errori logici in cui l'IA aveva frainteso il funzionamento di un'istruzione informatica. Fondamentalmente, il sistema ha trovato questi errori senza l'intervento umano sul codice.
Il "Punto Cieco": Il sistema ha anche individuato un limite. Se due traduttori diversi commettono lo stesso identico errore (perché entrambi hanno frainteso la stessa regola), il sistema non può intercettarlo. Questo è chiamato "fallimento di modo comune". L'articolo ammette che questo è un rischio, ma il sistema è progettato per minimizzarlo utilizzando fonti diverse per le traduzioni.
Giocatori LLM: Hanno testato se un'IA potesse usare il sistema per rispondere a delle domande. In un esperimento, un'IA senza strumenti ha risposto correttamente a 7 domande su 8, ma ha tirato a indovinare sull'ultima. L'IA con il sistema ha ottenuto 8 risposte su 8, e ogni risposta era accompagnata da una prova verificata dalla macchina.

Conclusione

Questo articolo non sostiene di aver risolto tutti i problemi di sicurezza informatica. Non dice che i traduttori IA sono diventati perfetti. Inveve, dimostra che è possibile costruire un sistema affidabile partendo da componenti inaffidabili.

Trattando ogni traduzione come un potenziale errore e costruendo un "meccanismo a cricchetto" che permette solo ai miglioramenti di restare, il sistema crea una scala di fiducia. Se la domanda è "Può accadere?", il sistema può riprodurre l'evento per provarlo. Se la risposta è "No, non può accadere", il sistema utilizza una catena di controlli indipendenti e certificati matematicamente verificati per esserne certo.

Gli autori concludono che questo approccio — utilizzare un grafo di percorsi, controllare ogni passaggio e riprodurre le prove — è un modo valido per gestire la complessità del software moderno, anche quando le persone (o le IA) che costruiscono gli strumenti sono fallibili. È un passaggio dal "fidarsi dell'autore" al "fidarsi dell'architettura".

Sintesi Tecnica: Autori non Affidabili, Risposte Affidabili

Problema

Il documento affronta la sfida fondamentale di rispondere a domande su programmi (ad esempio, raggiungibilità, validità di asserzioni) quando gli strumenti utilizzati per tradurre e analizzare tali programmi sono non affidabili. Gli approcci tradizionali si basano o sulla prova della correttezza di un singolo traduttore una volta per tutte (ad esempio, CompCert) o sulla validazione di ogni esecuzione di un singolo traduttore. Tuttavia, questi metodi assumono un singolo "bordo" di traduzione. Il documento sostiene che in un ecosistema complesso che coinvolge molteplici linguaggi sorgente, diversi target di ragionamento e potenziali autori non affidabili (inclusi i modelli LLM), il processo di traduzione forma un grafo di molti linguaggi e percorsi. In questo grafo, ogni traduzione è un potenziale punto di fallimento. Il problema centrale è come comporre queste traduzioni eterogenee, costruite indipendentemente e potenzialmente non affidabili, in un sistema che fornisca risposte affidabili senza richiedere la prova universale di ogni componente.

Metodologia: Il Calcolo delle Traduzioni con Grado di Fedeltà

Gli autori propongono un calcolo formale e una piattaforma implementativa chiamata hurdy-gurdy. La metodologia si basa su due "piani" distinti che si incontrano in un registro condiviso:

1. Il Piano d'Uso (Rispondere alle Domande)

Questo piano tratta la traduzione come un grafo dove i nodi sono i linguaggi e gli archi sono le coppie di traduzione.

La Coppia e il Quadrato: L'unità fondamentale è una coppia $(A, B)$ $(A, B)$ composta da un traduttore $T$ $T$ , un ritorno al sorgente $\Lambda$ $Λ$ (target-to-source carry-back) e interpreti condivisi. Una coppia è validata tramite un quadrato commutativo direzionale:
- Esattezza: Il comportamento sorgente è uguale al comportamento target riportato indietro (una bisimulazione sulle osservabili mantenute).
- Sovra-approssimazione: Il comportamento sorgente è simulato dal comportamento target (permettendo comportamenti spurii ma preservando quelli sorgente).
- Decidibilità: Per ogni specifico programma, il quadrato è verificato eseguendo entrambi i lati e confrontando le tracce proiettate. Se divergono, il fallimento è localizzato a un passaggio specifico e a un'osservabile.
Composizione e Contratti: I percorsi sono cammini attraverso il grafo. Il contratto di un percorso è l'incontro componente per componente dei contratti dei suoi passaggi, definito da quattro assi:
- Classe di Assicurazione: Una gerarchia da nessuna a replay, per-esecuzione e universale.
- Direzione: Esatta o sovra-approssimazione.
- Osservabili Mantenute: L'intersezione delle osservabili preservate da ogni passaggio (la perdita si accumula).
- Costo: Misurato in tempo di esecuzione.
Meccanismi di Fiducia:
- Riestabilimento Per-Esecuzione: Anche un passaggio "affidabile" può essere validato dinamicamente se l'oracolo del quadrato passa per quella specifica esecuzione.
- Corroborazione tra Rami: Se due percorsi derivati indipendentemente (prefissi diversi) concordano sul verdetto, l'evidenza è più forte del grado individuale di ciascun percorso.
- Asimmetria Esistenziale/Universale:
  - Risposte Esistenziali (Raggiungibile): Auto-certificanti. La testimonianza (witness) del solver viene riportata indietro e riprodotta nell'interprete sorgente. Se la riproduzione mostra il comportamento, la risposta è vera indipendentmente dagli errori del traduttore (Base di Fiducia: Adeguatezza dell'Interprete Sorgente).
  - Risposte Universali (Irraggiungibile): Non auto-certificanti. Queste dipendono dalla composizione dei gradi, dall'accordo tra i rami e dai certificati formali (ad esempio, prove DRAT controllate da verificatori verificati).

2. Il Piano dell'Evoluzione (Far Crescere il Grafo)

Questo piano gestisce la crescita del grafo di traduzione.

Generazione Non Affidabile: Le coppie sono implementate da agenti LLM indipendenti partendo da brevi descrizioni.
Il Ratchet (Cricchetto): Il sistema impone un modello di crescita additiva. I nuovi contributi devono estendere la copertura senza invalidare i verdetto precedenti.
Domanda e Registrazione: Le domande non rispondibili vengono registrate come "domanda". Le raccomandazioni per nuove coppie vengono generate sulla base delle evidenze. La registrazione umana è l'ultimo gate; il sistema non risponde autonomamente alle domande, ma espande solo la capacità di farlo.

Contributi Chiave

Un Calcolo di Coppie Direzionali con Grado di Fedeltà: Un framework formale dove l'esattezza è un caso speciale di sovra-approssimazione, e la composizione è definita da un incontro di "anello debole" attraverso assicurazione, direzione, perdita e costo.
L'Algebra dei Contratti: Un meccanismo per comporre evidenze eterogenee. Il documento formalizza come i controlli "per-esecuzione" e le garanzie "universali" si combinano, e come la perdita (osservabili scartate) si accumula lungo un percorso.
L'Asimmetria Esistenziale/Universale: Un principio architettonico che distingue tra risposte che portano testimonianze (auto-certificanti tramite riproduzione sorgente) e quelle che non lo fanno (richiedendo gradi di fiducia e certificati).
L'Architettura a Due Piani: Una separazione tra i piani di "uso" (rispondere) ed "evoluzione" (costruire), permettendo ad autori non affidabili di costruire il sistema mentre l'architettura garantisce la fiducia attraverso controlli incrociati, diversità e l'effetto ratchet.
Meccanizzazione: Il nucleo compositivo, inclusi il teorema di incollamento (pasting theorem), la localizzazione e i teoremi di asimmetria end-to-end, è meccanizzato in Lean 4 (circa 1.250 linee) con un audit degli assiomi pulito.

Risultati e Valutazione

Il documento valuta uno "snapshot di luglio 2026" della piattaforma hurdy-gurdy, costruita interamente da agenti LLM senza alcuna revisione semantica umana del codice.

Copertura e Correttezza: Il sistema copre 13 linguaggi e 15 coppie registrate. Ha composto con successo percorsi per RISC-V, AArch64, eBPF, Wasm, EVM, Python e altri.
- Accordo tra i Rami: Due percorsi per RISC-V (derivato manualmente vs derivato da Sail) e AArch64 hanno concordato su tutte le 12 domande di raggiungibilità testate, incluse quelle universali (irraggiungibilità).
- Benchmark di Conformità: Un benchmark derivato di 78 domande dal set di test RISC-V è stato risolto con il 100% di accordo tra i percorsi e il 100% di correttezza rispetto alla verità di base (ground truth).
Rilevamento Difetti: L'architettura ha colto 24 difetti nel codice generato dagli LLM, tra cui:
- Decodifica silenziosa errata di istruzioni (ad esempio, MUL come ADD) dove sia l'interprete che il traduttore concordavano (un "punto cieco" colto solo dalla diversità esterna).
- Rappresentazioni intermedie malformate tollerate da un solver ma rifiutate da altri.
- Flaws nelle strumentazioni stesse della piattaforma (ad esempio, un adattatore di controllo che accettava prove false).
Esperimenti di Tasso di Fuga (Escape Rate): Mutazioni semantiche indotte nel traduttore RISC-V sono state testate contro i gate del sistema.
- La "suite del quadrato" (sonde congiunte) ha colto 51/55 mutanti.
- I restanti 4 sono stati colti dal benchmark derivato.
- Zero fughe sono state osservate nell'ultimo round, sebbene gli autori notino che questo misura la famiglia di mutazione, non un tasso di fuga zero per tutti i possibili errori.
- I fallimenti di modo comune (dove entrambi i lati di un quadrato sono errati in modo identico) sono stati colti solo dal ramo divergente (percorso Sail) o da differenziali esterni, validando la necessità di ancoraggi semantici indipendenti.
Esperimento LLM Player: Un agente LLM è stato incaricato di rispondere a domande usando la piattaforma.
- In una seconda iterazione (v2), l'LLM player ha ottenuto 8/8 risposte corrette su difficili domande di raggiungibilità BTOR2, mentre un LLM non assistito ha ottenuto 7/8.
- Fondamentalmente, le risposte dell'LLM player erano accompagnate da artefatti di evidenza verificati da macchina (ad esempio, testimonianze riprodotte, certificati LRAT), mentre l'LLM non assistito si affidava a "parole" e punteggi di confidenza.
Prestazioni: L'overhead della disciplina (controllare ogni passaggio, riprodurre le testimonianze) è piccolo rispetto alla chiamata del solver. La traduzione richiede millisecondi; il solver domina il tempo.

Significato e Dichiarazioni

Il documento afferma che la fiducia nella traduzione può essere fabbricata dall'architettura piuttosto che fidandosi dell'autore.

Posizione sui Sistemi Distribuiti: Tratta i traduttori come componenti che possono fallire, contenendo il fallimento attraverso proiezioni dichiarate, controlli decidibili e percorsi indipendenti, invece di prevenirlo tramite prova universale.
Il "Ratchet" della Fiducia: Il sistema è progettato per evolversi. La copertura e l'assicurazione crescono monotonicamente; i verdetto precedenti sono preservati anche mentre il grafo si espande.
Ambito Modesto: Gli autori sono espliciti nel dichiarare che il sistema è un "ritratto di capacità datato". Non pretendono di risolvere l'indecidibilità o di sostituire tutta la verifica formale. Il livello "provato" è abitato solo per specifiche domande limitate con certificati formali. Il sistema si affida all'evidenza empirica dell'adeguatezza dell'interprete e delle assunzioni di diversità strutturale.
L'Asimmetria: Il documento conclude che per le risposte esistenziali, la fiducia è "quasi gratuita" (tramite riproduzione), mentre per le risposte universali, il sistema deve "acquistare" consapevolmente l'assicurazione attraverso livelli graduati, rami e certificati.

Il lavoro pone che un sistema costruito su questi principi può permettere ad autori non affidabili (umani o IA) di contribuire a un'infrastruttura di ragionamento verificata, a condizione che l'architettura imponga controlli incrociati rigorosi e contratti compositivi.