Sintesi Tecnica: Diversificare per Verificare

Definizione del Problema

Sebbene i Large Language Models (LLM) siano diventati efficaci nella sintesi di codice eseguibile da linguaggio naturale, la generazione di software formalmente verificato rimane una sfida significativa. Nei framework di verifica deduttiva come Why3, la correttezza non è stabilita semplicemente superando dei casi di test; richiede una specifica semantica formale (contratti, precondizioni, postcondizioni) e una guida alla prova sufficiente (invarianti, varianti, lemmi) per soddisfare un risolutore di teoremi automatizzato.

Il problema centrale affrontato è che la struttura dell'implementazione di un programma — specificamente la sua rappresentazione dei dati (es. array vs liste) e il flusso di controllo (es. ricorsivo vs imperativo) — può influenzare drasticamente la sua verificabilità automatizzata. Una singola semantica a livello di task può essere soddisfatta da molteplici implementazioni, eppure alcune strutture possono generare condizioni di verifica intrattabili per gli attuali SMT solver, mentre altre sono facilmente dimostrabili. Gli approcci esistenti spesso trattano la generazione del codice come un compito "single-shot", fallendo nel sfruttare il potenziale della diversità di implementazione per trovare artefatti "amichevoli alla verifica".

Metodologia: Diversify2Verify

Gli autori introducono Diversify2Verify, una pipeline basata su LLM a stadi, progettata per generare e verificare artefatti Why3. La pipeline decompone il processo di generazione in tre fasi distinte, imponendo confini rigorosi per garantire che il successo della verifica non sia ottenuto indebolendo la specifica o alterando la semantica fondamentale del task.

1. Architettura della Pipeline

• Fase 1: Generazione del Contratto.
  • Input: Task in linguaggio naturale, firma target, esempi concreti e una rappresentazione target (array o lista).
  • Processo: L'LLM inferisce un contratto formale specifico per la rappresentazione (precondizioni, postcondizioni, predicati ausiliari).
  • Validazione: Il contratto viene controllato dal punto di vista dei tipi in Why3, e si tenta di dimostrare dei "test lemmas" derivati dagli esempi concreti.
  • Policy: Una volta che un contratto supera la validazione, esso viene congelato. Esso funge da target semantico immutabile per le fasi successive. La riparazione è permessa solo prima del congelamento per correggere sintassi, tipi o inconsistenze semantiche con gli esempi.
• Fase 2: Generazione dell'Implementazione.
  • Processo: La pipeline genera candidati WhyML eseguibili per lo stesso contratto congelato.
  • Strategia di Diversità: Per ogni task, vengono generate quattro distinte famiglie di implementazione:
    1. Array-Ricorsivo
    2. Array-Imperativo
    3. Lista-Ricorsivo
    4. Lista-Imperativo
  • Validazione: I candidati sono filtrati tramite controllo dei tipi e superamento di un sottoinsieme di test eseguibili.
  • Policy: La riparazione è limitata (5 tentativi) e ristretta alla stessa rappresentazione e famiglia di struttura di controllo (ad esempio, un candidato array-imperativo non può essere riparato in un lista-ricorsivo).
• Fase 3: Verifica Completa e Riparazione.
  • Processo: Il contratto congelato e un'implementazione testata vengono combinati. L'LLM aggiunge le necessarie annotazioni di prova (invarianti di ciclo, varianti, codice ghost, asserzioni) per collegare lo stato locale del programma alla semantica globale del contratto.
  • Verifica: Why3 (con SMT solver Z3, Alt-Ergo, CVC4) tenta di soddisfare tutte le condizioni di verifica.
  • Policy di Riparazione: Se la verifica fallisce, viene eseguita una riparazione limitata (2 tentativi). Le riparazioni sono strettamente orientate alla prova (rafforzamento degli invarianti, aggiunta di lemmi) e devono preservare il contratto congelato e la famiglia di implementazione.

2. Costruzione del Benchmark

Gli autori hanno costruito un benchmark orientato alla verifica derivato dal LeetCodeDataset:

• Ambito: 73 task che coinvolgono interi, array e liste.
• Criteri di Selezione: I task sono stati filtrati per garantire che ammettessero contratti formali, supportassero molteplici implementazioni plausibili e fossero adatti al ragionamento supportato da SMT.
• Scala: Il benchmark produce 292 varianti di implementazione (4 per task).
• Nota: Il benchmark è intenzionalmente orientato verso tipi di dati SMT-friendly per isolare l'effetto della rappresentazione e della struttura di controllo sulla verificabilità.

