Ferramenta de IA de Stanford verificou parte do código do Signal em meio dia e com US$ 500, em vez de 5 meses

A verificação formal, isto é, a prova matemática de que um programa faz exatamente o que se espera dele, ficou por décadas restrita a entusiastas e aos sistemas mais críticos. Agora a IA generativa tenta transformá-la em uma ferramenta comum. A pesquisadora de Stanford Chuyue Sun e colegas mostraram em um artigo recente que a ferramenta de IA deles concluiu um projeto de engenharia em menos de meio dia e por menos de US$ 500. Três especialistas altamente qualificados levaram cinco meses para fazer o mesmo trabalho. O projeto envolvia parte do código que criptografa as conversas no mensageiro Signal.

Por que a matemática de repente ficou mais barata

A verificação clássica é difícil por dois motivos. Os engenheiros precisam registrar com exatidão o que esperam do programa e, depois, traduzir o código em fórmulas que possam ser verificadas. As empresas já rodam testes complexos de qualquer forma, mas raramente investem em verificação formal, embora ela pegue falhas mais exóticas.

As novas startups apostam na automação da primeira etapa. A IA deve escrever as especificações: para ordenar uma tabela, por exemplo, elas exigem que o conjunto de elementos antes e depois seja o mesmo, mudando apenas a ordem. A tradução posterior do código para o formato dos sistemas de prova Lean, Rocq e Isabelle pode dispensar a IA.

Sun passou em agosto para a &Truth, que foi lançada publicamente na quinta-feira. A startup levantou US$ 70 milhões e quer, com o tempo, verificar código em qualquer linguagem. O diretor científico da &Truth, Ilya Sergey, compara a ideia à construção civil: pontes e prédios não caem porque são calculados de antemão, e as tecnologias para esse tipo de raciocínio em código já existiam, mas escalavam mal.

Quem mais atua nesse mercado

A concorrente Harmonic, cofundada por Vlad Tenev, CEO da Robinhood, levantou US$ 295 milhões. Nesta semana, a empresa anunciou que seu agente de IA para matemática, o Aristotle, consegue verificar software em C e descrições de hardware em Verilog. A tecnologia está sendo avaliada por potenciais clientes, entre eles a fabricante de chips Tensordyne e a Nvidia, cujo fundo de venture capital é um dos investidores da Harmonic.

Uma semana antes, a Anthropic e a startup Theorem disseram ter usado IA para encontrar, em software de código aberto, erros que passaram despercebidos por trilhões de testes. Elas também lançaram uma extensão para o Claude que ajuda desenvolvedores com verificação. O custo do primeiro projeto não foi divulgado. Madan Musuvathi, que deixou a Microsoft Research após mais de 20 anos, fundou a Truidic: segundo ele, a IA é muito poderosa nas mãos de atacantes, e a verificação pode tornar sistemas de IA seguros.

A Beneficial AI Foundation, com uma bolsa da Anthropic, verificou neste ano o mesmo código criptográfico que Sun. Michael Rosenberg, mantenedor da biblioteca curve25519-dalek, espera por um financiamento sustentável, mas não sabe de onde virá, e considera errado depender da boa vontade das empresas de IA.

Onde estão o ceticismo e as limitações

A verificação já está em aviões da Boeing, em servidores da Amazon e em mais de 2,5 bilhões de dispositivos ativos da Apple, mas em geral se trata de código ligado à segurança. Byron Cook, da AWS, diz que o método eliminou parte das preocupações dos clientes de nuvem e acelerou equipes internas. Em contrapartida, várias empresas de médio porte contaram à WIRED que verificaram, no máximo, uma função-chave.

Os motivos: falta de especialistas, custo superior aos riscos possíveis e receio de que semanas de espera atrasem o lançamento do produto. Dois responsáveis por cibersegurança em grandes empresas, que nunca verificaram código formalmente, não têm certeza de que a automação mudará essa conta, mas estão dispostos a pagar aos grandes laboratórios de IA por código gerado "verificado".

A tecnologia ainda está na fase de protótipos. Não está claro quanto os clientes aceitam pagar nem como querem adotá-la: diretamente ou por intermediários como a Anthropic. O método se apoia em premissas sobre como computadores e pessoas interagem com o software, e por isso parte dos especialistas duvida que ele detecte erros de usuários e falhas de hardware.

Will Wilson, chefe da startup Antithesis, que busca bugs com IA, chama a verificação formal de "armadilha" para matemáticos como ele. A empresa gastou milhões de dólares para verificar parte de sua proteção, descreveu o processo como doloroso e, ainda assim, encontrou erros adicionais com a própria ferramenta. A Antithesis também encontrou bugs em software de clientes que já havia sido verificado. Segundo ele, a verificação formal dá alguma confiança, mas só o teste exaustivo pode confirmá-la. Vitalik Buterin também escreveu em seu blog que ela não é uma panaceia.

Outra ressalva diz respeito às próprias especificações. Os fundadores da Proofcraft, June Andronick e Gerwin Klein, dizem que o interesse supera a capacidade deles e dos concorrentes, mas temem a "confiança injustificada" em resultados com especificações geradas por IA. Para as equipes, a conclusão prática é esta: a IA torna a verificação barata o bastante para ser testada em módulos críticos, como criptografia, mas não promete substituir os testes.