Em conjunto com a sua parceira Theorem, a Anthropic usou o modelo de IA Claude para tentar provar matematicamente que código de software existente funciona corretamente. O trabalho incidiu sobre 123 bibliotecas de código aberto incluídas no OSS-Fuzz, um projeto de segurança da Google. Em poucas semanas, foram gerados cerca de 180 milhões de linhas de código para provas e, segundo a empresa, foram também descobertos centenas de bugs que os testes convencionais não tinham detetado.
A distância entre «passou nos testes» e «foi provado que está correto»
Quando se fala em verificar a qualidade do software, muitas pessoas pensam logo em testes: fornecer as entradas previstas e confirmar se o resultado corresponde ao esperado. Mas os testes só permitem verificar aquilo que foi testado. Não dizem como o programa se comportará em situações que não foram experimentadas.
É aí que entra a verificação formal. O comportamento de um programa é tratado como um problema matemático, para provar que funciona sempre corretamente dentro das condições definidas. Em teoria, é uma abordagem poderosa, mas exigia um esforço incomparavelmente maior. Só a verificação do seL4, um pequeno kernel de sistema operativo, terá consumido o equivalente a 20 anos de trabalho de uma equipa de especialistas. Não admira que a sua utilização tenha ficado limitada a casos extremos, como o software de controlo de aviões de passageiros.
Desta vez, a Frontier Red Team da Anthropic juntou-se à Theorem e confiou a Claude este trabalho de prova. Não lhe pediu para escrever código novo. Em vez disso, aplicou o processo a software já existente, transformou testes de deteção de falhas em problemas matemáticos e encarregou o modelo de analisar até ao código de máquina após a compilação e de construir um grande número de provas.
Outro programa faz a «avaliação» das provas
Não é convincente que uma IA declare «aprovada» uma prova que ela própria escreveu. É neste ponto que o mecanismo de avaliação se torna interessante: as provas geradas são verificadas automaticamente pelo Rocq, um programa de verificação independente. Segundo a Anthropic, este processo quase não requer revisores humanos.
A equipa de investigação descreve o processo como geração de provas «totalmente autónoma». No entanto, as ferramentas e as bases formais usadas nas provas foram criadas por pessoas da Theorem. Em vez de a IA ter criado tudo do zero, a descrição mais fiel será a de que escreveu de uma só vez uma enorme quantidade de provas num quadro preparado por humanos.
Centenas de bugs encontrados durante a elaboração das provas
Ao avançar com as provas, Claude encontrou centenas de bugs e também teve autorização para os corrigir. Segundo os investigadores, muitos só se manifestavam em condições muito específicas, como ficheiros de entrada extremamente grandes ou acessos à memória numa determinada ordem. Não é de admirar que passassem despercebidos nos testes convencionais.
Foram apresentados exemplos concretos. Na verificação de um leitor de PDF amplamente utilizado, foram encontrados numa semana tantos bugs de segurança quantos os que normalmente são reportados nesse software ao longo de um ano. Noutra aplicação, foi descoberto um erro lógico que passara despercebido durante mais de dez anos.
Outro aspeto que não deve ser ignorado é o que acontece quando uma prova não chega a ser concluída. A Anthropic explica que, mesmo quando a prova falha, podem surgir bugs reais durante o processo. Assim, a prova não serve apenas para obter um «certificado de aprovação»: também pode funcionar como uma sonda para descobrir bugs. Em vez de substituir os testes convencionais, parece complementar aquilo que lhes escapa.
Não interpretar mal o alcance de «verificado formalmente»
Ainda assim, é perigoso interpretar «verificado formalmente» como «sem falhas». A própria Anthropic reconhece que a validade das provas se limita a condições rigorosas. Os pressupostos incluem uma configuração específica do processador, programas executados numa única thread e entradas com menos de 64 MB. Na realidade, as bibliotecas funcionam com diferentes tipos de hardware e configurações.
Os custos também não são baixos. Em alguns casos, cada prova pode exigir centenas de milhões de tokens. O custo total do projeto não foi divulgado. Por outro lado, experiências adicionais de menor dimensão mostraram que as provas podem ser reutilizadas e que os modelos mais recentes tendem a ser mais eficientes. Segundo a empresa, o Opus 5.5 precisa de cerca de 40% menos tokens do que o Opus 5 para resolver metade das provas.
A pergunta deixa de ser «consegue programar?»
Se a IA consegue escrever código e garantir, sob determinadas condições, que está correto, muda a forma de colocar a questão. Em vez de «a IA consegue programar?», passa a ser «a IA consegue provar a segurança do código que escreveu?». Esta mudança não é insignificante para as equipas de desenvolvimento preocupadas com a fiabilidade do código gerado por IA. Se a IA conseguir verificar o seu próprio código, poderá reduzir o peso das revisões humanas e os custos não só da verificação, mas de todo o processo de desenvolvimento.
A Anthropic prevê que, num futuro próximo, a verificação formal por IA se torne tão comum como os testes convencionais. O roteiro da Theorem inclui software de infraestruturas críticas como glibc, OpenSSL e cURL.
Aqui, o que importa é saber ler não o «conteúdo» da prova, mas as suas «premissas». Que ambiente e que dados de entrada pressupõe a prova? Numa era em que confiamos também à IA a tarefa de verificar, a literacia humana para confirmar essas premissas poderá ser a última linha de defesa da segurança.
コメント