Sintesi Tecnica: TLA-Prover

Definizione del Problema

TLA+ è un linguaggio di specifica formale utilizzato per la verifica di sistemi distribuiti e protocolli critici per la sicurezza, accoppiato con il model checker TLC per l'esplorazione esaustiva dello spazio degli stati. Sebbene i Large Language Models (LLM) mostrino una promessa nel generazione di codice, incontrano difficoltà significative con TLA+ a causa della sua rappresentazione scarsa nei corpora di pre-training e della sua sintassi idiosincratica (ad esempio, operatori temporali, comprensione degli insiemi).

I baseline esistenti, come lo studio FormaLLM, indicano che gli LLM open-weight non ottimizzati raggiungono solo un tasso di successo dell'8,6% nel superare il model checker TLC su 25 modelli. Una sfida critica nell'addestramento di LLM per la verifica formale è il reward hacking (ottimizzazione impropria della ricompensa). Nel contesto di TLA+ e TLC, un modello può ottimizzare il segnale binario "pass" generando invarianti banali e tautologici (ad esempio, TypeOK == TRUE). Queste specifiche passano il controllo di TLC in ogni stato raggiungibile, ma non trasmettono proprietà significative sul protocollo, rendendo la verifica inutile. Gli approcci standard di apprendimento per rinforzo che si affidano esclusivamente al segnale pass/fail di TLC sono vulnerabili a questo modo di fallimento.

Metodologia

Gli autori presentano TLA-Prover, un modello da 20 miliardi di parametri (basato su gpt-oss-20b) progettato per la sintesi di specifiche TLA+. L'approccio combina il Supervised Fine-Tuning (SFT) con una nuova pipeline di addestramento che integra la Group Relative Policy Optimization (GRPO) basata sulla riparazione e una gerarchia di validazione a quattro livelli.

1. Gerarchia di Validazione a Quattro Livelli

Per prevenire il reward hacking e garantire la validità semantica, ogni output del modello viene valutato da una pipeline deterministica esterna in uno di quattro livelli:

• Bronze (Bronzo): L'output fallisce il parser SANY (sintatticamente non valido).
• Silver (Argento): L'output è sintatticamente corretto ma non riesce a caricarsi o a girare in TLC (ad esempio, timeout, errori di tipo).
• Gold (Oro): L'output supera sia SANY che TLC; il model checker esaurisce lo spazio degli stati e tutti gli invarianti sono soddisfatti.
• Diamond (Diamante): L'output supera il livello Gold e l'invariante è sensibile alla mutazione.
  • Meccanismo: Viene applicata una mutazione automatica a livello di AST al predicato dell'invariante (ad esempio, negando una congiunzione, invertendo operatori relazionali o scambiando costanti). La specifica mutata viene rieseguita attraverso TLC.
  • Criterio: Se la mutazione causa un controesempio in TLC, l'invariante originale è considerato non banale (Diamond). Se TLC passa ancora (ad esempio, perché l'invariante era TRUE), l'output fallisce il controllo Diamond. Questo passaggio blocca esplicitamente gli invarianti tautologici.

2. Pipeline di Addestramento

Il processo di addestramento consiste in due fasi primarie, con un'ablation DPO per il confronto:

• Fase 1: Supervised Fine-Tuning (SFT)

  • Corpus: Un dataset curato di 1.053 specifiche, rigorosamente filtrato al livello Diamond. I dati provengono dalla distribuzione TLA+ Foundation e dal repository tlaplus/examples, aumentati da un generatore Ollama e filtrati da un giudice LLM e dalla pipeline a quattro livelli.
  • Architettura: Un adapter LoRA (rank 8, alpha 16) è applicato alle proiezioni di attenzione del modello base da 20B.
  • Obiettivo: Insegnare al modello il vocabolario strutturale e la sintassi di TLA+.

