Builds a benchmark translating Python property-based tests into Lean 4 specifications with sorry placeholders.
Abstract
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.
Problem
Existing formal verification benchmarks are too small, focused on mathematical Olympiad problems, or derived from expert-written proofs, leaving a gap in benchmarks for AI-assisted formal verification of real-world software.
Approach
The authors scrape 11,039 property-based tests (PBTs) from real-world Python repositories using Hypothesis, then use a three-agent LLM pipeline to transpile 2,772 PBTs (25%) into 9,415 Lean 4 specifications with sorry placeholders. Each specification includes a Lean implementation of the Python function and Lean theorems corresponding to the PBT assertions. A structural-faithfulness scoring metric evaluates translation quality across parameter coverage, type correspondence, strategy, and assertion coverage.
Figure 4: Structural-faithfulness scores across the published FVSpec:FV dataset. Left : histogram of per-sample overall scores (median 0.65; the multi-modal shape reflects the discrete denominators of the underlying ratios). Right : mean per-sub-metric scores. Type correspondence ( 1.00 ) and assertion coverage ( 0.97 ) are near-saturated—most translations preserve types and predicates—while param
Results
The benchmark yields 9,415 Lean 4 challenges containing 75,005 theorems across 333 repositories. Baseline prove rates from automated and model-based approaches remain low, with median structural faithfulness of 0.65, indicating the benchmark is challenging for current systems.
