Anthropic lança biblioteca de verificação formal em larga escala Claude

A empresa de inteligência artificial Anthropic, através da sua Frontier Red Team, publicou uma pesquisa no dia 22 de outubro, afirmando que os grandes modelos de linguagem agora conseguem redigir automaticamente provas formais em uma escala maior. A equipe colaborou com a Theorem, utilizando o Claude para provar propriedades de segurança em mais de 100 bibliotecas de código aberto reais no nível de montagem RISC-V, marcando a primeira vez que a IA realiza verificação formal em larga escala de software de produção a esse nível. Durante o processo de escrita das provas, foram descobertas vulnerabilidades que estavam ocultas por anos. O experimento converteu testes de fuzzing compiláveis já existentes no Google OSS-Fuzz em especificações, sob suposições de binário estático de thread única, orçamento de memória fixo, CPU RISC-V e Linux, onde para qualquer entrada abaixo de 64 MB, o programa deve sair normalmente sem acionar erros de segurança de memória ou falhas de asserção. Após corrigir os problemas, o Claude provou as propriedades mencionadas em 239 pontos de entrada de 123 bibliotecas do OSS-Fuzz, provando que, para as instruções RISC-V compiladas, cerca de 180 milhões de linhas de Rocq foram verificadas pelo núcleo do Rocq. A página observa que isso não significa que essas bibliotecas estejam isentas de vulnerabilidades, e que problemas remanescentes podem estar localizados fora dos componentes confiáveis ou do escopo da prova. A equipe também fez com que o Claude formalizasse o RFC 1950 e provou que a implementação do zlib no núcleo do Linux atende a essa especificação no nível binário x86; um interpretador escrito em Rust que cobre um grande subconjunto do Python teve uma taxa de 99,95% de consistência com o comportamento do CPython em mais de 1,7 milhão de programas gerados aleatoriamente. Em 36 pequenas tarefas de verificação, o Opus 5.5 provou que a metade delas exigia cerca de 40% menos tokens do que o Opus 5.