• Fase 2: Repair-Based Group Relative Policy Optimization (GRPO)

  • Motivazione: La GRPO standard fallisce quando tutti i campioni in un gruppo falliscono il verificatore (ricompense scarse), risultando in un vantaggio nullo e assenza di flusso del gradiente.
  • Meccanismo: Il modello riceve una specifica "rotta" (tratta da tentativi precedenti falliti) e ha il compito di ripararla.
  • Segnale di Ricompensa: Un punteggio di miglioramento continuo basato sulle transizioni di livello (Bronze→Silver: 0.1, Silver→Gold: 0.3, Gold→Diamond: 0.6). Ciò fornisce gradienti densi anche quando l'output finale non è perfetto, purché il livello migliori.
  • Processo: Il modello corregge iterativamente i propri output utilizzando i messaggi di errore di TLC come feedback.

• Studio di Ablation (DPO): Una variante di Direct Preference Optimization è stata addestrata dallo stesso checkpoint SFT utilizzando coppie di preferenze statiche (Diamond > Gold > Silver > Bronze). Questa è servita come baseline per confrontare l'approccio dinamico della riparazione-GRPO.

Risultati Chiave

Il modello è stato valutato su un benchmark di 30 problemi utilizzando la decodifica greedy single-shot.

• Performance: TLA-Prover (checkpoint finale repair-GRPO) ha raggiunto un tasso di successo del 30% (9/30) sia ai livelli Gold che Diamond.
• Confronto con il Baseline: Questo rappresenta un miglioramento di 3,5 volte rispetto al baseline FormaLLM non ottimizzato dell'8,6%.
• Confronto con l'Ablation: La variante DPO ha raggiunto un tasso di successo Diamond del 20%, superata dall'approccio repair-GRPO (30%).
• Validazione Anti-Reward-Hacking: Fondamentalmente, i tassi di passaggio Gold e Diamond coincidevano a ogni checkpoint nella pipeline di produzione (differenza 0). Ciò indica che il modello non ha imparato a generare invarianti tautologici che passano TLC ma falliscono il test di mutazione. L'unica eccezione è stata un singolo caso nell'ablation DPO, che il livello Diamond ha intercettato con successo.
• Strategie di Inferenza:
  • Il Best-of-8 sampling ha aumentato il tasso di successo Diamond al 37% (11/30).
  • L'unione Greedy ∪ Best-of-8 suggerisce un tetto massimo del 43% (13/30), indicando che il modello possiede la capacità di risolvere più problemi con più tentativi.
  • L'auto-correzione (feedback TLC a 3 step) non ha prodotto miglioramenti, suggerendo che i fallimenti sono dovuti a lacune di conoscenza piuttosto che a errori di campionamento casuale.

Significato e Contributi

L'articolo rivendica tre contributi primari:

1. TLA-Prover con una Gerarchia a Quattro Livelli: L'introduzione di una gerarchia di validazione dove il livello superiore (Diamond) utilizza il testing di mutazione per escludere invarianti tautologici. Questo affronta il rischio specifico di reward-hacking inerente all'uso di TLC come segnale di ricompensa, garantendo che il "passaggio" implichi una specifica non banale.
2. Pipeline GRPO basata sulla Riparazione: Una pipeline di addestramento a due stadi che combina SFT su un corpus di livello Diamond con la riparazione-GRPO. Questo approccio sfrutta il feedback online dal verificatore per fornire segnali di ricompensa densi, superando le ablazioni statiche DPO.
3. Analisi Empirica Anti-Reward-Hacking: L'osservazione che i tassi di passaggio Gold e Diamond coincidono in tutti i checkpoint fornisce una prova empirica che la pipeline previene con successo il modo di fallimento "invariante sempre vero".

Gli autori posizionano questo lavoro come il primo studio di addestramento mirato a TLA+ che supera sostanzialmente i baseline di FormaLLM. Evidenziano che, sebbene il modello migliori significativamente la sintesi delle specifiche, attualmente si specializza in specifiche di tipo invariante con piccoli spazi di stato e fatica con protocolli complessi che richiedono analisi di casi o manipolazione di quantificatori. Il lavoro sottolinea che l'addestramento guidato dal verificatore senza una validazione anti-reward-hacking (come il livello Diamond) è insufficiente per produrre specifiche formali significative.