New Benchmark Evaluates AI on Formal Verification via Lean 4

Researchers have introduced a benchmark to assess AI models and agents on real-world formal software verification. The dataset comprises 11,039 property-based tests scraped from Python repositories, of which 2,772 (25%) were automatically translated into 9,415 Lean 4 specifications containing 'sorry' placeholders, averaging about three formalizations per PBT. Translating imperative PBTs into dependent-typed Lean code involves modeling Python semantics, inferring logical properties, and addressing challenges in a seldom-used programming language. A three-agent LLM pipeline was developed for transpilation, with coverage and quality metrics evaluated. Proof generation baselines using multiple automated and model-based approaches are provided, and all code and data are publicly available.