Sintesi Tecnica: Sintesi di Progettazione Concettuale Guidata da LLM e Verificata

Definizione del Problema

I moderni sistemi software sono sempre più assemblati componendo unità comportamentali riutilizzabili (ad esempio, autenticazione, etichettatura, controllo degli accessi). Sebbene la definizione del comportamento delle singole unità sia spesso semplice, la specifica della logica di coordinamento che assicura che queste unità interagiscano in modo sicuro è difficile. La metodologia Concept Design [Jac21] affronta questo problema organizzando le applicazioni attorno a "concetti" (unità di funzionalità autosufficienti e rivolte all'utente) collegati da "reazioni" (regole di sincronizzazione).

Tuttavia, il Concept Design attualmente manca di una semantica formale per le reazioni. Questa assenza rende difficile:

1. Definire con precisione cosa significhi un design.
2. Verificare automaticamente che un design preservi gli invarianti di sicurezza (ad esempio, "i dati sensibili non devono rimanere in una coda di messaggi errati").
3. Sintetizzare automaticamente una logica di coordinamento sicura.

Inoltre, anche se un design soddisfa un invariante di sicurezza, potrebbe non corrispondere all'intento dell'utente. Molti diversi design di reazione possono soddisfare lo stesso invariante, inclusi quelli implausibili (ad esempio, declassare dati sensibili per soddisfare un invariante invece di spostare i dati). Il documento identifica la necessità di un meccanismo per guidare la sintesi verso il design inteso dall'utente senza richiedere all'utente di formalizzare completamente il proprio intento in complessi vincoli logici.

Metodologia

Il documento introduce foundry, un prototipo che implementa un ciclo di Sintesi Induttiva Guidata da Controesempio (CEGIS) pilotato da Large Language Models (LLM). La metodologia consiste in tre componenti principali:

1. Semantica Formale

Gli autori definiscono una semantica basata su automi per concetti e reazioni:

• Concetti: sono modellati come semiautomati parziali inizializzati (macchine a stati deterministiche con input ma senza output).
• Reazioni: sono modellate come un semiautomato monitor parziale che osserva l'automa del concetto composto. Le reazioni si attivano in base a trigger (when), condizioni di stato (where) ed effetti (then).
• Composizione: l'applicazione è una composizione sincrona degli automi dei concetti e del monitor della reazione.
• Obiettivo di Verifica: la sicurezza viene verificata controllando che l'applicazione sia "stabile" (senza obblighi pendenti) esattamente quando l'invariante di sicurezza è soddisfatto. Questo è codificato in Alloy 6 e controllato tramite model checking limitato.

2. Ciclo di Sintesi Guidato da LLM

Il processo di sintesi opera come segue:

1. Proposta: un LLM propone reazioni candidate (o revisiona quelle esistenti) per soddisfare un dato invariante.
2. Traduzione: un secondo agente traduce le descrizioni dei concetti, le reazioni e gli invarianti (attualmente scritti in linguaggio naturale) in Alloy 6.
3. Verifica: il model checker di Alloy verifica il design candidato rispetto all'invariante e a qualsiasi scenario fornito.
4. Feedback: se la verifica fallisce, il controesempio (una traccia che viola l'invariante o lo scenario) viene fornito all'LLM per raffinare il design.

3. Meccanismi di Guida (Steering)

Per affrontare la natura "sotto-vincolata" della sintesi basata solo su invarianti, il documento propone due meccanismi di guida:

• Prompt in Linguaggio Naturale: fornire descrizioni testuali del comportamento desiderato insieme all'invariante.
• Sintesi Guidata da Scenari: fornire scenari positivi (consentiti) e negativi (proibiti). A differenza dei prompt, gli scenari hanno una semantica formale e possono essere controllati automaticamente contro i design candidati.
• Elicitazione di Scenari: una procedura guidata da LLM in cui il modello propone brevi prefissi di azione che violano l'invariante, e l'utente li classifica come desiderabili o indesiderabili. Il modello propone quindi riparazioni (suffissi) per i prefissi desiderabili. Ciò sposta il compito dell'utente dalla redazione di scenari alla loro classificazione.

Contributi Chiave

1. Semantica Formale: una semantica basata su automi per i concetti e le reazioni del Concept Design, che consente la verifica limitata di invarianti e scenari.
2. Ciclo di Sintesi Verificato: una procedura di sintesi guidata da LLM in stile CEGIS per generare design di reazione, integrata con un meccanismo guidato da scenari per orientare la sintesi verso i design intesi.
3. Elicitazione di Scenari: una tecnica guidata da LLM per supportare la fase iniziale di esplorazione del design, permettendo agli utenti di classificare gli scenari che violano l'invariante proposti, anziché redigerli da zero.
4. Valutazione Empirica: una valutazione completa su tre applicazioni (Dead-Letter Queue con dati sensibili, Sistema di Gestione Corsi, Link di Evidenza Univoci) e dodici varianti di design utilizzando l'LLM GPT-5.5.

Risultati

La valutazione, condotta su un benchmark di 12 varianti di design, ha prodotto i seguenti risultati:

• Sintesi basata solo sull'Invariante:

  • Gli LLM raggiungono spesso un design verificato rapidamente (spesso al primo tentativo).
  • Tuttavia, i design sono raramente stabili tra un'esecuzione e l'altra.
  • La sintesi basata solo sull'invariante produce frequentemente design implausibili (ad esempio, proibendo azioni valide o declassando dati) perché gli invarianti da soli sottovincolano il design.

• Guida tramite Scenario vs. Prompt:

  • La sintesi guidata da scenari ha recuperato i design intesi in modo più consistente rispetto al prompting in linguaggio naturale (10/12 varianti rispetto a 8/12 con input iniziali).
  • Gli scenari sono più facili da revisionare meccanicamente (puramente additivi) rispetto ai prompt, che possono essere fragili e ambigui.
  • Overfitting: l'uso di set minimi di scenari può portare all'overfitting, in cui il modello non riesce a generalizzare (ad esempio, gestendo solo cardinalità specifiche di messaggi). L'aggiunta di scenari con diverse cardinalità ha mitigato questo problema.

• Elicitazione di Scenari:

  • L'elicitazione di 20 scenari ha recuperato il design inteso in 9/12 varianti, rispetto a 5/12 con 10 scenari.
  • Non-determinismo: la proposta di scenari da parte dell'LLM è non deterministica; esecuzioni diverse elicitano set di scenari differenti, portando a risultati non monotoni (più scenari non garantiscono sempre una copertura migliore).
  • Comportamenti Mancanti: se il processo di elicitazione manca uno scenario critico (ad esempio, un percorso di iscrizione specifico), la sintesi può convergere verso un design che proibisce quel comportamento, che non era l'intento.

• Modalità di Fallimento:

  • Le modalità di fallimento primarie sono state la mancanza di scenari critici (mancanza di copertura) e l'overfitting (fallimento nella generalizzazione).
  • I problemi di qualità hanno incluso reazioni e condizioni ridondanti, sebbene ciò non abbia influito sulla correttezza rispetto all'invariante.

Significato e Rivendicazioni

Il documento sostiene che la verifica formale è essenziale quando si utilizzano gli LLM per la sintesi di design di alto livello. Sebbene gli LLM possano spesso generare design che soddisfano semplici invarianti, non possono essere considerati affidabili per produrre il design inteso senza ulteriori guide.

Il significato del lavoro risiede nel dimostrare che gli scenari fungono da artefatti di guida efficaci e verificabili. Essi colmano il divario tra i requisiti di sicurezza formali (invarianti) e l'intento informale dell'utente. Il documento argomenta che mentre gli invarianti garantiscono la sicurezza, gli scenari garantiscono plausibilità e allineamento con l'intento.

Gli autori rimangono modesti riguardo allo stato attuale del prototipo:

• La traduzione dal linguaggio naturale ad Alloy dipende da un LLM, introducendo una potenziale fonte di errore (sebbene l'ispezione manuale non abbia riscontrato problemi nei design verificati finali).
• La verifica è limitata; l'assenza di controesempi non garantisce la correttezza illimitata.
• La valutazione è limitata a una singola configurazione di LLM (GPT-5.5) e a un set specifico di benchmark, sebbene un controllo incrociato con Claude Fable 5 abbia mostrato un successo simile, suggerendo che l'approccio non è specifico per un modello.
• È necessario un lavoro futuro per sostituire la traduzione basata su LLM con un linguaggio sorgente formale, scalare la verifica ad applicazioni più grandi e migliorare l'elicitazione degli scenari per gestire meglio il non-determinismo e le lacune di copertura.