FVSpec: Praktijkgerichte eigenschapsgebaseerde tests als Lean-uitdagingen

Samenvatting

Wij presenteren een benchmark voor het evalueren van AI-modellen en -agenten op realistische formele software-verificatietaken. Eerst schrapen we 11.039 eigenschapsgebaseerde tests (PBT's) uit echte Python-repositories, waarna we er 2.772 (25%) automatisch vertalen naar 9.415 Lean 4-specificaties met sorry-plaatshouders (ongeveer 3 formaliseringen/PBT; we behouden meerdere pogingen wanneer geen enkele domineert op kwaliteitsmetrieken). Het vertalen van PBT's naar Lean-specificaties is uitdagend: het vereist modellering van Python-semantiek in Lean, het afleiden van de logische eigenschap die in een imperatieve PBT gecodeerd is, en het omgaan met de inherente moeilijkheden van afhankelijk getypeerd programmeren in een weinig gebruikte taal. We beschrijven een drie-agent LLM-pijplijn voor het transpileren van PBT's naar Lean-specificaties, evalueren dekkings- en kwaliteitsmetrieken, en bieden basislijnen voor bewijsgeneratie met behulp van verschillende geautomatiseerde en modelgebaseerde benaderingen. Alle code (schraper en agenten) en gegevens (PBT's en Lean-specificaties) zijn open source. Onze benchmark beoogt vooruitgang te stimuleren op het onderbelichte probleem van AI-ondersteunde formele verificatie van realistische software, hetgeen van toenemend belang is naarmate AI steeds meer van 's werelds code produceert.

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.