Riepilogo Tecnico: VeriContest

Enunciato del Problema

Sebbene i Large Language Models (LLM) abbiano dimostrato competenza nella generazione di codice eseguibile a partire dal linguaggio naturale, le loro uscite mancano di garanzie formali di correttezza. Gli approcci esistenti basati sui test campionano solo il comportamento del programma e non possono garantire l'assenza di errori funzionali o difetti di sicurezza. La verifica formale offre un'alternativa più robusta richiedendo prove verificabili automaticamente che il codice soddisfi specifiche formali. Tuttavia, i progressi nella "generazione di codice verificabile" – dove un modello deve produrre simultaneamente codice, specifiche formali e prove – sono ostacolati dalla mancanza di benchmark rigorosi. I benchmark attuali sono spesso ridotti, si concentrano su fasi isolate della pipeline (ad esempio, solo codice o solo prove), mancano di prove di verità fondamentale (ground-truth) o mirano a contesti di verifica disconnessi dallo sviluppo software mainstream.

Metodologia

Gli autori introducono VeriContest, un benchmark composto da 946 problemi di programmazione competitiva tratti da LeetCode e Codeforces, specificamente progettati per la generazione di codice verificabile in Rust utilizzando il framework di verifica Verus.

Pipeline di Costruzione del Benchmark

VeriContest è costruito attraverso una pipeline in tre fasi per garantire alta qualità e scalabilità:

