MAGS: framework multiagente usa Dafny para dar garantias formais de segurança a código gerado por IA
Pesquisadores propõem o MAGS, um framework multiagente que traduz código gerado por agentes de IA para Dafny, uma linguagem com verificação formal, a fim de provar matematicamente que certas propriedades de segurança são respeitadas. O sistema atingiu 100% de sucesso na verificação formal contra especificações congeladas em 220 casos testados, mas avaliações independentes revelaram que a garantia formal nem sempre corresponde a segurança ou funcionalidade real quando a formalização não captura todo o comportamento relevante.
Pesquisadores apresentaram o MAGS (Multi-agent Auto-formalization Guarantees Safety), um framework que combina múltiplos agentes de IA com verificação formal para reduzir os riscos de segurança de código gerado por agentes de codificação em larga escala. A motivação central é que agentes de IA hoje produzem programas complexos em volume que torna a revisão humana completa inviável, e técnicas tradicionais de checagem, como fuzzing, análise estática e uso de LLMs como verificadores, detectam falhas mas não cobrem todos os casos de borda possíveis.
Tecnicamente, o MAGS usa Dafny, uma linguagem com suporte nativo a verificação formal, como representação intermediária entre o código gerado e a garantia de segurança: obrigações de prova em Dafny são traduzidas e checadas por um solver SMT. O processo começa com o congelamento de APIs e requisitos de segurança auditados por humanos; em seguida, um agente traduz o código gerado para Dafny preservando o comportamento original, repara violações detectadas pelo verificador de forma iterativa, sem poder alterar as especificações já congeladas, e por fim recompila o programa verificado de volta para a linguagem-alvo. Na avaliação, com 100 kernels CUDA, 100 scripts de terminal e 20 tarefas de braço robótico, o framework atingiu 100% de sucesso em produzir programas com verificação formal contra as especificações congeladas.
Esse resultado importa como um lembrete de que verificação formal não é uma bala de prata: em testes de segurança e funcionalidade independentes, fora do laço de verificação, o desempenho caiu de forma desigual entre domínios — os kernels CUDA mantiveram alta aprovação em checagens externas, mas os scripts de terminal passaram em apenas 82% de um benchmark de segurança independente, e apenas 11 das 20 políticas robóticas preservaram a funcionalidade pretendida em testes posteriores. Os próprios autores atribuem essas falhas a casos em que a semântica auto-formalizada não capturou integralmente o comportamento-alvo, por exemplo especificações que não cobriam certas classes de vulnerabilidade ou que eram genéricas o suficiente para permitir soluções trivialmente seguras mas funcionalmente inúteis. Ou seja, a garantia matemática vale exatamente para o que foi formalizado, e erros de formalização, não de execução, continuam sendo o elo fraco da cadeia de segurança.