🤖 AI

Neurosymbolic Auditing of Natural-Language Software Requirements

Questo articolo introduce VERIMED, una pipeline neurosimbolica che sfrutta modelli linguistici di grandi dimensioni e solver SMT per verificare i requisiti software in linguaggio naturale rilevando l'ambiguità attraverso variazioni stocastiche di formalizzazione e verificando coerenza e sicurezza mediante riparazione guidata da controesempi, ottenendo un significativo aumento dell'accuratezza nei requisiti di sicurezza per dispositivi medici.

Autori originali: Bethel Hall, William Eiers

Pubblicato 2026-05-14

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Bethel Hall, William Eiers

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di essere l'architetto di una macchina salvavita, come un dispositivo per dialisi che pulisce il sangue dei pazienti. Scrivi le regole su come questa macchina dovrebbe comportarsi in inglese semplice: "Se il flusso sanguigno si interrompe, suona l'allarme".

Il problema è che il linguaggio umano è disordinato. Le parole possono essere vaghe, le frasi possono contraddirsi a vicenda, oppure una regola potrebbe essere impossibile da seguire senza che nessuno se ne accorga. Se un programma informatico tenta di costruire questa macchina basandosi sui tuoi appunti disordinati, potrebbe realizzare qualcosa che sembra perfetto sulla carta ma è in realtà pericoloso nella vita reale.

