Faithful Autoformalization via Roundtrip Verification and Repair

Riepilogo Tecnico: Autoformalizzazione Fedele tramite Verifica e Riparazione in Ciclo Chiuso

Enunciato del Problema
Il lavoro affronta una lacuna critica nell'autoformalizzazione: la mancanza di un metodo affidabile per verificare se un Modello Linguistico su Grande Scala (LLM) abbia catturato fedelmente il significato semantico di un enunciato in linguaggio naturale quando lo traduce in una rappresentazione formale, verificabile automaticamente. I metodi di valutazione esistenti si basano sulla validità sintattica o sul successo in compiti downstream, che non testano direttamente la fedeltà semantica. Inoltre, quando si verificano errori, le attuali strategie di riparazione sono limitate alla rigenerazione end-to-end, mancando della capacità di diagnosticare dove nel processo di traduzione il significato sia andato perso. Ciò è particolarmente impegnativo in domini come il diritto statutario, dove le formalizzazioni di verità fondamentale (ground-truth) non sono disponibili.

Metodologia
Gli autori propongono un Framework di Verifica in Ciclo Chiuso e Riparazione Contestualizzata che opera senza annotazioni di verità fondamentale. Il meccanismo centrale prevede una pipeline di traduzione in tre fasi:

1. T1 (Autoformalizzazione): Traduce l'input in linguaggio naturale $x$ in un'espressione formale $y_{orig}$ in un formalismo target $\Sigma$.
2. T2 (Retro-traduzione): Traduce $y_{orig}$ nuovamente in linguaggio naturale $x'$.
3. T3 (Riformalizzazione): Traduce $x'$ nuovamente in un'espressione formale $y_{rt}$.

Verifica: Il sistema verifica l'equivalenza logica tra la formalizzazione iniziale ($y_{orig}$) e la formalizzazione in ciclo chiuso ($y_{rt}$) utilizzando uno strumento formale (nello specifico, un risolutore SMT negli esperimenti). Se $y_{orig} \equiv_\Sigma y_{rt}$, la pipeline è considerata auto-coerente.

Diagnosi e Riparazione: Quando l'equivalenza fallisce, il framework impiega una procedura di diagnosi basata sulle fasi. Un giudice LLM esamina gli artefatti ($x, y_{orig}, x', y_{rt}$) per identificare la prima fase in cui si è verificata una deriva semantica (Fase 1, 2 o 3). Crucialmente, la diagnosi è "contestualizzata" (scoped), il che significa che la spiegazione è vincolata agli artefatti rilevanti solo per quella specifica fase.

• Riparazione Contestualizzata: Invece di rigenerare l'intera pipeline, un operatore di riparazione mirato ($R_i$) corregge solo la fase difettosa identificata. Le fasi a valle vengono quindi rigenerate per mantenere la coerenza della pipeline.
• Ciclo Iterativo: Questo processo si ripete fino a un budget fisso ($K=3$) fino a quando non viene raggiunta l'equivalenza o il budget viene esaurito.

Segnale Semantico Ausiliario: Per valutare la qualità semantica delle formalizzazioni indipendentemente dal ciclo di riparazione, gli autori utilizzano un modello bidirezionale di Inferenza in Linguaggio Naturale (NLI). Ciò funge da diagnosi post-hoc per misurare la "deriva" (ad esempio, contraddizioni o irrilevanza) tra il testo originale e il testo ricostruito, distinguendo tra regole formalmente coerenti ma semanticamente derivate.

Contributi Chiave

1. Framework di Verifica in Ciclo Chiuso: Un metodo per segnalare la fedeltà dell'autoformalizzazione senza formalizzazioni di verità fondamentale, applicabile a qualsiasi formalismo che ammetta un controllo di equivalenza (ad es. SMT, type checker).
2. Riparazione Contestualizzata Guidata dalla Diagnosi: Una procedura che localizza gli errori in passaggi di traduzione specifici, consentendo correzioni mirate invece di costose rigenerazioni dell'intera pipeline.
3. Analisi Empirica dei Colli di Bottiglia: Uno studio condotto su due domini statutari (Codice dei Trasporti del Texas e Codice dei Parchi e della Fauna Selvatica del Texas) e due famiglie di modelli (Claude Opus 4.6 e GPT-5.2) che identifica il passo di diagnosi come il principale collo di bottiglia per la riparazione contestualizzata, piuttosto che la pipeline o gli operatori di riparazione stessi.

Risultati
Il framework è stato valutato su 150 regole sul traffico e 77 regole sulla fauna selvatica.

• Efficacia della Riparazione: La riparazione contestualizzata guidata dalla diagnosi ha raggiunto i tassi più alti di equivalenza verificata al costo più basso quando la funzione di diagnosi era affidabile.
• Dipendenza dal Modello: Con Claude che eseguiva la pipeline e la diagnosi, la riparazione contestualizzata ha superato le linee di base (nessuna riparazione, selezione casuale della fase, rigenerazione completa). Tuttavia, con GPT, il passo di diagnosi era inaffidabile (fortemente distorto verso l'attribuzione della colpa alla Fase 1), causando una prestazione inferiore della riparazione contestualizzata e rendendola più costosa della rigenerazione completa.
• Intervento Cross-Modello: Sostituendo solo il passo di diagnosi di GPT con Claude (mantenendo GPT per la pipeline e la riparazione) si è ripristinata l'efficienza e l'efficacia della riparazione contestualizzata, dimostrando che la funzione di diagnosi è la variabile critica.
• Previsione della Fedeltà: L'equivalenza formale è un forte predittore della fedeltà semantica. Le regole che hanno superato il controllo di equivalenza (UNSAT) hanno mostrato una deriva NLI da 1,4× a 2,5× inferiore rispetto a quelle fallite (SAT). Tuttavia, l'equivalenza formale è necessaria ma non sufficiente; circa il 16% delle regole formalmente equivalenti ha comunque mostrato deriva semantica.

Significato e Affermazioni
Il lavoro afferma che l'equivalenza formale funge da segnale pratico, privo di verità fondamentale, per la fedeltà semantica nell'autoformalizzazione. Dimostra che la riparazione contestualizzata, guidata da una diagnosi accurata a livello di fase, è una strategia più economica ed efficiente rispetto alla rigenerazione completa. Gli autori sottolineano che l'affidabilità della funzione di diagnosi è il fattore determinante per il successo di questo approccio.

Il lavoro è modesto nel suo ambito, notando che il framework è euristico e non garantisce la correttezza rispetto all'intento originale in linguaggio naturale (poiché la pipeline potrebbe stabilizzarsi su un punto fisso semanticamente diverso). Gli autori affermano esplicitamente che il sistema non è adatto per applicazioni critiche per la sicurezza senza una revisione indipendente da parte di esperti e che la valutazione attuale è limitata a testi statutari in inglese, richiedendo ulteriori studi per altri generi come il codice o testi scientifici.