Contributi Chiave

1. Pipeline Diversify2Verify: Una pipeline LLM a stadi che separa l'inferenza del contratto, la generazione dell'implementazione e l'annotazione della prova, imponendo una disciplina di "contratto congelato" per prevenire la deriva della specifica durante la riparazione.
2. Generazione di Implementazioni Diverse: Un approccio sistematico per generare varianti ricorsive e imperative su entrambe le rappresentazioni (array e liste), consentendo il confronto diretto di programmi strutturalmente diversi contro lo stesso target semantico.
3. Benchmark Orientato alla Verifica: Un set curato di 73 task con 292 artefatti generati, inclusi contratti accettati, implementazioni WhyML e log di verifica, rilasciato pubblicamente.
4. Studio Empirico della Verificabilità: Un'analisi che quantifica come il successo della verifica vari in base alla rappresentazione e allo stile di implementazione, misurando i guadagni derivanti dalla generazione di più varianti.

Risultati

La valutazione dimostra che la diversità di implementazione migliora significativamente il tasso di successo della verifica automatizzata:

• Verifica a Livello di Artefatto:
  • Iniziale: 96 su 292 artefatti (32,9%) verificati senza riparazione.
  • Dopo la Riparazione: 154 su 292 artefatti (52,7%) verificati dopo due passaggi di riparazione.
  • Impatto della Riparazione: La riparazione è stata responsabile della verifica di 58 ulteriori artefatti, con il primo passaggio che ha prodotto il guadagno maggiore.
• Verifica a Livello di Task:
  • Almeno una variante è stata verificata per 49 dei 73 task, raggiungendo un tasso di successo del 67,1% a livello di task.
  • La famiglia più forte (Array-Ricorsivo) ha verificato 44 task.
  • Ciò indica che la diversità fornisce un aumento misurabile della copertura dei task; fare affidamento su un singolo stile di implementazione significherebbe perdere molti task risolvibili.
• Differenze Strutturali:
  • Ricorsivo vs Imperativo: Le varianti ricorsive sono state verificate più spesso (60,3% per gli array, 54,8% per le liste) rispetto alle varianti imperative (47,9% per entrambi). Ciò è attribuito al fatto che le implementazioni ricorsive spesso si allineano meglio con le specifiche ricorsive, mentre le implementazioni imperative richiedono invarianti di ciclo complessi per riassumere lo stato mutabile.
  • Array vs Liste: I tassi di verifica aggregati per array e liste sono stati simili, suggerendo che la scelta della struttura di controllo (ricorsivo vs imperativo) abbia un effetto più pronunciato rispetto alla scelta della rappresentazione dei dati in questo contesto.
• Analisi dei Fallimenti:
  • La maggior parte degli artefatti non verificati (138 rimanenti) aveva pochissime obbligazioni di prova residue (media di 2,5 obiettivi radice), suggerendo che i fallimenti fossero dovuti a una mancanza di scaffolding di prova (es. invarianti specifici) piuttosto che a implementazioni fondamentalmente errate.
  • Un audit manuale ha confermato che la pipeline ha preservato con successo i contratti congelati in 291 casi su 292, con un solo caso in cui l'LLM ha aggiunto precondizioni non presenti nel contratto originale.

Significato e Claim

Il paper sostiene che implementazioni equivalenti per task possono differire sostanzialmente in termini di verificabilità. L'ipotesi centrale è supportata: generare varianti diverse aumenta la probabilità di trovare un'implementazione la cui struttura è idonea alla verifica deduttiva automatizzata.

Gli autori sottolineano che questo approccio non si affida a una singola generazione "perfetta", ma piuttosto alla diversità come strumento pratico per navigare nello spazio delle condizioni di verifica. Decoupling (decomponendo) la generazione della specifica dalla generazione dell'implementazione e imponendo confini rigorosi durante la riparazione, il sistema assicura che il successo della verifica non sia ottenuto indebolendo la specifica o cambiando la semantica del task.

Il lavoro suggerisce che, per la programmazione verificata assistita da LLM, la diversità di implementazione è un potente meccanismo per migliorare la copertura dei task, specialmente quando combinata con una riparazione guidata dal verificatore e limitata. Gli autori notano che questi risultati sono specifici al contesto dei task su interi e sequenze utilizzando Why3 e suggeriscono che il lavoro futuro dovrebbe esplorare strutture dati più ricche e altri framework di verifica.