Riepilogo Tecnico: BRIDGE – Costruzione di Rappresentazioni nella Sintesi di Programmi Verificati Guidata dal Dominio

1. Enunciato del Problema

I Modelli Linguistici di Grande Dimensione (LLM) sono sempre più capaci di generare codice, ma nel contesto della verifica formale, i programmi generati spesso appaiono corretti mentre nascondono bug sottili, casi limite mancanti o assunzioni non corrispondenti. Negli assistenti di prova come Lean, la verifica dei programmi non è un compito di singola generazione, ma un problema di previsione multi-artefatto. Una verifica riuscita richiede la coerenza reciproca di quattro artefatti accoppiati:

1. Codice Esecutivo: L'implementazione.
2. Specificazione Formale: Vincoli comportamentali (precondizioni, postcondizioni, invarianti).
3. Enunciati di Teorema: Affermazioni che collegano il codice alla specifica.
4. Tentativi di Dimostrazione: Script verificati dal kernel per confermare le affermazioni.

I sistemi LLM attuali faticano in questo contesto perché trattare questi artefatti in modo indipendente porta a una deriva semantica. Un modello potrebbe generare codice che supera i test ma fallisce i controlli di terminazione di Lean, una specifica che passa il controllo dei tipi ma è vacua, o un teorema dimostrabile ma irrilevante per il compito originale. La sfida fondamentale consiste nel tradurre un'intento informale in una sequenza di artefatti in cui sintassi, tipi, strutture di ricorsione, contratti e obblighi di prova rimangono allineati.

2. Metodologia: Il Framework BRIDGE

Gli autori propongono BRIDGE, un framework di prompting strutturato che scompone il processo di codifica verificabile in tre domini collegati: Codice, Specificazione e Teorema/Prova. Invece di chiedere a un modello di passare direttamente dal linguaggio naturale a una prova finale, BRIDGE impone un flusso di ragionamento strutturato in cui gli artefatti si vincolano e si controllano a vicenda.

2.1 Scomposizione dei Domini

• Il Dominio del Codice: Produce l'implementazione finale in Lean. BRIDGE confronta la generazione diretta in Lean con impalcature di ragionamento intermedie.
  • Impalcature Funzionali: Ispirate a OCaml e Haskell, queste incoraggiano dati immutabili, matching di pattern, ricorsione strutturale e definizioni composizionali. Questo si allinea naturalmente con la teoria dei tipi dipendenti di Lean e la disciplina di terminazione.
  • Impalcature Imperative: Ispirate a Python e C++, queste incoraggiano cicli e mutazione.
  • Insight Chiave: Il programma intermedio è un'impalcatura di ragionamento, non un artefatto sorgente certificato. Non deve essere compilabile nel suo linguaggio sorgente; il suo scopo è orientare il modello verso una struttura che Lean possa verificare.
• Il Dominio della Specificazione: Descrive le garanzie intese. BRIDGE utilizza vari stili di ragionamento (Design by Contract, Test basati sulle Proprietà, Sviluppo Guidato dai Test, Programmazione Difensiva) per rendere esplicite le assunzioni, i casi limite e le garanzie. Le specifiche sono valutate non solo per il controllo dei tipi, ma per la non vacuità e la loro capacità di distinguere implementazioni corrette da plausibili implementazioni errate.
• Il Dominio Teorema/Prova: Rende esplicite le affermazioni di correttezza. I modelli sono sollecitati a proporre proprietà (limiti, invarianti, monotonia) e tentare dimostrazioni. Questo dominio funge da diagnostico per la verifica a valle, verificando se i teoremi generati possono essere elaborati e se le prove possono essere completate senza sorry (segnaposto per obiettivi non dimostrati).

2.2 Ipotesi di Ragionamento

L'ipotesi centrale è che il successo della verifica dipenda dalla struttura del ragionamento intermedio. La generazione diretta costringe il modello a recuperare l'algoritmo, esprimerlo in Lean, soddisfare i vincoli di tipo/terminazione e inferire le specifiche simultaneamente. BRIDGE separa queste pressioni. Nello specifico, gli autori riscontrano che un ordinamento che inizia con la generazione di codice funzionale è particolarmente efficace: il modello genera prima codice compatibile con Lean utilizzando un'impalcatura funzionale, quindi utilizza tale implementazione come ancoraggio semantico per le specifiche e gli enunciati dei teoremi.

3. Contributi Chiave

