IA verifica com matemática parte do código do Signal em meio dia e US$ 500, em vez de 5 meses

Chuyue Sun, pesquisadora de Stanford, e colegas criaram uma ferramenta de IA que concluiu um projeto de engenharia em menos de meio dia e por menos de US$ 500: verificou parte do código que criptografa as conversas do mensageiro Signal. Três especialistas altamente qualificados gastaram cinco meses para fazer o mesmo trabalho manualmente. A verificação não foi comum, e sim formal: em vez de submeter o programa a milhares de testes, prova-se matematicamente que ele se comporta como planejado. A ideia é antiga, mas até agora era cara e lenta demais. Agora startups com centenas de milhões de dólares e grandes laboratórios de IA apostam nela.

Por que matemática em vez de testes

O teste convencional mostra que o programa não quebrou nos casos que lhe foram apresentados. A verificação formal prova que ele não vai quebrar em nenhum caso da classe descrita. Os engenheiros escrevem afirmações precisas sobre o objetivo do programa e depois convertem o código em fórmulas, que sistemas especializados checam. Lean, Rocq e Isabelle estão entre esses sistemas.

Mas o trabalho é pesado. As especificações precisam ser formuladas com muito cuidado. Um exemplo simples: uma função que ordena uma tabela deve devolver os mesmos elementos que recebeu, apenas em outra ordem. Para uma pessoa, isso é óbvio; para um sistema matemático, é preciso escrever de forma rigorosa.

Por isso, o método é usado onde o custo de um erro é alto. Segundo divulgações das próprias empresas, há código verificado formalmente em aviões da Boeing, em servidores da Amazon e em mais de 2,5 bilhões de dispositivos ativos da Apple. Em geral, é código ligado à segurança. Byron Cook, da Amazon Web Services, diz que a verificação eliminava dúvidas de clientes sobre a proteção da nuvem e acelerava as equipes internas: erros graves eram pegos cedo.

Quem aposta em IA e como

As startups querem automatizar a parte mais tediosa: redigir a descrição de como o programa deve se comportar. Os demais passos, possivelmente sem IA, convertem o código para um formato que os sistemas matemáticos aceitam.

• &Truth. Levantou US$ 70 milhões; Sun se juntou à empresa em agosto, e o lançamento público ocorreu na quinta-feira. O objetivo é, com o tempo, verificar código em qualquer linguagem de programação.

O diretor científico, Ilya Sergey, compara a abordagem à construção civil: pontes e prédios não desabam porque foram calculados antes de erguidos, então por que não fazer o mesmo com o código? • Harmonic. Tem como cofundador Vlad Tenev, CEO da Robinhood, e captou US$ 295 milhões.

Nesta semana, a empresa anunciou que seu agente de IA matemático, o Aristotle, consegue verificar programas em C e descrições de chips em Verilog. A tecnologia está em avaliação por clientes em potencial, incluindo os fabricantes de chips Tensordyne e Nvidia; o braço de venture capital da Nvidia é um dos investidores. • **Anthropic e Theorem.

** Uma semana atrás, informaram que usaram IA para encontrar erros em software de código aberto que trilhões de testes não detectaram. Também foi lançado um complemento para o Claude que ajuda desenvolvedores com a verificação. O custo do primeiro projeto não foi divulgado.

• Truidic. Fundada por Madan Musuvathi, que deixou a Microsoft Research depois de mais de 20 anos. Na opinião dele, a IA é muito poderosa nas mãos de atacantes, e a verificação pode tornar a IA segura.

• Proofcraft. Trabalha há muito tempo com verificação clássica. Seus líderes, June Andronick e Gerwin Klein, dizem que o volume de pedidos excede a capacidade tanto deles quanto dos concorrentes.

Projetos abertos também estão testando o método. A Beneficial AI Foundation, organização sem fins lucrativos, verificou neste ano, com um grant da Anthropic, o mesmo código criptográfico analisado por Sun. Michael Rosenberg, um dos mantenedores da biblioteca curve25519-dalek, espera que esse tipo de trabalho tenha financiamento permanente, mas não sabe de onde ele virá e não quer depender da boa vontade das empresas de IA.

Onde o método esbarra no teto

Por ora, a tecnologia está na fase de protótipos. Não está claro quanto os clientes aceitam pagar nem em que formato querem receber o produto: diretamente ou por intermediários como a Anthropic. Várias empresas de tecnologia de médio porte disseram à Wired que verificaram no máximo uma função-chave do produto, ou nenhuma. Os motivos: falta de engenheiros de verificação, custo acima do risco potencial e medo de que semanas de espera pela verificação atrasem o lançamento de atualizações. Até a Apple precisa adicionar código novo com cautela em sua biblioteca de criptografia corecrypto, para conseguir verificá-lo a tempo.

Há também objeções de princípio. A prova se apoia em premissas sobre como computadores e pessoas interagem com o programa. Erros de usuários e falhas de hardware podem passar despercebidos.

Will Wilson, chefe da startup Antithesis (busca de bugs com IA), chama a verificação formal de «armadilha» para entusiastas de matemática como ele. Sua empresa gastou milhões para verificar parte da própria proteção e descreveu o processo como «um pé no saco». Ainda assim, a ferramenta da própria Antithesis encontrou erros adicionais nesse código, além de bugs em software de clientes que eles já tinham verificado formalmente.

A conclusão de Wilson: a verificação dá alguma confiança, mas só o teste exaustivo pode confirmá-la. Vitalik Buterin também escreveu em seu blog que a verificação formal não é uma panaceia, embora a considere uma defesa importante contra ciberataques feitos com IA.

Andronick e Klein veem um risco à parte: se a descrição do problema foi escrita por IA, surge uma «confiança injustificada» no resultado. A prova só é tão correta quanto a descrição do que se considera correto.

Conclusão prática para engenheiros: a IA reduz drasticamente o custo da etapa mais cara, mas será preciso verificar tanto as próprias especificações quanto o trabalho, com testes. Duas empresas que hoje não verificam formalmente seu código estariam dispostas a pagar aos laboratórios de IA por código «verificado» gerado por IA. Se isso funcionar, a verificação formal vai sair do território de NASA e Apple.