SpecPylot: Python Specification Generation using Large Language Models

1. Il Problema

La scrittura manuale di specifiche formali (precondizioni, postcondizioni e invarianti) per i programmi Python è un processo lento, soggetto a errori e spesso evitato dagli sviluppatori. Questa carenza limita l'adozione di strumenti di verifica automatica e testing avanzato.
Sebbene i recenti Large Language Models (LLM) siano promettenti nella generazione di specifiche a partire dal codice sorgente, le specifiche prodotte direttamente dagli LLM presentano spesso problemi critici:

• Errori di sintassi.
• Vincoli eccessivamente restrittivi.
• Incoerenze con il comportamento reale del programma.
  Senza un meccanismo di validazione robusto, queste contratti generati sono difficili da riutilizzare o fidarsi.

2. Metodologia: SpecPylot

SpecPylot è uno strumento Python che implementa una pipeline di sintesi e verifica di contratti, combinando la generazione basata su LLM con l'esecuzione simbolica guidata da solver. Il flusso di lavoro si articola come segue:

• Generazione dei Contratti: Un LLM (supporto per provider come OpenAI e Anthropic) riceve il codice sorgente e genera annotazioni eseguibili utilizzando la libreria icontract. Il modello produce un wrapper contenente il codice annotato con @require (precondizioni) e @ensure (postcondizioni).
• Verifica con CrossHair: Il codice annotato viene sottoposto a verifica tramite CrossHair, uno strumento di esecuzione simbolica per Python. CrossHair analizza se i contratti sono coerenti con il comportamento del programma.
  • Stato PASSED: Nessun controesempio trovato entro i limiti di esplorazione.
  • Stato REFUTED: CrossHair trova un controesempio concreto (un caso di input che viola il contratto).
  • Stato INCONCLUSIVE: L'esplorazione simbolica non è stata esaustiva a causa di limiti di tempo o complessità (es. loop annidati), senza trovare controesempi.
• Loop di Raffinamento (Refinement Loop): Se il contratto viene REFUTED e rientra in un budget definito dall'utente, SpecPylot avvia un ciclo di raffinamento:
  1. Estrae il controesempio concreto e il contesto diagnostico da CrossHair.
  2. Invia queste informazioni all'LLM insieme al codice annotato corrente.
  3. L'LLM rivede solo i contratti (il codice sorgente rimane intatto) per correggere l'errore.
  4. Il processo di verifica viene ripetuto fino a quando il contratto passa, diventa inconclusivo o si esaurisce il numero massimo di iterazioni.
• Generazione di Test: Opzionalmente, lo strumento può generare stub di test pytest basati sulla copertura del codice utilizzando crosshair cover.

3. Contributi Chiave

• Strumento Pratico: Sviluppo di SpecPylot come strumento di ricerca utilizzabile, non solo come prototipo, con supporto per diversi backend LLM, budget configurabili e generazione di artefatti di debug.
• Approccio Iterativo Guidato dai Controesempi: Integrazione di feedback concreti da CrossHair per correggere automaticamente contratti errati o troppo restrittivi senza modificare il codice originale.
• Separazione delle Preoccupazioni: Distinzione chiara tra la generazione semantica (affidata all'LLM) e la validazione esecutiva (affidata al solver simbolico).
• Valutazione Empirica: Analisi dettagliata su un set di benchmark, fornendo dati su tempi di esecuzione, costi API e tassi di successo.

4. Risultati Sperimentali

Gli autori hanno valutato SpecPylot su 20 programmi Python (tradotti da Java e nativi), utilizzando due modelli LLM avanzati: GPT-4o e Claude Sonnet 4.5.

• Efficacia:
  • Claude Sonnet 4.5: Ha raggiunto un tasso di successo (PASSED) dell'80% (16/20 programmi) e un tasso inconclusivo del 20%.
  • GPT-4o: Ha raggiunto un tasso di successo del 75% (15/20 programmi) e un tasso inconclusivo del 25%.
  • I casi INCONCLUSIVE si sono verificati principalmente in programmi con loop complessi o ramificazioni profonde, dove l'esplorazione simbolica ha esaurito i limiti di budget prima di poter provare la correttezza.
• Efficienza e Costi:
  • GPT-4o è risultato più veloce e meno costoso in termini di token consumati (media di 4.756 token per problema vs 5.480 di Claude).
  • Il costo totale API per l'intero set di 20 programmi è stato di $0.80 per GPT-4o e $1.09 per Claude Sonnet 4.5.
  • Il ciclo di raffinamento è stato necessario raramente, con una media di circa 1.02 iterazioni per esecuzione, indicando che la maggior parte dei contratti generati inizialmente erano già validi o richiedevano pochissime correzioni.

5. Significato e Limitazioni

Significato:
SpecPylot dimostra che è possibile automatizzare la generazione di specifiche eseguibili per Python con un alto tasso di successo, riducendo il carico manuale sugli sviluppatori. L'approccio "verifier-in-the-loop" (dove il solver guida la correzione dell'LLM) si rivela efficace per colmare il divario tra la capacità generativa degli LLM e la necessità di correttezza formale.

Limitazioni:

• Esplorazione Simbolica Limitata: Un risultato "PASSED" non è una prova matematica di correttezza assoluta, ma indica solo che non sono stati trovati controesempi entro i limiti di esplorazione configurati.
• Complessità del Controllo: Programmi con loop annidati o strutture di controllo complesse tendono a causare timeout o risultati inconclusivi a causa dell'esplosione dei percorsi simbolici.
• Dipendenza dai Tipi: La precisione dei risultati dipende fortemente dalla disponibilità di annotazioni di tipo accurate nel codice Python.
• Variabilità degli LLM: La qualità delle specifiche varia in base al modello utilizzato e alle configurazioni di prompting.

In conclusione, il lavoro apre la strada a futuri sviluppi che potrebbero includere contratti basati su docstring (PEP 316) e l'estensione del lavoro a livello di intero repository per gestire contesti di progetto più ampi.