ИССЛЕДОВАНИЕ · RESEARCH · #606
MAGS: мультиагентная автоформализация обеспечивает формальные гарантии безопасности для агентных программ
В статье представлен MAGS — мультиагентная система, которая автоформализует программы, сгенерированные LLM, переводит их в Dafny, исправляет ошибки по отклику верификатора и компилирует проверенный код обратно в исполняемые файлы. На 100 CUDA-ядрах, 100 терминальных скриптах и 20 задачах для манипулятора (всего 220 примеров) MAGS создал программы с машинно-проверяемыми гарантиями безопасности относительно зафиксированных спецификаций, при этом отмечены сбои, когда автоформализованная семантика не полностью отражала целевое поведение.
КЛЮЧЕВЫЕ ТЕЗИСЫ
- В статье представлен MAGS — мультиагентная система, которая автоформализует программы, сгенерированные LLM, переводит их в Dafny, исправляет ошибки по отклику верификатора и компилирует проверенный код обратно в исполняемые файлы.
- На 100 CUDA-ядрах, 100 терминальных скриптах и 20 задачах для манипулятора (всего 220 примеров) MAGS создал программы с машинно-проверяемыми гарантиями безопасности относительно зафиксированных спецификаций, при этом отмечены сбои, когда автоформализованная семантика не полностью отражала целевое поведение.
- Это демонстрирует практический частично автоматизированный путь к машинно-проверяемым гарантиям безопасности для кода от LLM-агентов, снижая потребность в ручной разработке доказательств и повышая надёжность результатов агентов.
ПОЧЕМУ ЭТО ВАЖНО
Это демонстрирует практический частично автоматизированный путь к машинно-проверяемым гарантиям безопасности для кода от LLM-агентов, снижая потребность в ручной разработке доказательств и повышая надёжность результатов агентов.