1. Un Framework Multi-Artefatto: BRIDGE introduce un approccio strutturato alla codifica verificabile che scompone il compito in domini collegati di Codice, Specificazione e Teorema/Prova, utilizzando il ragionamento tra artefatti per ridurre la deriva semantica.
2. Il Ragionamento Funzionale Migliora la Sintesi: Su un benchmark Lean di 178 problemi, un ragionamento intermedio allineato funzionalmente migliora la correttezza eseguibile di Lean fino a 1,5 volte rispetto al prompting diretto. Raggiunge tassi di successo comparabili con circa 2 volte meno valutazioni Lean, indicando una maggiore efficienza del campione.
3. Artefatti a Valle Migliorati: Il prompting in stile BRIDGE produce artefatti formali più utili. Genera più enunciati di teorema che si elaborano con successo in Lean e più tentativi di prova completati allineati all'implementazione. Il prompting guidato dalla specifica migliora anche la generazione di codice convenzionale (fino a 17,5 punti percentuali in Python).
4. Bias Induttivo Apprendibile: Il Fine-Tuning Supervisionato (SFT) su tracce funzionali in stile BRIDGE supera il fine-tuning su tracce dirette corrispondenti (ad esempio, un guadagno di 9,1 punti percentuali sul benchmark VERINA). Ciò suggerisce che il framework cattura un bias induttivo apprendibile piuttosto che essere un effetto di prompting una tantum.

4. Risultati Sperimentali

Gli autori hanno valutato BRIDGE su un benchmark Lean personalizzato di 178 problemi e su benchmark pubblici inclusi VERINA, CLEVER e un pilota DAFNYBENCH supportato da solver.

• Correttezza Esecutiva: Utilizzando impalcature funzionali, il tasso di successo sul benchmark di 178 compiti è aumentato da 44/178 (Diretto) a 59/178 (Funzionale) nell'impostazione del nucleo minimo. Con round di riparazione, il divario è rimasto positivo (83/178 vs. 77/178).
• Efficienza del Campione: Le impalcature funzionali hanno raggiunto risultati comparabili con circa la metà del numero di valutazioni Lean rispetto al prompting diretto, riducendo il costo di verifica dei candidati.
• Trasferibilità: I benefici si sono trasferiti ai benchmark pubblici. Su VERINA, il prompting funzionale ha migliorato i tassi di successo fino a 6,3 punti percentuali. Su DAFNYBENCH, ha migliorato la verifica pass@5 di 7,3 punti percentuali.
• Diagnostica delle Prove: In un esperimento di prova completo, il codice funzionale ha prodotto più prove completate senza sorry (34/178 vs. 20/178 con il prover SFT funzionale) e ha generato implementazioni più brevi e pulite, più facili da risolvere per i modelli di prova.
• Guadagni SFT: Il fine-tuning su tracce funzionali ha migliorato le prestazioni su VERINA dal 20,3% al 29,4%, dimostrando che la struttura di ragionamento può essere interiorizzata dal modello.

5. Significato e Limitazioni

Il documento afferma che la rappresentazione del ragionamento conta. Strutturando il processo di generazione per allinearlo al sistema di verifica target (Lean), BRIDGE riduce i fallimenti di sintassi, tipo e terminazione. Il framework fornisce un bias induttivo orientato alla verifica che collega codice, specifiche, enunciati di teorema e tentativi di prova, rendendo la pipeline più facile da ispezionare e più adatta alla ricerca di prove a valle.

Affermazioni Modeste e Limitazioni:

• Non è una Verifica Completa: BRIDGE studia il "front end" della sintesi verificata. Non afferma di risolvere la verifica semantica completa su larga scala. Le specifiche e gli enunciati di teorema generati possono comunque essere deboli, vuoti o eccessivamente plasmati dall'implementazione.
• Ambito: La valutazione si concentra su compiti algoritmici locali. Gli autori non hanno ancora testato BRIDGE su grandi librerie formali, programmi complessi con stato o prove a lungo termine.
• Dipendenza dal Modello: I risultati variano tra modelli, prompt e budget di ricerca. BRIDGE è presentato come un utile bias induttivo piuttosto che un miglioramento universale indipendente dal modello sottostante.
• Lavoro Futuro: Gli autori notano che il prossimo passo è chiudere il ciclo tra gli artefatti BRIDGE e una ricerca di prove più forte, integrando potenzialmente prover di teoremi che utilizzano strumenti, recupero di librerie formali e apprendimento per rinforzo da ricompense verificabili.

In sintesi, BRIDGE dimostra che scomporre la codifica verificata in passaggi di ragionamento strutturati e allineati al dominio migliora significativamente la qualità e la verificabilità degli artefatti generati, offrendo una via verso una sintesi formale più affidabile senza richiedere l'automazione completa del processo di prova.