Claude prova matematicamente que 123 bibliotecas de código aberto não falham e encontra centenas de erros

Quase todo o software tem erros, e os modelos de IA estão a ficar cada vez melhores a encontrá-los e a explorá-los. A Anthropic, criadora do Claude, defende que a resposta passa por provar, com matemática, que o código não tem certos tipos de falhas. Num estudo publicado a 22 de outubro, feito em conjunto com a empresa Theorem, mostra que a sua IA já consegue fazer esse trabalho em grande escala, em bibliotecas de código aberto usadas por muitos outros programas.

O que é a verificação formal

Na verificação formal, o código é traduzido para um modelo matemático e prova-se que cumpre sempre um conjunto de regras, por exemplo, que nunca lê ou escreve fora da memória que lhe pertence. Se a prova falha, isso aponta para um erro. O problema é o esforço: a Anthropic lembra que o núcleo do sistema operativo seL4 levou duas pessoas-ano a programar e 20 pessoas-ano a verificar. Por isso, a técnica ficou reservada a casos críticos, como o software de aviónica da Airbus.

No estudo, a equipa partiu dos testes automáticos que os próprios programadores já escrevem para o projeto OSS-Fuzz, da Google, e transformou-os em especificações. Ao longo de algumas semanas, o Claude corrigiu os erros que foi encontrando e provou que 239 pontos de entrada de 123 bibliotecas nunca falham com qualquer entrada até 64 MB. As provas, com cerca de 180 milhões de linhas, são verificadas por um programa independente, o Rocq, e não precisam de ser lidas por pessoas. Valem, por agora, para programas compilados para processadores RISC-V a correr em Linux.

Erros que os testes não apanhavam

Pelo caminho apareceram centenas de erros. Num descompressor, o Claude encontrou um erro que permitia escrever fora da memória, mas só com ficheiros de cerca de 20 MB e uma estrutura rara. Num descodificador de imagens, a falha exigia uma entrada de 64 MB e mais de 2 GB de memória, longe do limite de cerca de 1 MB com que estes testes costumam trabalhar. Voltou também a descobrir uma vulnerabilidade já catalogada no libexpat, uma biblioteca de leitura de XML.

Noutras experiências, o Claude provou que a implementação do zlib, o formato de compressão, no núcleo do Linux cumpre a especificação oficial, e encontrou num programa muito usado um erro lógico com mais de dez anos. Ao tentar verificar um leitor de PDF muito popular, cujo nome não é revelado, a equipa diz ter encontrado numa semana tantas falhas de segurança como as que costumam ser reportadas num ano.

Os limites

A Anthropic sublinha que "formalmente verificado" não significa "sem erros". A prova só garante que o programa cumpre a especificação, e se esta ou o modelo da máquina estiverem errados, os erros continuam lá. O maior travão é o custo: cada prova pode consumir centenas de milhões de tokens. A empresa diz que o Claude Opus 5.5 resolve metade de um conjunto de testes com cerca de 40% menos tokens do que o Opus 5 e que partilhar provas entre agentes poupa 17%.

Para quem usa estes programas no computador ou no telemóvel, não há nada a fazer. A Anthropic diz que parte dos erros está a ser comunicada aos projetos de origem, e as correções chegam depois nas atualizações habituais de cada programa. A Theorem oferece-se para aplicar o mesmo processo a outros projetos de código aberto e publicou parte das provas, deixando de fora as que poderiam revelar erros ainda por corrigir.

AnthropicClaudeVerificação formalCódigo abertoCibersegurança