Riepilogo Tecnico: Agente Event-B

Enunciato del Problema

Lo sviluppo di software "corretto per costruzione" si basa su metodi formali, in cui il comportamento del sistema e i requisiti sono espressi matematicamente e verificati tramite dimostrazione di teoremi e model checking. Tuttavia, la ripida curva di apprendimento e la richiesta di competenze matematiche hanno ostacolato l'adozione diffusa di tali metodi. Sebbene i Modelli Linguistici di Grande Dimensione (LLM) abbiano mostrato promesse nell'autoformalizzazione, gli approcci esistenti sono in gran parte limitati a compiti isolati, come la dimostrazione di teoremi senza formalizzazione o la sintesi di modelli verificata solo tramite model checking limitato.

Crucialmente, i metodi attuali basati su LLM non riescono a supportare l'evoluzione iterativa e congiunta di modelli formali e delle relative prove. Nella pratica, lo sviluppo formale richiede che, quando un dimostratore di teoremi non riesce a scaricare un obbligo di prova (PO), il sistema consenta revisioni sia al modello formale che ai suoi artefatti di prova. Gli strumenti esistenti o assumono un modello fisso e cercano prove (assistenti di prova LLM) o costruiscono modelli senza una rigorosa verifica basata su prove (autoformalizzazione). Manca un quadro concettuale che formuli lo sviluppo formale come un processo coordinato su uno spazio di stati congiunto di modelli e prove, consentendo affinamento e riparazione iterativi.

Metodologia: Agente Event-B

Per colmare queste lacune, gli autori propongono Agente Event-B, un nuovo framework neurosimbolico per la sintesi e la riparazione end-to-end di modelli formali. Il framework è progettato per assumere requisiti in linguaggio naturale e costruire un modello formale Event-B attraverso un processo iterativo che integra affinamento, sintesi e riparazione.

La metodologia consta di tre fasi principali:

1. Pianificazione della Strategia di Affinamento

Riconoscendo che il ragionamento automatico su sistemi complessi è impegnativo a causa della rapida crescita dello spazio di ricerca, Agente Event-B impiega LLM per pianificare una strategia di affinamento.

• Decomposizione: L'agente partiziona l'insieme dei requisiti in linguaggio naturale in sottoinsiemi disgiunti, distribuendoli su più passaggi di affinamento.
• Invarianti di Incollamento: Per ogni transizione tra i passaggi di affinamento, l'LLM propone "invarianti di incollamento" — predicati che relazionano variabili astratte e concrete per garantire la coerenza.
• Validazione: Queste invarianti vengono validate tramite controllo di controesempi (utilizzando un model checker) e tentativi di prova prima di essere accettate, assicurando che le proprietà dimostrate nei passaggi precedenti siano preservate.

2. Sintesi del Modello

Per ogni passaggio di affinamento, l'agente sintetizza un modello formale basato sui requisiti assegnati e sulle invarianti di incollamento.

• Generazione Guidata da Schema: Per mitigare gli errori di sintassi comuni nella generazione LLM, il sistema utilizza uno schema JSON che codifica la grammatica Event-B. Ciò garantisce la correttezza strutturale (ad esempio, eventi obbligatori, dichiarazioni di variabili).
• Ciclo di Correttezza: Il modello generato viene compilato. Eventuali errori di compilazione (ad esempio, incongruenze di tipo, variabili non dichiarate) vengono restituiti all'LLM per una riparazione iterativa finché il modello non è sintatticamente valido e corretto per i tipi.

3. Riparazione di Modello e Prova

Questa è il contributo principale del framework, progettato per gestire l'evoluzione congiunta di modelli e prove.

• Ciclo di Verifica: I modelli sintetizzati sono prima controllati da un model checker (ProB) per violazioni di invarianti all'interno di stati limitati. Se vengono trovati controesempi, il modello viene riparato.
• Dimostrazione di Teoremi: Il modello è quindi sottoposto a dimostrazione di teoremi illimitata. Se le prove falliscono, il sistema analizza lo stato della prova per diagnosticare il problema.
• Raccomandazione di Regole di Riparazione: Il sistema impiega un componente innovativo che mappa gli stati di prova a specifiche regole di riparazione (ad esempio, "Obiettivo Contraddittorio", "Obiettivo Esistenziale", "Preservazione di Invariante Quantificata"). Queste regole sono derivate empiricamente dalle esperienze manuali di scarico delle prove.
• Esecuzione di Riparazione Atomica: Un LLM di "decisione della strategia di fix" seleziona da una libreria di funzioni di riparazione atomiche (ad esempio, StrengthenGuard, AddInvariant, InstantiateHypothesis) e le esegue. Ciò limita le modifiche dell'LLM a operazioni corrette e verificabili.
• Correttezza (Soundness): Il sistema garantisce la correttezza rieseguendo tutte le prove dopo qualsiasi modifica al modello. Una riparazione è accettata solo se l'effetto combinato scarica l'PO target, verificato da solver SMT e dimostratori di teoremi.

