A matemática ‘pé no saco’ que poderia salvar a codificação do Vibe de si mesma
No início deste ano, a equipe de segurança da Apple disse que alguns dos problemas de verificação formal descobertos em sua biblioteca “corecrypto”, usada para criptografia, não poderiam ter sido encontrados de outra forma. Mas a empresa acrescentou que precisa ser “conservadora” ao adicionar novo código ao corecrypto para garantir que possa acompanhar a revisão.
Dois executivos de segurança cibernética de grandes empresas que não verificaram formalmente nenhum código dizem que não têm certeza se a automação valerá a pena. Mas os executivos, que não estavam autorizados a falar publicamente, dizem que poderiam imaginar pagar grandes laboratórios de IA por código “verificado” gerado por IA.
Os desenvolvedores de projetos de software de código aberto, que são a base de muitos aplicativos, estão cada vez mais experimentando a verificação auxiliada por IA. A organização sem fins lucrativos Beneficial AI Foundation usou uma doação da Anthropic para validar o mesmo código de criptografia este ano que a Sun fez em Stanford. Michael Rosenberg, mantenedor da biblioteca conhecida como curve25519-dalek, espera que surja financiamento sustentável para esforços contínuos de verificação. “No entanto, não tenho ideia de como isso vai acontecer e certamente não deveríamos confiar na boa vontade das empresas de IA”, diz ele.
Algumas das startups ansiosas por expandir a verificação também não têm certeza se devem implantar suas ferramentas diretamente aos clientes ou por meio de intermediários como a Anthropic. Seu plano geral é usar IA para automatizar grande parte do trabalho envolvido na definição de como um programa deve se comportar. Por exemplo, as especificações de uma tabela de dados podem exigir que ela contenha os mesmos itens antes e depois da classificação, apenas em uma ordem diferente. Esforços adicionais de automação, que podem não envolver IA, traduziriam esse código em um formato que ferramentas matemáticas como Lean, Rocq e Isabelle possam usar para verificar se o código funciona conforme o esperado.
Outro participante recente no campo da verificação formal é Madan Musuvathi, que deixou a Microsoft Research após mais de 20 anos para fundar a startup Truidic. Após incidentes como o hack OpenAI do Hugging Face, ele sentiu que havia uma necessidade urgente de comercializar seus estudos. “A IA nas mãos dos invasores pode ser extremamente poderosa”, diz Musuvathi, mas a verificação pode “tornar a IA segura e protegida para todos, em qualquer lugar”.
A Proofcraft, uma das poucas empresas que oferece há muito tempo a verificação tradicional, diz que o crescente entusiasmo com o processo está se traduzindo em uma enxurrada de consultas de clientes em potencial. June Andronick, CEO da empresa, e Gerwin Klein, seu cientista-chefe, dizem que o interesse supera facilmente o que eles e a concorrência podem oferecer.
Mas ambos temem que as especificações geradas pela IA possam inspirar “confiança injustificada” nos resultados. Os verificadores também estão ansiosos para preservar a alegria que seu trabalho lhes traz. Klein chama isso de “muito viciante, como um jogo de quebra-cabeça”. Se tudo correr bem, ele estará resolvendo mais do que nunca.
