Resumo Técnico: FVSpec

Declaração do Problema

O artigo aborda a lacuna crítica na verificação formal (FV) assistida por IA para software do mundo real. As propostas de segurança de IA dependem cada vez mais de agentes autônomos para verificar formalmente o código gerado por IA, mas os benchmarks atuais falham em apoiar esse objetivo. Os benchmarks existentes (ex: Minif2f, PutnamBench) focam em problemas de olimpíadas matemáticas ou código de provadores de teoremas escrito por especialistas, o que difere significamente do cenário de engenharia de software "normal". O software do mundo real envolve árvores de dependências complexas, APIs externas de caixa-preta e componentes escritos em diferentes linguagens, tornando-o inerentemente mais difícil de verificar do que sistemas monolíticos e fechados. Além disso, há uma falta de conjuntos de dados de alta qualidade e grande escala derivados de código escrito por engenheiros sem intenção de verificação formal, o que é necessário para treinar agentes que possam operar "fora da distribuição" (out-of-distribution) em relação aos seus dados de treinamento.

Metodologia

Os autores introduzem o FVSpec, um pipeline de geração de benchmark que transforma Testes Baseados em Propriedades (PBTs) do mundo real em desafios de verificação formal em Lean 4. O processo envolve três estáções principais:

1. Coleta de Dados (FVSpec:PBT):

   • A equipe extraiu 11.039 PBTs únicos de 333 repositórios Python de código aberto usando o framework Hypothesis.
   • Os repositórios foram filtrados por licenças permissivas e duplicatas (incluindo forks) foram removidas para garantir diversidade.
   • O corpus resultante representa a engenharia de software "comum", com testes variando de asserções triviais a testes de múltiplas estratégias complexas.

2. Transpilação Agêntica (FVSpec:FV):

   • Um pipeline de LLM de três agentes traduz os PBTs Python e seu código associado para Lean 4.
   • Descoberta de Função: Utiliza tree-sitter para extrair a Função Sob Teste (FUT) e seu fechamento transitivo de dependências locais.
   • Tradução: Um agente de formalização gera dois arquivos: Impl.lean (uma porta computável da função) e Spec.lean (enunciados de teoremas correspondentes às asserções do PBT, com provas deixadas como placeholders sorry).
   • Reparo Iterativo: O pipeline emprega um loop de Protocolo de Servidor de Linguagem (LSP). Se o código Lean gerado falhar na compilação (via lake build), os diagnósticos do compilador são retroalimentados ao agente para revisão. Este loop executa por até 16 iterações.
   • Tratamento de Efeitos: Para código envolvendo efeitos colaterais (ex: Redis, I/O de arquivo), o agente axiomatiza esses sistemas externos como interfaces não interpretadas. Os teoremas são enunciados sobre esses axiomas, garantindo que a obrigação de prova permaneça significativa em relação à lógica do código, mesmo que os detalhes de implementação concreta sejam abstraídos.

3. Pós-Produção e Filtragem:

   • As amostras geradas passam por validação rigorosa. Falhas são categorizadas (ex: timeouts, incompatibilidades de tipo, identificadores desconhecidos).
   • Uma pontuação de "fidelidade estrutural" é computada com base em cinco sub-métricas: cobertura de parâmetros, correspondência de tipos, cobertura de estratégia, cobertura de asserção e cobertura de dependência.
   • As amostras são classificadas por dificuldade (Fácil/Difícil) usando um juiz LLM calibrado (claude-haiku-4-5).
   • O conjunto de dados final retém múltiplas formalizações por PBT se nenhuma tentativa única domine nos critérios de qualidade, resultando em 9.415 desafios derivados de 2.772 PBTs únicos.

Principais Contribuições

1. FVSpec:PBT: Um corpus de 11.039 PBTs Python deduplicados extraídos de repositórios de código aberto, representando o primeiro conjunto de dados de grande escala e de licença limpa de PBTs de desenvolvimento de software comum (excluindo programação competitiva ou código de ITP curado).
2. FVSpec:FV: Um conjunto de dados de 9.415 desafios de verificação formal em Lean 4. Cada desafio inclui o código Python original, o PBT original, uma implementação em Lean e um enunciado de teorema em Lean com obrigações de prova. O conjunto apresenta uma fidelidade estrutural mediana de 0,65, com 62% dos desafios classificados como "difíceis".
3. Avaliações de Linha de Base: Métricas de desempenho para modelos de fronteira (Claude Sonnet 4.6, Claude Opus 4.7 e GPT-5.4). Os modelos alcançaram uma taxa de sucesso média de 70% em problemas "fáceis" e 49% em problemas "difíceis", indicando que o benchmark ainda não está saturado.
4. Lançamento de Código Aberto: O pipeline completo (scraper, extrator de dependências, agente de formalização e scripts) e os conjuntos de dados são lançados sob uma licença dupla MIT/Apache.

Resultados

• Rendimento do Pipeline: O pipeline de transpilação converteu com sucesso 25% dos 11.039 PBTs iniciais em desafios válidos em Lean (9.415 amostras).
• Métricas de Qualidade: A pontuação mediana de fidelidade estrutural é 0,65. A correspondência de tipos (1,00) e a cobertura de asserção (0,97) são altas, enquanto a cobertura de parâmetros (0,24) e a cobertura de dependência (0,48) são menores, indicando áreas onde a fidelidade da tradução varia.
• Desempenho do Modelo: Modelos de linha de base resolveram 70% das amostras fáceis e 49% das difíceis. As taxas de recusa foram baixas (4–8% para fáceis, 3–25% para difíceis), sugerindo que os modelos geralmente tentam as tarefas.
• Complexidade: A amostra mediana contém 6 teoremas. O conjunto de dados inclui uma ampla gama de complexidade, desde algoritmos de ordenação simples até complexos agendadores de tarefas de fluxo de trabalho envolvendo timeouts e transições de estado.

Significância e Alegações

O artigo afirma que o FVSpec fornece uma fundação necessária para avançar a verificação formal assistida por IA de software do mundo real. Ao contrário de benchmarks anteriores que dependem de provas escritas por especialistas ou problemas matemáticos, o FVSpec deriva especificações de engenheiros que não tinham intenção de verificação formal. Isso garante que os problemas estejam "fora da distribuição" em relação aos dados de treinamento padrão dos modelos, oferecendo um teste mais rigoroso da capacidade de generalização de um agente.

Os autores posicionam este trabalho como um passo em direção à "IA Garantidamente Segura" e "Supervisão Formal Escalável", onde agentes autônomos devem verificar o software tão rápida e efetivamente quanto o escrevem. Ao fornecer um benchmark realista de grande escala, o FVSpec visa impulsionar o progresso no treinamento de agentes capazes de lidar com as complexidades dos ecossistemas de software modernos, incluindo dependências externas e efeitos colaterais, que são frequentemente ignorados em benchmarks sintéticos. O artigo reconhece modestamente limitações, como o potencial de a axiomatização perder especificidades semânticas de efeitos colaterais e a falta de baselines de especialistas humanos para calibração de dificuldade.