Questo articolo presenta VERIMED, un nuovo sistema "neurosimbolico" (un termine sofisticato per indicare una collaborazione tra un'IA creativa e un robot logico rigido) progettato per agire come un super-revisore di queste regole di sicurezza.

Ecco come funziona VERIMED, spiegato attraverso analogie di tutti i giorni:

1. Il Traduttore e il Robot Logico

Immagina il sistema come avente due parti:

Il Traduttore (L'LLM): Questa è un'IA creativa che legge le tue regole in inglese e tenta di tradurle in un linguaggio matematico rigoroso (SMT) che un computer può verificare.
Il Robot Logico (Il Risolutore SMT): Questa è una macchina rigida e inflessibile che verifica la matematica. Non le importano i "sentimenti" o le "intenzioni"; le importa solo se le regole hanno senso logico.

2. Il "Test di Stress" per le Regole

Prima che la macchina venga costruita, VERIMED esegue quattro test specifici sulle regole tradotte per individuare difetti nascosti:

Il Test "Può Succedere?" (Vacuità): Immagina una regola che dice: "Se la macchina è sott'acqua, spegni l'alimentazione". Se la macchina non dovrebbe mai essere sott'acqua, questa regola è inutile. Il Robot Logico verifica: "È effettivamente possibile che la macchina si trovi sott'acqua?". Se la risposta è "No", il robot segnala la regola come un fantasma: esiste ma non fa nulla.
Il Test "Può Rompersi?" (Violabilità): Il robot tenta di infrangere le regole. Si chiede: "Posso far fare alla macchina qualcosa di non sicuro rispettando comunque le regole?". Se trova un modo per compromettere la sicurezza, ti mostra esattamente come (un "controesempio"), come una prova che dice: "Vedi? Se imposti il quadrante a 50, l'allarme non suona, anche se hai detto che dovrebbe".
Il Test "Doppia Contabilità" (Ridondanza): A volte, scrivi due regole che dicono esattamente la stessa cosa. Una potrebbe essere: "Non far superare la pressione a 200", e un'altra dice: "Non far superare la pressione a 200". Il robot trova questi duplicati e dice: "Ti stai ripetendo. Vuoi averli entrambi o uno di essi è sbagliato?".
Il Test "Armonia Globale" (Coerenza): Il robot verifica se tutte le regole si combattono a vicenda. Se la Regola A dice "Accendi la pompa" e la Regola B dice "La pompa deve essere spenta", e entrambe dovrebbero accadere allo stesso tempo, il robot grida: "Questo è impossibile!".

3. Il "Rilevatore di Ambiguità" (Il Trucco Magico)

Questa è l'idea più creativa dell'articolo. A volte, una frase è così vaga che può essere interpretata in due modi diversi.

L'Analogia: Immagina di dire a uno chef: "Cuoci la bistecca finché è cotta". Lo chef potrebbe pensare che "cotta" significhi al sangue, mentre tu intendevi ben cotta.
Come VERIMED lo individua: Invece di chiedere all'IA di tradurre la regola una sola volta, le chiede di tradurre la stessa regola cinque volte diverse, come chiedere a cinque chef diversi di interpretare "cotta".
- Se tutti e cinque gli chef scrivono la ricetta esatta, la regola è chiara.
- Se uno chef scrive "al sangue" e un altro "ben cotta", il sistema individua il disaccordo. Quindi dice all'umano: "Ehi, la tua regola è ambigua! Ecco due modi diversi in cui la tua frase potrebbe essere letta. Per favore chiarisci".

4. Il "Laboratorio di Riparazione"

Quando il Robot Logico trova un errore o un'ambiguità, non dice solo "Errore". Agisce come un meccanico utile:

Per la logica rotta: Mostra all'IA lo scenario esatto in cui la regola ha fallito (il controesempio). L'IA riscrive quindi la regola per colmare quella specifica falla.
Per il linguaggio vago: Mostra all'umano il punto specifico di confusione (ad esempio: "I 200 gradi sono inclusi o esclusi?"). L'umano chiarisce e il sistema ritraduce finché tutti non sono d'accordo.

Cosa Hanno Scoperto?

I ricercatori hanno testato questo sistema su un insieme di 64 regole di sicurezza per una macchina per dialisi.

I Risultati: Il sistema ha rilevato che 2 regole erano ridondanti (duplicati) e 12 regole erano ambigue (potevano essere lette in modi multipli).
La Correzione: Quando hanno utilizzato il feedback del "controesempio" (mostrando all'IA esattamente come aveva fallito), la capacità dell'IA di rispondere a domande sulla sicurezza è passata da circa il 55% di accuratezza a quasi il 99%.
La Correzione dell'Ambiguità: Dopo che il sistema ha segnalato le regole vaghe e gli umani le hanno chiarite, l'IA ha smesso di produrre traduzioni conflittuali. L'"ambiguità" è scesa a zero.

La Conclusione

VERIMED è una rete di sicurezza. Utilizza un'IA creativa per tradurre le regole umane in matematica e un robot logico rigido per verificare se quelle regole matematiche sono coerenti, non ambigue e effettivamente sicure. Non controlla solo se il codice funziona; controlla se le istruzioni per il codice hanno senso prima che la macchina venga mai costruita.

Nota Importante: L'articolo afferma esplicitamente che questo è stato testato sui requisiti di dispositivi medici (macchine per dialisi) e su una pompa per la gestione del dolore. Gli autori avvertono che questo sistema è uno strumento per esperti che revisionano i requisiti, non una sostituzione per esperti umani, e non dovrebbe essere utilizzato nella vita reale senza una revisione umana indipendente.

Riepilogo Tecnico: Audit Neurosimbolico dei Requisiti Software in Linguaggio Naturale

Enunciato del Problema

I requisiti software in linguaggio naturale, in particolare in domini critici per la sicurezza come i dispositivi medici, soffrono frequentemente di ambiguità, incoerenza e sottospecificazione. Questi difetti sono pericolosi perché si propagano nei modelli formali e nelle implementazioni, potenzialmente portando alla verifica di specifiche errate o al dispiegamento di comportamenti non sicuri. Sebbene i Modelli Linguistici di Grande Dimensione (LLM) abbiano fatto avanzare il campo della autoformalizzazione (traduzione del linguaggio naturale in specifiche verificabili automaticamente), la sola validità sintattica è insufficiente. Una specifica formale ben formata può comunque essere globalmente incoerente, contenere condizioni di attivazione irraggiungibili (vacuità) o ammettere molteplici interpretazioni plausibili del testo sorgente. In assenza di una formalizzazione di verità fondamentale (ground-truth), non esiste un oracolo per rilevare questi fallimenti semantici, poiché gli LLM tendono spesso a optare per la lettura statisticamente più comune o a omettere vincoli impliciti.

Metodologia: Il Framework VERIMED

Gli autori propongono VERIMED, una pipeline neurosimbolica progettata per auditare i requisiti in linguaggio naturale traducendoli in un modello SMT (Satisfiability Modulo Theories) unificato e sfruttando query del risolutore per rilevare difetti. Il framework opera su uno schema fisso di variabili di stato tipizzate (stati di controllo booleani e parametri a valore reale) e vincoli di dominio.

La pipeline consta di quattro fasi:

Risolvitore di Ambiguità: Prima della formalizzazione, ogni requisito viene sottoposto a screening per la stabilità. Il sistema campiona $N$ formalizzazioni indipendenti dall'LLM a temperatura elevata. Eseguendo controlli di equivalenza SMT bidirezionali tra coppie di codifiche, se le codifiche non sono equivalenti, il requisito viene segnalato come sensibile all'ambiguità. Il risolutore genera "testimoni" concreti (stati specifici in cui le codifiche non concordano), che vengono reimmessi nell'LLM per riscrivere il requisito fino a quando tutti i campioni convergono verso una singola codifica.
Autoformalizzatore: I requisiti disambiguati vengono tradotti in un'unica specifica SMT-LIB. Il sistema impiega un ciclo di riparazione sintattica vincolato in cui i messaggi di errore del risolutore guidano l'LLM a rigenerare codice malformato fino alla produzione di un modello valido.
Verificatore di Proprietà: Questo modulo esegue quattro query di audit specifiche sul modello assemblato $M$ $M$ :
- Coerenza Globale: Verifica se $M$ è soddisfacibile. Se insoddisfacibile, un nucleo insoddisfacibile (unsat core) identifica i requisiti conflittuali.
- Vacuità: Per i requisiti condizionali, verifica se la condizione di attivazione possa mai essere soddisfatta nell'ambito dei vincoli di dominio.
- Violabilità: Verifica se un requisito possa essere violato all'interno del dominio, restituendo un'assegnazione di violazione concreta se possibile.
- Ridondanza: Verifica se un requisito sia già imposto dal resto della specifica.
Verificatore di Query: Questa fase verifica domande di sicurezza basate su scenari. Verifica se una risposta proposta sia implicata dal modello ( $M \land s \land \neg a$ è insoddisfacibile). Se viene trovata una violazione, il risolutore restituisce un controesempio. Tale controesempio, insieme ai requisiti violati, funge da feedback per un ciclo di riparazione volto a correggere la risposta dell'LLM.

Contributi Chiave

Il paper introduce i seguenti contributi:

Un Framework Neurosimbolico: VERIMED opera la traduzione dei requisiti in linguaggio naturale in un unico modello SMT, utilizzando gli output del risolutore come segnale primario per la revisione a valle.
Audit SMT a Livello di Requisito: Gli autori formulano quattro audit (coerenza, vacuità, violabilità, ridondanza) che operazionalizzano criteri di qualità consolidati.
Rilevamento dell'Ambiguità tramite Stocasticità: Il paper introduce un metodo per rilevare l'ambiguità sfruttando la natura stocastica degli LLM. Campionando multiple formalizzazioni e verificando l'iniquivalenza SMT bidirezionale, il sistema segnala i requisiti che ammettono molteplici letture plausibili. I testimoni generati dal risolutore guidano quindi la chiarificazione in linguaggio naturale.
Riparazione Guidata da Controesempi (CEGR): Lo studio dimostra che la granularità del feedback simbolico influisce significativamente sull'efficacia della riparazione.

Risultati Sperimentali

Il framework è stato valutato su un corpus di 64 requisiti di sicurezza in linguaggio naturale tratti da una specifica per una macchina per emodialisi, con una valutazione secondaria su una specifica per una pompa PCA.

Autoformalizzazione e Audit: Il sistema ha generato con successo un modello SMT verificabile dal risolutore per tutti i 64 requisiti. Il modello era globalmente coerente e non conteneva requisiti vacui. L'audit ha segnalato 2 requisiti (3,1%) come ridondanti. L'equivalenza semantica di andata e ritorno (traduzione da SMT a testo e riformalizzazione) è stata raggiunta per il 100% dei requisiti, con una media di similarità coseno del 96,2% tra i testi originali e quelli ricostruiti.
Rilevamento di Mutazioni: La pipeline ha rilevato il 97,3% delle 256 requisiti mutati (rappresentanti difetti come soppressione di falsi allarmi e violazioni di limiti) in quattro categorie di difetti.
Riparazione Guidata da Controesempi: In un'attività di risposta a domande, l'uso di controesempi SMT concreti come feedback (CEGR) ha aumentato l'accuratezza verificata da una linea di base del 55,4% (nessun feedback) al 98,5%. Fornire solo i requisiti violati (senza il controesempio concreto) ha prodotto un'accuratezza dell'80,0%, dimostrando che lo stato del testimone concreto è il motore critico per la riparazione.
Risoluzione dell'Ambiguità: Il risolutore di ambiguità ha segnalato 12 dei 64 requisiti (18,8%) come produttori di multiple codifiche distinte. Dopo la chiarificazione guidata da SMT, tutti i requisiti segnalati hanno convergito verso una singola codifica (100% di accordo pairwise), riducendo la media delle codifiche distinte per requisito da 1,59 a 1,00.

Significato e Affermazioni

Il paper afferma che VERIMED opera con successo l'audit dei requisiti software tramite query basate su SMT, affrontando la natura "invisibile" dei difetti semantici nell'autoformalizzazione. Gli autori sottolineano che:

La variazione stocastica è un segnale: Il disaccordo tra formalizzazioni indipendenti è un indicatore affidabile di ambiguità nel testo sorgente.
La granularità conta: L'utilità del feedback simbolico dipende fortemente dalla sua specificità; i controesempi concreti sono significativamente più efficaci per la riparazione rispetto a elenchi astratti di requisiti.
La coerenza è insufficiente: La coerenza interna di un modello formale non garantisce l'assenza di difetti; la preservazione comportamentale e il rilevamento dell'ambiguità sono complementi necessari.

Gli autori mantengono un ambito modesto, notando che i loro risultati sono specifici per dispositivi medici legati alla somministrazione di infusioni e che l'approccio si basa su segnali proxy (coerenza, sensibilità alle mutazioni, ecc.) piuttosto che su una misura diretta della fedeltà all'intento. Affermano esplicitamente che i risultati non devono essere utilizzati in applicazioni critiche per la sicurezza senza una revisione indipendente da parte di esperti e che l'implementazione corrente non supporta la logica temporale completa, approssimando i requisiti temporali tramite condizioni di stato corrente.