Contributi Chiave

Il documento delinea tre contributi principali:

1. Framework: Agente Event-B è il primo framework end-to-end per la sintesi e la riparazione di modelli formali che supporta lo sviluppo basato su affinamento con costruzione coordinata del modello e derivazione delle prove, incarnando il principio di correttezza per costruzione.
2. Strumento: Uno strumento proof-of-concept integrato nell'IDE Rodin (l'ambiente standard per Event-B), che sfrutta ProB per il model checking e i dimostratori Rodin standard per la dimostrazione di teoremi.
3. Valutazione: Una valutazione completa su 27 sistemi formali (che vanno da semplici a complessi) confrontando Agente Event-B con baseline, inclusi studi di ablazione e analisi dell'efficienza.

Risultati Sperimentali

Il framework è stato valutato su 27 sistemi formali con una media di 182,41 obblighi di prova per sistema. I risultati dimostrano miglioramenti sostanziali rispetto alle baseline (LLM + dimostratori automatici, Cursor e PAT-Agent):

• Coerenza (Tasso di Scarico degli Obblighi di Prova - PDR): Agente Event-B ha raggiunto un PDR del 97,86%, superando significativamente le baseline (da 89,20% a 95,56%). Ha mantenuto un PDR superiore al 97,0% su tutti i livelli di complessità, mentre le baseline hanno mostrato una varianza maggiore e un degrado delle prestazioni con la complessità.
• Correttezza (Copertura dei Requisiti - RC e Soddisfacimento - RF):
  • RC: Agente Event-B ha raggiunto il 97,13%, superando il secondo miglior metodo del 4,63%.
  • RF: Agente Event-B ha raggiunto il 93,79%, superando il secondo miglior metodo del 18,01%.
  • Il rapporto RF/RC (0,97) indica che, una volta catturato un requisito, l'agente scarica con successo le prove associate, a differenza delle baseline dove i requisiti catturati rimanevano spesso non dimostrati.
• Efficienza: Il tempo medio per sintetizzare e riparare un sistema è stato di 74,45 minuti. Il tempo medio per tentare di scaricare un singolo PO è stato di 0,24 minuti, suggerendo che l'overhead di riparazione scala linearmente con il numero di PO anziché esplodere con la complessità del sistema.
• Studi di Ablazione: La rimozione della strategia di affinamento o del componente di guida alla riparazione ha portato a cali delle prestazioni, confermando che questi due componenti si rafforzano a vicenda. L'affinamento riduce la complessità delle prove, mentre la guida alla riparazione garantisce la correttezza dei passaggi di affinamento.

Significato e Affermazioni

Gli autori affermano che Agente Event-B rappresenta un passo promettente verso uno sviluppo formale pratico, corretto e assistito da LLM. Trattando lo sviluppo formale come uno spazio di stati congiunto di modelli e prove, il framework supera i limiti dell'autoformalizzazione isolata o della dimostrazione di teoremi.

Il documento sottolinea che:

• L'affinamento è essenziale per gestire la complessità, permettendo all'agente di scomporre problemi difficili in passaggi gestibili preservando la correttezza.
• La riparazione guidata dalle prove è necessaria perché il model checking da solo (limitato) è insufficiente per la correttezza generale; è richiesta la dimostrazione di teoremi (illimitata), ma ciò necessita di un meccanismo per riparare sia il modello che la prova quando il ragionamento automatico fallisce.
• L'approccio neurosimbolico combina con successo la flessibilità semantica degli LLM con la rigorosa correttezza degli strumenti di verifica simbolica.

Gli autori rimangono modesti riguardo all'ambito attuale, notando che la libreria di regole di riparazione è derivata empiricamente e non esaustiva, e che la gestione di requisiti in linguaggio naturale incoerenti rimane una sfida per lavori futuri. Tuttavia, i risultati suggeriscono che il framework proposto colma efficacemente il divario tra requisiti in linguaggio naturale e modelli formali corretti per costruzione.