PROMISE: Proof Automation as Structural Imitation of Human Reasoning

1. Il Problema: Scalabilità nella Verifica Formale

La verifica formale di software critico (come kernel operativi o sistemi di sicurezza) offre garanzie matematiche di correttezza, ma il suo adozione è limitata dalla scarsa scalabilità. La costruzione di prove formali richiede un enorme sforzo umano e tempo, spesso superiore alla dimensione del codice stesso (es. il kernel seL4 ha richiesto decenni di lavoro cumulativo).

Sebbene i Large Language Models (LLM) abbiano mostrato successo nella generazione di codice e nella sintesi di prove matematiche semplici, faticano a scalare su progetti di verifica su larga scala come seL4, FSCQ o CertiKOS. Le limitazioni principali delle approcci attuali basati su LLM sono:

• Generazione "Single-shot" o ricerca superficiale: Molti sistemi trattano la generazione della prova come un compito di generazione testuale singola o una ricerca basata su recupero di informazioni (RAG) superficiale.
• Recupero basato su parole chiave: I sistemi esistenti recuperano premesse o prove intere basandosi sulla similarità testuale superficiale. Questo fallisce nel catturare le dipendenze strutturali profonde e i pattern di ragionamento ricorrenti che caratterizzano le grandi basi di codice di verifica.
• Mancanza di consapevolezza dello stato: Le prove non sono entità statiche, ma sequenze dinamiche di trasformazioni degli stati di prova (proof states). Gli approcci attuali non modellano efficacemente come gli obiettivi e le assunzioni evolvono durante la derivazione.

2. Metodologia: PROMISE

PROMISE (PROof MIning via Structural Embeddings) è un framework di "mining" delle prove che ripensa la generazione automatica come un processo di ricerca iterativo e stato-consapevole, guidato dall'imitazione strutturale del ragionamento umano.

Concetti Chiave

• Rappresentazione come Transizioni di Stato: Invece di vedere la prova come un testo, PROMISE la modella come una sequenza di transizioni di stato indotte dall'applicazione di tattiche (tactics). Ogni passo modifica l'obiettivo, introduce nuove assunzioni o riduce i sottogol.
• Recupero Strutturale (Structural Retrieval): A differenza dei metodi che cercano prove simili per contenuto testuale, PROMISE cerca tracce di transizione di stato strutturalmente simili. Il sistema recupera frammenti di prove che hanno un'evoluzione logica analoga allo stato corrente, indipendentemente dalla sintassi specifica.
• Recupero dei Nomi (Name Retrieval): Per garantire la validità logica, il sistema recupera anche i nomi concreti di lemmi e definizioni disponibili nel contesto attuale, separando la struttura del ragionamento dai fatti specifici.

Architettura e Flusso di Lavoro

PROMISE opera attraverso un ciclo di Beam Search guidato da un generatore di comandi:

1. Costruzione del Contesto: Per ogni nodo nella ricerca (uno stato di prova parziale), il sistema esegue due recuperi:
   • Strutturale: Identifica lemmi risolti in passato con pattern di transizione simili (usando embedding e metriche di similarità strutturale).
   • Di Nome: Identifica lemmi e definizioni validi nel contesto corrente (tramite analisi del contesto Isabelle e ricerca n-gram).
2. Prompting Grounded Few-Shot: Viene costruito un prompt che include lo stato corrente, le assunzioni attive, e template di tattiche estratte dai frammenti strutturali recuperati. Il modello LLM è istruito a generare candidati di passi successivi (1-2 comandi Isabelle) basandosi su questi pattern.
3. Generazione e Filtraggio: I candidati generati vengono normalizzati, filtrati staticamente (per sintassi e validità dei riferimenti) e poi verificati meccanicamente tramite un bridge Scala-Isabelle.
4. Valutazione e Beam Search: I candidati che fanno progressi (riducono i sottogol) vengono valutati con una funzione di punteggio che premia la riduzione dei goal, la concisione della prova e la diversità delle tattiche. I migliori candidati formano il "beam" per il prossimo livello di profondità.
5. Terminazione: Una prova è accettata solo se chiude lo stato locale e passa un controllo di coerenza dell'intera teoria (whole-theory check) in Isabelle.

3. Contributi Chiave

1. Nuova Prospettiva sulla Generazione di Prove: Sposta il focus dalla previsione di tattiche o dalla generazione di prove intere alla modellazione della evoluzione strutturale delle prove come segnale primario per il ragionamento su larga scala.
2. Framework PROMISE: Un sistema agnostico rispetto al modello (model-agnostic) che integra il recupero strutturale delle transizioni di stato con la generazione guidata da LLM, senza richiedere addestramento aggiuntivo sui modelli.
3. Valutazione Completa: Un'ampia valutazione empirica su benchmark reali derivati da seL4/l4v, confrontando PROMISE con approcci all'avanguardia come Selene e Rango.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su 223 teoremi del progetto seL4 (livelli P1, P2, P3) utilizzando diversi backend LLM (Qwen2.5-Coder-7B, GPT-3.5-Turbo, GPT-4.1).

• Prestazioni Superiori: PROMISE supera costantemente gli approcci precedenti.
  • Su Qwen2.5-Coder-7B, PROMISE raggiunge un tasso di successo del 77% su P1 e 36% su P2, contro il 30% e 2% di Selene (ACC5).
  • Il miglioramento relativo raggiunge fino al +186% rispetto alle baseline in alcuni scenari.
  • Su GPT-3.5-Turbo, PROMISE ottiene l'85% di successo su P1, superando significativamente Rango (35%) e Selene.
• Robustezza Cross-Modello: PROMISE mantiene prestazioni elevate e stabili indipendentemente dal modello LLM sottostante (dai modelli open-weight 7B ai modelli proprietari più grandi), a differenza di altri metodi che mostrano grandi variazioni di performance.
• Eccellenza su Compiti Difficili (P3): Su lemmi complessi (P3), PROMISE risolve 7 casi su 23, più del doppio rispetto alla baseline migliore (Rango con 3 casi).
• Analisi del Caso di Fallimento: L'unico caso in cui PROMISE non supera Rango è su GPT-4.1 per P2 (33% vs 35%). Gli autori ipotizzano che la forte capacità di GPT-4.1 di seguire istruzioni complesse possa essere stata eccessivamente vincolata dal prompt strutturato di PROMISE, limitando la sua capacità di esplorare strategie di ricerca più libere che Rango permette.

5. Significato e Impatto

Il lavoro dimostra che per scalare l'automazione delle prove in sistemi software reali, non basta migliorare la capacità di ragionamento dei modelli linguistici; è necessario cambiare il paradigma di recupero delle informazioni.

• Superamento delle Limitazioni Attuali: PROMISE risolve il problema della "crescita esponenziale" della complessità nelle grandi basi di codice, recuperando non solo cosa è stato provato, ma come è stato provato (i pattern di transizione).
• Validazione Pratica: L'uso di seL4 come benchmark conferma che l'approccio è applicabile a sistemi di produzione con dipendenze complesse e requisiti di sicurezza elevati.
• Futuro della Verifica: Il paper suggerisce che l'imitazione strutturale del ragionamento umano (basata su stati e transizioni) è la via maestra per rendere la verifica formale automatizzata praticabile per l'industria, riducendo drasticamente il carico di lavoro umano necessario per la costruzione di prove.

In sintesi, PROMISE rappresenta un passo fondamentale verso la verifica formale scalabile, trasformando la generazione di prove da un compito di generazione testuale a un processo di ricerca strutturale guidato da dati.