VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
O artigo apresenta o VeriSoftBench, um novo conjunto de benchmarks de 500 obrigações de prova em Lean 4 extraídas de repositórios de verificação de software real, demonstrando que os modelos de linguagem especializados em matemática transferem-se mal para esse contexto e que o desempenho é fortemente limitado pela complexidade das dependências transitivas do repositório.
Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo
Imagine que você está tentando ensinar um robô superinteligente (uma Inteligência Artificial) a ser um advogado de defesa ou um engenheiro de software. O objetivo é que ele consiga provar matematicamente que um código de computador está livre de erros.
Até agora, os cientistas treinavam esses robôs usando "problemas de matemática pura", como os que você vê em competições de olimpíadas ou livros didáticos. É como se estivéssemos ensinando o robô a resolver equações em um quadro negro limpo, onde todas as regras são universais e conhecidas por todos.
O Problema:
Na vida real, quando um engenheiro de software precisa provar que um sistema bancário ou um carro autônomo é seguro, ele não trabalha em um quadro limpo. Ele trabalha dentro de um arquivo gigante e bagunçado, cheio de códigos específicos daquela empresa, com regras que só existem naquele projeto e que dependem de outros arquivos distantes. É como tentar consertar um motor de avião sem saber qual peça de qual caixa você precisa, e com o manual escrito em um dialeto que só os mecânicos daquele hangar conhecem.
A Solução (VeriSoftBench):
Os autores deste artigo criaram um novo "campo de treinamento" chamado VeriSoftBench. Em vez de dar ao robô apenas problemas de matemática limpa, eles pegaram 500 desafios reais de projetos de software de código aberto.
Eles embalaram esses desafios de uma forma especial:
- O Contexto Real: O robô recebe não só o problema, mas também o "arquivo de instruções" completo do projeto, com todas as dependências cruzadas (como um quebra-cabeça onde as peças estão espalhadas por várias caixas).
- Dois Tipos de Teste:
- O Teste "Guia de Ouro": Eles dão ao robô apenas as peças exatas que ele precisa para resolver o problema (como se alguém apontasse para a caixa certa).
- O Teste "Caos Total": Eles dão ao robô a biblioteca inteira do projeto (milhares de páginas de código) e veem se ele consegue encontrar as peças certas sozinho.
O Que Eles Descobriram?
Ao testar os robôs mais inteligentes do mundo (como GPT-5, Claude e outros), eles viram três coisas surpreendentes:
- O "Mestre da Matemática" é um "Amador" no Mundo Real: Os robôs que são gênios resolvendo problemas de matemática pura (como os do Mathlib) falham miseravelmente quando colocados nesses projetos de software reais. Eles se perdem na bagunça.
- A Distância Importa: Quanto mais "passos" o robô precisa dar para conectar uma ideia a outra (por exemplo, usar uma regra do Arquivo A que depende de uma definição do Arquivo B, que depende de uma função do Arquivo C), menor a chance de ele conseguir. É como tentar seguir um mapa onde as instruções estão escondidas em camadas profundas de um labirinto.
- Ajudar é Bom, mas Não é o Suficiente: Quando os pesquisadores deram apenas as peças necessárias (o "Guia de Ouro"), o robô funcionou melhor do que quando tinha tudo. Mas, mesmo com a ajuda, ele ainda falhou muito. Isso mostra que o problema não é apenas "achar a informação", mas sim raciocinar com ela de forma complexa.
A Analogia Final:
Imagine que resolver um problema de matemática é como seguir uma receita de bolo simples: "Misture farinha e ovos".
Resolver um problema de verificação de software no VeriSoftBench é como ser um chef em uma cozinha gigante, onde você precisa:
- Encontrar o ingrediente certo em um dos 50 armários.
- Saber que aquele ingrediente foi modificado por um cozinheiro no andar de cima.
- E ainda assim, criar uma receita nova que funcione perfeitamente, sem que o bolo desmorone.
Conclusão:
O VeriSoftBench nos diz que, embora nossas IAs estejam ficando muito boas em matemática, elas ainda têm muito o que aprender para serem úteis na engenharia de software real. Precisamos de novos métodos que ensinem as IAs a navegar em bibliotecas gigantes e a entender a lógica complexa de projetos específicos, não apenas a resolver equações soltas.
Afogado em artigos na sua área?
Receba digests diários dos artigos mais recentes que correspondam às suas palavras-chave de pesquisa — com resumos técnicos, no seu idioma.