Naukowcy opracowali MAGS, ujednoliconą platformę wieloagentową, która generuje wykonywalne programy z formalnie zweryfikowanymi gwarancjami bezpieczeństwa. Problem, który rozwiązuje, jest istotny: agenty AI oparte na dużych modelach językowych tworzą teraz tak złożone programy na taką skalę, że dokładny przegląd przez człowieka staje się praktycznie niemożliwy. Tradycyjne podejścia - fuzzy testing, analiza statyczna, czy weryfikacja za pomocą samych modeli AI - potrafiące wychwycić wiele błędów, nie są w stanie pokryć wszystkich przypadków brzegowych.
Rozwiązanie opiera się na formalnej weryfikacji, która dostarcza gwarancji sprawdzalnych maszynowo dla określonych właściwości. MAGS wykorzystuje język Dafny jako pośrednią reprezentację uwzględniającą weryfikację, gdzie właściwości bezpieczeństwa mogą być mechanicznie sprawdzane. System formaliza i zamraża audytowane przez ludzi API oraz wymagania bezpieczeństwa, tłumaczy wygenerowany kod na Dafny, naprawia naruszenia korzystając ze sprzężenia zwrotnego z weryfikatora i kompiluje zweryfikowane programy z powrotem na kod wykonywalny.
Wyniki testów na 220 programach - 100 jądrach CUDA, 100 skryptach terminalowych i 20 zadaniach robotyki - pokazują doskonałą wydajność. MAGS osiągnął 100% wskaźnik sukcesu w tworzeniu programów z nietrywialnych gwarancji bezpieczeństwa wobec zamrożonych specyfikacji. Niezależne ewaluacje bezpieczeństwa i funkcjonalności wykazały silne wyniki we wszystkich trzech domenach, choć ujawniły też nieudane przypadki gdy automatycznie sformalizowana semantyka nie w pełni oddawała docelowe zachowanie.