Sintesi Tecnica: KBSpec

Definizione del Problema

La generazione automatizzata di specifiche formali è un passaggio critico per la comprensione dei programmi e la verifica formale. Sebbene i Large Language Models (LLM) abbiano mostrato potenziale nella generazione di codice, la loro applicazione alla specifica formale (ad esempio, il Java Modeling Language, JML) affronta un ostacolo significativo: la scarsità di corpora di specifiche formali nei dati di addestramento. Questo stato di "scarsità di risorse" (low-resource) porta a frequenti errori sintattici e fallimenti semantici (ad esempio, controlli dei limiti mancanti, invarianti errati).

I tentativi esistenti di potenziare gli LLM con conoscenze esterne (ad esempio, la documentazione ufficiale) sono insufficienti perché le risorse per le specifiche formali sono spesso incomplete, mancano di copertura su diversi pattern di verifica o contengono funzionalità sperimentali non completamente supportate dai verificatori. Inoltre, fare affidamento esclusivamente sulla conoscenza esterna statica non riesce a catturare i vincoli sfumati e specifici del verificatore necessari per una verifica di successo.

Metodologia: KBSpec

Gli autori propongono KBSpec (Knowledge Base-Augmented Specification Generation), un framework che potenzia gli LLM con una base di conoscenza a doppia sorgente e auto-evolutiva. Il sistema opera senza modificare i parametri dell'LLM o richiedere dati di ground-truth etichettati, affidandosi invece al feedback dei verificatori formali.

La pipeline di KBSpec consiste in tre fasi principali:

1. Inizializzazione della Base di Conoscenza

Il sistema inizializza una base di conoscenza per le specifiche ($M$) utilizzando la conoscenza esterna proveniente dalla documentazione ufficiale (ad esempio, tutorial di OpenJML, esempi ed esercizi) e da linee guida di riparazione scritte da esseri umani. Ogni elemento di conoscenza è strutturato come una tripletta: contenuto originale ($c_i$), un riassunto ($s_i$) e parole chiave ($k_i$), generati da un LLM per facilitare il recupero.

2. Evoluzione della Base di Conoscenza (Fase di Addestramento)

Questa è l'innovazione principale. La base di conoscenza viene aggiornata dinamicamente attraverso una pipeline di generazione e riparazione eseguita su un corpus di "addestramento" di programmi Java.

• Generazione: Per un dato programma, l'LLM genera una specifica di base. Successivamente, recupera elementi di conoscenza rilevanti e genera nuove specifiche basate su diverse combinazioni di conoscenza recuperata.
• Verifica e Punteggio: Le specifiche generate vengono verificate utilizzando un verificatore formale (OpenJML). Un punteggio di utilità (helpfulness score) viene assegnato a ciascun elemento di conoscenza recuperato in base al fatto che abbia aiutato l'LLM a superare la verifica quando precedentemente era fallito, o che abbia causato il fallimento quando precedentemente era passato.
• Riparazione Iterativa: Per le specifiche che falliscono, il sistema esegue fino a tre round di riparazione. L'LLM utilizza la specifica originale, il messaggio di errore del verificatore e la conoscenza recuperata per generare una versione corretta. L'utilità degli elementi recuperati viene aggiornata in base alla riduzione degli errori o al successo della verifica.
• Aggiornamento e Filtraggio: Dopo ogni epoca, la base di conoscenza viene aggiornata. Gli elementi con bassi punteggi di utilità vengono filtrati e nuovi successi (generazione o riparazione) vengono aggiunti. La ridondanza è gestita tramite controlli di similarità.

3. Inferenza Potenziata dalla Conoscenza

Durante la fase di valutazione, KBSpec utilizza la base di conoscenza evoluta per assistere la generazione delle specifiche. A differenza della fase di addestramento, che utilizza il campionamento casuale di gruppi di conoscenza, la fase di inferenza impiega un selettore basato su LLM. L'LLM sceglie autonomamente gli elementi di conoscenza più rilevanti (fino a 3) dall'insieme recuperato per guidare la generazione e la successiva riparazione delle specifiche.

Contributi Chiave

1. Framework KBSpec: Un approccio innovativo e privo di parametri per la generazione di specifiche formali che integra una base di conoscenza auto-evolutiva guidata dal feedback del verificatore.
2. Conoscenza a Doppia Sorgente: L'identificazione e la validazione del fatto che combinare la documentazione esterna (per la comprensione iniziale del linguaggio) con la conoscenza interna (distillata dal feedback del verificatore su traiettorie di generazione/riparazione) è essenziale per superare i limiti degli LLM nella specifica formale.
3. Validazione Empirica: Una valutazione completa sul benchmark FormalBench (generazione di specifiche JML) che dimostra come KBSpec superi significativamente le controparti allo stato dell'arte, inclusi SpecGen e varie strategie di prompting (Few-shot, Least-to-Most, Self-repair).

Risultati

Gli esperimenti sono stati condotti utilizzando tre backend LLM: GPT-5.2, GPT-5-mini e DeepSeek-v3.2.

• Miglioramento del Tasso di Successo (Pass Rate): KBSpec ha migliorato i tassi di verifica di successo del 10–25% rispetto agli approcci basati su LLM allo stato dell'arte (ad esempio, SpecGen). Su GPT-5.2, il tasso di successo è passato dal 43,35% (SpecGen) al 58,94%.
• Riduzione dei Fallimenti: Il framework ha ridotto sostanzialmente i tassi di fallimento (ad esempio, riducendo il tasso di fallimento per GPT-5.2 al 20,6%).
• Completezza: Sebbene i punteggi medi di completezza abbiano mostrato una certa varianza, KBSpec ha prodotto il maggior numero di specifiche ad alta completezza (completezza $\ge$ 0,5). L'analisi dei programmi verificati mutuamente ha mostrato che KBSpec mantiene o migliora la completezza rispetto a SpecGen, indicando che i guadagni nel tasso di successo non sono stati ottenuti generando contratti trivialmente deboli.
• Studio di Ablazione: Lo studio ha confermato che il meccanismo di evoluzione della base di conoscenza (conoscenza interna) era la componente più critica, contribuendo alle prestazioni più della documentazione esterna iniziale. Anche la riparazione iterativa è stata identificata come un importante motore di successo.

Significato e Rivendicazioni

Il documento afferma che KBSpec affronta la natura "low-resource" dei linguaggi di specifica formale creando un ciclo di auto-miglioramento in cui il sistema impara dai propri successi e fallimenti tramite il feedback del verificatore.

• Indipendenza dal Modello (Model Agnostic): L'approccio è leggero e può essere applicato a qualsiasi LLM senza fine-tuning.
• Generalizzabilità: Sebbene valutato su JML, gli autori affermano che il design è indipendente dal linguaggio e può essere adattato a qualsiasi linguaggio di specifica con un verificatore automatizzato.
• Ingegneria Pragmatica: L'analisi della conoscenza appresa rivela che il sistema impara efficacemente strategie di riparazione pragmatiche (ad esempio, gestione degli overflow aritmetici, rimozione di costrutti non supportati) piuttosto che indebolire semplicemente le specifiche per superare la verifica.

Gli autori concludono che l'integrazione della conoscenza derivata dalla documentazione con l'evoluzione della memoria basata sul verificatore migliora sostanzialmente la capacità degli LLM di generare specifiche formali sintatticamente corrette e semanticamente verificabili.