Anthropic usa Claude para gerar provas formais de código existente
Segundo a Anthropic, o modelo Claude produziu cerca de 180 milhões de linhas de prova para 123 bibliotecas, detectando falhas ocultas.
Resumo rápido
- O modelo Claude produziu cerca de 180 milhões de linhas de prova para 123 bibliotecas.
- A ferramenta identificou e corrigiu centenas de bugs não detectados por testes convencionais.
- As provas matemáticas funcionam apenas sob condições restritas de hardware e entrada.
Entenda o contexto
A verificação formal de software consiste em utilizar métodos matemáticos para provar que um programa está correto e livre de erros sob determinadas condições. Historicamente, essa prática exige equipes especializadas e alto investimento de tempo e recursos, sendo restrita a sistemas críticos.
A Anthropic e a parceira Theorem utilizaram o modelo de linguagem Claude para realizar a verificação matemática de códigos de software existentes e gerar provas formais de correção. Em um período de poucas semanas, a ferramenta produziu aproximadamente 180 milhões de linhas de código de prova para 123 bibliotecas de código aberto presentes no projeto de segurança OSS-Fuzz, mantido pela Google, conforme divulgado pelo The Decoder.
Diferente da criação de softwares do zero, a abordagem consistiu em traduzir testes de falha em problemas matemáticos, analisar o código compilado e gerar extensas provas. Um programa de verificação independente chamado Rocq faz a checagem automática dessas provas, processo que, segundo a Anthropic, dispensa quase totalmente revisores humanos.
Detecção de falhas e limites das provas
Durante a geração das provas, Claude encontrou centenas de bugs que haviam escapado de testes convencionais por se manifestarem apenas sob condições específicas, como arquivos de entrada anômalos ou sequências particulares de acesso. Em um teste com um leitor de PDF amplamente utilizado, a equipe registrou em uma semana um volume de bugs de segurança equivalente ao reportado em um ano inteiro de uso.
Apesar dos resultados, a Anthropic reconhece que a verificação formal tem limites estritos. As provas obtidas só são válidas sob condições específicas, como uma arquitetura de processador determinada, programas de thread única e entradas inferiores a 64 MB. Além disso, o custo computacional é elevado, embora modelos mais recentes como o Opus 5.5 tenham apresentado maior eficiência que a versão anterior Opus 5.
A empresa pretende ampliar a verificação formal com inteligência artificial para componentes de infraestrutura crítica como glibc, OpenSSL e cURL.
Referências
- Reportagem consultada: The Decoder
Links para conferência: não indicam endosso das fontes ao conteúdo do portal.
Gostou? Compartilhe:
Comentários 0
Ninguém comentou ainda. Seja o primeiro!
