FVSpec: Testes Baseados em Propriedades do Mundo Real como Desafios Lean

Resumo

Apresentamos um benchmark para avaliar modelos e agentes de IA em tarefas reais de verificação formal de software. Primeiramente, coletamos 11.039 testes baseados em propriedades (PBTs) de repositórios Python reais e, em seguida, traduzimos automaticamente 2.772 deles (25%) em 9.415 especificações Lean 4 com placeholders `sorry` (cerca de 3 formalizações/PBT; mantemos múltiplas tentativas quando nenhuma domina nas métricas de qualidade). A tradução de PBTs para especificações Lean é desafiadora: exige modelar a semântica do Python em Lean, inferir a propriedade lógica codificada em um PBT imperativo e lidar com as dificuldades inerentes à programação com tipos dependentes em uma linguagem pouco utilizada. Descrevemos um pipeline de três agentes LLM para transpilar PBTs em especificações Lean, avaliamos métricas de cobertura e qualidade, e fornecemos linhas de base para geração de provas usando diversas abordagens automatizadas e baseadas em modelos. Todo o código (scraper e agentes) e dados (PBTs e especificações Lean) são de código aberto. Nosso benchmark visa impulsionar o progresso no problema ainda pouco explorado de verificação formal assistida por IA de software real, questão de interesse crescente à medida que a IA produz cada vez mais o código do mundo.

English

We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically translate 2,772 of them (25%) into 9,415 Lean 4 specifications with sorry placeholders (about 3 formalizations/PBT; we retain multiple attempts when none dominates on quality metrics). Translating PBTs into Lean specifications is challenging: it requires modeling Python semantics in Lean, inferring the logical property encoded in an imperative PBT, and handling the inherent difficulties of dependently-typed programming in a seldom-used language. We describe a three-agent LLM pipeline for transpiling PBTs into Lean specifications, evaluate coverage and quality metrics, and provide baselines for proof generation using several automated and model based approaches. All code (scraper and agents) and data (PBTs and Lean specifications) are open source. Our benchmark aims to drive progress on the underexplored problem of AI-assisted formal verification of real-world software, which is of increasing interest as AI produces more and more of the world's code.