The Pulse
MAGS verifica il codice scritto dagli agenti, poi ne espone i limiti
Il framework MAGS traduce i programmi generati dagli agenti in Dafny e li verifica rispetto a specifiche bloccate, mentre i suoi autori avvertono che una semantica formalizzata automaticamente ma incompleta potrebbe non riuscire a cogliere
AI.info Team ·
Un nuovo sistema mira a fornire garanzie formali di sicurezza per i programmi generati dagli agenti, traducendoli in Dafny, verificandoli rispetto a specifiche bloccate, correggendo le violazioni e ricompilando in codice eseguibile i programmi verificati.
MAGS, descritto in un articolo inviato ad arXiv il 16 settembre, valuta l’approccio su 220 esempi: 100 kernel CUDA, 100 script per terminale e 20 attività con bracci robotici. Secondo l’abstract, il sistema ha raggiunto un tasso di successo del 100% nella produzione di programmi con garanzie di sicurezza non banali rispetto a specifiche bloccate.
«Su tutti i 220 esempi, raggiunge un tasso di successo del 100% nella produzione di programmi con garanzie di sicurezza non banali rispetto a specifiche bloccate.»
L’articolo presenta Dafny come una rappresentazione intermedia progettata per la verifica. Le proprietà di sicurezza vengono codificate in questo linguaggio, così da poter essere verificate meccanicamente prima che i programmi risultanti siano ricompilati nella loro forma eseguibile.
Il benchmark copre tre diverse categorie di software generato. I kernel CUDA rappresentano programmi paralleli per GPU. Gli script per terminale mettono alla prova una categoria distinta di programmi eseguibili, mentre il benchmark di robotica comprende attività con bracci robotici. Nell’abstract, l’articolo descrive il framework come un sistema multi-agente unificato, progettato per generare programmi eseguibili con garanzie formali di sicurezza.
Le garanzie dipendono dalle specifiche
MAGS non sostiene che un certificato dimostri la sicurezza in ogni possibile situazione reale. Le sue garanzie si applicano alle proprietà rappresentate nelle specifiche bloccate usate nella procedura di verifica.
Questa distinzione è centrale nella valutazione dell’articolo. Oltre ai risultati della verifica formale, gli autori riportano valutazioni indipendenti della sicurezza e del funzionamento in tutti e tre gli ambiti. Queste valutazioni rivelano dei malfunzionamenti quando la semantica formalizzata automaticamente non coglie pienamente il comportamento dei programmi di destinazione.
Il risultato definisce chiaramente i limiti di ciò che il sistema dimostra. Un programma può soddisfare il modello formale e tuttavia non superare una valutazione esterna, se il modello omette un comportamento o una proprietà di sicurezza rilevante. La verifica formale dipende quindi non solo dal fatto che una dimostrazione abbia esito positivo, ma anche dalla capacità delle specifiche di rappresentare accuratamente i rischi e i requisiti del programma esaminato.
Una procedura, non una garanzia di sicurezza assoluta
MAGS affronta un problema pratico del software scritto dagli agenti: gli agenti di programmazione possono generare programmi complessi più rapidamente di quanto le persone riescano a esaminare ogni possibile caso limite. Approcci esistenti come i test fuzz, l’analisi statica e la verifica basata su modelli linguistici possono individuare molti malfunzionamenti, ma secondo l’articolo potrebbero non coprire tutti i casi possibili.
L’approccio consiste nell’inserire il codice generato in una procedura verificabile automaticamente. Le API sottoposte a verifica umana e i requisiti di sicurezza vengono formalizzati e bloccati, il codice generato viene tradotto in Dafny e i riscontri del verificatore vengono usati per correggere le violazioni. Il sistema ricompila quindi in codice eseguibile i programmi che soddisfano i requisiti specificati.
Il risultato ottenuto sui 220 esempi mostra che un’unica procedura può produrre programmi con garanzie formali di sicurezza in diversi modelli di esecuzione. Non dimostra che i programmi generati siano sicuri indipendentemente da come viene modellato il loro comportamento. Le valutazioni indipendenti dell’articolo sottolineano invece il rischio che la semantica formalizzata automaticamente ometta comportamenti importanti nell’ambiente di destinazione.
MAGS formula quindi un’affermazione più circoscritta rispetto a una garanzia generale della sicurezza del codice scritto dagli agenti. Dimostra un metodo per verificare i programmi generati rispetto a specifiche esplicite e bloccate. La sua affidabilità resta legata alla completezza e all’accuratezza di tali specifiche.