FVSpec: Real-World Property-Based Tests as Lean Challenges
AIPR assessment
Problem difficulty is high. The paper tackles a crowded but still underexplored intersection of real-world software, property-based testing, Lean formalization, and benchmark construction, where the hard part is not just scale but also the semantic mismatch between Python code, PBTs, and theorem statements. The strengths reinforce each other: the open corpus, the clear pipeline, and the baseline evaluation all support the claim that this is a usable benchmark rather than a one-off demo. The weak
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.
Score Breakdown
More from this week
- Towards Interactive Video World Modeling: Frontiers, Challenges, Benchmarks, and Future Trends
- On Thin Perfect Matchings up to Polylogarithmic Factors
- ViBE: Co-Optimizing Workload Skew and Hardware Variability for MoE Serving
- LeAP: Learnable Adaptive Permutation for Feature Selection in Heterogeneous and Sparse Recommender Systems
- PolySpeech-100: A Large-Scale Benchmark for Speech Understanding Across 100+ Languages and Dialects