1. Fase I (Costruzione Manuale): Esperti hanno manualmente costruito 91 problemi "seed". Per ciascuno, hanno scritto specifiche formali (precondizioni e postcondizioni), codice Rust accettato dal giudice e prove verificate da Verus. Queste specifiche sono state rigorosamente validate per correttezza (ogni soluzione corretta soddisfa la specifica) e completezza (ogni soluzione che soddisfa la specifica è corretta).
2. Fase II (Espansione Semi-Automatizzata): Un agente LLM (supportato da GPT-5.3-Codex) ha espanso il benchmark a 946 problemi. Questa fase ha impiegato un processo di revisione "human-in-the-loop". L'agente ha filtrato i problemi che richiedevano funzionalità Rust non supportate (ad esempio, aritmetica in virgola mobile, strutture dati complesse) e ha generato specifiche, codice e prove. Esperti umani hanno verificato l'output tramite accettazione da parte del giudice online, revisione manuale delle specifiche e verifica indipendente con Verus.
3. Fase III (Generazione e Validazione dei Casi di Test): Per validare la completezza delle postcondizioni, gli autori hanno generato suite di test positive e negative.
   • Test Positivi: Generati sintetizzando programmi generatori verificati da Verus che producono input validi.
   • Test Negativi: Generati tramite mutation testing (mutazione semantica, sintattica e mutazione diretta dell'output) per creare input accoppiati con output errati.
   • Post2Exe: Uno strumento innovativo che converte le postcondizioni Verus supportate in programmi Rust eseguibili. Questi vengono eseguiti contro i casi di test negativi per rilevare e segnalare automaticamente le postcondizioni incomplete (quelle che accettano output errati), che vengono quindi inviate per revisione.

Protocollo di Valutazione

VeriContest supporta sia la valutazione isolata che compositiva attraverso quattro compiti fondamentali:

• SpecGen: Generazione di specifiche formali a partire dal linguaggio naturale.
• CodeGen: Generazione di codice eseguibile a partire dal linguaggio naturale, dalle specifiche o da entrambi.
• ProofGen: Generazione di prove Verus data una specifica e un codice.
• End-to-End: Generazione dell'intero programma verificato (specifica, codice e prova) a partire da una descrizione in linguaggio naturale.

La valutazione misura l'accuratezza pass@1, con metriche aggiuntive per la riparazione delle prove (repair@k) e il campionamento (pass@k).

Contributi Chiave

1. Benchmark VeriContest: Un dataset su larga scala di 946 problemi di programmazione competitiva caratterizzato da specifiche Verus validate da esperti, codice Rust accettato dal giudice, prove Verus di verità fondamentale e suite di test positive/negative complete.
2. Pipeline di Costruzione: Una metodologia scalabile in tre fasi che combina la creazione manuale dei seed, l'espansione semi-automatizzata con revisione umana e la validazione automatizzata basata sui test della completezza delle postcondizioni tramite Post2Exe.
3. Framework di Valutazione Modulare: Un protocollo che isola la generazione di specifiche, codice e prove valutando al contempo la sintesi end-to-end, permettendo un'analisi granulare dei colli di bottiglia.
4. Analisi Empirica: Una valutazione di dieci LLM all'avanguardia (inclusi GPT-5.5, Claude Opus 4.7 e DeepSeek V4) che rivela significativi divari di prestazioni tra la codifica standard e la generazione di codice verificabile.

Risultati

La valutazione di dieci modelli all'avanguardia su VeriContest rivela un netto declino delle prestazioni all'aumentare della complessità del compito, passando dalla generazione di codice alla verifica completa:

• Generazione di Codice (CodeGen): I modelli performano relativamente bene. Il modello più forte, GPT-5.5, raggiunge un'accuratezza del 92.18% nella generazione da linguaggio naturale a codice. Tuttavia, le prestazioni calano significativamente quando l'input è una specifica formale da sola (67.65%), suggerendo un disallineamento nella distribuzione di addestramento dove i modelli sono più familiari con le descrizioni dei problemi in linguaggio naturale rispetto ai vincoli logici formali.
• Generazione di Specifiche (SpecGen): Le prestazioni calano drasticamente. GPT-5.5 raggiunge solo il 48.31% nella generazione da linguaggio naturale a specifica, e i modelli open-source performano significativamente peggio (ad esempio, Qwen 3.6 allo 0.32%). Ciò indica che gli LLM sono molto meno familiari con la sintassi e la semantica delle specifiche formali rispetto al codice.
• Generazione di Prove (ProofGen): Questo è identificato come il principale collo di bottiglia. Anche con specifiche e codice di verità fondamentale forniti, GPT-5.5 raggiunge solo un'accuratezza del 13.95%. La maggior parte dei modelli rimane sotto l'8%.
• End-to-End: Il tasso di successo per la generazione di un programma completamente verificato da zero è estremamente basso. GPT-5.5 raggiunge solo il 5.29%. Gli autori notano che il successo end-to-end richiede che specifica, codice e prova siano allineati perfettamente; un fallimento in qualsiasi singolo componente causa il fallimento dell'intera pipeline.

Analisi degli Errori:

• CodeGen: Gli errori sono dominati da output errati per i modelli forti, ma si spostano verso errori di sintassi quando sono coinvolte specifiche formali.
• ProofGen: La modalità di fallimento dominante è il Fallimento di Verifica (la prova non soddisfa il verificatore) e la Modifica di Spec/Codice (i modelli alterano il codice o la specifica forniti invece di aggiungere solo le prove).
• SpecGen: Gli errori sono pesantemente dominati da errori di sintassi in Verus, seguiti da disallineamenti nelle pre/postcondizioni.

Significato e Affermazioni

Il paper afferma che VeriContest stabilisce una piattaforma rigorosa per misurare e addestrare futuri sistemi capaci di generare codice con correttezza verificabile automaticamente. Gli autori affermano che:

• La generazione di prove e specifiche sono i colli di bottiglia centrali per gli attuali LLM nella pipeline di generazione di codice verificabile.
• Esiste un divario sostanziale tra la capacità di un modello di scrivere codice e la sua capacità di verificarlo formalmente.
• Il successo end-to-end è attualmente limitato non solo dalla generazione di codice, ma dalla difficoltà di allineare specifiche, codice e prove in un insieme coerente.
• Il benchmark funge da fonte di supervisione per l'addestramento di modelli sulla generazione di codice verificabile, andando oltre la semplice correttezza funzionale verso garanzie formali.

Gli autori mantengono un atteggiamento modesto riguardo alla portata, riconoscendo che VeriContest è limitato a Rust/Verus e a problemi di programmazione competitiva, e non copre ancora codice di sistema, protocolli distribuiti o altri framework di verifica come Dafny o Lean. Suggeriscono che il lavoro futuro dovrebbe espandersi a più linguaggi e domani man mano che strumenti e capacità dei modelli migliorano.