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

A empresa de inteligência artificial Anthropic, por meio da Frontier Red Team, publicou uma pesquisa em 22 de outubro, afirmando que grandes modelos de linguagem agora podem redigir automaticamente provas formais em uma escala maior. A equipe colaborou com a Theorem para usar Claude na camada de montagem RISC-V para provar propriedades de segurança de mais de 100 bibliotecas de código aberto reais, marcando a primeira vez que a IA realiza verificação formal em larga escala de software de produção na camada de montagem. Durante o processo de escrita das provas, foram descobertas vulnerabilidades que não haviam sido detectadas por anos. O experimento converteu testes de fuzzing compiláveis já existentes no Google OSS-Fuzz em especificações, sob suposições de binários estáticos 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, Claude provou as propriedades mencionadas em 239 pontos de entrada de 123 bibliotecas OSS-Fuzz, com provas para as instruções RISC-V compiladas, cerca de 180 milhões de linhas de Rocq, verificadas pelo núcleo Rocq. A página afirma que isso não significa que essas bibliotecas estejam isentas de vulnerabilidades, pois problemas remanescentes podem estar localizados em componentes confiáveis ou fora do escopo da prova. A equipe também fez Claude formalizar o RFC 1950 e provou na camada binária x86 que a implementação do zlib no núcleo do Linux está em conformidade com essa especificação; um interpretador escrito em Rust que cobre um grande subconjunto do Python teve uma taxa de consistência de 99,95% em relação ao 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.